Lecture 14: Binary Decision Diagrams (Continued)

In this last technical lecture we shall see how the BDD data structure can be used to represent finite-state transition systems (e.g. regular CCS processes) and parallel compositions of such processes. We shall then see how BDDs can be subsequently applied in efficient bisimulation- and model-checking.

Reading material

• Henrik Reif Andersen. An Introduction to Binary Decision Diagrams. DTU, Sep. 1997 (Mandatory)
  This will be the reading for both this and the next lecture.
• Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24(3), pp. 293-318, Sep. 1992 (optional). PostScript, PDF

Exercises

A --a--> A
B --b--> A and
C --b--> A.

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.)