5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 83
Текст из файла (страница 83)
. , bi ∈ {0, 1}. Thus, the functionı : Vg × Vf1 × Vf2 → VITE(g, f1 , f2 ) , ı(g , f1 , f2 ) = ITE(g , f1 , f2 )that maps any triple (g , f1 , f2 ) where g is a node in Bg (i.e., a ℘-consistent cofactor ofg) and fi a node in Bfi (i.e., a ℘-consistent cofactor of fi ) to the node ITE(g , f1 , f2 )of BITE(g, f1 , f2 ) yields a surjective mapping from Vg × Vf1 × Vf2 to some superset ofVITE(g, f1 , f2 ) .
Hence:NITE(g, f1 , f2 ) = |VITE(g, f1 , f2 ) | |Vg × Vf1 × Vf2 | = Ng · Nf1 · Nf2Observe that only the triples (g , f1 , f2 ) ∈ Vg × Vf1 × Vf2 where g , f1 , f2 arise from g, f1 , f2by the same evaluation [z1 = b1 , . . . , zi = bi ] are mapped via ı to nodes of BITE(g, f1 , f2 ) .Furthermore, ITE(g , f1 , f2 ) = ITE(g , f1 , f2 ) is possible for (g , f1 , f2 ) = (g , f1 , f2 ).Therefore, NITE(g, f1 , f2 ) can be much smaller than Ng · Nf1 · Nf2 .As a consequence of Lemma 6.77, the size of the ℘-ROBDD for f1 ∨f2 is bounded above bythe product of the sizes of the ℘-ROBDDs for f1 and f2 .
Recall that f1 ∨f2 = ITE(f1 , 1, f2 )and henceNf1 ∨f2 Nf1 · N1 · Nf2 = Nf1 · Nf2 .The same holds for conjunction and even for any other binary Boolean connective. Thisalso applies to operators like ⊕ (xor, parity) where f ⊕ g = ITE(f, ¬g, g), i.e., negation414Computation Tree Logicis needed to express f ⊕ g by ITE, f and g. Lemma 6.77 yields the bound Nf · Ng2 forthe ℘-ROBDD size for f ⊕ g.
However, since the ℘-ROBDDs for g and ¬g are isomorphicup to exchanging the values of the drains, the recursive calls in the ITE-algorithms havethe form ITE(u, v, w) where fv = ¬fw . Hence, the number of nodes in the ℘-ROBDD forf ⊕ g is bounded by the number of triples (f , ¬g , g ) where f is a ℘-consistent cofactorof f and g a ℘-consistent cofactor of g. This yields the upper bound Nf · Ng for the sizeof the ℘-ROBDD of f ⊕ g.Computed Table The problem with Algorithm 22 is that its worst-case running timeis exponential. The reason for this is that, if there are several paths that lead from(u, v1 , v2 ) to (u , v1 , v2 ), then ITE(u , v1 , v2 ) is invoked several times and the whole subOBDDs of these nodes u , v1 , v2 are traversed in each of these recursive invocations.
Toavoid such redundant recursive invocations one uses a computed table that stores the tuples(u, v1 , v2 ), where ITE(u, v1 , v2 ) has already been executed, together with the result, i.e.,the SOBDDD-node w with fw = ITE(fu , fv1 , fv2 ). Thus, we may refine the ITE-algorithmas shown in Algorithm 23 on page 414.Algorithm 23 ITE(u, v1 , v2 )if there is an entry for (u, v1 , v2 , w) in the computed table thenreturn node welse(* no entry for ITE(u, v1 , v2 ) in the computed table *)if u is terminal thenif val(u) = 1 then w := v1 else w := v2 fielsez := min{var(u), var(v1 ), var(v2 )};w1 := ITE(u|z=1 , v1 |z=1 , v2 |z=1 );w0 := ITE(u|z=0 , v1 |z=0 , v2 |z=0 );if w0 = w1 then w := w1 else w := find or add(z, w1 , w0 ) fi;insert (u, v1 , v2 , w) in the computed table;return node wfifiThe number of recursive calls in Algorithm 23 for the input-nodes u, v1 , v2 agrees with the℘-ROBDD size of ITE(fu , fv1 , fv2 ), which is bounded by Nu · Nv1 · Nv2 , where Nv = Nfvdenotes the number of nodes in the sub-OBDD of node v.
The cost per recursive callis constant when the time to access the computed table and to perform the find or addoperation is assumed to be constant. This is an adequate assumption if suitable hashingtechniques are used to organize both tables. However, in practice the running time of theITE algorithm is often much better than this upper bound. First, only in extreme casesSymbolic CTL Model Checking415is the size of the ℘-ROBDD for ITE(fu , fv1 , fv2 ) roughly Nu · Nv1 · Nv2 . Second, the use ofthe ITE operator yields the advantage that all synthesis algorithms that are expressiblevia ITE rely on the same computed table. This increases the hit rate and makes it possiblethat the computation aborts due to an entry in the computed table that has been madeduring the synthesis of another function.
Moreover, there are several tricks to intensifythis phenomenon. One simple trick is to make use of equivalence rules, such asf1 ∨ f2 = ITE(f1 , 1, f2 ) = ITE(f2 , 1, f1 ) = ITE(f1 , f1 , f2 ) = . . . ,and to transform the arguments of ITE into so-called standard triples. Furthermore, theITE-algorithm can be refined by terminating the traversal in certain special cases. E.g.,we have ITE(g, f, f ) = f and ITE(g, 1, 0) = g, which allows aborting the computation ifeither the last two arguments agree or they equal the pair consisting of the 1- and 0-drains.Remark 6.78.The Negation OperatorWe noticed above that the negation operator can be realized as an instance of the ITEoperator as we have ¬f = ITE(f, 0, 1). However, applying the ITE algorithm seems to beunnecessarily complicated since the ℘-ROBDDs for f and ¬f just differ in the values ofthe drains.
In fact, swapping the values of the drains is an adequate technique to realizenegation on ROBDDs, but it is not for shared OBDDs (since changing the values of thedrains also affects the functions of all other root nodes). However, there is a simple trickto perform negation in SOBDDs in constant time. It relies on the use of complement bitsfor the edges. This permits the representation of f and ¬f by a single node. Negationthen just means swapping the value of the complement bit of the incoming edge.
Besidesleading to smaller SOBDD sizes, the use of complement bits also tightens the effect ofstandard triples, since now more equivalence rules can be used to identify the input triplesfor ITE or for early termination. E.g., we haveITE(f1 , 1, f2 ) = f1 ∨ f2 = ¬(¬f1 ∧ ¬f2 ) = ¬ITE(¬f1 , ¬f2 , 0)and ITE(g, 0, 1) = ¬g. However, to ensure canonicity some extra requirements are needed.For instance, the constant function 0 could be represented by the 0-drain (with unnegatedcomplement bit) or the 1-drain with negated complement bit. To guarantee the uniqueness,one could require that only the 1-drain be used and that complement bits be used onlyfor the 0-edges (i.e., edges from the inner nodes to their 0-successors) and the pointersto the root nodes.
For more information on such advanced implementation techniques,further theoretical considerations on OBDDs and variants thereof, we refer to textbookson BDDs, such as [134, 292, 300, 418].Other Operators on OBDDs Although all Boolean connectives can be expressed bythe ITE operator, some more operators are required to perform, e.g., the CTL model416Computation Tree Logicchecking procedure with an SOBDD representation of the transition system.
Recall thatin the symbolic computation of Sat(∃♦B) and Sat(∃B) (see Algorithms 20 and 21 onpage 391) we use iterations of the formfj+1 (x ) := fj (x ) op ∃x .( Δ(x , x ) ∧ fj (x ) )where op ∈ {∨, ∧} and fj = χT is the characteristic function of some set T . Thus, fj+1 isthe characteristic function of T ∩ Pre(T ) (if op = ∧) and T ∪ Pre(T ) (if op = ∨). (For thetreatment of constrained reachability properties like ∃(C U B), we have an additional conjunction with χC , but this is just a technical detail.) Besides disjunction and conjunction,these iterations use existential quantification and renaming. The major difficulty is thepreimage computation, i.e., the computation of the symbolic representation of Pre(T ) bymeans of the expression ∃x .(Δ(x , x ) ∧ fj (x )), which is often called a relational product.Let us start with the rename operator which is inherent in fj (x ) since fj is a switchingfunction for the variables in x and fj (x ) = fj {x ← x } means the function that resultsfrom fj when renaming the unprimed variables xi into their primed copies xi .
At firstglance, the renaming operator appears to be trivial as we simply may modify the variablelabeling function by replacing xi with xi . This operation certainly transforms a givenROBDD for f (x ) into a ROBDD for f (x ). However, if we are given an arbitrary variableordering ℘ where the relative order of the unprimed variables can be different from therelative order of the primed variables (i.e., xi <℘ xj while xj <℘ xi ) then this renamingoperator is no longer adequate, since the resulting ROBDD for f (x ) would rely on anotherordering than ℘. Furthermore, for an implementation with shared OBDDs, modifyingexisting nodes is not appropriate since then the functions for all root nodes might beaffected.
In fact, it is not possible to design a general rename operator which runs in timepolynomial in the size of the input ROBDD. To see why, consider the functionf = (z1 ∧ y1 ) ∨ (z2 ∧ y2 ) ∨ . . . ∨ (zm ∧ ym )of Example 6.73 (page 404). Suppose Var = {zi , yi , zi , yi | 1 i m} and ℘ = , y , . . . , y ) and that we are given the ℘-ROBDD B for f in(zm , ym , . . . , z1 , y1 , z1 , . . . , zmfm1the form of a root node v of a ℘-SOBDD.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
