Linear Temporal Logic (LTL)

a modal logic for reasoning about dynamic scenarios

similar to temporal modal logic, plus:


Trace

trace: sequence of propositional interpretations

equivalent to a Kripke model in modal logic

called trace because in LTL the term model means something else


Modal operators

G
globally: true now and forever
(like of temporal logic)
F
eventually (finally): true now or sometime in the future
(like of temporal logic)
X
next: true in the next state
(does not exist in temporal logic)
U
until: something true until something else happens
(does not exist in temporal logic)

Evaluation

a modal formula can be true or false in a trace

example:

in this trace:

x ∨ ¬y
true: is true in the first state of the trace
X¬y
true, because y is false in the second state
XXy
false, because y is false in the third state
Gx
true, because x is true in all states
Gy
false, because y is not true in all states
(it is true only in some states)

Evaluation

same trace:

GFy
true: for all states of the sequence, there is some future point where y is true
xU¬y
true: x is true until ¬y becomes true;
(in the first state x is true, then ¬y becomes true)
X(yU¬x)
false: in the next state, y is false but x not (yet) true
yUXXy
true: in the first state y is true, in the second state XXy is true
(because y is true two states later)
G(yUXXy)
not straightforward to check: all states have to be checked for yUXXy
in turn, check XXy in all states

labeling algorithm: mark states with subformulae true there


Current state

semantics: formula true or false in a trace?

trace: [s0, s1, s2, s3 …]

in which state of the trace?

assumption: we always evaluate the formula in s0
(first state of the trace)

how to evaluate in s2, for example?

to evaluate in s2, use the trace [s2, s3 … ]

in general, [si, si+1, … ]


Semantics

in a trace [s0, s1, s2, s3 … ]:
(some explanations next)

x
true if x is true in s0
A ∧ B
true if A is true in [s0, s1, s2, s3 … ] and B is true in [s0, s1, s2, s3 … ]
¬A, A ∨ B
same
XA
true if A true in [s1, s2, s3 … ]
FA
true if there exists i such that A is true in [si, si+1, si+2, … ]
GA
true if, for all i, formula A is true in [si, si+1, si+2, … ]
AUB
true if there exists i such that:

some explanation, now...


Time point

in the semantics of the traces, no reference to "time points"

cannot say "formula is true at time 2"

can only say "formula is true at time 0"

works because no reference to the past can be made
no formula for: in the previous step F was true, etc.
(=no problem if the new trace does not contain s0 and s1)


Semantics: propositional operators

A ∧ B
true if A is true in [s0, s1, s2, s3 … ] and B is true in [s0, s1, s2, s3 … ]

why not just: both A and B true in s0?

A and B may contain modal operators


Semantics: next, eventually, globally

all based on the same concept:

evaluating at time i = evaluating in the trace [si, si+1, si+2, si+3 … ]

for example, FA means: A is true at some time i

expressed as: there exists i such that A is true in [si, si+1, si+2, si+3 … ]


Semantics: until

AUB
true if there exists i such that:

meaning:

still using the formalization of "true at time i"


Structure

compact way of representing a set of traces

intuition:

given some domain, represent possible transitions between states

traces are infinite paths from the initial states in such a graph
(initial state denoted by a "short arrow", in this case ab)

since they have to be infinite, each node must have at least a successor


Traces: example (1)

trace:

[ab, a¬b, ¬ab, ab, a¬b, … ]


Traces: example (2)

trace:

[ab, ¬ab, ¬ab, ¬ab, … ]


Traces: example (3)

trace:

[ab, ¬ab, ab, ¬ab, ab, … ]


Traces: example (4)

(second time in a state we can make a different choice)

trace:

[ab, a¬b, ¬ab, ab, ¬ab, ¬ab, ¬ab, … ]


Evaluation in a structure

a structure defines a set of traces
(all paths that can be taken from the initial state)

a formula can be true or false in a trace

formula is true in a structure if:

existential evaluation
formula is true in at least one trace
universal evaluation
formula is true in all traces

Kind of evaluation: difference

formula Gb is:

therefore: true in at least a trace, not in all traces


LTL: limit

evaluation can be done in two ways: "exists a trace" or "in all traces"

they cannot be mixed

cannot say: there exists a path to a state where formula becomes then true in all subsequent paths

can be done in CTL*