Page 189 -

180 M. Pesic
Definition 2 (LTL syntax). Each atomic proposition p is an LTL formula. Using
various operators, more complex expressions can be constructed. If ˆ and ‰ are
LTL formulas, then :ˆ; ˆ _ ‰; ˆ,and ˆU ‰ are also LTL formulas. The seman-
tics of these constructs are given in Definition 3. Moreover, the following operators
are so-called derived LTL operators. These operators can be expressed in terms of
the basic operators.
ˆ ^ ‰ :.:ˆ _:‰/
ˆ ) ‰ :ˆ _ ‰
ˆ , ‰ .ˆ ) ‰/ ^ .‰ ) ˆ/
true ˆ _:ˆ
false :true
♦ˆ trueUˆ
ˆ :♦:ˆ
ˆW ‰ .ˆU ‰/ _ ˆ
LTL formulas can be used to express that (1) ˆ should hold at the next element of
the trace ( ˆ), (2) ˆ should hold eventually (♦ˆ), (3) ˆ should always hold ( ˆ),
(4) ˆ should hold until eventually ‰ holds (ˆU ‰), and (5) ˆ should hold until ‰
holds, but ‰ is not required to hold eventually (‰W ˆ). The formal semantics of the
basic temporal operators are given in Definition 3.
Definition 3 (LTL semantics). Let p be an atomic proposition, Dh 1 ; 2 ;
3 ;:::i be a trace. Then
p , 1 =p
:ˆ , not ˆ
ˆ _ ‰ , ˆ or ‰
ˆ ,h 2 ; 3 ;:::i ˆ
ˆU ‰ ,9 1 i Œh i ; iC1 ; iC2 ;:::i ‰ ^8 1 j<i Œh j ; j C1 ;:::i ˆ

Note that the semantics of the other operators are provided in an indirect manner, for
example, ♦ˆ is semantically equivalent to trueUˆ, etc. Figure 6.4 shows some
example traces to clarify some of the constructs. Note that LTL is typically defined
on infinite traces, but all results for infinite sequences can be mapped onto finite
sequences.

p p p p p p p p p p
] 1 [ σ ] 2 [ σ ] 3 [ σ ] 4 [ σ ] 5 [ σ ] 6 [ σ ] 7 [ σ ] 8 [ σ ] 9 [ σ ] 1 [ σ ] 2 [ σ ] 3 [ σ ] 4 [ σ ] 5 [ σ ] 6 [ σ ] 7 [ σ ] 8 [ σ ] 9 [ σ
(a) always - [] p (b) eventually - <> p

p p p p p p p q q q
] 1 [ σ ] 2 [ σ ] 3 [ σ ] 4 [ σ ] 5 [ σ ] 6 [ σ ] 7 [ σ ] 8 [ σ ] 9 [ σ ] 1 [ σ ] 2 [ σ ] 3 [ σ ] 4 [ σ ] 5 [ σ ] 6 [ σ ] 7 [ σ ] 8 [ σ ] 9 [ σ
(c) next - O p (d) until - p U q

Fig. 6.4 Semantics of some LTL operators