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.
2019-10-08
CTL examples
• EF[ a ∧ ¬b]
• AG[ Req =⇒ AF repair ]
• AG[ Req =⇒ EF repair ]
• AG[ AF b ]
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.
2019-10-08
CTL examples
• AF Rome
• AG[ ¬Death =⇒ EX ¬Death]
• AG[ Robbed =⇒ ( EX Defend ∧ EX ¬Defend )]
do not confuse with AG[ Robbed =⇒ EX ( Defend ∧ ¬Defend )]
or with AG[ Robbed =⇒ EX ( Defend ∨ ¬Defend )]
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
2019-10-08
CTL examples
• Whenever there is an error, it is in a repair mode until it gets
operational.
• Whenever there is an error, it stays without error until it gets
operational or it stays without error forever.
Whenever there is an error, there is no other error in the subsequent
state before getting operational.
• There is always an option/possibility to restart the system
eventually.
• There is always an option/possibility to restart the system
immediatelly.
• All paths has to satisfy the regular expression p∗
q∗
r in its prefix.
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) =⇒ ψ
2019-10-08
CTL vs. LTL examples
• AG[EF( restart)] - not expressible in LTL
• AG[ p =⇒ AF q ] vs. G[ p =⇒ Fq ] - the same
• AF[AG p] vs. FG p - different
• AG[AF p] vs. GF p - the same
• AF[AX p] vs. FX p - different
EF[ a∧¬b] - not directly, we can express (and check) its negation (GF p]∧
G[F q]) =⇒ ψ - fairness is not directly expressible in CTL