5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 84
Текст из файла (страница 84)
The goal is now to rename zi into zi and yi intoyi in f , i.e., to compute the ℘-ROBDD representation of ∧ y ).f {zi ← zi , yi ← yi | 1 i m} = (z1 ∧ y1 ) ∨ . . . ∨ (zmmBy the results of Example 6.73: while the ℘-ROBDD size of f is 2m + 2, the ℘-ROBDDsize of f {. . .} is Ω(2m ). This observation shows that there is no linear-time algorithm thatrealizes the rename operator for arbitrary variable orderings.
However, if we suppose thatxi and xi are neighbors in the ordering ℘, e.g., xi <℘ xi and there is no variable z with xs <℘z <℘ xi , then renaming xi into xi for a function f (x ) is simple. As for the ITE operator, wecan work with a DFS-based traversal of the sub-OBDD for the node representing f (x ) andSymbolic CTL Model Checking417generate the ROBDD for f (x ) in a bottom-up manner; see Algorithm 24. The algorithmtakes as input a node v of a π-SOBDD and tuples x = (x1 , . .
. , xn ), x = (x1 , . . . , xn ), ofpairwise distinct variables such that x1 , . . . , xn are not essential for fv and xi und xi areneighbors in π. The output is a node w such that fw = fv {x ← x }. To avoid multipleinvocations of the algorithms with the same input node v, we use a computed table thatstores all nodes v where Rename(v, x ← x ) has already been executed together with theoutput node w, i.e., the node w with fw = fv {x ← x }.Algorithm 24 Rename(v, x ← x )if there is an entry (v, w) in the computed table thenreturn welseif v ist terminal thenw := velsew0 := Rename(succ0 (v), x ← x );w1 := Rename(succ1 (v), x ← x );if var(v) = zj for some j ∈ {1, .
. . , n} thenz := zjelsez := var(v)fiw := find or add(z , w1 , w0 );fiinsert (u, w) in the computed table;return wfiRemark 6.79.(* replace zj with zj *)Interleaved Variable Orderings for Transition SystemsWe noticed before (page 409) that interleaved variable orderings, such as (x1 , x1 , . . . , xn , xn ),are favorable for the representation of transition systems. The rename operator yields onereason, as interleaved variable orderings permit use of the renaming that is inherent in theOBDD algorithms for the preimage computation by the above algorithm. Another formalargument for interleaved variable orderings is that they are beneficial for the constructionof the ROBDD representation for the transition relation of a composite transition system.In Remark 6.59 (page 389) we saw that if TS arises from the synchronous product oftransition systems TS1 , . .
. , TSm , then the switching function Δ(x 1 , . . . , x n , x 1 , . . . , x n ) forTS’s transition relation is obtained by the conjunction of the switching functions Δi (x i , x i )for the transition relations in TSi , i = 1, . . . , m. Since the Δi ’s do not have commonvariables the ℘-ROBDD size of Δ is bounded byNΔ NΔ1 + .
. . + NΔm418Computation Tree Logicwhenever ℘ is an interleaved variable ordering where all variables in x i and x i are groupedtogether. Thus, there is no exponential blowup for the ROBDD sizes! Although Lemma6.77 yields the upper bound NΔ1 · . . . · NΔm for any variable ordering, for such interleavedvariable orderings ℘ at most linear growth of the ℘-ROBDD sizes is guaranteed. This is dueto the fact that the ℘-ROBDD for Δ arises by linking the ℘-ROBDDs for Δ1 , . .
. , Δm . E.g.,if we suppose that all variables in x i , x i appear after the variables in x 1 , x 1 , . . . , x i−1 , x i−1in ℘, then we may simply redirect any edge to the 1-drain in the ℘-ROBDD for Δi−1 tothe root of the ℘-ROBDD for Δi (for 1 i < m). This yields the ℘-ROBDD for Δ.A slightly more involved argument applies to the interleaving TS = TS1 ||| . . . ||| TSmwhere Δ arises by the disjunction of the Δi ’s together with the side conditions x j = x jfor i = j.
With an interleaved variable ordering where the variables for TSi appear beforethe variables of TSi+1 , . . . , TSm , we can guarantee that the ℘-ROBDD size NΔ is boundedby O( (NΔ1 + . . . + NΔm ) · n2 ) where the n is the total number of variables in TS. Theadditional factor O(n2 ) stands for the representation of the conditions x i = x i .Existential quantification is reducible to ITE and the cofactor operator, as we have ∃x .f =f |x =0 ∨ f |x =1 . As we mentioned in the explanations for the ITE operator, the cofactoroperator f → f |x =b is trivial if x ℘ z for the first essential variable z of f in thegiven variable ordering ℘, since then f |z =b is represented by the b-successor of the noderepresenting f , if x = z , and f |x =b = f , if x <℘ z or f is constant.
If a representation forf |x =b is required where z <℘ x , then we may use the fact that (f |x =b )|z =c = (f |z =c)|x =band apply the cofactor-operator recursively to the successors of the node representing f .This leads to Algorithm 25 on 419. Here, again, we use a computed table that organizesall pairs (v, w) where the cofactor fv |x =b is known to be represented by node w.The time complexity of the renaming algorithm, as well as the algorithm for obtainingcofactors is bounded by O(size(Bv )) as both rely on a DFS-based traversal of the subOBDD Bv , assuming constant time for accessing the entries in the unique and computedtable. The ℘-ROBDD size of f agrees with the ℘-ROBDD size of f {x ← x } under theassumptions we made for x , x and ℘.
The ℘-ROBDD size of f |x =b is at most the ℘ROBDD size of f . This follows from the fact that given the ℘-ROBDD Bf for f , an℘-ROBDD for f |x =b is obtained by redirecting any edge w → u that leads to an x -nodeu to the b-successor of u and then removing all x -nodes.7 In summary, the preimagecomputation via the relational product∃x .(Δ ∧ f {x ← x })– which is required for, e.g., the symbolic computation of Sat(∃B) – could be performedby first applying the rename operator to f , then the conjunction operator (as an instance ofAlthough this yields a correct operator for constructing the ℘-ROBDD for f |x =b from the ℘-ROBDDfor f , the redirection of edges is not adequate for an implementation with shared OBDDs.7Symbolic CTL Model Checking419Algorithm 25 Cof(v, x , b)if there is an entry (v, w) in the computed table thenreturn welseif v ist terminal thenw := velseif x ℘ var(v) thenw := v|x =belsez := var(v);w1 := Cof(succ1 (v), x , b); w0 := Cof(succ0 (v), x , b);if w0 = w1 then w := w1 else w := find or add(z , w1 , w0 ) fififiinsert (u, w) in the computed table;return node wfiITE operator) to the nodes representing Δ and f (x ), and finally computing the existentialquantifications by cofactors and disjunctions.
This naive approach is very time-consumingas it relies on several top-down traversals in the shared OBDD. It also yields the problemthat the ROBDD representation for Δ ∧ f {x ← x } could be very large.A more elegant approach for a BDD-based preimage computation by means of the relational product ∃x . ( Δ ∧ f {x ← x } ) is to realize the existential quantifications, renamingand conjunction simultaneously by a single DFS traversal of the sub-OBDDs of the nodesrepresenting Δ and f , with intermediate calls of the ITE operator to realize the disjunctions that are inherent in the existential quantification.
Algorithm 26 on page 420summarizes the main steps of this approach.The input of Algorithm 26 are two nodes u and v of a ℘-SOBDD such that fu = Δ(x , x )and fv = f (x ). The assumptions about the variable tuples x , x are as above, i.e.,x = (x1 , . . . , xn ) and x = (x1 , . . . , xn ) are tuples consisting of pairwise distinct variablessuch that the unprimed variables xi and their primed copies xi are neighbours in ℘. Forsimplicity, let us suppose that ℘ interleaves the unprimed and primed variables, sayx1 <℘ x1 <℘ x2 <℘ x2 <℘ .
. . <℘ xn <℘ xn .The output of Algorithm 26 is a (possibly new) node w with fw = ∃x . ( Δ(x , x )∧f (x ) ) =∃x .(fu ∧ fv ). The termination condition of Algorithm 26 is given by the cases: (i) thereexists an entry in the computed table, or (ii) Δ = 0 or f = 0 in which case ∃x .(Δ ∧ f ) = 0,420Computation Tree LogicAlgorithm 26 Relational product RelProd(u, v)if there exists an entry (u, v, w) in the computed table then return w fi;if u or v is the 0-drain then return the 0-drain fi;if u and v are the 1-drain then return the 1-drain fi;y := min{var(u), var(v)}, say y ∈ {xi , xi }if y = xi thenw1,0 := RelProd(u|xi =1,xi =0 , v|xi =0 );w1,1 := RelProd(u|xi =1,xi =1 , v|xi =1 );w1 := ITE(w1,0 , 1, w1,1 );w0,0 := RelProd(u|xi =0,xi =0 , v|xi =0 , x , x );w0,1 := RelProd(u|xi =0,xi =1 , v|xi =1 , x , x );w0 := ITE(w0,0 , 1, w0,1 );if w1 = w0 thenw := w1elsew := find or add(xi , w1 , w0 )fielsew0 := RelProd(u|xi =0 , v); w1 := RelProd(u|xi =1 , v);w := ITE(w0 , 1, w1 )fiinsert (u, v, w) in the computed table;return w(* elimination rule *)Symbolic CTL Model Checking421or (iii) Δ = f = 1 in which case ∃x .(Δ ∧ f ) = 1.
In the remaining cases, the traversal ofthe sub-OBDDs of u and v relies on the expansion rule:∃x1 ∃x2 . . . ∃xn . ( Δ ∧ f {x1 ← x1 , x2 ← x2 , . . . , xn ← xn } ) )|x1 =b= ∃x2 . . . ∃xn . ( Δ|x1 =b,x1 =0 ∧ f |x1 =0 {x2 ← x2 , . . . , xn ← xn } )∨∃x2 . . . ∃xn . ( Δ|x1 =b,x1 =1 ∧ f |x1 =1 {x2 ← x2 , . . . , xn ← xn } )In the literature, several techniques have been proposed that serve to improve the imageor preimage computation. These range from techniques that rely on partitionings of thevariables that attempt to perform the existential quantification as soon as possible (as theydecrease the number of essential variables and often lead to smaller ROBDD sizes). Othertechniques rely on so-called input- or output splitting (which use alternative expansionrules), and special ROBDD operators that attempt to replace, e.g., Δ with other switchingfunctions Δ̃ such that Δ ∧ f = Δ̃ ∧ f and such that the ℘-ROBDD for Δ is smaller thanthe ℘-ROBDD for Δ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
