Lecture 6: Symbolic Model Checking A. PnueliSymbolic Model CheckingNext, we consider the symbolic approach to model checking. Note that everyassertion over a finite-domain FDS can be represented as a boolean formula overboolean variables. We assume that a finite-state FDS is represented by suchformulas, including the initial condition Θ and the bi-assertion ρ representing thetransition relation.A key development for symbolic model checking was the development of binarydecision diagrams (BDD) as an efficient representation of boolean assertions.Analysis of Reactive Systems, NYU, Spring, 2006 95Lecture 6: Symbolic Model Checking A. PnueliBDD’sWe start with a binary decision diagram. For example, following is a decisiondiagram (tree) for the formula (x1= y1) ∧ (x2= y2):x1y1y1x2y2y21 0 0 1 0x2y2y20 1 0 10In general, it requires an exponential number of nodes.Analysis of Reactive Systems, NYU, Spring, 2006 96Lecture 6: Symbolic Model Checking A. PnueliOptimize• Identify identical subgraphs.• Remove redundant tests.Yielding:x1y10y2y2x21y1Analysis of Reactive Systems, NYU, Spring, 2006 97Lecture 6: Symbolic Model Checking A. PnueliDefinitionsA binary decision diagram BDD is a rooted, directed acyclic graph with• One or two nodes of out-degree zero (leaves) labeled 0 or 1, and• A set of variable nodes u of out-degree 2. The two outgoing edges are givenby the functions low(u) and high(u). A variable var(u) is associated with eachnode.A BDD is ordered (OBDD) if the variables respect a given linear orderx1< x2< · · · < xnon all paths through the graph. An OBDD is reduced (ROBDD)if it satisfies:• Uniqueness – no two distinct nodes are the roots of isomorphic subgraphs.• No redundant tests – low(u) 6= high(u) for all nodes u in the graph.For simplicity, we will refer to ROBDD simply as BDDs.Analysis of Reactive Systems, NYU, Spring, 2006 98Lecture 6: Symbolic Model Checking A. PnueliCanonicityClaim 12. For every function f : Booln→ Bool and variable orderingx1< x2< · · · < xn, there exists exactly one BDD representing this function.Analysis of Reactive Systems, NYU, Spring, 2006 99Lecture 6: Symbolic Model Checking A. PnueliSensitivity to Variable OrderingThe complexity of BDD representation is very sensitive to the variable ordering.For example, the BDD representation of (x1= y1) ∧ (x2= y2) under the variableordering x1< x2< y1< y2is:x1x2y1y1y1y1x21 0y2y2Analysis of Reactive Systems, NYU, Spring, 2006 100Lecture 6: Symbolic Model Checking A. PnueliImplementation of BDD PackagesTypes and Variables:node = naturalsvar num = naturalsnode rec =record ofvar : var num;low, high : nodeend recordT : node → node recH : node rec → node ∪ {⊥}Operations:init(T ) Initialize T to contain only 0 and 1u := new(T, i, ℓ, h) allocate a new node u, such thatT (u) = hi, ℓ, hiinit(H) initialize H to ⊥H is the inverse of T . That is, H(T (u)) = u, for every u ∈ dom(T ).We will write var(u), low(u), high(u), and H(i, ℓ, h) as abbreviations for T (u ). var,T (u).low, T (u).high, and H(hi, ℓ, hi).Analysis of Reactive Systems, NYU, Spring, 2006 101Lecture 6: Symbolic Model Checking A. PnueliInternal Representationx20x1x4x4x31x27:6:5:4:2:3:T : u → hi, ℓ, hiu var low high012 4 1 03 4 0 14 3 2 35 2 4 06 2 0 47 1 5 6Analysis of Reactive Systems, NYU, Spring, 2006 102Lecture 6: Symbolic Model Checking A. PnueliMaking or Retrieving a node idFunction MK (i : var num; ℓ, h : node) : node– – Make or retrieve a node with attributes (i, ℓ, h)1: if ℓ = h then return ℓ2: if H(i, ℓ, h) 6= ⊥ then return H(i, ℓ, h)3: u := new(i, ℓ, h)4: H(i, ℓ, h) := u5: return uAnalysis of Reactive Systems, NYU, Spring, 2006 103Lecture 6: Symbolic Model Checking A. PnueliApplying a Binary Boolean Operation to Two BDD’sLet op : Bool × Bool → Bool be a binary boolean operation. The followingfunction uses the auxiliary dynamic array G : node × node → node.Function Apply(op ; u1, u2: node) : node – – Apply op to BDD’s u1and u2G : = ⊥function App(u1, u2: node) : node =if G[u1, u2] 6= ⊥ then u := G[u1, u2]else if u1∈ {0, 1} ∧ u2∈ {0, 1} then u := op(u1, u2)else if var(u1) = var(u2) thenu := MK(var(u1),App(low(u1), low(u2)),App(high(u1), high(u2)))else if var(u1) < var(u2) thenu := MK(var(u1), App(low(u1), u2), App(high(u1), u2))else (∗var(u1) > var(u2)∗)u := MK(var(u2), App(u1, low(u2)), App(u1, high(u2)))G[u1, u2] := ureturn uend Appreturn App( u1, u2)Analysis of Reactive Systems, NYU, Spring, 2006 104Lecture 6: Symbolic Model Checking A. PnueliRestriction (Substitution)Function REST (u : node; j : var num; b : Bool) : node– – Substitute b for xjin BDD ufunction res(u : node) : node =if var(u) > j then return uif var(u) < j thenreturn MK(var(u), res(low(u)), res(high(u)))(∗var(u) = j∗) if b = 0 then return low(u)else return high(u)end resreturn res(u)Restriction is the same as substitution. We denote by t[x 7→ b] the result ofsubstituting b for x in assertion t.Analysis of Reactive Systems, NYU, Spring, 2006 105Lecture 6: Symbolic Model Checking A. PnueliQuantificationExistential quantification can be computed, using the equivalence∃x : t ∼ t[x 7→ 0] ∨ t[x 7→ 1]Universal quantification can be computed dually:∀x : t ∼ t[x 7→ 0] ∧ t[x 7→ 1]Analysis of Reactive Systems, NYU, Spring, 2006
View Full Document