IA169 Model Checking
Symbolic model checking for CTL
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Motivation
system states typically correspond to variable assignments
for finite systems, the number of variables is finite and their domains are finite
we can assume that state is an assignment s : V → {0, 1}, where V is a finite
set of state variables
IA169 Model Checking: Symbolic model checking for CTL 2/22
Motivation
system states typically correspond to variable assignments
for finite systems, the number of variables is finite and their domains are finite
we can assume that state is an assignment s : V → {0, 1}, where V is a finite
set of state variables
a set of states can be described by propositional formulas
for example, a set of states where the values of two bitvectors of length 2
agree (i.e. x1x2 = y1y2) can be represented by
IA169 Model Checking: Symbolic model checking for CTL 3/22
Motivation
system states typically correspond to variable assignments
for finite systems, the number of variables is finite and their domains are finite
we can assume that state is an assignment s : V → {0, 1}, where V is a finite
set of state variables
a set of states can be described by propositional formulas
for example, a set of states where the values of two bitvectors of length 2
agree (i.e. x1x2 = y1y2) can be represented by
(x1 ∧ y1 ∧ x2 ∧ y2) ∨ (x1 ∧ y1 ∧ ¬x2 ∧ ¬y2) ∨
∨ (¬x1 ∧ ¬y1 ∧ x2 ∧ y2) ∨ (¬x1 ∧ ¬y1 ∧ ¬x2 ∧ ¬y2)
or by x1 ⇔ y1 ∧ x2 ⇔ y2
such a formula can be equivalently seen as a Boolean funcion
aternatively, a set can be described by a binary decision diagram (BDD)
IA169 Model Checking: Symbolic model checking for CTL 4/22
Agenda and sources
agenda
binary decision diagrams (BDDs) and their properties
Kripke structures represented by BDDs
CTL model checking algorithm based on BDDs
source
Chapter 8 of E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith:
Model Checking, Second Edition, MIT, 2018.
IA169 Model Checking: Symbolic model checking for CTL 5/22
Binary decision diagrams (BDDs) and their properties
Binary decision diagrams (BDDs)
"one of the only really fundamental data structures that came out in the last
twenty-five years" [Donald Knuth, 2008]
investigated by Randal Bryant in 1986
can represent an arbitrary Boolean function f : {0, 1}n → {0, 1} or the set of
models of a propositional formula φ
IA169 Model Checking: Symbolic model checking for CTL 7/22
Binary decision diagrams (BDDs)
"one of the only really fundamental data structures that came out in the last
twenty-five years" [Donald Knuth, 2008]
investigated by Randal Bryant in 1986
can represent an arbitrary Boolean function f : {0, 1}n → {0, 1} or the set of
models of a propositional formula φ
Definition (binary decision diagram, BDD)
A binary decision diagram (BDD) is a finite rooted directed acyclic graph with two
kinds of nodes and two kinds of edges:
each terminal (i.e., a node without any successor) is labeled with 0 or 1,
each nonterminal node v is labeled with a variable var(v) and has a low
successor low(v) and a high successor high(v).
IA169 Model Checking: Symbolic model checking for CTL 8/22
Binary decision diagrams (BDDs)
low(v) = w is depicted by a dashed/dotted edge from v to w
high(v) = w is depicted by a solid edge from v to w
nodes are directly labeled with var(v), terminal nodes with 0 or 1
x
y
z z
z
y y
1 0
IA169 Model Checking: Symbolic model checking for CTL 9/22
Semantics of BDDs
a BDD with variables x1, . . . , xn describes a Boolean function f(x1, . . . , xn)
for b1, . . . , bn ∈ {0, 1}, the value of f(b1, . . . , bn) is the value of the terminal
node reached from the root by following
low(v) whenever var(v) = xi and bi = 0
high(v) whenever var(v) = xi and bi = 1
x
y
z z
z
y y
1 0
IA169 Model Checking: Symbolic model checking for CTL 10/22
Semantics of BDDs
a BDD with variables x1, . . . , xn describes a Boolean function f(x1, . . . , xn)
for b1, . . . , bn ∈ {0, 1}, the value of f(b1, . . . , bn) is the value of the terminal
node reached from the root by following
low(v) whenever var(v) = xi and bi = 0
high(v) whenever var(v) = xi and bi = 1
x
y
z z
z
y y
1 0
f(x, y, z) =



1 for x = 1, y = 1, z = 1
or x = 1, y = 0, z = 0
or x = 0, z = 0, y = 1
0 otherwise
IA169 Model Checking: Symbolic model checking for CTL 11/22
Semantics of BDDs
Definition
Consider a BDD labeled with (some of) variables x1, . . . , xn. Every node v of the
BDD describes a Boolean function fv (x1, . . . , xn) defined inductively as follows.
if v is a terminal node labeled with 0, then fv (x1, . . . , xn) = 0
if v is a terminal node labeled with 1, then fv (x1, . . . , xn) = 1
if v is a nonterminal node labeled with a variable xi, then
fv (x1, . . . , xn) = (¬xi ∧ flow(v)(x1, . . . , xn)) ∨ (xi ∧ fhigh(v)(x1, . . . , xn))
The BDD represents the Boolean function corresponding to its root.
IA169 Model Checking: Symbolic model checking for CTL 12/22
Semantics of BDDs
Definition
Consider a BDD labeled with (some of) variables x1, . . . , xn. Every node v of the
BDD describes a Boolean function fv (x1, . . . , xn) defined inductively as follows.
if v is a terminal node labeled with 0, then fv (x1, . . . , xn) = 0
if v is a terminal node labeled with 1, then fv (x1, . . . , xn) = 1
if v is a nonterminal node labeled with a variable xi, then
fv (x1, . . . , xn) = (¬xi ∧ flow(v)(x1, . . . , xn)) ∨ (xi ∧ fhigh(v)(x1, . . . , xn))
The BDD represents the Boolean function corresponding to its root.
x
y
z z
z
y y
1 0
IA169 Model Checking: Symbolic model checking for CTL 13/22
Semantics of BDDs
Definition
Consider a BDD labeled with (some of) variables x1, . . . , xn. Every node v of the
BDD describes a Boolean function fv (x1, . . . , xn) defined inductively as follows.
if v is a terminal node labeled with 0, then fv (x1, . . . , xn) = 0
if v is a terminal node labeled with 1, then fv (x1, . . . , xn) = 1
if v is a nonterminal node labeled with a variable xi, then
fv (x1, . . . , xn) = (¬xi ∧ flow(v)(x1, . . . , xn)) ∨ (xi ∧ fhigh(v)(x1, . . . , xn))
The BDD represents the Boolean function corresponding to its root.
x
y
z z
z
y y
1 0
f(x, y, z) =
= x ∧ (y ⇐⇒ z) ∨ ¬x ∧ ¬z ∧ y
IA169 Model Checking: Symbolic model checking for CTL 14/22
Ordered BDD
Definition (ordered BDD)
A BDD is ordered if there exists a linear ordering < on its variables such that for
every node v with a nonterminal successor w it holds var(v) < var(w).
x
y
z z
z
y y
1 0
IA169 Model Checking: Symbolic model checking for CTL 15/22
Ordered BDD
Definition (ordered BDD)
A BDD is ordered if there exists a linear ordering < on its variables such that for
every node v with a nonterminal successor w it holds var(v) < var(w).
x
y
z z
z
y y
1 0
x
y
z z
y
z z
1 0
IA169 Model Checking: Symbolic model checking for CTL 16/22
Reduced BDD
Definition (reduced BDD)
A BDD is reduced if it does not contain any nonterminal node with identical low
and high child and any isomorphic subgraphs.
x
y
z z
y
z z
1 0
IA169 Model Checking: Symbolic model checking for CTL 17/22
Reduced BDD
Definition (reduced BDD)
A BDD is reduced if it does not contain any nonterminal node with identical low
and high child and any isomorphic subgraphs.
a BDD can be reduced by repeated applications of the following steps
1 merge all terminal nodes with the same label
2 remove each nonterminal node v with low(v) = high(v) and redirect all
incomming edges to low(v)
3 merge each pair v, w of nonterminal nodes satisfying var(v) = var(w),
low(v) = low(w), and high(v) = high(w)
x
y
z z
y
z z
1 0
IA169 Model Checking: Symbolic model checking for CTL 18/22
Reduced BDD
Definition (reduced BDD)
A BDD is reduced if it does not contain any nonterminal node with identical low
and high child and any isomorphic subgraphs.
a BDD can be reduced by repeated applications of the following steps
1 merge all terminal nodes with the same label
2 remove each nonterminal node v with low(v) = high(v) and redirect all
incomming edges to low(v)
3 merge each pair v, w of nonterminal nodes satisfying var(v) = var(w),
low(v) = low(w), and high(v) = high(w)
x
y
z z
y
z z
1 0
x
y
z z
y
z
1 0
IA169 Model Checking: Symbolic model checking for CTL 19/22
Reduced BDD
Definition (reduced BDD)
A BDD is reduced if it does not contain any nonterminal node with identical low
and high child and any isomorphic subgraphs.
a BDD can be reduced by repeated applications of the following steps
1 merge all terminal nodes with the same label
2 remove each nonterminal node v with low(v) = high(v) and redirect all
incomming edges to low(v)
3 merge each pair v, w of nonterminal nodes satisfying var(v) = var(w),
low(v) = low(w), and high(v) = high(w)
x
y
z z
y
z z
1 0
x
y
z z
y
z
1 0
x
y
z z
y
1 0
IA169 Model Checking: Symbolic model checking for CTL 20/22
Properties of BDDs
we assume that all BDDs are reduced and ordered
for a fixed variable order, BDDs are a canonical representation of Boolean
functions, i.e., two Boolean functions are equivalent (regardless their
description) iff the corresponding BDDs are isomorphic
BDD size heavily depends on considered variable order
x2
y2 y2
x1
y1 y1
1 0
x2 < y2 < x1 < y1
“x1x2 = y1y2”
x2
x1 x1
y2 y2 y2 y2
y1 y1
1 0
x2 < x1 < y2 < y1
some BDDs are exponential in the number of variables regardless their order
IA169 Model Checking: Symbolic model checking for CTL 21/22
Operations on BDDs
variable instantiation
fxi ←b(x1, . . . , xn) = f(x1, . . . , xi−1, b, xi+1, . . . , xn)
operation on the corresponding BDD
1 if the root r is labeled with xi then the new BDD will have root
low(r) if b = 0
high(r) if b = 1
2 going from top to bottom, any edge leading to a nonterminal node v labeled
with xi is reconnected to
low(v) if b = 0
high(v) if b = 1
3 unreachable nodes are removed and BDD is reduced
IA169 Model Checking: Symbolic model checking for CTL 22/22