5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 80
Текст из файла (страница 80)
It remains to show that ı preserves the variable labeling of inner nodes andmaps the successors of an inner node v of C to the successors of fv = ı(v) in B.Let v be an inner node of C, say a z -node, and let w0 and w1 be the 0- and 1-successorsof v in C. Then, the cofactor fv |z =0 agrees with fw0 , and similarly, fw1 = fv |z =1 . (Thisholds in any OBDD.) As C is reduced, fv is nonconstant (since otherwise fv = fw0 = fw1 ).Variable z must be the first essential variable of fv according to <℘ , i.e., z = var(fv ).
Letus see why. Let y = var(fv ). The assumption z <℘ y yields that z is not essential forfv , and therefore fw0 = fv |z =0 = f = fv |z =1 = fw1 . But then w0 , w1 and v representthe same function. Since w0 = v and w1 = v, this contradicts the assumption that C isreduced. The assumption y <℘ z is also impossible since then no y-node would appear inthe sub-OBDD Cv , which is impossible as y = var(fv ) is essential for fv by definition.But then var(ı(v)) = z = varC(v) and, for b ∈ {0, 1}:succb (ı(v)) = fv |z =b = fsuccC (v) = ı(succCb (v))bHence, ı is an isomorphism.400Computation Tree LogicTheorem 6.70 permits speaking about “the ℘-ROBDD” for a given switching function ffor Var.
The ℘-ROBDD-size of f denotes the size (i.e., number of nodes) in the ℘-ROBDDfor f .Corollary 6.71.Minimality of Reduced OBDDsLet B be a ℘-OBDD for f . Then, B is reduced if and only if size(B) size(C) for each℘-OBDD C for f .Proof: This follows from the facts that (i) each ℘-consistent confactor of f is representedin any ℘-OBDD C for f by at least one node, and (ii) a ℘-OBDD B for f is reduced if andonly if the nodes of B stand in one-to-one-correspondence to the ℘-consistent cofactors off.Reduction rules. When the variable ordering ℘ for Var is fixed, then reduced ℘-OBDDsprovide unique representations of switching functions for Var.
(Of course, uniqueness isup to isomorphism.) Although reducedness is a global condition for an OBDD, there aretwo simple local reduction rules (see Figure 6.23), which can successively be applied totransform a given nonreduced ℘-OBDD into an equivalent ℘-ROBDD.Elimination rule: If v is an inner node of B with succ0 (v) = succ1 (v) = w, then removev and redirect all incoming edges u → v to w.Isomorphism rule: If v, w are nodes in B with v = w and either v, w are drains withval(v) = val(w) or v, w are inner nodes withvar(v), succ1 (v), succ0 (v) = var(w), succ1 (w), succ0 (w),then remove node v and redirect all incoming edges u → v to node w.Both rules delete node v.
The redirection of the incoming edges u → v to node w meansthe replacement of the edges u → v which u → w. Formally, this means that we deal withthe modified successor functions given bysuccb (u)if succb (u) = vsuccb (u) =wif succb (u) = vfor b = 0, 1. The transformations described in Examples 6.60 and 6.61 rely on the application of the isomorphism and elimination rule.Symbolic CTL Model Checking401uuuuvbecomeswwbecomes1vv0v0w1w0w1wwwbecomes010Figure 6.23: Reduction rules for OBDDs.1402Computation Tree LogicBoth reduction rules are sound in the sense that they do not affect the semantics, i.e., ifC arises from a ℘-OBDD B by applying the elimination or isomorphism rule, then C isagain a ℘-OBDD and fB = fC.
This is due to the fact that both rules simply collapsetwo nodes v and w with fv = fw . For the elimination rule applied to a z -node v withw = succ0 (v) = succ1 (v), we havefv = (¬z ∧ fsucc0 (v) ) ∧ (z ∧ fsucc1 (v) ) = (¬z ∧ fw ) ∧ (z ∧ fw ) = fw .Similarly, if the isomorphism rule is applied to z -nodes v and w thenfv = (¬z ∧ fsucc0 (v) ) ∧ (z ∧ fsucc1 (v) ) = (¬z ∧ fsucc0 (w) ) ∧ (z ∧ fsucc1 (w) ) = fw .Since the application of the reduction rules decreases the number of nodes, the process togenerate an equivalent ℘-OBDD by applying the reduction rules as long as possible alwaysterminates. In fact, the resulting OBDD is reduced:Theorem 6.72.Completeness of Reduction Rules℘-OBDD B is reduced if and only if no reduction rule is applicable to B.Proof: ⇒: The applicability of a reduction rule implies the existence of at least two nodesrepresenting the same switching function. Thus, if B is reduced, then no reduction ruleis applicable.⇐: We prove the other direction by induction on the number of variables.
More precisely,suppose that we are given a ℘-OBDD B for the variable ordering ℘ = (z1 , . . . , zm ) suchthat neither the elimination nor the isomorphism rule is applicable and show by inductionon i thatfv = fw for all nodes v, w ∈ Vi where v = w.Here, Vi denotes the set of all nodes v ∈ V on level i or lower. Formally, Vi is the set of allnodes v in B such that zi ℘ var(v). Recall that var(v) = ⊥ (undefined) for each drain vand that z <℘ ⊥ for all variables z .We start the induction with the bottom level i = m + 1. The statement fv = fw for alldrains v, w where v = w is trivial since the nonapplicability of the isomorphism rule yieldsthat there is at most one drain with value 0 and at most one drain with value 1.
In theinduction step i + 1 =⇒ i (m i 0) we suppose that fv = fw for all nodes v, w ∈ Vi+1with v = w (induction hypothesis). Suppose there are two nodes v, w ∈ Vi with v = wand fv = fw . At least one of the nodes v or w must be on level i. Say v ∈ Vi \ Vi+1 . Then,var(v) = zi .Symbolic CTL Model Checking403Let us first suppose that w ∈ Vi+1 . Then, either w is a drain or a zj -node for some j > i.In either case, variable zi is not essential for fv = fw . As v is a zi -node this yields thatfv agrees with the switching functions fv0 and fv1 of its successors v0 = succ0 (v) andv1 = succ1 (v). But then v0 , v1 ∈ Vi+1 and fv0 = fv1 . The induction hypothesis yields thatv0 = v1 .
But then the elimination rule would be applicable. Contradiction.Suppose now that w is a zi -node too. Let v0 = succ0 (v), v1 = succ1 (v) and w0 = succ0 (w),w1 = succ1 (w). The assumption fv = fw yields thatfv0 = fv |zi =0 = fw |zi =0 = fw0and fv1 = fw1 . As v0 , v1 , w0 , w1 ∈ Vi+1 the induction hypothesis yields that v0 = w0 andv1 = w1 . But then the ismorphism rule is applicable. Contradiction.Theorem 6.70 suggests a reduction algorithm which takes as input a nonreduced ℘-OBDDB and constructs an equivalent ℘-OBDD by applying the reduction rules as long as possible. According to the inductive proof of the completeness of the reduction rules inTheorem 6.72, this technique is complete if the candidate nodes for the reduction rules areconsidered in a bottom-up manner.
That is, initially we identify all drains with the samevalue. Then, for the levels m, m − 1, . . . , 1 (in this order) we apply the elimination andisomorphism rule. At level i, we first remove all nodes with identical successors (elimination rule) and then check the pairs of zi -nodes where the isomorphism rule is applicable.To support the isomorphism rule a bucket technique can be used that groups together (1)all zi -nodes with the same 0-successor and (2) splits all buckets consisting of zi -nodes withthe same 0-successor into buckets consisting of zi -nodes with exactly the same successors.Then, application of the isomorphism rule simply means that the nodes in the bucketsresulting from step (2) have to be collapsed into a single node. The time complexity of thisalgorithm is in O(size(B)). In particular, given two ℘-OBDDs B and C, the equivalenceproblem “Does fB = fC hold?” can be solved by applying the reduction algorithm toboth and then checking isomorphism for the reduced ℘-ROBDDs (see Exercise 6.12 onpage 436).
We will see later that with tricky implementation techniques, which integratethe steps of the reduction algorithm in the synthesis algorithms for ROBDDs and thus ensure that at any time the decision graph is reduced, the equivalence problem for ROBDDscan even be solved in constant time.The Variable Ordering Problem The result stating the canonicity of reduced OBDDs crucially depends on the fact that the variable ordering ℘ is assumed to be fixed.Varying the variable ordering can lead to totally different ROBDDs, possibly ranging fromROBDDs of linear size to ROBDDs of exponential size. The results established before yieldthat the size (i.e., number of nodes) in the ℘-ROBDD for a switching function f agrees404Computation Tree Logicz1y1z2y2z3y310Figure 6.24: ROBDD for the function f3 = (z1 ∧ y1 ) ∨ (z2 ∧ y2 ) ∨ (z3 ∧ y3 )for the variable ordering ℘ = (z1 , y1 , z2 , y2 , z3 , y3 ).with the number of ℘-consistent cofactors of f .
Thus, reasoning about the memory requirements of ROBDD-based approaches relies on counting the number of order-consistentcofactors.Example 6.73.A Function with Small and Exponential-Size ROBDDsTo illustrate how the size of ROBDDs can be determined by analyzing the cofactors weconsider a simple switching function which has both ROBDDs of linear size and ROBDDswith exponentially many nodes. Let m 1 andfm = (z1 ∧ y1 ) ∨ (z2 ∧ y2 ) ∨ . .
. ∨ (zm ∧ ym ).For the variable ordering ℘ = (zm , ym , zm−1 , ym−1 , . . . , z1 , y1 ), the ℘-ROBDD for fm has2m + 2 nodes, while Ω(2m ) nodes are required for the ordering ℘ = (z1 , z2 , . . . , zm ,y1 , . . . , ym ). Figures 6.25 and 6.24 show the ROBDDs for the linear-size and exponentialsize variable orderings for m=3. We first consider the ordering ℘ which groups the variableszi and yi that appear in the same clause. In fact, the variable ordering ℘ is optimal forfm as the ℘-ROBDD for fm contains one node for each variable. (This is the best we canhope to have as all 2n variables are essential for fm and must appear in any ROBDD forSymbolic CTL Model Checking405z1z2z2z3z3z3z3y1y1y1y1y2y2y301Figure 6.25: ROBDD for the function f3 = (z1 ∧ y1 ) ∨ (z2 ∧ y2 ) ∨ (z3 ∧ y3 )for the variable ordering ℘ = (z1 , z2 , z3 , y1 , y2 , y3 ).fm .) Note that for 1 i m:fm |zm =am ,zm =bm ,...,zi =ai ,zi =bi =⎧⎨ 1⎩fi−1if aj = bj = 1for some j ∈ {i, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
