a modal logic for reasoning about dynamic scenarios
similar to temporal modal logic, plus:
more complex modal operators
compact, graphical representation of sets of Kripke models
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:
B is true in
[si, si+1, si+2, … ]
for all j such that 0 ≤ j < i,
formula A is true in
[sj, sj+1, sj+2, … ]
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"
cannot express "formula is true at time 2 in trace
[s0, s1, s2, s3 … ]"
expressed in the equivalent way: "formula is true in the trace
[s2, s3, s4, s5 … ]"
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
x ∧ Gy would become: x true in s0 and
Gy true in s0
s0 tells the value of x, but…
no way to evaluate Gy knowing only s0
(requires whole trace)
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:
B is true in
[si, si+1, si+2, … ]
for all j such that 0 ≤ j < i,
formula A is true in
[sj, sj+1, sj+2, … ]
meaning:
B is true at time i
for times between 0 and i-1, formula A is true
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:
true in the trace
[ab, ¬ab, ¬ab, ¬ab, … ]
false in the trace
[ab, a¬b, ¬ab, ab, a¬b, ¬ab, … ]
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