5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 78
Текст из файла (страница 78)
( Δ(x , x ) ∧ fj (x ) ) );j := j + 1until fj (x ) = fj−1 (x );return fj (x ).If we are just interested in the one-step predecessors, i.e., properties of the form ∃ B,then no iteration is needed and the characteristic function of the set of states s ∈ S withPost(s) ∩ B = ∅ is obtained by∃x . ( Δ(x , x ) ∧ χB (x ) ). s ∈ Post(s)s ∈BIn a similar way, the set Sat(∃B) of all states s that have an infinite path consisting ofstates in a given set B can be computed symbolically.
Here, we mimic the computationof the largest set T ⊆ B with Post(t) ∩ T = ∅ for all t ∈ T by the iteration T0 = B andTj+1 = Tj ∩ {s ∈ S | ∃s ∈ S s.t. s ∈ Post(s) ∧ s ∈ Tj }Symbolic CTL Model Checking391Algorithm 21 Symbolic computation of Sat(∃B)f0 (x ) := χB (x );j := 0;repeatfj+1 (x ) := fj+1 (x ) ∧ ∃x . ( Δ(x , x ) ∧ fj (x ) );j := j + 1until fj (x ) = fj−1 (x );return fj (x ).in a symbolic way, as shown in Algorithm 21 on page 391.These considerations show that the CTL model checking problem “Does CTL formulaΦ hold for TS?” can be solved symbolically by means of switching functions fΨ thatrepresent the satisfaction sets Sat(Ψ) of the subformulae Ψ of Φ.
The satisfaction sets fafor the atomic propositions a ∈ AP are supposed to be given. Union, intersection, andcomplementation of sets of states correspond to disjunction, conjunction, and negation onthe level of switching functions. E.g., the satisfaction set for Ψ1 ∧¬Ψ2 , is obtained by fΨ1 ∧¬fΨ2 . The treatment of formulae ∃(Ψ1 U Ψ2 ) and ∃Ψ relies on the techniques sketchedin Algorithms 20 and 21.
To treat full CTL, we can either transform any CTL formulainto an equivalent CTL formula in existential normal form or use analogous symbolicalgorithms for universally quantified formulae such as ∀(Φ U Ψ).The major challenge is to find an appropriate data structure for the switching functions.Besides yielding compact representations of the satisfaction sets and the transition relation, this data structure has to support the Boolean connectives (disjunction, conjunction,complementation) and the comparison of two switching functions. The latter is needed inthe termination criteria for the repeat loops in Algorithms 20 and 21.Before presenting the definition of binary decision diagrams that have proven to be veryefficient in many applications, let us first discuss other potential data structures.
Truthtables can be ruled as they always have the size 2n for switching functions with n variables. The same holds for binary decision trees since they always have 2n+1 − 1 nodes.Conjunctive or disjunctive normal forms for the representation of switching functions bypropositional logic formulae yield the problem that checking equivalence (i.e., equality forthe represented switching functions) is expensive, namely coNP-complete. Furthermore,there are switching functions fm with m essential variables where the length of any representation by a conjunctive normal form formula grows exponentially in m.
The sameholds for disjunctive normal forms. However, the latter is no proper argument againstconjunctive or disjunctive normal forms, because there is no data structure that ensuresrepresentations of polynomial size for all switching functions. The reason for this is that the392Computation Tree Logicnumber of switching functions for m variables z1 , . . . , zm is double exponential in m. Notethat |Eval(z1 , . . . , zm )| = 2m , and hence, the number of functions Eval(z1 , .
. . , zm ) → {0, 1}mis 22 . Suppose we are given a universal data structure for switching functions (i.e., adata structure that can represent any switching function) such that Km is the number ofswitching functions for z1 , . . .
, zm that can be represented by at most 2m−1 bits. Then:Km m−122i = 22m−1 +1− 1 < 22m−1 +1.i=0But then there are at least22m− 22m−1 +1= 22m−1 +1 m m−1 m−1m−1 +1−1−1· 22 −2− 1 = 22· 22−1switching functions for z1 , . . . , zm where the representation requires more than 2m−1 bits.This calculation shows that we cannot expect a data structure which is efficient for allswitching functions. Nevertheless there are data structures which yield compact representations for many switching functions that appear in practical applications. A datastructure that has been proven to be very successful for model checking purposes, in particular in the area of hardware verification, is ordered binary decision diagrams (OBDDs).Besides yielding compact representation for many “realistic” transition systems, they enjoy the property that the Boolean connectives can be realized in time linear in the sizeof the input OBDDs and that (with appropriate implementation techniques) equivalencechecking can even be performed in constant time.In the remainder of this section, we explain those aspects of ordered binary decisiondiagrams that are relevant to understanding the main concepts of symbolic model checkingwith these data structures.
Further theoretical aspects on binary decision diagrams, theirvariants and applications, can be found, e.g., in the textbooks [134, 180, 292, 300, 418].For details on OBDD-based symbolic model checking we refer to [74, 92, 288, 374].6.7.3Ordered Binary Decision DiagramsOrdered binary decision diagrams (OBDDs for short), originally proposed by Bryant [70],yield a data structure for switching functions that relies on a compactification of binarydecision trees. The rough idea is to skip redundant fragments of a binary decision tree.This means collapsing constant subtrees (i.e., subtrees where all terminal nodes have thesame value) into a single node and identifying nodes with isomorphic subtrees.
In thisway, we obtain a directed acyclic graph of outdegree 2 where – as in binary decision trees– the inner nodes are labeled by variables and their outgoing edges stand for the possibleevaluations of the corresponding variable. The terminal nodes are labeled by the functionvalue.Symbolic CTL Model Checking393z1z1z2z2z31z301010Figure 6.21: Binary decision diagram for z1 ∧ (¬z2 ∨ z3 ).Example 6.60.From Binary Decision Tree to OBDDBefore presenting the formal definition of binary decision diagrams, we explain the mainideas by means of the function f (z1 , z2 , z3 ) = z1 ∧ (¬z2 ∨ z3 ).
A binary decision tree for fhas been shown in Figure 6.20 on page 385. Since all terminal nodes in the right subtreeof the root have value 0 (which reflects the fact that the cofactor f |z1 =0 agrees with theconstant function 0), the inner tests for variables z2 and z3 in that subtree are redundantand the whole subtree can be replaced by a terminal node with value 0. Similarly, thesubtree of the z3 -node representing the cofactor f |z1 =1,z2 =0 = 1 can be replaced with aterminal node for the value 1.
This leads to the graph shown on the left of Figure 6.21.Finally, we may identify all terminal nodes with the same value, which yields the graphshown on the right of Figure 6.21.Example 6.61.From Binary Decision Tree to OBDDAs another example, consider the switching function f = (z1 ∧ z3 ) ∨ (z2 ∧ z3 ). The upperpart of Figure 6.22 on page 394 shows a binary decision tree for f . The subtree of the z3node on the right is constant and can be replaced by a terminal node.
The three subtreesof the z3 -nodes for the cofactors f |z1 =0,z2 =1 , f |z1 =1,z2 =0 , and f |z1 =1,z2 =1 are isomorphicand can thus be collapsed. This yields the decision graph shown in the middle part ofFigure 6.22. But now the z2 -node for the cofactor f |z1 =1 becomes redundant, as regardlesswhether z2 = 0 or z2 = 1, the same node will be reached.
This permits removing this z2 node and redirecting its incoming edge. This yields the binary decision diagram depictedin the lower part of Figure 6.22.394Computation Tree Logicz1z2z2z3z3101z301z3000z1z2z2z310z1z2z310Figure 6.22: Binary decision diagrams for f = (z1 ∧ z3 ) ∨ (z2 ∧ z3 ).Symbolic CTL Model CheckingNotation 6.62.395Variable OrderingLet Var be a finite set of variables. A variable ordering for Var denotes any tuple ℘ =(z1 , .
. . , zm ) such that Var = {z1 , . . . , zm } and zi = zj for 1 i < j m. We write <℘ forthe induced total order on Var. I.e., for ℘ = (z1 , . . . , zm ) the binary relation <℘ on Var isgiven by zi <℘ zj if and only if i < j. We write zi ℘ zj iff either zi <℘ zj or i = j.Definition 6.63.Ordered Binary Decision Diagram (OBDD)Let ℘ be a variable ordering for Var. An ℘-ordered binary decision diagram (℘-OBDD forshort) is a tupleB = (V, VI , VT , succ0 , succ1 , var, val, v0 )consisting of• a finite set V of nodes, disjointly partitioned into VI and VT where the nodes in VIare called inner nodes, while the nodes in VT are called terminal nodes or drains;• successor functions succ0 , succ1 : VI → V that assign to each inner node v a0-successor succ0 (v) ∈ V and a 1-successor succ1 (v) ∈ V ;• a variable labeling function var : VI → Var that assigns to each inner node v avariable var(v) ∈ Var;• a value function val : VT → { 0, 1 } that assigns to each drain a function value 0 or1;• a root (node) v0 ∈ V .Consistency of the variable labeling function with the variable ordering ℘ is required inthe following sense.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
