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