Temporal logics
It is natural to invoke the standard (propositional) logic when defining whatever requirements – we require that “if this and that conditions are satisfied, then yet another condition must not hold”, and so on.
However, the spectrum of requirements expressed with propositional logic is not rich enough when specifying requirements for discrete-event and hybrid systems whose states evolve causally in time. Temporal logics add some more expressiveness.
Indeed, the plural is correct – there are several temporal logics. Before listing the most common ones, we introduce the key temporal operators that are going to be used together with logical operators.
Temporal operators
The name might be misleading here – the adjective temporal has nothing to do with time as measured by the wall clock. Instead, as (discrete) state trajectories form sequencies, temporal operators help express when certain properties must (or must not) be satisfied along the state trajectories.
Example 1 (Insufficiency of propositional logic to express requirement on a traffic light controller) Consider the state automaton for a controller for two traffic lights (but note that we intentionally simplify here a lot compared to real traffic light controllers). The state trajectory for each light is a sequence of color states \{\text{green}, \text{yellow}, \text{red}, \text{red-yellow}\} of the traffic light. We may want to impose a requirement such that \text{green} is never on at both lights at the same time. This we can easily express just with the standard logical operators, namely, \neg(\text{green}_1 \land \text{green}_2). But now consider that we require that sooner or later, \text{green} must be on for each light (to guarantee fairness). And that this must be true all the time, that is, \text{green} must come infinitely often. And, furthermore, that \text{red} cannot come imediately after its respective \text{green}.
Requirements like these cannot be expressed with standard logical operators such as \lnot, \land, \lor, \implies and \iff, and temporal operators must be introduced. Here they are.
Symbol | Alternative symbol | Meaning |
---|---|---|
\mathbf{F} | \Diamond | Eventually (Finally) |
\mathbf{G} | \Box | Globally (Always) |
\mathbf{X} | \bigcirc | NeXt |
\mathbf{U} | \sqcup | Untill |
We are going to explain their use while introducing our first temporal logic.
Linear temporal logic (LTL)
“Linear” refers to linearity in time (one after another, as opposed to branching). Consider a sequence of discrete states (aka state trajectory or path) of a given discrete-event or hybrid system that is initiated at some state x.
We now consider some property \phi(x) of a sequence of states emanating from the state x, \phi(x) evaluates to true
or false
. And indeed, while the argument of \phi is a particular state, when evaluating \phi, the full sequence is taken into consideration when evaluating \phi(x).
In order to be able to express requirements on future states, \phi() cannot be just a logical formula, it must by an LTL formula. Here comes a formal definition \phi = \text{true} \, | \, p \, | \, \neg \phi_1 \, | \, \phi_1 \land \phi_2 \, | \, \phi_1 \lor \phi_2 \, | \, \bigcirc \phi_1 \, | \, \Diamond \phi_1 \, | \, \Box \phi_1 | \, \phi_1 \sqcup \phi_2, where p is an atomic formula, and \phi_1 and \phi_2 are some LTL sub-formulas.
Having an LTL formula, we write that a state sequence iniciated at the given discrete state x satisfies the formula as x \models \phi if \phi is true for all possible state trajectories starting at this state.
Example 2 (Some LTL formulas) \Box \neg \phi
\Box\Diamond \phi
\Diamond\Box \phi
\Diamond(\phi_1 \land \bigcirc\Diamond\phi_2)
Computation tree logic (CTL)
Also branching termporal logic as it supports branching. Path quantifiers needed
Symbol | Alternative symbol | Meaning |
---|---|---|
\mathbf{A} | \forall | Universal quantifier (for All) |
\mathbf{E} | \exists | Existential quantifier (there Exists) |
Temporal operators and path quantifiers always come in pairs when forming CTL formulas.
CTL*
CTL mixed with LTL. It turns out that there is no advantage in restricting to either instead of considering the full CTL*.
Timed computation tree logic (TCTL)
Timing added to CTL. Used by UPPAAL.
Metric temporal logic (MTL)
Timing added to LTL.
Example 3 \square (\mathrm{pressWalkButton} \Rightarrow \Diamond_{(1,10)} \mathrm{greenLight})
Metric interval temporal logic (MITL)
An extension of MTL, which does not allow singleton time intervals allowed by MTL. The motivation for this extension is that the verification of MTL requirements has been shown to be undecidable.
Signal temporal logic (STL)
STL is then an extension of MTL with real-valued constraints. Available for both continuous- and discrete-time systems.
It allows combinations of surveillance (“visit regions A, B, and C every 10–60 s”), safety (“always between 5–25 s stay at least 1 m away from D”), and many others. I
Example 4 (Examples of STL formulas) \square (x(t) \leq 5.5 \Rightarrow \Diamond_{(1,10)} \mathrm{greenLight})
\Diamond_{(0,60)}\square_{(0,20)} (x(t)\leq 5.5)
\square\Diamond_{[0,10]} (\bm x(t) \in \mathcal A) \land \square\Diamond_{[0,10]} (\bm x(t) \in \mathcal B)