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 )
2020-11-09
LTL examples
• X rain - it will rain tomorrow
• F rain - it will rain eventually
• pick-up R kin-gar - pick-up releases a child from kindergarten
• G(drop-off =⇒ (kin-gar U pick-up)) - contrary to the previous one
pick-up can be out of kin-gar
• G (¬(cs1 ∧ cs2)) - mutual exclusion (in critical sections)
• G (req =⇒ F resp) . . . Does it guarantee that #req = #resp? - no
• G F chocolate - chocolate infinitely many times
• (G F req) =⇒ (G F resp) - only infinitely many requests cause
infinitely many responses
• sin =⇒ (F G hell ) - sin causes hell
• F(sin ∧ (¬confession U death)) =⇒ (F G hell ) - improved with
confession
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.
2020-11-09
LTL properties - example
• Whenever Alice eats, she is on the left
G (ae =⇒ al)
• Whenever Bob is on the left, he will eat eventually
G (bl =⇒ F be)
• Whenever Bob eats, he will immediately go to the left
G (be =⇒ X bl)
• If Alice does not eat before Bob, she will never eat
((¬ae) U be) =⇒ G (¬ae)
• Alice and Bob will never be on the same side from some point
FG((al ∧ br) ∨ (ar ∧ bl))
• Bob chases Alice until they both eat together
((al =⇒ X bl) ∧ (ar =⇒ X br)) W (ae ∧ be)
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 ψ)
2020-11-09
LTL properties - distributivity questions
• 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 ψ)