IA169 Model Checking
CTL model checking
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Linear vs. branching time
linear time view
Amir Pnueli, 1977
system behavior can be seen as a set of state sequences
property is a restriction applied to each such a sequence
property can be described by LTL
IA169 Model Checking: CTL model checking 2/33
Linear vs. branching time
linear time view
Amir Pnueli, 1977
system behavior can be seen as a set of state sequences
property is a restriction applied to each such a sequence
property can be described by LTL
branching time view
Edmund M. Clarke and E. Allen Emerson, 1980
system behavior is a computation tree, i.e., a branching structure of possible
successors of each reachable state of the system
property is a restriction on the tree
property can be described by CTL or CTL*
IA169 Model Checking: CTL model checking 3/33
Example of a system and its computation tree
1 2
11 1 1
2 2 2 2
2 2 2 2
· · ·
...
...
...
...
IA169 Model Checking: CTL model checking 4/33
Agenda and sources
agenda
computation tree logic (CTL)
CTL model checking
CTL*
source
Chapters 5 and 6 of E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and R.
Bloem: Model Checking, Second Edition, MIT, 2018.
IA169 Model Checking: CTL model checking 5/33
Computation tree logic (CTL)
Intuition for CTL
we present only state-based CTL model checking
for a given in node of a computation tree, the subtree rooted by the node
represents all possible runs from the node
CTL formula talks about runs from this node
CTL uses temporal operators X, U, F, G known from LTL, but extended with
quantifier A saying that the formula should hold on all runs or quantifier E
saying that there exists a run satisfying the formula
for example, EFa says that there exists a run from the node such that a holds
somewhere on the run
IA169 Model Checking: CTL model checking 7/33
Computation tree logic (CTL)
Definition (computation tree logic, CTL)
Formulae of Computation Tree Logic (CTL) are defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | EXφ | E(φ1 U φ2) | A(φ1 U φ2)
where ⊤ stands for true and a ranges over a countable set AP.
By AP(φ) we denote the set of atomic propositions appearing in φ.
IA169 Model Checking: CTL model checking 8/33
Computation tree logic (CTL)
Definition (computation tree logic, CTL)
Formulae of Computation Tree Logic (CTL) are defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | EXφ | E(φ1 U φ2) | A(φ1 U φ2)
where ⊤ stands for true and a ranges over a countable set AP.
By AP(φ) we denote the set of atomic propositions appearing in φ.
abbreviations
standard ones for ⊥, ∨, ⇒, ⇔
EFφ ≡ E(⊤ U φ)
AFφ ≡ A(⊤ U φ)
EGφ ≡ ¬AF¬φ
AGφ ≡ ¬EF¬φ
AXφ ≡ ¬EX¬φ
IA169 Model Checking: CTL model checking 9/33
Intuitive semantic of CTL
EXa AXa
E(a U b) A(a U b)
EFa AFa
EGa AGa
IA169 Model Checking: CTL model checking 10/33
Semantics of CTL
we interpret CTL over states of a Kripke structure
we assume that each state of a Kripke structure has at least one successor
Definition (path)
Let K = (S, T, S0, L) be a Kripke structure and s ∈ S be its state. An (infinite) path
of K starting in s is an infinite sequence π = s0s1s2 . . . of states such that s0 = s
and (si, si+1) ∈ T holds for each i ≥ 0.
By π(i) we denote the state si of π.
By πi we denote the infinite path π(i)π(i + 1)π(i + 2) . . ..
By PK (s) we denote the set of all infinite paths starting in s.
IA169 Model Checking: CTL model checking 11/33
Semantics of CTL
Definition
The relation K, s |= φ, meaning that state s of a Kripke structure K = (S, T, S0, L)
satisfies CTL formula φ, is defined inductively as follows.
K, s |= ⊤
K, s |= a iff a ∈ L(s)
K, s |= ¬φ iff K, s ̸|= φ
K, s |= φ1 ∧ φ2 iff K, s |= φ1 ∧ K, s |= φ2
K, s |= EXφ iff ∃π ∈ PK (s) . K, π(1) |= φ
K, s |= E(φ1 U φ2) iff ∃π ∈ PK (s) . ∃i ≥ 0 . K, π(i) |= φ2 ∧
∧ ∀ 0 ≤ j < i . K, π(j) |= φ1
K, s |= A(φ1 U φ2) iff ∀π ∈ PK (s) . ∃i ≥ 0 . K, π(i) |= φ2 ∧
∧ ∀ 0 ≤ j < i . K, π(j) |= φ1
IA169 Model Checking: CTL model checking 12/33
Semantics of CTL
Definition
The relation K, s |= φ, meaning that state s of a Kripke structure K = (S, T, S0, L)
satisfies CTL formula φ, is defined inductively as follows.
K, s |= ⊤
K, s |= a iff a ∈ L(s)
K, s |= ¬φ iff K, s ̸|= φ
K, s |= φ1 ∧ φ2 iff K, s |= φ1 ∧ K, s |= φ2
K, s |= EXφ iff ∃π ∈ PK (s) . K, π(1) |= φ
K, s |= E(φ1 U φ2) iff ∃π ∈ PK (s) . ∃i ≥ 0 . K, π(i) |= φ2 ∧
∧ ∀ 0 ≤ j < i . K, π(j) |= φ1
K, s |= A(φ1 U φ2) iff ∀π ∈ PK (s) . ∃i ≥ 0 . K, π(i) |= φ2 ∧
∧ ∀ 0 ≤ j < i . K, π(j) |= φ1
K satisfies φ, written K |= φ, if K, s0 |= φ holds for every s0 ∈ S0.
IA169 Model Checking: CTL model checking 13/33
Exercise
condsider a Kripke structure with atomic propositions {a, b, r, restart}
express the following properties by CTL formulae
1 it is possible to reach a state where a holds and b does not
2 whenever request r is received, the system eventually generates
acknowledgment a
3 whenever b holds, it is possible that b will never hold again
4 there is always an option to reset by system, i.e., to reach a state where restart
holds
IA169 Model Checking: CTL model checking 14/33
CTL model checking
CTL model checking problems
Let K = (S, T, S0, L) be a Kripke structure and φ be a CTL formula. We can
consider the following problems.
to decide whether K |= φ
local CTL model checking problem: to decide whether K, s |= φ holds for a
given state s ∈ S
global CTL model checking problem: to compute the set of states where φ
holds, i.e., the set {s ∈ S | K, s |= φ}.
IA169 Model Checking: CTL model checking 16/33
CTL model checking problems
Let K = (S, T, S0, L) be a Kripke structure and φ be a CTL formula. We can
consider the following problems.
to decide whether K |= φ
local CTL model checking problem: to decide whether K, s |= φ holds for a
given state s ∈ S
global CTL model checking problem: to compute the set of states where φ
holds, i.e., the set {s ∈ S | K, s |= φ}.
We present an algorithm that can decide all the problems on finite Kripke
structures. Since now on, we consider only Kripke structures with finitely many
states.
IA169 Model Checking: CTL model checking 17/33
Idea of the algorithm
let K = (S, T, S0, L) be a Kripke structure and φ be a CTL formula
we transform φ to the form that uses only existentially quantified temporal
operators EX, EG, EU (i.e., not AU) using the equivalence
A(φ U ψ) ≡ ¬EG¬ψ ∧ ¬E(¬ψ U (¬φ ∧ ¬ψ))
hence, we assume that φ is of the form
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | EXφ | EGφ | E(φ1 U φ2)
let subf(φ) denote all subformulae of φ, for example
subf(E(¬a U EG(b ∧ c))) = {E(¬a U EG(b ∧ c)), ¬a, a, EG(b ∧ c), b ∧ c, b, c}
the algorithm computes function label : S → 2subf(φ) assigning to each state s
the set of all subformulae ψ satisfying K, s |= ψ
the function is built gradually, starting with the atomic proposition of φ and
proceeding towards more complex subformulae, ending with φ itself
IA169 Model Checking: CTL model checking 18/33
CTL model checking algorithm
input : a Kripke structure K = (S, T, S0, L) and a CTL formula φ
output: function label : S → 2subf(φ)
satisfying φ ∈ label(s) iff K, s |= φ for each s ∈ S
procedure CTLmc(K, φ)
forall s ∈ S do label(s) ← (L(s) ∩ AP(φ)) ∪ ({⊤} ∩ subf(φ))
solved ← AP(φ) ∪ ({⊤, ⊥} ∩ subf(φ))
while φ ̸∈ solved do
choose ψ ∈ subf(φ) ∖ solved such that subf(ψ) ∖ {ψ} ⊆ solved
updateLabel(ψ)
solved ← solved ∪ {ψ}
return label
procedure updateLabel(ψ)
if ψ ≡ E(ρ1 U ρ2) then checkEU(ρ1, ρ2)
if ψ ≡ EGρ then checkEG(ρ)
forall s ∈ S do
if ψ ≡ ¬ρ and ρ ̸∈ label(s) then label(s) ← label(s) ∪ {ψ}
if ψ ≡ ρ1 ∧ ρ2 and ρ1, ρ2 ∈ label(s) then label(s) ← label(s) ∪ {ψ}
if ψ ≡ EXρ and there exists s′
∈ S such that (s, s′
) ∈ T and ρ ∈ label(s′
) then
label(s) ← label(s) ∪ {ψ}
IA169 Model Checking: CTL model checking 19/33
CTL model checking algorithm
procedure checkEU(ρ1, ρ2)
Q ← {s | ρ2 ∈ label(s)}
forall s ∈ Q do label(s) ← label(s) ∪ {E(ρ1 U ρ2)}
while Q ̸= ∅ do
choose s ∈ Q
Q ← Q ∖ {s}
forall s′
such that (s′
, s) ∈ T do
if ρ1 ∈ label(s′
) and E(ρ1 U ρ2) ̸∈ label(s′
) then
label(s′
) ← label(s′
) ∪ {E(ρ1 U ρ2)}
Q ← Q ∪ {s′
}
IA169 Model Checking: CTL model checking 20/33
CTL model checking algorithm
procedure checkEG(ρ)
S′
← {s | ρ ∈ label(s)}
Q ← {s | s is a node of some nontrivial SCC of graph (S′
, T ∩ (S′
× S′
))}
forall s ∈ Q do label(s) ← label(s) ∪ {EGρ}
while Q ̸= ∅ do
choose s ∈ Q
Q ← Q ∖ {s}
forall s′
such that (s′
, s) ∈ T do
if ρ ∈ label(s′
) and EGρ ̸∈ label(s′
) then
label(s′
) ← label(s′
) ∪ {EGρ}
Q ← Q ∪ {s′
}
IA169 Model Checking: CTL model checking 21/33
Example
check if microwave oven satisfies
AG(Start ⇒ AF Heat)
IA169 Model Checking: CTL model checking 22/33
Transformation of formula AG(Start ⇒ AF Heat)
AG(Start ⇒ AF Heat) ≡ ¬EF(¬(Start ⇒ AF Heat))
≡ ¬EF(Start ∧ ¬AF Heat)
≡ ¬EF(Start ∧ EG¬Heat)
≡ ¬E(⊤ U (Start ∧ EG¬Heat))
IA169 Model Checking: CTL model checking 23/33
Transformation of formula AG(Start ⇒ AF Heat)
AG(Start ⇒ AF Heat) ≡ ¬EF(¬(Start ⇒ AF Heat))
≡ ¬EF(Start ∧ ¬AF Heat)
≡ ¬EF(Start ∧ EG¬Heat)
≡ ¬E(⊤ U (Start ∧ EG¬Heat))
subformuala ρ states satisfying ρ, i.e. {s | K, s |= ρ}
⊤ {1, 2, 3, 4, 5, 6, 7}
Start {2, 5, 6, 7}
Heat {4, 7}
¬Heat {1, 2, 3, 5, 6}
EG¬Heat {1, 2, 3, 5}
Start ∧ EG¬Heat {2, 5}
⊤ U (Start ∧ EG¬Heat) {1, 2, 3, 4, 5, 6, 7}
¬E(⊤ U (Start ∧ EG¬Heat)) ∅
IA169 Model Checking: CTL model checking 24/33
Complexity of the CTL model checking algorithm
each formula φ has at most |φ| subformulae
decomposition of every subgraph (S′, T ∩ (S′ × S′)) of K into SCCs can be
done in time O(|S| + |T|)
every call of updateLabel(ψ) terminates in time O(|S| + |T|)
CTLmc runs in time O(|φ| · (|S| + |T|)) and in space O(|φ| · |S|)
IA169 Model Checking: CTL model checking 25/33
Complexity of the CTL model checking algorithm
each formula φ has at most |φ| subformulae
decomposition of every subgraph (S′, T ∩ (S′ × S′)) of K into SCCs can be
done in time O(|S| + |T|)
every call of updateLabel(ψ) terminates in time O(|S| + |T|)
CTLmc runs in time O(|φ| · (|S| + |T|)) and in space O(|φ| · |S|)
despite its linear complexity, the algorithm also suffers from state-space
explosion as the Kripke structure can be extremely large
in fact, the problem is common for all explicit-state model checking algorithms,
where states are handled individually
IA169 Model Checking: CTL model checking 26/33
CTL*
Comparison of LTL and CTL
LTL and CTL are expressively incomparable
there is no CTL formula φ such that K |= φ ⇐⇒ K |= FG a for each K
there is no LTL formula φ such that K |= φ ⇐⇒ K |= AGEF a for each K
IA169 Model Checking: CTL model checking 28/33
Comparison of LTL and CTL
LTL and CTL are expressively incomparable
there is no CTL formula φ such that K |= φ ⇐⇒ K |= FG a for each K
there is no LTL formula φ such that K |= φ ⇐⇒ K |= AGEF a for each K
CTL*
a common generalization of both CTL and LTL
a branching time logic
the main idea is to decouple temporal operators and quantifiers
for example, A(a ∧ FG b) is a CTL* formula, but not CTL formula
IA169 Model Checking: CTL model checking 29/33
CTL*
the syntax distinguishes two types of formulae: path and state formulae
aplication of quantifiers E, A on a path formula results in a state formula
Definition (CTL*)
Formulae of CTL* are inductively defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | Eψ (state formuale)
ψ ::= φ | ¬ψ | ψ1 ∧ ψ2 | Xψ | ψ1 U ψ2 (path formulae)
where ⊤ stands for true and a ranges over a countable set AP, φ represents state
formulae and ψ represents path formulae.
IA169 Model Checking: CTL model checking 30/33
CTL*
the syntax distinguishes two types of formulae: path and state formulae
aplication of quantifiers E, A on a path formula results in a state formula
Definition (CTL*)
Formulae of CTL* are inductively defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | Eψ (state formuale)
ψ ::= φ | ¬ψ | ψ1 ∧ ψ2 | Xψ | ψ1 U ψ2 (path formulae)
where ⊤ stands for true and a ranges over a countable set AP, φ represents state
formulae and ψ represents path formulae.
similar abbreviations can be defined as for LTL and CTL
IA169 Model Checking: CTL model checking 31/33
CTL*
the syntax distinguishes two types of formulae: path and state formulae
aplication of quantifiers E, A on a path formula results in a state formula
Definition (CTL*)
Formulae of CTL* are inductively defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | Eψ (state formuale)
ψ ::= φ | ¬ψ | ψ1 ∧ ψ2 | Xψ | ψ1 U ψ2 (path formulae)
where ⊤ stands for true and a ranges over a countable set AP, φ represents state
formulae and ψ represents path formulae.
similar abbreviations can be defined as for LTL and CTL
path/state formulae are interpreted over paths/states in a Kripke structure
we assume that each state of a Kripke structure has at least one successor
IA169 Model Checking: CTL model checking 32/33
Semantics of CTL*
π(i) denotes the (i + 1)-st state of π and πi denotes the path π(i)π(i + 1) . . .
Definition
Let K be a Kripke structure, s be its state, and π be its infinite path. The relations
K, s |= φ, meaning that state s satisfies a state formula φ, and K, π |= ψ, meaning
that path π satisfies a path formula ψ, are defined inductively as follows.
K, s |= ⊤
K, s |= a iff a ∈ L(s)
K, s |= ¬φ iff K, s ̸|= φ
K, s |= φ1 ∧ φ2 iff K, s |= φ1 ∧ K, s |= φ2
K, s |= Eψ iff ∃π ∈ PK (s) . K, π |= ψ
K, π |= φ iff K, π(0) |= φ
K, π |= ¬ψ iff K, π ̸|= ψ
K, π |= ψ1 ∧ ψ2 iff K, π |= ψ1 ∧ K, π |= ψ2
K, π |= Xψ iff K, π1 |= ψ
K, π |= ψ1 U ψ2 iff ∃i ≥ 0 . K, πi |= ψ2 ∧ ∀ 0 ≤ j < i . K, πj |= ψ1
IA169 Model Checking: CTL model checking 33/33