5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 82
Текст из файла (страница 82)
As we mentioned before, the chosen variable ordering ℘ canbe crucial for the size of the SOBDD representing a transition system. Experimental studies have shown that typically good variable orderings are obtained when grouping togetherthe unprimed variables xi and their copies xi . Later we will give some formal argumentswhy such interleaved variable orderings, like ℘ = (x1 , x1 , . . . , xn , xn ), are advantageous.To perform the CTL model-checking procedure in a symbolic way, the shared OBDD Bwith root nodes for Δ and the fa ’s has to be extended by new root nodes representing thecharacteristic functions of the satisfaction sets Sat(Ψ) for the state subformulae Ψ of theCTL formula Φ to be checked.
For instance, if Φ = a ∧ ¬b with atomic propositions a, b,then we first have to insert a root node for the characteristic function f¬b = ¬fb for Sat(¬b)and then a root node for the switching function fa ∧ f¬b . The treatment of formulae of theform, e.g., ∃♦Ψ or ∃Ψ by means of Algorithms 20 or 21, requires creating additional rootnodes for the functions fi representing the current approximations of satisfaction sets. Ofcourse, adding a new root node for some switching function f also means that we have toadd nodes for all order-consistent cofactors of f that are not yet represented by a node inB.To support such dynamic changes of the set of switching functions to be represented, therealization of shared OBDDs typically relies on the use of two tables: the unique table,which contains the relevant information about the nodes and serves to keep the diagramreduced during the execution of synthesis algorithms, and a computed table, which isneeded for efficiency reasons.
Let us first explain the ideas behind the use of the uniquetable. The implementation of synthesis algorithms and the use of the computed table willbe explained later.The Unique TableThe entries of the unique table are triples of the forminfo(v) = var(v), succ0 (v), succ0 (v)for each inner node v. Note that these info-triples contain the relevant information whichis necessary for the applicability of the isomorphism rule. Accessing the unique table issupported by a find or add-operation which takes as argument a triple z , v1 , v0 consistingof a variable z and two nodes v1 and v0 with v1 = v0 .
The task of the find or addoperation is to check whether there exists a node v in the shared OBDD B such thatinfo(v) = z , v1 , v0 . If so, then it returns node v, otherwise it creates a new z -node vwith 1-successor v1 and 0-successor v0 , and makes a corresponding entry in the uniquetable. Thus, the find or add operation can be viewed as the SOBDD realization of theisomorphism rule. In most BDD packages, the unique table is organized using appropriatehashing techniques.
We skip such details here and assume constant expected time to accessthe into-triple for any node, and to perform the find or add-operation.410Computation Tree LogicBoolean Operators Let us now consider how synthesis algorithms can be realized onSOBDDs, using the unique table. An elegant, but also very efficient way is to support aternary operator, called ITE for “if-then-else”, that covers all Boolean connectives. TheITE operator takes as arguments three switching functions g, f1 , f2 and composes themaccording to “if g then f1 else f2 ”.
Formally:ITE(g, f1 , f2 ) = (g ∧ f1 ) ∨ (¬ g ∧ f2 )For the special case where g is constant we have ITE(0, f1 , f2 ) = f2 and ITE(1, f1 ,f2 ) = f1 . The ITE operator fits very well with the representation of the SOBDD nodes inthe unique table by their info-triples as we have:fv = ITE( z, fsucc1 (v) , fsucc0 (v) ).The negation operator is obtained by ¬f = ITE(f, 0, 1). Also all other Boolean connectives can be expressed by the ITE-operator.
For example:f1 ∨ f2f1 ∧ f2f1 ⊕ f2f1 → f2====ITE(f1 , 1, f2 )ITE(f1 , f2 , 0)ITE(f1 , ¬f2 , f2 ) = ITE(f1 , ITE(f2 , 0, 1), f2 )ITE(f1 , f2 , 1)The realization of the ITE operator on an SOBDD B requires a procedure that takesas input three nodes u, v1 , v2 of B and returns a possibly new node w such that fw =ITE(fu , fv1 , fv2 ), by reusing existing nodes whenever possible and adding new nodes toB if necessary. For this, the sub-OBDDs for the input nodes u, v1 , and v2 are traversedsimultaneously in a top-down fashion, while the synthesis of the sub-ROBDD for w (andgeneration of new nodes) is performed in a bottom-up manner. This method relies on thefollowing observation.Lemma 6.76.Cofactors of ITE(·)If g, f1 , f2 are switching functions for Var, z ∈ Var and b ∈ {0, 1}, thenITE(g, f1 , f2 )|z =b = ITE(g|z =b , f1 |z =b , f2 |z =b ).Proof: For simplicity, let us assume that g, f1 , f2 are switching functions for the samevariable set Var = {z , y1 , .
. . , ym }. This, in fact, is no proper restriction as we maysimply take the union of the variable sets of g, f1 and f2 and regard all three functions asswitching functions for the resulting variable sets. Let (a, c) be a short-form notation forSymbolic CTL Model Checking411the evaluation [z = a, y = c] ∈ Eval(Var). Then, we haveITE(g, f1 , f2 )|z =b (a, c)= ITE(g, f1 , f2 )(b, c)= ( g(b, c) ∧ f1 (b, c) ) ∨ ( ¬g(b, c) ∧ f2 (b, c) )= ( g|z =b (a, c) ∧ f1 |z =b (a, c) ) ∨ ( ¬g|z =b (a, c) ∧ f2 |z =b (a, c) )= ITE(g|z =b , f1 |z =b , f2 |z =b )(a, c).Thus, a node in a ℘-SOBDD for representing ITE(g, f1 , f2 ) is a node w such that info(w) =z , w1 , w0 where• z is the minimal essential variable of ITE(g, f1 , f2 ) according to <℘ ,• w1 , w0 are SOBDD nodes with:fw1 = ITE(g|z =1 , f1 |z =1 , f2 |z =1 ) and fw0 = ITE(g|z =0 , f1 |z =0 , f2 |z =0 ).This observation suggests a recursive algorithm which determines z and then recursivelycomputes the nodes for ITE applied to the cofactors of g = fu , f1 = fv1 , f2 = fv2 forvariable z .
Since the explicit computation of z can be hard, we use the decomposition intocofactors for the minimal variable z that is essential for fu , fv1 or fv2 :z = min{var(u), var(v1 ), var(v2 )}where the minimum is taken according to the total order <℘ on Var ∪ {⊥}. (Recallthat we put var(v) = ⊥ for any drain v and that x <℘ ⊥ for all x ∈ Var.) If z isthe first essential variable of ITE(fu , fv1 , fv2 ), then z ℘ z , since no variable y <℘ zappears in the sub-OBDDs of nodes u, v1 , v2 , and hence, no such variable y can beessential for ITE(fu , fv1 , fv2 ). The case z <℘ z is possible, if accidentally the cofactorsITE(fu , fv1 , fv2 )|z =0 and ITE(fu , fv1 , fv2 )|z =1 agree.
In this case, however, we are in thesituation of the elimination rule and the ITE algorithm returns the node representingITE(fu , fv1 , fv2 )|z =0 . Otherwise, i.e., if the nodes w0 and w1 that have been recursivelydetermined for ITE(fu , fv1 , fv2 )|z =0 and ITE(fu , fv1 , fv2 )|z =1 , respectively, are different,then z = z and a node for representing ITE(fu , fv1 , fv2 ) is obtained by the find or addoperation applied to the info-triple z , w1 , w0 .412Computation Tree LogicThe question remains how to obtain the cofactors fu |z =b , fv1 |z =b , and fv2 |z =b . Nodes thatrepresent these functions are obtained easily since (by choice of variable z ) nodes u, v1 ,and v2 are on the z -level or below, i.e., z ℘ var(v) for v ∈ {u, v1 , v2 }.
If var(v) = z , thenfv |z =b is represented by the b-successor of v. If z <℘ var(v), then z is not essential for fvand we have fv |z =b = fv . Thus, if we definesuccb (v)if var(v) = zv|z =b =uif z <℘ var(v),then v|z =b is the node in B representing fv |z =b . Hence, a node representing the functionITE(fu , fv1 , fv2 )|z =b is obtained by a recursive call of the ITE algorithm with the argumentsu|z =b , v1 |z =b and v2 |z =b (Lemma 6.76). Note that these are already existing nodes in theSOBDD B.The steps to realize the ITE-operator on a shared OBDD by means of a DFS-basedtraversal of the sub-OBDDs of u, v1 , and v2 to determine the relevant cofactors (whererecursive calls of the ITE-algorithm are required) have been summarized in Algorithm 22on page 412.Algorithm 22 ITE(u, v1 , v2 ) (first version)if u is terminal thenif val(u) = 1 thenw := v1elsew := v2fielsez := 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 thenw := w1 ;elsew := find or add(z, w1 , w0 );fifireturn w(* ITE(1, fv1 , fv2 ) = fv1 *)(* ITE(0, fv1 , fv2 ) = fv2 *)(* elimination rule *)(* isomorphism rule (?) *)Before discussing the complexity of the ITE algorithms, we will first study how the size ofthe SOBDD can change through performing the ITE algorithm.
The size of the sub-OBDDfor the (possibly new) node w representing ITE(u, v1 , v2 ) is bounded by Nu ·Nv1 ·Nv2 whereNv denotes the number of the nodes in the sub-OBDD Bv for node v. This follows fromSymbolic CTL Model Checking413the fact that each node w in the generated sub-OBDD for ITE(u, v1 , v2 ) corresponds toone or more triples (u , v1 , v2 ), where u is a node in Bu and vi a node in Bvi Formally:Lemma 6.77.ROBDD Size of ITE(g, f1 , f2 )The size of the ℘-ROBDD for ITE(g, f1 , f2 ) is bounded by Ng · Nf1 · Nf2 where Nf denotesthe size of the ℘-ROBDD for f .Proof: Let ℘ = (z1 , . . . , zm ) and let Bf denote the ℘-ROBDD for f where the nodes arethe ℘-consistent cofactors of f (see the proof of part (a) of Theorem 6.70). We write Vffor the node set of Bf , i.e.,Vf = { f |z1 =b1 ,...,zi =bi | 0 i m, b1 , .
. . , bi ∈ {0, 1} }.Note that several of the cofactors f |z1 =b1 ,...,zi =bi might agree, and hence, they stand for thesame element (node) of Vf . By Lemma 6.76, the node set VITE(g, f1 , f2 ) of the ℘-ROBDDBITE(g, f1 , f2 ) for ITE(g, f1 , f2 ) agrees with the set of switching functionsITE(g|z1 =b1 ,...,zi =bi , f1 |z1 =b1 ,...,zi =bi , f2 z1 = b1 , . . . , zi = bi )where 0 i m, b1 , . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
