Lecture 6: Symbolic Model Checking A. PnueliSymbolic Model CheckingNext, we consider the symbolic approach to model checking. Note that everyassertion over a finite-domainFDS can be represented as a boolean formula overboolean variables. We assume that a finite-stateFDS is represented by suchformulas, including theinitial condition Θ and the bi-assertion ρ representing thetransition relation.A key development for symbolic model checking was the development ofbinarydecision diagrams(BDD) as an efficient representation of boolean assertions.Timed and Hybrid Systems, NYU, Spring, 2007 99Lecture 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.Timed and Hybrid Systems, NYU, Spring, 2007 100Lecture 6: Symbolic Model Checking A. PnueliOptimize• Identify identical subgraphs.• Remove redundant tests.Yielding:x1y10y2y2x21y1Timed and Hybrid Systems, NYU, Spring, 2007 101Lecture 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 functionslow(u) and high(u). A variable var(u) is associated with eachnode.ABDD 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.Timed and Hybrid Systems, NYU, Spring, 2007 102Lecture 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.Timed and Hybrid Systems, NYU, Spring, 2007 103Lecture 6: Symbolic Model Checking A. PnueliSensitivity to Variable OrderingThe complexity of BDD representation is very sensitive to the variable ordering.For example, theBDD representation of (x1= y1) ∧ (x2= y2) under the variableorderingx1< x2< y1< y2is:x1x2y1y1y1y1x21 0y2y2Timed and Hybrid Systems, NYU, Spring, 2007 104Lecture 6: Symbolic Model Checking A. PnueliImplementation ofBDD PackagesTypes and Variables:node = naturalsvar num = naturalsnode rec =record ofvar : var num;low, high : nodeend recordT : node → noderecH : noderec → 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).Timed and Hybrid Systems, NYU, Spring, 2007 105Lecture 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 6Timed and Hybrid Systems, NYU, Spring, 2007 106Lecture 6: Symbolic Model Checking A. PnueliMaking or Retrieving anode 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 uTimed and Hybrid Systems, NYU, Spring, 2007 107Lecture 6: Symbolic Model Checking A. PnueliApplying a Binary Boolean Operation to TwoBDD’sLet op : Bool × Bool → Bool be a binary boolean operation. The followingfunction uses the auxiliary dynamic arrayG : 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)Timed and Hybrid Systems, NYU, Spring, 2007 108Lecture 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 thenreturnMK(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 ofsubstitutingb for x in assertion t.Timed and Hybrid Systems, NYU, Spring, 2007 109Lecture 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]Timed and Hybrid Systems, NYU, Spring, 2007 110Lecture 6: Symbolic Model Checking A. PnueliApplication ofBDD’s to Symbolic Model CheckingLet V be the state variables for the FDS D. Taking a vocabulary U = V ∪ V′, werepresent the state formulasΘ, J for each J ∈ J , pi, qi, for each hpi, qii ∈ C,and theINV symbolic working variables new and old as BDD’s over U which areindependent ofV′.The transition relationρ is represented as a BDD over U which may be fullydependent on bothV and V′.All the boolean operations used in theINV algorithm can be implemented by theApply function. Negation can be computed by ¬t = t ⊕ 1, where ⊕ is sum modulo2.To check for equivalence such asold = new we compute t := (old ↔ new) andthen verify that the result is the singletonBDD 1.The existential pre-conditiontransformer is computed byρ ψ = ∃V′: ρ(V, V′) ∧ ψ(V′)Priming an assertion ψ is performed byprime(ψ) = ∃V : ψ(V ) ∧ V′= VTimed and Hybrid Systems, NYU, Spring, 2007