IA169 System Verification and Assurance
Symbolic Representations
in CTL Model Checking
Jiří Barnat
State Space Explosion Problem and Model Checking
Requirements
Specification
Property
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelingFormalization
IA169 System Verification and Assurance – 07 str. 2/31
State Space Explosion Problem and Model Checking
Verification Failure
Requirements
Specification
Property
System
System Model
Model Checking
Simulation
Counterexample
Invalid
Valid
ErrorModelingFormalization
IA169 System Verification and Assurance – 07 str. 2/31
Motivation
Observation
Computation state is given by valuation of state variables.
Every variable has a finite domain, its value may be stored
using a fixed number of bits.
Computation state represented as a bit vector (a1, . . . , an)
of fixed length n.
Set of States
Algorithms for verification store set of states.
Set of state can be viewed as a set of binary vectors.
Set of binary vectors may be described with a Boolean
function.
IA169 System Verification and Assurance – 07 str. 3/31
Boolean Functions
Boolean Functions
These are formulae in propositional logic over a given set
of Boolean variables.
Task
Let system state be given by valuation of four bit
variables (a1, b1, a2, b2).
A state is erroneous if the values of a1 and b1 and values
of a2 and b2 agree.
Describe a set of erroneous states with Boolean function.
Some Possible Solutions
IA169 System Verification and Assurance – 07 str. 4/31
Boolean Functions
Boolean Functions
These are formulae in propositional logic over a given set
of Boolean variables.
Task
Let system state be given by valuation of four bit
variables (a1, b1, a2, b2).
A state is erroneous if the values of a1 and b1 and values
of a2 and b2 agree.
Describe a set of erroneous states with Boolean function.
Some Possible Solutions
(a1 ∧ b1 ∧ a2 ∧ b2) ∨ (a1 ∧ b1 ∧ ¬a2 ∧ ¬b2)∨
(¬a1 ∧ ¬b1 ∧ ¬a2 ∧ ¬b2) ∨ (¬a1 ∧ ¬b1 ∧ a2 ∧ b2)
a1 ⇔ b1 ∧ a2 ⇔ b2
IA169 System Verification and Assurance – 07 str. 4/31
Representation of Boolean Functions
Binary Decision Trees (BDTs)
Directed tree with a single root state.
Every inner node is denoted with a Boolean variable (v)
and lead to exactly two successors referred to as to
(low(v), high(v)).
Every leaf is assigned a binary value, i.e. 0 or 1.
Coding of Boolean Functions with BDTs
Every combination of values of input variables corresponds
to exactly one path from the root of BDT to a leaf.
Values stored at leaves give the the value of the function
for the corresponding input values.
IA169 System Verification and Assurance – 07 str. 5/31
Binary Decision Tree ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2)
IA169 System Verification and Assurance – 07 str. 6/31
Representation of Boolean Functions
Disadvantage of BDTs
BDTs are uselessly space demanding (contain redundant
information).
Task
Identify isomorphic sub-trees of the BDT from the
previous slide.
Binary Decision Diagrams (BDD)
Acyclic directed graph, of which vertices have output
degree either zero (leaf) or two (inner vertex).
Vertices of BDD have otherwise the same properties as
BDT nodes.
IA169 System Verification and Assurance – 07 str. 7/31
Computing (minimal) BDD
Initialisation
For a given Boolean function take arbitrary BDD or BDT.
Eliminate unreachable vertices
Eliminate duplicate
1) Remove all but one leaves with the same value.
2) All edges incident with eliminated leaves reconnect to the the
remaining leaf with the same value.
Repeat Until Fixpoint
Eliminate duplicate inner vertices.
If there are two inner vertices u, v with the same label such
that low(v) = low(u) a high(v) = high(u), then remove u and
reconnect edges originally leading to u to v.
Eliminate useless tests
Eliminate inner vertex v if low(v) = high(v). Reconnect edges
originally leading to v to low(v).
IA169 System Verification and Assurance – 07 str. 8/31
BDD for ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2)
IA169 System Verification and Assurance – 07 str. 9/31
Coding of Boolean Functions with BDDs
Observation
Every vertex v of BDD encodes some Boolean function
Fv (x1, . . . , xn).
Computing Fv (x1, . . . , xn) for values h1, . . . , hn.
If v is a leaf then
Fv (h1, . . . , hn) = 1, if v is labelled with value 1.
Fv (h1, . . . , hn) = 0, if v is labelled with value 0.
If v is an inner vertex then
Fv (h1, . . . , hn) = Flow(v)(h1, . . . , hn), if hi == 0.
Fv (h1, . . . , hn) = Fhigh(v)(h1, . . . , hn), if hi == 1.
IA169 System Verification and Assurance – 07 str. 10/31
Ordering Variables in BDD — OBDD
Observation
Some intermediate representation computed during
minimisation of a BDD are also valid BDDs.
A given Boolean function may be represented with
multiple different BDDs.
Canonical Form for BDD
Minimal BDD computed from a BDD, or BDT with a
fixed ordering on variables in inner vertices is unique.
BDD with a fixed variable ordering is referred to as to
Ordered BDD (OBDD).
Computing Canonical Form
Apply algorithm for minimal BDD.
If performed in a bottom-up manner, obtained in linear
time w.r.t. the size of initial BDT or BDD.
IA169 System Verification and Assurance – 07 str. 11/31
OBDDs for Different Variable Ordering
IA169 System Verification and Assurance – 07 str. 12/31
Restriction Operator for OBDDs
Observation
Every OBDD represents some Boolean function.
Boolean functions can be combined/composed using
unary and binary logic operators such as
¬, ∧, ∨, =⇒ , XOR, . . ..
OBDDs can be composed similarly.
Application of Logic Operators on OBDD
Let O and O be OBDDs corresponding to functions
f and f , respectively.
We will refer to function Apply(O, O , ), as to function
that computes OBDD that represents result of application
of logic operator to functions f and f .
IA169 System Verification and Assurance – 07 str. 13/31
Operation of Restriction
Operation of Restriction
Fxi ←b(x1, . . . , xn) = F(x1, . . . , xi−1, b, xi+1, . . . , xn)
Produces Boolean function with all but one free variables.
Realisation for OBDD
If root r is denoted with the restricted variable xi , the
resulting OBDD will have new root
low(r) if b = 0
high(r) if b = 1
Any edge leading to a inner vertex t that is denoted with
the restricted variable xi is reconnected to
low(t) if b = 0
high(t) if b = 1
OBDD is minimised (contains unreachable nodes).
IA169 System Verification and Assurance – 07 str. 14/31
Shannon expansion
Shannon expansion
Any binary logic operator can be applied on OBDDs using
Shannon expansion:
F = (¬x ∧ Fx←0) ∨ (x ∧ Fx←1)
If F = f f , for any binary logic operation , then
f f = (¬x ∧ (fx←0 fx←0)) ∨ (x ∧ (fx←1 fx←1))
IA169 System Verification and Assurance – 07 str. 15/31
Algorithm for Application of Binary Operators on OBDDs
Apply(O, O , )
Let v, v be root nodes of O, O , denoted with x, x , respectively.
If v and v are leaves denoted with values h and h , respectively,
then return a leave denoted with h h .
Otherwise, if
x = x then return a new node w denoted with variable x, where
low(w) = Apply(low(v), low(v ), )
high(w) = Apply(high(v), high(v ), )
x < x then return a new node w denoted with variable x, where
low(w) = Apply(low(v), O , )
high(w) = Apply(high(v), O , )
x < x then return a new node w denoted with variable x , where
low(w) = Apply(O, low(v ), )
high(w) = Apply(O, high(v ), )
IA169 System Verification and Assurance – 07 str. 16/31
Negation Operation and Emptiness Check
Observation
Let OBDD X encodes function FX , then OBDD Y
encoding negation function ¬FX is created as a copy of
OBDD X in which values of leaves are switched.
Emptiness Check
OBDDs have canonical form.
Canonical OBDD representing an empty set is made of a
single leaf denoted with 0.
Test for a Presence of Set Member (complicated way)
Create an OBDD describing the tested member.
Apply operation ∧ on tested and newly created OBDDs.
Employ emptiness check on the resulting OBDD.
IA169 System Verification and Assurance – 07 str. 17/31
Section
Symbolic Representation of Kripke Structure
IA169 System Verification and Assurance – 07 str. 18/31
Encoding of Transitions of Kripke Structure
Observation
A state of Kripke structure M = (S, T, I) is given by n
binary variables a1, . . . , an.
Every set of states of Kripke structure can be encoded by
an OBDD with n variables.
Similarly, transition relation T ⊆ S × S can be encoded
by Boolean function with 2n variables.
Simplification of OBDD
Edges leading to zero leaf can be omitted.
Non-existence of an edge indicates an edge to zero leaf.
IA169 System Verification and Assurance – 07 str. 19/31
Task
M = ({00, 01, 11}}, {(11, 00), (11, 01), (01, 00)}, I)
11 01
00
T can be encoded as F(a, b, a , b )
F(a, b, a , b ) =
(a∧b ∧¬a ∧b )∨(a∧b ∧¬a ∧¬b )∨(¬a∧b ∧¬a ∧¬b )
Assume variable ordering a < b < a < b and draw
OBDD for F.
IA169 System Verification and Assurance – 07 str. 20/31
Successors of States
Observation
Assume M = (S, T, I) and OBDDT (a, b, a , b ).
Let X be a set of states given with OBDDX (a, b).
Using OBDDT and OBDDX , OBDDX (a , b ) representing
set of successors of states in X can be computed, i.e.
X = {v ∈ S | u ∈ X ∧ (u, v) ∈ T}.
IA169 System Verification and Assurance – 07 str. 21/31
Successors of States – Algorithm Idea
Computing OBDDX (intuitively)
OBDDX = Apply(OBDDT , OBDDX , ∧)
Modify OBDDX so that every path of it contains vertex
labelled with a .
In OBDDX erase all vertices labelled with a and b.
Iterate over all a vertices, consider them as root and
compute respective minimal OBDDs.
The computed set of OBDDs combine with operation ∨.
Minimise the resulting OBDD.
Rename primed variables to unprimed.
Task
Compute OBDD representing successors of states
{00, 11}.
IA169 System Verification and Assurance – 07 str. 22/31
Predecessors of States
Computing Predecessors (intuitively).
Modify all vertices of OBDDX to be labelled with primed
variables.
OBDDX = Apply(OBDDT , OBDDX , ∧)
Modify OBDDX so that every path contains vertex
labelled with a .
Those a that cannot reach leaf labelled with 1 replace
with a new zero leaf.
Other a vertices replace with the other leaf.
Remove all primed nodes and old leaves, and minimise
OBDD.
Task
Compute OBDD representing predecessor of state {00}.
IA169 System Verification and Assurance – 07 str. 23/31
Section
Symbolic Approach to Model Checking CTL
IA169 System Verification and Assurance – 07 str. 24/31
Reminder
Observation
If validity of formulae ϕ and ψ is known for all states of
Kripke structure, validity of formulae ¬ϕ, ϕ ∨ ψ, EX ϕ,
etc., can be easily deduced.
Algorithm Idea for Model Checking CTL
Let M = (S, T, I) be a Kripke structure and ϕ a CTL
formula.
Labelling function label : S → 2ϕ
is computed, stating
which sub-formulae of ϕ are valid in which states of M.
Obviously, s0 |= ϕ ⇐⇒ ϕ ∈ label(s0).
Function label is computed gradually for every
sub-formula of ϕ starting with the simplest sub-formulae
(atomic propositions) and terminating after computing
the validity of ϕ.
IA169 System Verification and Assurance – 07 str. 25/31
Symbolic Approach
Idea
Set of states in which particular sub-formulae hold can be
efficiently represented with OBDDs.
Computation of label function for more complex
sub-formulae employs manipulation with respective
OBDDs.
Realisation
Set of states are represented with OBDDs.
Initial OBDDs are defined by functions to evaluate atomic
propositions.
OBDDs for more complex sub-formulae are composed
from OBDDs of the simpler sub-formulae.
Test for membership of initial state of Kripke structure in
the set of states satisfying the verified formula.
IA169 System Verification and Assurance – 07 str. 26/31
Atomic Propositions and Logic Operators
Recall Syntax of CTL
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ
Computing Set of States Satisfying CTL Formula
Notation
F(ψ) denotes (a function describing) set of states satisfying ψ.
Succ(X) denotes immediate successors of states in the set X.
Pred(X) denotes immediate predecessors of states in the set
X.
Boolean Functions for Atomic Proposition
Atomic propositions describe properties of state variables.
Atomic Propositions can be encoded as Boolean functions.
Computing Boolean Operators ¬ and ∨
F(¬ψ1) = ¬(Fψ1)
F(ϕ ∨ ψ) = F(ϕ) ∨ F(ψ)
IA169 System Verification and Assurance – 07 str. 27/31
Temporal operators EX(ϕ), E[ϕ U ψ] and EG(ϕ)
Operator EX(ϕ)
F(EX(ϕ)) = Pred(F(ϕ))
Operator E(ϕ U ψ)
F(E(ϕ U ψ)) = X,
where X is the least fix-point of recursive rule
X = F(ψ) ∪ (F(ϕ) ∩ Pred(X))
Operator EG (ϕ)
F(EG ϕ) = X,
where X is the greatest fix-point of recursive rule
X = F(ϕ) ∩ EX(X)
IA169 System Verification and Assurance – 07 str. 28/31
Computing Fix-Points of Function f
The Least Fix-Point
proc LFP(f )
X = ∅
Xold = ∅
do
Xold = X
X := f (X)
while (X = Xold)
end
The Greatest Fix-Point
proc GFP(f )
X = S
Xold = S
do
Xold = X
X := f (X)
while (X = Xold)
end
IA169 System Verification and Assurance – 07 str. 29/31
Section
Model Checking – Summary
IA169 System Verification and Assurance – 07 str. 30/31
Model Checking – Summary
Enumerative × Symbolic Approach
Enumerative – focused on "control-flow"
Symbolic – focused on "data-flow"
Pros w.r.t. Testing
No source-code necessary (can be applied on models).
Suitable for testing of parallel programs.
Pros w.r.t. Static Analysis
Complete for systems with a finite state space.
Verification of temporal properties.
Cons
State space explosion problem.
IA169 System Verification and Assurance – 07 str. 31/31