LTL examples
What formulas are true on what systems?
If not, show a counterexample.
¬a ∧ b
F a
¬a U b
G b
F G b
a, ¬b
¬a, ¬bstart
¬a, b
¬a, b
a, ¬b
¬a, ¬bstart
¬a, b
¬a, b
a, ¬b
¬a, ¬bstart
¬a, b
¬a, b
a, ¬b
¬a, ¬b
¬a, bstart
¬a, b
LTL examples
X rain
F rain
pick-up R kin-gar
G(drop-off =⇒ (kin-gar U pick-up))
G (¬(cs1 ∧ cs2))
G (req =⇒ F resp) . . . Does it guarantee that #req = #resp?
G F chocolate
(G F req) =⇒ (G F resp)
sin =⇒ (F G hell )
F(sin ∧ (¬confession U death)) =⇒ (F G hell )
2
LTL properties - example
You have two fishes, say Alice (A) and Bob (B). There is an
aquarium divided into two parts: left (L) and right (R). Both fish
start on the right side of the aquarium and do the following
sequence of steps (independently): They move to the left, eat,
move back to the right. Formulate using LTL:
Whenever Alice eats, she is on the left.
Whenever Bob is on the left, he will eat eventually.
Whenever Bob eats, he will immediately go to the left.
If Alice does not eat before Bob, she will never eat.
Alice and Bob will never be on the same side from some point.
Bob chases Alice until they both eat together.
3
LTL properties - negation
Note and discuss that
ψ =⇒ ϕ U ψ
ψ U ψ ≡ ψ
true U ϕ ≡ Fϕ
(¬ψ) U ψ ≡ Fψ
¬(X ϕ) ≡ X ¬ϕ
¬(G ϕ) ≡ F ¬ϕ
ϕ W ψ ≡ ϕ U ψ ∨ G ϕ
¬(ϕ R ψ) ≡ ¬ϕ U ¬ψ
ϕ R ψ ≡ ψ W (ϕ ∧ ψ)
4
LTL - temporal properties
Note and discuss that
F ϕ ≡ F (F ϕ)
G ϕ ≡ G (G ϕ)
ϕ U ψ ≡ ϕ U (ϕ U ψ)
ϕ U ψ ≡ ψ ∨ (ϕ ∧ X (ϕ U ψ))
ϕ W ψ ≡ ψ ∨ (ϕ ∧ X (ϕ W ψ))
ϕ R ψ ≡ ψ ∧ (ϕ ∨ X (ϕ R ψ))
G ϕ ≡ ϕ ∧ X (G ϕ)
F ϕ ≡ ϕ ∨ X (F ϕ)
X F ϕ ≡ F (X ϕ)
X G ϕ ≡ G (X ϕ)
X(ϕ U ψ) ≡ (Xϕ) U (Xψ)
5
LTL properties - distributivity questions
Is it true that ...
X(ϕ ∨ ψ)
?
≡ Xϕ ∨ Xψ
X(ϕ ∧ ψ)
?
≡ Xϕ ∧ Xψ
F(ϕ ∨ ψ)
?
≡ Fϕ ∨ Fψ GF(ϕ ∨ ψ)
?
≡ GFϕ ∨ GFψ
F(ϕ ∧ ψ)
?
≡ Fϕ ∧ Fψ GF(ϕ ∧ ψ)
?
≡ GFϕ ∧ GFψ
G(ϕ ∨ ψ)
?
≡ Gϕ ∨ Gψ FG(ϕ ∨ ψ)
?
≡ FGϕ ∨ FGψ
G(ϕ ∧ ψ)
?
≡ Gϕ ∧ Gψ FG(ϕ ∧ ψ)
?
≡ FGϕ ∧ FGψ
ϕ U (ψ1 ∨ ψ2)
?
≡ (ϕ U ψ1) ∨ (ϕ U ψ2)
ϕ U (ψ1 ∧ ψ2)
?
≡ (ϕ U ψ1) ∧ (ϕ U ψ2)
(ϕ1 ∨ ϕ2) U ψ
?
≡ (ϕ1 U ψ) ∨ (ϕ2 U ψ)
(ϕ1 ∧ ϕ2) U ψ
?
≡ (ϕ1 U ψ) ∧ (ϕ2 U ψ)
6