5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 81
Текст из файла (страница 81)
. . , m}otherwisefm |zm =am ,zm =bm ,...,zi+1 =ai+1 ,zi+1 =bi+1 ,zi =ai ∈ { 1, yi ∨ fi−1 }where f0 = 0. Hence, the ℘-ROBDD for fm has exactly one zi -node representing thefunction fi , exactly one yi -node for the function yi ∨ fi−1 (for 1 i m), and two drains.To see why the variable ordering ℘ leads to a ℘ -ROBDD of exponential size, we considerthe ℘ -consistent cofactors!yifb = fm |z1 =b1 ,...,zm =bm =i∈Ibwhere b = (b1 , . . . , bn ) and Ib = {i ∈ {1, .
. . , m} | bi = 1. The set of essential variables offb is {yi | i ∈ Ib }. As f b, c ∈ {0, 1}m , b = c the index sets Ib and Ic are different, the fband fc have different essential variables. Therefore, fb = fc if b = c. But then the numberof ℘ -consistent cofactors is at least 2m . This yields that the ℘ -ROBDD for fm has atmost 2m nodes.406Computation Tree LogicSince for many switching functions the ROBDD sizes for different variable ordering canvary enormously, the efficiency of BDD-based computations crucially relies on the useof techniques that improve a given variable ordering.
Although the problem to find anoptimal variable ordering is known to be computationally hard (already the problem todecide whether a given variable ordering is optimal is NP-hard [56, 386]), there are severalefficient heuristics for improving the current ordering. Most promiment is the so-calledsifting algorithm [358] which relies on a local search for the best position for each variable,when the ordering of the other variables is supposed to be fixed. Explanations on suchvariable reordering algorithms and further discussions on the variable ordering problemare beyond the scope of this monograph. We refer the interested reader to the textbooks[292, 418] and conclude the comments on the influence of the variable ordering by theremark that there are also types of switching functions with ROBDDs of polynomial sizeunder all variable orderings and types of switching functions where any variable orderingleads to a ROBDD of exponential size.
An example of the latter is the middle bit ofthe multiplication function [71]. Examples of switching functions where each variableordering leads to a ROBDD of at most quadratic size are symmetric functions. These areswitching functions where the function values just depend on the number of variables thatare assigned to 1. Stated differently, f ∈ Eval(z1 , . .
. , zm ) is symmetric if and only iff ([z1 = b1 , . . . , zm = bm ]) = f ([z1 = bi1 , . . . , zm = bim ])for each permutation (i1 , . . . , im ) of (1, . . . , m). Examples of symmetric functions forVar = {z1 , . . . , zm } are z1 ∨z2 ∨. . .∨zm , z1 ∧z2 ∧.
. .∧zm , the parity function z1 ⊕z2 ⊕. . .⊕zm(which returns 1 iff the number of variables that are assigned to 1 is odd), and the majorityfunction (which returns 1 iff the number of variables that are assigned to 1 is greater thanthe number of variables that are assigned to 0).
The ROBDDs for symmetric functionshave the same topological structure for all variable orderings. This follows from the factthat the ℘-ROBDD for a symmetric function can be transformed into the ℘ -ROBDD byjust modifying the variable labeling function.Lemma 6.74.ROBDD-Size for Symmetric FunctionsIf f is a symmetric function with m essential variables, then for each variable ordering ℘the ℘-ROBDD has size O(m2 ).Proof: Given a symmetric function f for m variables and a variable ordering ℘, say℘ = (z1 , . . . , zm ), then the ℘-consistent cofactors f |z1 =b1 ,...,zi =bi and f |z1 =c1 ,...,zi =ci agreefor all bit tuples (b1 , . .
. , bi ) and (c1 , . . . , ci ) that contain the same number of 1’s. Thus,there are at most i + 1 different ℘-consistent cofactors of f that arise by assigning valuesto thethe total number of ℘-consistent cofactors is bounded above first i variables.
Hence,2 ).(i+1)=O(mby mi=0Symbolic CTL Model Checking407ROBDDs vs. CNF/DNF Both the parity and the majority function provide examplesfor switching functions with small ROBDD representations, while any representation ofthem by conjunctive or disjunctive normal forms (CNF, DNF) requires formulae of exponential length. Vice versa, there are also switching functions with short conjunctive ordisjunctive normal forms, while the ROBDD under any variable ordering has exponentiallength (see, e.g., [418]). In fact, ROBDDs yield a totally different picture for complexitytheoretic considerations than CNF or DNF.
For example, given a CNF representation fora switching function f , the task to generate a CNF for ¬f is expensive, as f might beexpressible by a CNF of polynomial length, while any CNF for ¬f has at least exponentially many clauses. For ROBDDs, however, negation is trivial as we may simply swapthe values of the drains. In particular, for any variable ordering ℘, the ℘-ROBDDs for fand ¬f have the same size. For another example, regard the satisfiability problem, whichis known to be NP-complete for CNF, but again trivial for ROBDDs, since f = 0 if andonly if the ℘-ROBDD for f does not contain a 0-drain. Similarly, the question whethertwo CNFs are equivalent is computationally hard (coNP-complete), but can be solved for℘-ROBDDs B and C by checking isomorphism.
The latter can be performed by a simultaneous traversal of the ℘-OBDDs in time linear in the sizes of B and C. See Exercise6.12, page 436. Note that these results do not contradict the complexity theoretic lowerbounds, since “linear time” for a ROBDD-based algorithm means linear in the size of theinput ROBDDs, which could be exponentially larger than equivalent input formulae (e.g.,CNF).6.7.4Implementation of ROBDD-Based AlgorithmsThe efficiency of ROBDD-based algorithms to manipulate switching functions cruciallyrelies on appropriate implementation techniques. In fact, with tricky implementationtechniques, equivalence checking for ROBDDs can even be realized in constant time.
Inthe sequel, we will explain the main ideas of such techniques, which provide the basisfor most BDD packages and serve as a platform for an efficient realization of synthesisalgorithms on ROBDDs. The purpose of synthesis algorithms is to construct a ℘-ROBDDfor a function f1 op f2 (where op is a Boolean connective such as disjunction, conjunction,implication, etc.), when ℘-ROBDDs for f1 and f2 are given.
Recall that the symbolicrealization of the CTL model-checking procedure relies on such synthesis operations.The idea, originally proposed in [301], is to use a single reduced decision graph with oneglobal variable ordering ℘ to represent several switching functions, rather than using separate ℘-ROBDDs for each of the switching functions. All computations on these decisiongraphs are interleaved with the reduction rules to guarantee redundance-freedom at anytime.
Thus, the comparison of two represented functions simply requires checking equalityof the nodes for them, rather than analyzing their sub-OBDDs.408Computation Tree Logicz1z1z2z1z2Figure 6.26: Example of a shared OBDD.We start with the formal definition of a shared ℘-OBDD which is the same as a ℘-ROBDD,the only difference being that we can have more than more root node.Definition 6.75.Shared OBDDLet Var be a finite set of Boolean variables and ℘ a variable ordering for Var.
A shared℘-OBDD (℘-SOBDD for short) is a tuple B = (V, VI , VT , succ0 , succ1 , var, val, v 0 )where V , VI , VT , succ0 , succ1 , var, and val are as in ℘-OBDDs (see Definition 6.63 onpage 395). The last component is a tuple v 0 = (v01 , . . . , v0k ) of roots. The requirements areas in ℘-ROBDDs, i.e., for all nodes v, w ∈ V , (1) var(v) <℘ var(succb (v)) if v ∈ VI andb ∈ {0, 1} and (2) v = w implies fv = fw , where the switching function fv for the nodesv ∈ V is defined as for OBDDs.Figure 6.26 shows a shared OBDD with four root nodes that represent the functionsz1 ∧ ¬z2 , ¬z2 , z1 ⊕ z2 and ¬z1 ∨ z2 .If v is a node in a ℘-SOBDD B, then the sub-OBDD Bv is the ℘-ROBDD that results fromB by removing all nodes that are not reachable from v and declaring v to be the root node.In fact, Bv is the ℘-ROBDD for fv , and thus, the size Nv of Bv is with the ℘-ROBDDsize of fv .
Thus, an alternative view of an SOBDD is the combination of several ROBDDsfor the same variable ordering ℘ by sharing nodes for common ℘-consistent cofactors. Inparticular, an SOBDD has exactly two drains for the constant functions 0 and 1 (where weignore the pathological case of an SOBDD with a single root node representing a constantfunction). Thus, if f1 , . . . , fk are the functions for the root nodes v01 , . . . , v0k of B, then thesize (i.e., total number of nodes) of B is often smaller than but at most Nf1 + . . .
+ Nfkwhere Nf denotes the ℘-ROBDD size of f .For the symbolic representation of a transition system by means of switching functionsΔ(x , x ) for the transition relation and switching functions fa (x ), a ∈ AP , for the satisfaction sets of the atomic propositions (see page 386), one might use a shared OBDD withSymbolic CTL Model Checking409root nodes for Δ and the fa ’s.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
