DOC PREVIEW
NYU CSCI-GA 3033 - Symbolic Model Checking

This preview shows page 1-2-3-4 out of 12 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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 recordT : 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

NYU CSCI-GA 3033 - Symbolic Model Checking

Documents in this Course
Design

Design

2 pages

Real Time

Real Time

17 pages

Load more
Download Symbolic Model Checking
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Symbolic Model Checking and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Symbolic Model Checking 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?