RTTL (real-time temporal logic)
is used to specify the properties to be verified. Given the timed transition
model
SUD
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$](img13.png)
(
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→
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'').