IA169 System Verification and Assurance
CTL Model Checking
Jiří Barnat
Liner vs. Branching Time
Pnueli, 1977
System is viewed as a set of state sequences — Runs.
System properties are given as properties of runs,
... and can be described with a linear-time logic.
Clarke & Emerson, 1980
System is viewed as a branching structure of possible
executions from individual system states — Computation
Tree.
System properties are given as properties of the tree,
... and can be described with a branching-time logic.
IA169 System Verification and Assurance – 07 str. 2/34
System and Computation Tree
1 2
1 1 1 1
2 2 2 2
2 2 2 2
IA169 System Verification and Assurance – 07 str. 3/34
Section
Computation Tree Logic (CTL)
IA169 System Verification and Assurance – 07 str. 4/34
CTL Informally
Possible Future Computations
For a given node of a computation tree, the sub-tree rooted in
the given node describes all possible runs the system can still
take.
Every such a run is possible future computation.
CTL Formulae Allow For
Specification of state qualities with atomic propositions.
Quantify over possible future computations.
Restrict the set of possible future computations with
(quantified) LTL operators.
Example
ϕ ≡ EF(a)
It is possible to take a future computation such that a will
hold true in the computation eventually.
IA169 System Verification and Assurance – 07 str. 5/34
Syntax of CTL
Let AP by a set of atomic propositions.
If p ∈ AP, then p is a CTL formula.
If ϕ is a CTL formula, then ¬ϕ is a CTL formula.
If ϕ and ψ are CTL formulae, then ϕ ∨ ψ is a CTL formula.
If ϕ is a CTL formula, then EX ϕ is a CTL formula.
If ϕ and ψ are CTL formulae, then E[ϕ U ψ] is a CTL formula.
If ϕ and ψ are CTL formulae, then A[ϕ U ψ] is a CTL formula.
Alternatively (Backus-Naur Form)
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | A[ϕ U ϕ]
IA169 System Verification and Assurance – 07 str. 6/34
Syntactic Shortcuts
Already Known
The standard shortcuts from the propositional logic.
Syntactic shortcuts from LTL
F ϕ ≡ true U ϕ
G ϕ ≡ ¬F ¬ϕ
Deduced CTL Operators
EF ϕ ≡ E[true U ϕ]
AF ϕ ≡ A[true U ϕ]
EG ϕ ≡ ¬AF ¬ϕ
AG ϕ ≡ ¬EF ¬ϕ
AX ϕ ≡ ¬EX ¬ϕ
IA169 System Verification and Assurance – 07 str. 7/34
Models of CTL formulae
Model of a CTL formula
Let AP be a set of atomic propositions.
Model of a CTL formula is a state s ∈ S of Kripke structure
M = (S, T, I, s0).
Reminder
Run of a Kripke structure is maximal path starting at the
initial state of the structure.
Finite maximal paths are viewed as infinite runs due to infinite
repetition of the last state on the path.
Notation
Let s ∈ S be a state of Kripke structure M = (S, T, I, s0).
PM(s) = {π | π is a run initiated at state s}
IA169 System Verification and Assurance – 07 str. 8/34
Semantics of CTL
Assumptions
Let AP be a set of atomic propositions.
Let p ∈ AP be an atomic proposition.
Let s ∈ S be a state of Kripke structure M = (S, T, I, s0).
Let ϕ, ψ denote syntactically correct CTL formulae.
Semantics
s |= p iff p ∈ I(s)
s |= ¬ϕ iff ¬(s |= ϕ)
s |= ϕ ∨ ψ iff s |= ϕ or s |= ψ
s |= EX ϕ iff ∃π ∈ PM(s).π(1) |= ϕ
s |= E[ϕ U ψ] iff ∃π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and
∀0 ≤ i < k.π(i) |= ϕ))
s |= A[ϕ U ψ] iff ∀π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and
∀0 ≤ i < k.π(i) |= ϕ))
IA169 System Verification and Assurance – 07 str. 9/34
Task
Atomic Propositions
AP={a, b, Req, Ack, Restart}
Express with CTL Formulae
A state where a is true, but b is not, is reachable.
Whenever system receives a request Req, it generates
acknowledgement Ack eventually.
In every run there are infinitely many b’s.
There is always an option to reset the system (reach state
Restart).
IA169 System Verification and Assurance – 07 str. 10/34
Section
Model Checking CTL
IA169 System Verification and Assurance – 07 str. 11/34
Problem Statements
Model Checking CTL
Let M = (S, T, I, s0) be a Kripke structure.
Let ϕ be a CTL formula.
Does initial state of M satisfies ϕ?
Alternatively
Let M = (S, T, I, s0) be a Kripke structure.
Let ϕ be a CTL formula.
Compute a set of states of M satisfying ϕ.
Above mentioned approaches are also referred to as to
Local model checking problem — M, s0 |= ϕ.
Global model checking problem — {s | M, s |= ϕ}.
IA169 System Verification and Assurance – 07 str. 12/34
Algorithm for CTL Model Checking — Idea
Observation
If the validity of formulae ϕ and ψ is known for all states, it is
easy to deduce validity of formulae ¬ϕ, ϕ ∨ ψ, EX ϕ, . . . .
CTL Model Checking – Sketch
Let M = (S, T, I) be a Kripke structure and ϕ a CTL
Formula.
A labelling function label : S → 22ϕ
is computed such that it
gives validity of all sub-formulae of ϕ for all states of Kripke
structure M.
Obviously, s0 |= ϕ ⇐⇒ ϕ ∈ label(s0).
Function label is computed gradually for individual
sub-formulae of ϕ, starting with the simplest sub-formula and
proceeding towards more complex sub-formulae, ending with
ϕ itself.
IA169 System Verification and Assurance – 07 str. 13/34
Sub-formulae of a CTL Formula
Sub-formulae of formula ϕ
Let ϕ be a CTL formula.
The set of all sub-formulae of formula ϕ is denoted by 2ϕ.
2ϕ is defined inductively according to the structure of ϕ.
Inductive Definition of 2ϕ
1) ϕ ∈ 2ϕ (ϕ is a sub-formula of ϕ)
2) If η ∈ 2ϕ and
η ≡ ¬ψ, then ψ ∈ 2ϕ
η ≡ ψ1 ∨ ψ2, then ψ1, ψ2 ∈ 2ϕ
η ≡ EX ψ, then ψ ∈ 2ϕ
η ≡ E[ψ1 U ψ2], then ψ1, ψ2 ∈ 2ϕ
η ≡ A[ψ1 U ψ2], then ψ1, ψ2 ∈ 2ϕ
3) Nothing else.
IA169 System Verification and Assurance – 07 str. 14/34
Equivalent Existential Form of CTL
Observation
Is is easier to proof validity of existential quantified modal
operators than validity of universally quantified ones.
For the purpose of verification of CTL-specified properties, it
is possible to express the CTL formula in an equivalently
expressive existential form of CTL.
Equivalent CTL Syntax
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ
Task
Express formula EG ϕ in the original syntax of CTL.
Give accordingly modified definition of the set of sub-formulae
of ϕ for the above mentioned equivalent syntax.
IA169 System Verification and Assurance – 07 str. 15/34
Algorithm for CTL Model-Checking
INPUT: Kripke structure M = (S, T, I, s0), CTL formula ϕ.
OUTPUT: True, if s0 |= ϕ; False otherwise.
proc CTLMC(ϕ, M)
label := I
Solved := AP ∩ 2ϕ
while ϕ ∈ Solved do
foreach ( η ∈ {¬ψ1, ψ1 ∨ ψ2, EX ψ1, E[ψ1 U ψ2], EG ψ1 | ψ1, ψ2 ∈ Solved})do
if (η ∈ 2ϕ
and η ∈ Solved)
then label := updateLabel(η, label, M)
Solved := Solved ∪ {η}
fi
od
od
return (ϕ ∈ label(s0))
end
IA169 System Verification and Assurance – 07 str. 16/34
Algorithm for CTL Model-Checking updateLabel()
proc updateLabel(η, label, M)
if (η ≡ E[ψ1 U ψ2])
then return checkEU(ψ1, ψ2, label, M)
fi
if (η ≡ EG ψ)
then return checkEG(ψ, label, M)
fi
foreach ( s ∈ S)do
if (η ≡ ¬ψ and ψ ∈ label(s)) or
(η ≡ ψ1 ∨ ψ2 and (ψ1 ∈ label(s) ∨ ψ2 ∈ label(s))) or
(η ≡ EX ψ and (∃t ∈ {t | (s, t) ∈ T} such that ψ ∈ label(t)))
then label(s) := label(s) ∪ {η}
fi
od
return label
end
IA169 System Verification and Assurance – 07 str. 17/34
Algorithm for CTL Model-Checking E[ψ1 U ψ2]
INPUT: Kripke structure M = (S, T, I),
Labelling function label : S → 2ϕ
, correct w.r.t validity of ψ1 and ψ2
OUTPUT: Labelling function label : S → 2ϕ
, correct w.r.t E[ψ1 U ψ2]
proc checkEU(ψ1, ψ2, label, M)
Q := {s | ψ2 ∈ label(s)}
foreach ( s ∈ Q)do
label(s) := label(s) ∪ {E[ψ1 U ψ2]}
od
while (Q = ∅) do
choose s ∈ Q
Q := Q {s}
foreach ( t ∈ {t | T(t, s)}) do /* all immediate predecessors */
if (E[ψ1 U ψ2] ∈ label(t) ∧ ψ1 ∈ label(t))
then label(t) := label(t) ∪ {E[ψ1 U ψ2]}
Q := Q ∪ {t}
fi
od
od
return label
end
IA169 System Verification and Assurance – 07 str. 18/34
Strongly Connected Components
Sub-graph
Let G = (V , E) be a graph, ie. E ⊆ V × V .
Graph G = (V , E ) is called sub-graph of G if it holds that
V ⊆ V and E = E ∩ V × V .
Sub-graph C = (V , E ) of G = (V , E) is called
Strongly Connected Component, if ∀u, v ∈ V it holds that
(u, v) ∈ E ∗ and (v, u) ∈ E ∗.
Maximal Strongly Connected Component (SCC), if C is
strongly connected component and for every v ∈ (V V ) it
is the case that (V ∪ {v}, E ∩ (V ∪ {v} × V ∪ {v})) is not.
Non-trivial SCC, if C is Strongly Connected Component and
E = ∅.
IA169 System Verification and Assurance – 07 str. 19/34
Algorithm for CTL Model-Checking EG ψ
INPUT: Kripke structure M = (S, T, I, s0),
Labelling function label : S → 2ϕ
, correct w.r.t. ψ
OUTPUT: Labelling function label : S → 2ϕ
, correct w.r.t. EG ψ
proc checkEG(ψ, label, M)
S’ := {s | ψ ∈ label(s)}
SCC := {C | C is non-trivial SCC G = (S , T ∩ S × S )}
Q := C∈SCC
{s | s ∈ C}
foreach ( s ∈ Q)do
label(s) := label(s) ∪ {EG ψ}
od
while Q = ∅ do
choose s ∈ Q
Q := Q {s}
foreach ( t ∈ (S ∩ {t | T(t, s)}))do /* all immediate predecessors in S */
if EG ψ ∈ label(t)
then label(t) := label(t) ∪ {EG ψ}
Q := Q ∪ {t}
fi
od
od
end
IA169 System Verification and Assurance – 07 str. 20/34
Complexity of Algorithm for CTL Model Checking
Observation
Every CTL formula ϕ is made of at most | ϕ | sub-formulae.
Decomposition of every sub-graph of G = (S, T) into SCCs
can be done in time O(| S | + | T |).
Every call to updateLabel terminates in time O(| S | + | T |).
Overall complexity
Algorithm CTLMC exhibits O(| ϕ || S |) space
and O(| ϕ | (| S | + | T |)) time complexity.
IA169 System Verification and Assurance – 07 str. 21/34
Example: Microwave oven AG(Start =⇒ AF(Heat))
IA169 System Verification and Assurance – 07 str. 22/34
Example: Microwave oven AG(Start =⇒ AF(Heat))
Transformation of formula ϕ ≡ AG(Start =⇒ AF(Heat))
AG(Start =⇒ AF(Heat))
AG(¬(Start ∧ ¬AF(Heat)))
AG(¬(Start ∧ EG(¬Heat)))
¬EF(Start ∧ EG(¬Heat))
¬E[true U (Start ∧ EG(¬Heat))]
Validity of sub-formulae [S(ϕ) = {s | s |= ϕ}]
S(Start) = {2, 5, 6, 7}
S(Heat) = {4, 7}
S(¬Heat) = {1, 2, 3, 5, 6}
S(EG(¬Heat)) = {1, 2, 3, 5}
S(Start ∧ EG(¬Heat)) = {2, 5}
S(E[true U (Start ∧ EG(¬Heat))]) = {1, 2, 3, 4, 5, 6, 7}
S(¬E[true U (Start ∧ EG(¬Heat))]) = ∅
IA169 System Verification and Assurance – 07 str. 23/34
Section
CTL∗
IA169 System Verification and Assurance – 07 str. 24/34
CTL∗
as Extension of CTL
Observation
Every use of temporal operator in a formula of CTL must be
immediately preceded with a quantifier, i.e. use of a modal
operator without quantification is not possible.
Logic CTL∗
Branching time logic.
Similar to CTL.
Unlike CTL, allows for standalone use of modal operators.
Example
A[p ∧ X(¬p)] is CTL∗, but is not CTL formula.
IA169 System Verification and Assurance – 07 str. 25/34
Syntax of CTL∗
Types of CTL∗ formulae
Quantifiers E and A are standalone operators in syntax
construction rules. As a result there are two types of formulae
in CTL: path and state formulae.
Application of E and A operators on a path formula (formula
of which model is a run of Kripke structure) results in a state
formula (formula of which model is a state of Kripke
structure)
Syntax of CTL∗
state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | E ψ
path formula ψ ::= ϕ | ¬ψ | ψ ∨ ψ | X ψ | ψ U ψ
IA169 System Verification and Assurance – 07 str. 26/34
Semantics of CTL∗
Assumption
Let AP be a set of atomic propositions, and p ∈ AP.
Let M = (S, T, I) be a Kripke structure.
Let ϕi denote CTL∗ state formulae, and ψi denote CTL∗ state
formulae.
Semantics
M, s |= p iff p ∈ I(s)
M, s |= ¬ϕ1 iff ¬(M, s |= ϕ1)
M, s |= ϕ1 ∨ ϕ2 iff M, s |= ϕ1 or M, s |= ϕ2
M, s |= E ψ1 iff ∃π ∈ PM (s).π |= ψ1
M, π |= ϕ1 iff M, π(0) |= ϕ1
M, π |= ¬ψ1 iff ¬(M, π |= ψ1)
M, π |= ψ1 ∨ ψ2 iff M, π |= ψ1 or M, π |= ψ2
M, π |= X ψ1 iff M, π1
|= ψ1
M, π |= ψ1 U ψ2 iff ∃k ≥ 0.(M, πk
|= ψ2 and
∀0 ≤ i < k.M, πi
|= ψ1)
IA169 System Verification and Assurance – 07 str. 27/34
Section
Comparison of Expressive Power of
LTL, CTL and CTL∗
IA169 System Verification and Assurance – 07 str. 28/34
Model Unification
Observation
Every LTL formula is a CTL∗ path formula.
Every CTL formula is a CTL∗ state formula.
Model of a path formula is a run of Kripke structure.
Model of a state formula is a state of Kripke structure.
Not very suitable for comparison.
Model Unification
For the purpose of comparison we define how a CTL∗ path
formula is evaluated in a state of Kripke structure.
Let ψ be CTL∗ path formula, then
M, s |= ψ iff M, s |= A ψ
IA169 System Verification and Assurance – 07 str. 29/34
Motivation
Goals
We intend to find out whether there are properties (formulae)
that can be expressed in one of the logic, but cannot be
expressed in another one.
We intend to find out in which logic more properties can be
expressed.
We intend to identify concrete properties, that cannot be
expressed in some other logic, i.e. to find out a formula of
logic L1, for which an equivalent formula of logic L2 does not
exist.
Formula Equivalence
Formulae ϕ and ψ are equivalent if and only if for any possible
Kripke structure M = (S, T, I, s0) and any state s ∈ S it is
true that
M, s |= ϕ iff M, s |= ψ.
IA169 System Verification and Assurance – 07 str. 30/34
Equivalent Expressive Power
Equivalently Expressive
Temporal logic L1 and L2 have the same expressive power, if
for all Kripke structures M = (S, T, I, s0) and states s ∈ S it
holds that
∀ϕ ∈ L1.(∃ψ ∈ L2.(M, s |= ϕ ⇐⇒ M, s |= ψ)) (1)
∧ ∀ψ ∈ L2.(∃ϕ ∈ L1.(M, s |= ϕ ⇐⇒ M, s |= ψ)). (2)
Less Expressiveness
If only statement (1) is valid, then logic L1 is less expressive
than logic L2, and vice versa.
IA169 System Verification and Assurance – 07 str. 31/34
Comparison of LTL, CTL, and CTL∗
Theorem
LTL and CTL are incomparable in expressive power.
1) AG(EF(q)) is a CTL formula that cannot be expressed in LTL.
2) FG(q) is an LTL formula that cannot be expressed in CTL.
Example – Proof Sketch for 1)
Find two different Kripke structures and identify two states
that can be differentiated with CTL formula AG(EF(q)), but
cannot be differentiated with any LTL formula (they generate
the same set of runs).
Example – Intuition behind 2) [proof is too complex]
Show that CTL formula AF(AG(q)) is not equivalent to LTL
formula FG(q).
IA169 System Verification and Assurance – 07 str. 32/34
Comparison of LTL, CTL, and CTL∗
Consequence
CTL∗ is strictly more expressive than LTL.
Every LTL formula is a CTL∗
formula.
CTL∗
formula AG(EFq) is not expressible in LTL.
Consequence 2
CTL∗ is strictly more expressive than CTL.
Every CTL formula is a CTL∗
formula.
CTL∗
formula FG(q) is not expressible in CTL.
Observation
There are properties expressible on both LTL and CTL.
CTL formula A[p U q] is equivalent to LTL formula p U q.
IA169 System Verification and Assurance – 07 str. 33/34
Homework
Homework
Solve The wolf, goat and cabbage problem with NuSMV
Moshe Vardi: Branching vs. Linear Time: Final Showdown
IA169 System Verification and Assurance – 07 str. 34/34