LTL syntax: LTL formulas ϕ are inductively defined as follows, through a contextfree grammar:
ϕ → x, a propositional variable
| ¬ϕ negation of an LTL formula
| (ϕ) parenthesization
| ϕ1 ∨ ϕ2 disjunction
| Gϕ henceforth ϕ
| Fϕ eventually ϕ (“future”)
| Xϕ next ϕ
| (ϕ1U ϕ2) ϕ1 until ϕ2
| (ϕ1W ϕ2) ϕ1 weak-until ϕ2
Note that G is sometimes denoted by while F is denoted by ♦. We also introduce the X operator into the syntax above to capture the notion of next in a time sense. It is clear that in many real systems— for example, in globally clocked digital sequential circuits—the notion of next time makes perfect sense. However, in reasoning about the executions of one sequential process Pi among a collection of parallel processes P1, . . . , Pn, the notion of next time does not have a unique
meaning. As far as Pi is concerned, it has a list of candidate “next” statements to be considered; however, these candidate statements may be selected only after an arbitrary amount of interleavings from other processes. Hence, what is “next” in a local sense (from the point of view of Pi alone) becomes “eventually” in a global sense. While conducting verification, we will most likely not be proving properties involving X. However, X as a temporal operator can help expand other operators such as G through recursion. With this overview, we now proceed to examine the semantics of LTL.
LTL semantics: Recall that the semantics of LTL are defined over (infinite) computational sequences. LTL semantics can be defined over computation trees by conjoining the truth of an LTL formula over every computational sequence in the computational tree. Let σ = σ0 = s0, s1, . . ., where the superscript 0 in σ0 emphasizes that the computational sequence begins at state s0. By the same token, let σi = si, si 1, . . ., namely the infinite sequence beginning at si. By σ |= ϕ we mean ϕ is true with respect to computation σ; σ |= ϕ means ϕ is false with respect to computation σ. Here is the inductive definition for the semantics of LTL:
σ |= x iff x is true at s0 (written s0(x))
σ |= ¬ϕ iff σ |= ϕ
σ |= (ϕ) iff σ |= ϕ
σ |= ϕ1 ∨ ϕ2 iff σ |= ϕ1 ∨ σ |= ϕ2
σ |= Gϕ iff σi |= ϕ for every i ≥ 0
σ |= Fϕ iff σi |= ϕ for some i ≥ 0
σ |= Xϕ iff σ1 |= ϕ
σ |= (ϕ1U ϕ2) iffσk |= ϕ2 for some k ≥ 0 and σj |= ϕ1 for all j < k
σ |= (ϕ1W ϕ2) iffσ |= Gϕ1 ∨ σ |= (ϕ1U ϕ2)
LTL example: Consider formula GF x (a common abbreviation for G(F x)). Its semantics are calculated as follows:
σ |= GFx iff σi |= Fx, for all i ≥ 0
σi |= Fx iff σj |= x, for some j ≥ i
Putting it all together, we obtain the meaning as: x is true infinitely often—meaning, beginning at no point in time is it permanently false.
