Binary Decision Diagrams

Literature

Some pointers:
H.R. Andersen, An Introduction to Binary Decision Diagrams, Lecture notes,
Department of Information Technology, IT University of Copenhagen
URL: http://www.itu.dk/people/hra/bdd97-abstract.html
Tools:
DDcal (“BDD calculator”)
URL: http://vlsi.colorado.edu/∼fabio/

2

Set representations
As we have seen, the solution of the model-checking problem for CTL can be
expressed by operations on sets:
states satisfying some atomic proposition: µ(p) for p ∈ AP
states satisfying (sub)formulae: [[ψ]]K
computation by set operations: pre , ∩, ∪, . . .
How can such sets be represented:
explicit list: S = {s1, s2, s4, . . .}
symbolic representation: compact notation or data structure
3

Symbolic representation

There are many ways of representing sets symbolically. Some are commonly
used in mathematics:
Intervals: [1, 10] for {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}
Characterizations: “odd numbers” for {1, 3, 5, . . .}
Every symbolic representation is suitable for some sets and less so for others
(for instance, intervals for odd numbers).
We are interested in a data structure suitable for representing sets of states in
hardware systems, and where the necessary operations (pre , ∩ etc) can be
implemented efficiently.

4

In the following, we assume that states can be represented as Boolean vectors
S = {0, 1}m

for some m ≥ 1

Example:
1-safe Petri nets (every place marked with at most one token)
circuits (all inputs and outputs are 0 or 1)
Remark: In general, the elements of any finite set can be represented by
Boolean vectors if m is chosen large enough. (However, this may not be
adequate for all sets.)
5

Example 1: Petri-net
Consider the following Petri net:
p1
t1
p2

p3
t2
p4

p5
t3
p6

A state can be written as (p1, p2, . . . , p6), where pi , 1 ≤ i ≤ 6 indicates
whether there is a token on Pi .
Initial state(1, 0, 1, 0, 1, 0);
other reachable states are, e.g., (0, 1, 1, 0, 1, 0) or (1, 0, 0, 1, 0, 1).
6

Example 2: Circuit

Half-adder:
x1

x2

sum

carry

The circuit has got two inputs (x1, x2) and two outputs (carry, sum). Their
admissible combinations can be denoted by Boolean 4-tuples, e.g. (1, 0, 0, 1)
(x1 = 1, x2 = 0, carry = 0, sum = 1) is a possible combination.

7

Characteristic functions

Let C ⊆ S = {0, 1}m .
(i.e., a set of Boolean vectors.)
The set C is uniquely defined by its characteristic function fC : S → {0, 1} given
by

fC (s) :=


1
0

if s ∈ C
if s ∈
/C

Remark: fC is a Boolean function with m inputs and therefore corresponds to a
formula F of propositional logic with m atomic propositions.

8

The characteristic function of the admissible combinations in Example 2
corresponds to the following formula of propositional logic:







F ≡ carry ↔ (x1 ∧ x2) ∧ sum ↔ (x1 ∨ x2) ∧ ¬carry



In the following, we shall treat
sets of states (i.e. sets of Boolean vectors)
characteristic functions
Formulae of propositional logic
simply as different representations of the same objects.
9

Representing formulae
Truth table:
x1

x2

carry

sum

F

0

0

0

0

1

0

0

0

1

0

1

1

···
0

1

0
···

A truth table is obviously not a compact representation.
However, we use it as a starting point for a graphical, more compact
representation.
10

Binary decision graphs
Let V be a set of variables (atomic propositions) and < a total order on V , e.g.
x1 < x2 < carry < sum
A binary decision graph (w.r.t. <) is a directed, connected, acyclic graph with the
following properties:
there is exactly one root, i.e. a node without incoming arcs;
there are at most two leaves, labelled by 0 or 1;
all non-leaves are labelled with variabls from V ;
every non-leaf has two outgoing arcs labelled by 0 and 1;
if there is an edge from an x-labelled node to a y -labelled node, then x < y.
11

Example 2: Binary decision graph (here: a full tree)
x1
1

0
x2

x2
1

1

0

carry

carry

0

carry

carry

1

0

1

0

1

0

1

sum

sum

sum

sum

sum

sum

sum

0
sum

1

0

1

0

1

0

1

0

1

0

1

0

1

0

1

0

0

1

0

0

0

0

1

0

0

0

1

0

0

0

0

1

Paths ending in 1 correspond to vectors whose entry in the truth table is 1.
12

Binary decision diagrams

A binary decision diagram (BDD) is a binary decision graph with two additional
properties:
no two subgraphs are isomorphic;
there are no redundant nodes, where both outgoing edges lead to the same
target node.
We also allow to omit the 0-node and the edges leading there.
Remarks: On the following slides, the blue edges are meant to be labelled by 1,
the red edges by 0.

13

Example 2: Eliminate isomorphic subgraphs (1/4)
x1

x2

x2

carry

sum

0

1

carry

sum

0

0

sum

0

0

carry

sum

1

0

sum

0

0

carry

sum

1

0

sum

0

0

sum

0

1

Alle 0- und 1-Knoten werden zusammengefasst.
14

Example 2: Eliminate isomorphic subgraphs (2/4)
x1

x2

x2

carry

sum

carry

sum

sum

carry

sum

1

sum

carry

sum

sum

sum

0

0-nodes and 1-nodes merged, respectively.
15

Example 2: Eliminate isomorphic subgraphs (3/4)
x1

x2

x2

carry

carry

sum

carry

sum

1

carry

sum

0

Merged the isomorphic sum -nodes.
16

Example 2: Eliminate isomorphic subgraphs (4/4)
x1

x2

x2

carry

carry

sum

carry

sum

1

sum

0

No isomorphic subgraphs are left → we are done.
17

Example 2: Remove redundant nodes (1/2)
x1

x2

x2

carry

carry

sum

carry

sum

sum

1

0

Both edges of the right sum-node point to 0.
18

Example 2: Remove redundant nodes (2/2)
x1

x2

x2

carry

carry

sum

carry

sum

1

0

No more redundant nodes → we are done.
19

Example 2: Omit 0-node
x1

x2

x2

carry

carry

sum

carry

sum

1

Optionally, we can remove the 0-node and edges leading to it, which makes the
representation clearer.
20

Preview

In the following, we shall investigate operations on BDDs that are needed for CTL
model checking.

Construction of a BDD (from a PL formula)
Equivalence check

Intersection, complement, union

Relations, computing predecessors

21

Propositional logic with constants

In the following, we will consider formulae of propositional logic (PL), extended
with the constants 0 and 1, where:

0 is an unsatisfiable formula;

1 is a tautology.

22

Substitution

Let F and G be formulae of PL (possibly with constants), and let x be an atomic
proposition.
F [x/G] denotes the PL formula obtained by replacing each occurrence of x in F
by G.
In particular, we will consider formulae of the form F [x/0] and F [x/1].
Example: Let F = x ∧ y . Then F [x/1] = 1 ∧ y ≡ y and F [x/0] = 0 ∧ y ≡ 0.

23

If-then-else
Let us introduce a new, ternary PL operator. We shall call it ite (if-then-else).
Note: ite does not extend the expressiveness of PL, it is simply a convenient
shorthand notation.
Let F , G, H be PL formulae. We define
ite(F , G, H) := (F ∧ G) ∨ (¬F ∧ H).
The set of INF formulae (if-then-else normal form) is inductively defined as
follows:

0 and 1 are INF formulae;
if x is an atomic proposition and G, H are INF formulae, then ite(x, G, H) is
an INF formula.
24

Shannon partitioning
Let F be a PL formula and x an atomic proposition. We have:
F ≡ ite(x, F [x/1], F [x/0])
Proof: In the following, G denotes the right-hand side of the equivalence above.
Let ν be a valuation s.t. ν |= F . Either ν(x) = 1, then ν is also a model of
F [x/1] and of x and therefore also of G. The case ν(x) = 0 is analogous. For
the other direction, suppose ν |= G. Then either ν(x) = 1 and the “rest” of ν is
a model of F [x/1]. Then, however, ν will be a model for any formula in which
some of the ones in F [x/1] are replaced by x, in particular also for F . The case
ν(x) = 0 is again analogous.
Remark: G is called the Shannon partitioning of F .
Corollary: Every PL formula is equivalent to an INF formula.
(Proof: apply the equivalence above multiple times.)
25

Construction of BDDs

We can now solve our first BDD-related problem: Given a PL formula F and
some ordering of variables <, construct a BDD w.r.t. < that represents F .
If F does not contain any atomic propositions at all, then either F ≡ 0 or F ≡ 1,
and the corresponding BDD is simply the corresponding leaf node.
Otherwise, let x be the smallest variable (w.r.t. <) occurring in F . Construct
BDDs B0 and B1 for F [x/1] and F [x/0], respectively (these formulae have one
variable less than F ).
Because of the Shannon partitioning, F is representable by a binary decision
graph whose root is labelled by x and whose subtrees are B0 and B1. To obtain
a BDD, we check whether B0 and B1 are isomorpic; if yes, then F is represented
by B0. Otherwise we merge all isomorphic subtrees in B0 and B1.
26

Example: BDD construction
Consider again the formula from Example 2:






F ≡ carry ↔ (x1 ∧ x2) ∧ sum ↔ (x1 ∨ x2) ∧ ¬carry



We have, e.g.:
F [x1/0] ≡ ¬carry ∧ (sum ↔ x2)
F [x1/1] ≡ (carry ↔ x2) ∧ (sum ↔ ¬carry)
F [x1/0][x2/0] ≡ ¬carry ∧ ¬sum
F [x1/0][x2/1] ≡ F [x1/1][x2/0] ≡ ¬carry ∧ sum
F [x1/1][x2/1] ≡ carry ∧ sum
27

Example: BDD construction
By applying the construction, we obtain the same BDD as before:
x1

x2

x2

carry

carry

sum

carry

sum

1

Remark: Obviously, we can also obtain an INF formula from each BDD.
28

BDDs are unique

Remark: The result of the previously given construction is unique (up to
isomorphism).

In other words, given F and <, there is (up to isomorphism) exactly one BDD
that respects < and represents F .

Remark: Different orderings still lead to different BDDs.
(possibly with vastly different sizes!)

29

Example: Variable orderings

Recall Example 1 (the Petri net), and let us construct a BDD representing the
reachable markings:

p1
t1
p2

p3
t2
p4

p5
t3
p6

Remark: P1 is marked iff P2 is not, etc.
30

The corresponding BDD for the ordering p1 < p2 < p3 < p4 < p5 < p6:
p1
p2

p2
p3

p4

p4
p5

p6

p6

1
31

Remarks:
If we increase the number of components from 3 to n (for some n ≥ 0), the
size of the corresponding BDD will be linear in n.
In other words, a BDD of size n can represent 2n (or even more) valuations.
However, the size of a BDD strongly depends on the ordering!
Example: Repeat the previous construction for the ordering
p1 < p3 < p5 < p2 < p4 < p6.

32

Equivalence test

To implement CTL model checking, we need a test for equivalence between
BDDs (e.g., to check the termination of a fixed-point computation).
Problem: Given BDDs B and C (w.r.t. the same ordering) do B and C represent
equivalent formulae?
Solution: Test whether B and C are isomorphic.
Special cases:
Unsatisfiability test: Check if the BDD consists just of the 0 leaf.
Tautology test: Check if the BDD consists just of the 1 leaf.

33

Implementing BDDs with hash tables

Suppose we want to write an application in which we need to manipulate multiple
BDDs.
Efficient BDDs implementations exploit the uniqueness property by storing all
BDD nodes in a hash table. (Recall that each node is in fact the root of some
BDD.)
Each BDD is then simply represented by a pointer to its root.
Initially, the hash table has only two unique entries, the leaves 0 and 1.

34

Every other node is uniquely identified by the triple (x, B0, B1), where x is the
atomic proposition labelling that node and B0, B1 are the subtrees of that node,
represented by pointers to their respective roots.
Usually, one implements a function mk(x, B0, B1) that checks whether the hash
table already contains such a node; if yes, then the pointer to that node is
returned, otherwise a new node is created.
A multitude of BDDs is then stored as a “forest” (a DAG with multiple roots).
Problem: garbage collection (by reference counting)

35

Equivalence test II

Let us reconsider the equivalence-checking problem.
(Given two BDDs B and C, do B and C represent equivalent formulae?)

If B and C are stored in hash tables (as described previously), then B and C are
representable by pointers to their roots.

Due to the uniqueness property, one then simply has to check whether the
pointers are the same (a constant-time procedure).

36

Logical operations I: Complement

Let F be a PL formula and B a BDD representing F .

Problem: Compute a BDD for ¬F .

Solution: Exchange the two leaves of B.

(Caution: This is not quite so simple with the hash-table implementation.)

37

Logical operations II: Disjunction/union

Let F , G be PL formulae and B, C the corresponding BDDs (with the same
ordering).
Problem: Compute a BDD for F ∨ G from B and C.
We have the following equivalence:
F ∨G ≡ ite(x, (F ∨ G)[x/1], (F ∨ G)[x/0]) ≡ ite(x, F [x/1] ∨ G[x/1], F [x/0] ∨ G[x/0])

If x is the smallest variable occurring in either F or G, then
F [x/1], F [x/0], G[x/1], G[x/0] are either the children of the roots of B and C
(or the roots themselves).

38

We construct a BDD for disjunction according to the following, recursive strategy:
If B and C are equal, then return B.
If either B or C are the 1 leaf, then return 1.
If either B or C are the 0 leaf, then return the other BDD.
Otherwise, compare the two variables labelling the roots of B and C, and let x
be the smaller among the two (or the one labelling both).
If the root of B is labelled by x, then let B1, B0 be the subtrees of B;
otherwise, let B1, B0 := B. We define C1, C0 analogously.
Apply the strategy recursively to the pairs B1, C1 and B0, C0, yielding BDDs
E and F . If E = F , return E, otherwise mk(x, E, F ).
39

Logical operations III: Intersection

Let F , G be PL formulae and B, C the corresponding BDDs (with the same
ordering).
Problem: Compute a BDD for F ∧ G from B and C.
Solution: Analogous to union, with the rules for 1 and 0 leaves adapted
accordingly.
Complexity: With dynamic programming: O(|B| · |C|) (every pair of nodes at
most once).

40

Computing predecesors

In the following, we derive a strategy for computing the set

pre (M) = { s | ∃s0 : (s, s0) ∈ → ∧ s0 ∈ M }.

Note that the relation → is a subset of S × S whereas M ⊂ S.
We represent M by a BDD with variables y1, . . . , ym .
→ will be represented by a BDD with variables x1, . . . , xm and y1, . . . , ym (states
“before” and “after”).

41

Remark: Every BDD for M is at the same time a BDD for S × M!

Thus, we can rewrite pre (M) as follows:
{ s | ∃s0 : (s, s0) ∈ → ∩ (S × M)}

Then, pre reduces to the operations intersection and existential abstraction.

42

Example

Let us consider the following Petri net with just one transition:

p1

t1

p3

p2

43

The BDD Ft1 describes the effect of t1, where p1, p2, p3 describe the state
before and p10 , p20 , p30 the state after firing t1.
p1
p1’
p2
p2’

p2’
p3
p3’

1
44

Existential abstraction

Existential abstraction w.r.t. an atomic proposition x is defined as follows:
∃x : F ≡ F [x/0] ∨ F [x/1]
I.e., ∃x : F is true for those valuations that can be extended with a value for x in
such a way that they become models for F .
Example: Let F ≡ (x1 ∧ x2) ∨ x3. Then
∃x1 : F ≡ F [x1/0] ∨ F [x1/1] ≡ (x3) ∨ (x2 ∨ x3) ≡ x2 ∨ x3
By extension, we can consider existential abstraction over sets of atomic
propositions (abstract from each of them in turn).
45

Example: Existential abstraction
(a) Ft1 [p20 /1];

(a)

(b) Ft1 [p20 /0];

(c) ∃p20 : Ft1 ;

(b)

p1

p1’

p2

p2
p2’

(c)

p1

p1’

p2’

(d) ∃p10 , p20 , p30 : Ft1

p2’

p1

(d)

p1

p1’

p2’

p3

p3

p3

p3’

p3’

p3’

1

1

1

p3

1
46

LTL with BDDs

Question: Can one implement also LTL model checking using BDDs?

Answer: Yes and no (worst-case: quadratical, but works ok in practice).

Problems: BDD not compatible with depth-first search, combination with
partial-order reduction difficult.

47

Symbolic algorithms for LTL

Idea: Find non-trivial SCCs with an accepting state, then search backwards for
an initial state.

Algorithms: Emerson-Lei (EL), OWCTY

48

Emerson-Lei (1986)

1. Assign to M the set of all states.
2. Let B := M ∩ F .
3. Compute the set C of states that can reach elements of B.
4. Let M := M ∩ pre (C).
5. If M has changed, then go to step 2, otherwise stop.

49

One-Way-Catch-Them-Young

(Hardin et al 1997, Fisler et al 2001)

Like EL, but after step 4 repeat M := M ∩ pre (M) until M does not change any
more.

50

EL and OWCTY

In the upper case, OWCTY is superior, in the lower case EL is.

In practice, OWCTY appears to work better.

51