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.Analysis of Reactive Systems, NYU, Fall, 2009 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, Fall, 2009 96Lecture 6: Symbolic Model Checking A. PnueliOptimize• Identify identical subgraphs.• Remove redundant tests.Yielding:x1y10y2y2x21y1Analysis of Reactive Systems, NYU, Fall, 2009 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 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 asBDDs.Analysis of Reactive Systems, NYU, Fall, 2009 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, Fall, 2009 99Lecture 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 0y2y2Analysis of Reactive Systems, NYU, Fall, 2009 100Lecture 6: Symbolic Model Checking A. PnueliImplementation of BDD 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 ⊥His the inverse of T . That is, H(T (u)) = u, for every u ∈ dom(T ).We will writevar(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, Fall, 2009 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, Fall, 2009 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, Fall, 2009 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 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)Analysis of Reactive Systems, NYU, Fall, 2009 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 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.Analysis of Reactive Systems, NYU, Fall, 2009 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, Fall, 2009 106Lecture 6: Symbolic Model Checking A. PnueliApplication of BDD’s to Symbolic Model CheckingLet V be the state variables for the FDS D. Taking a vocabulary U = V ∪ V0, 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 ofV0.The transition relationρ is represented as a BDD over U which may be fullydependent on bothV and V0.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ρ ψ = ∃V0: ρ(V, V0) ∧ ψ(V0)Priming an assertion ψ is performed byprime(ψ) = ∃V : ψ(V ) ∧ V0= VAnalysis of Reactive Systems, NYU, Fall, 2009