Lecture 13: Binary Decision Diagrams and the Compact Representation of Transition Systems

In the last two lectures of the course we will be studying in some depth the data structure `Reduced Ordered Binary Diagrams ' (or BDDs for short) introduced by Randal E. Bryant in 1986. BDDs offers an extremely compact representation of sets over a finite universe (e.g. the reachable states of a finite state CCS process) via an encoding in terms of boolean functions. The BDD data structure allows for efficient implementation of essentially all set operations, e.g. intersection, union, complement, as well as set inclusion. In the first lecture I shall present the basics of the BDD data structure and you will be able to experiment with it via the tool IBEN. In the next (and last) lecture we shall see how the BDD data structure can be used to represent CCS processes, and can be subsequently applied in efficient bisimulation- and model-checking. Randal E. Bryant shared the 1998 ACM Paris Kanellakis Award with Edmund M. Clarke, E. Allen Emerson and Kenneth L. McMillan for the invention of "symbolic model checking".

Reading material


To construct BDDs we shall use a tool called IBEN. IBEN offers a shell-like interface to packages implementing BDDs and BDD-operations. The current version of IBEN uses the Buddy BDD-package by Jørn Lind-Nielsen, DTU. The IBEN shell allows for the construction of BDDs using the operations from the note.

A Solaris version (ultrasparc) has been installed and can be executed with the following command:


You can read the manual by entering the command help into IBEN (alternatively you can add the /pack/FS/pack/iben-1.1/man directory to your manpath at run man iben).

How to read satisfying assignments in IBEN. This is best explained by means of a simple example session.

iben> vars x y (This declares two boolean variables x (the 0th variable) and y (the first variable))
iben> satisfy x & y
<0:1, 1:1> (This says that the only satisfying assignment is one in which the 0th variable, namely x, is true, and so is the first one, namely y.)
iben> vars z (This declares the variable z with index 2)
iben> satisfy x & y & !z
<0:1, 1:1, 2:0>
iben> satisfy x + (!x & y & !z)
<0:0, 1:1, 2:0><0:1>(This says that there are two families of satisfying assignments. In the second one, the only thing that matters is that x is true.)

One of the currently most efficient BDD packages is the CUDD package developed at University of Colorado.


Exercise 1

You may find Mia's schedule in the input language of IBEN here.  Figure out what 'konfliktfri' is doing.  Change the schedule so that includes conflicts. Also,   use IBEN to settle various questions that you may have.

Exercise 2

Exercises 4.1, 4.4 and 4.5 in the note by Henrik R. Andersen. After having solved the exercises manually, use IBEN to check your solution.

Exercise 3 (Two-dimensional matching)

Per, Kristian, Ole and Jens are to hold an Xmas-party. Unfortunately, they are almost out of money which severely limits the amount of beer at the party. In fact, they have to make do with 1 Tuborg, 1 Carlsberg, 1 Xmas (a Danish Xmas beer), and one Carls Special.  However, the four guys have individual requirements which must be fulfilled at all costs. In particular, Per only drinks Tuborg and Carlsberg; Kristian only drinks Carlsberg and Xmas; Ole essentially drinks everything except Xmas, and Jens can only drink Carlsberg and Carls Special.  Is it possible to plan the party drinking so that they all get something to drink?  Of course you should use IBEN to help them!

Exercise 4

Use IBEN to check whether the two circuits on page 30 in Henrik R. Andersen's note are equivalent or not.

Exercise 5

Use IBEN to solve the 4-queen problem.

Exercise 6

Exercise 7.1 in Henrik R. Andersen's note for N=4.  That is, use IBEN to solve the knight's tour problem on a board of size 4x4.