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


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