Concise specification language:

RTTL (real-time temporal logic) is used to specify the properties to be verified. Given the timed transition model SUD $\;\stackrel{{\rm def}}{{=}}\;$ plant| controller, the objective is to check that SUD satisfies a specification S (which is a formula of RTTL).

An example of an RTTL formula is the bounded response time given by

∀T[(red∧t = T)→$\displaystyle \Diamond$(green∧T + 3≤t≤T + 5)]

In the above formula, the clock variable t is a flexible variable. The quantified variable T is a rigid variable. The clock variable is called flexible because it changes from state to state in the trajectory. By contrast, the rigid variable T retains the same value over all states in the trajectory, and is used to record the time when red becomes true. Accordingly, the above formula asserts that if the traffic light is red at time T, then eventually within 3 to 5 ticks from T the light must turn green. The bounded response property may be abbreviated by the formula

red→$\displaystyle \Diamond_{{[3,5]}}^{}$  green

RTTL is an explicit clock logic because an RTTL formula may explicitly use the clock time variable t with any of the arithmetic operators (e.g. + , - , = ,≤, >), using arbitrary first order quantification over rigid time variables. Hence RTTL is very expressive but undecidable (see Section 5.1.2). RTTL may be used to: (a) refer to absolute times (e.g. ``do some action on January 22nd 1998''), or (b) relate adjacent temporal contexts (e.g. ``every stimulus A is followed by a response B, and then by another response C that is within 5 ticks of the original stimulus A'').