CTL intuitive recall
(C) Alessandro Artale Known picture drawback - the runs should form trees!
1
CTL examples
Express in CTL:
A state where a is true, but b is not, is reachable.
Whenever system receives a request Req then it generates an
acknowledgement Ack eventually.
Whenever system receives a request Req then it is possible
that it will generate an acknowledgement Ack eventually.
In every run there are infinitely many b.
2
CTL examples
Express in CTL:
All the paths lead to Rome.
All the time if I have not died yet, then I have a chance to
survive one more day.
All the time if I get robbed then I can react by defending
myself or not defending myself.
3
CTL examples
Read CTL formula:
AG[ error =⇒ E(repair U operational) ]
AG[ error =⇒ AX A(!error W operational) ]
AG[ EF(restart) ]
AG[ EX(restart) ]
A[ p U A(q U r) ]
How to read:
AX, EX - necessarily next, possibly next
AF - necessarily in the future (or Inevitably)
EF - possibly in the future (or Possibly)
AG - globally (or Always)
AG(φ =⇒ ψ) - Whenever φ then ψ.
EG - possibly henceforth
AU, EU - necessarily until, possibly until
4
CTL properties
¬AGϕ ≡ EF¬ϕ
¬EGϕ ≡ AF¬ϕ
¬EXϕ ≡ AX¬ϕ
discuss ¬Gp in LTL
EX(ϕ ∨ ψ) ≡ EXϕ ∨ EXψ
EX(ϕ ∧ ψ) ≡ EXϕ ∧ EXψ
AX(ϕ ∨ ψ) ≡ AXϕ ∨ AXψ
AX(ϕ ∧ ψ) ≡ AXϕ ∧ AXψ
5
CTL vs. LTL examples
Express in LTL: EF[ a ∧ ¬b]
Compare the following formulae:
AG[ EF restart ] vs. G[ ¬(G¬ restart) ]
AG[ p =⇒ AF q ] vs. G( p =⇒ Fq )
AF[ AG p ] vs. FG p
AG[ AF p ] vs. GF p
AF[ AX p ] vs. FX p
Express in CTL: (GF p ∧ GF q) =⇒ ψ
6