>> [CS656/556 Course Materials]
Mon Mar 3 16:42:35 PST 2003
656/556 2003 1w 15 OBDDs
Assigned work:3.2 #1b (fig 3.10) using SMV
Study Section 6.3 Model checking with OBDDs (pages 351-358)
6.3 Applications of OBDDs
BDDs made model checking highly feasible.
OBDDs are a good way to express complex boolean functions.
6.3.1 Coding sets of states as OBDDs
(1) code each element as a bit-vector
(2) code a set as a bit-vlaued function of the bit-vector.
(3) code the function using OBDD
Ex 6.11 (page 354)
Warning. Typo in some books. Arrowhead missing.
There is transition from s1 to s3.
6.3.2 Coding transition relations
(1) Code a set of pairs.
Each pair becomes two concatenated vectors
(2) Transition is a boolean function of double length vectors.
6.3.3 Coding backtracing operators
Operators: pre[some] and pre[all].
Only need pre[some]
use exists and apply algorithms.
Ex 6.12(p 657)
6.3.4 Calculate OBDDS directly from SMV expressions
(and/or circuit/logic diagrams).
Use the apply algorithm.
Ex 6.13 p360
Assigned work: Ex6.12 (p657) #1(a) & #1(b).
A fun example of SMV: goat+wolf+cabbage
Study the SMV source code:
What can you discover.
next: Verifying programs