## 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

The same as for lecture 14. In addition, you might wish to consider
the use of BDDs (and IBEN) in stuyding reachability and bisimulation
equivalence questions over the LTS with states A, B, and C, actions a
and b, and transitions
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.)