5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 79
Текст из файла (страница 79)
If ℘ = (z1 , . . . , zm ), then for each inner node v: if var(v) = zi andw ∈ {succ0 (v), succ1 (v)} ∩ VI , then var(w) = zj for some j > i. Furthermore, it is requiredthat each node v ∈ V \ {v0 } has at least one predecessor, i.e., v = succb (w) for some w ∈ Vand b ∈ {0, 1}.The underlying digraph of a ℘-OBDD is obtained by using V as node set and establishing an edge from node v to w if and only if w is an successor of v, i.e., if w ∈{succ0 (v), succ1 (v)}. The last condition in Definition 6.63, which states that each nodeof an OBDD, except for the root, has a predecessor, is equivalent to the condition thatall nodes of an OBDD are reachable from the root.
The size of an OBDD B, denotedsize(B), is the number of nodes in B.396Computation Tree LogicAn equivalent formulation for the order consistency of B (i.e., the condition stating thatthe variable of an inner node appears in ℘ before the variables of its successors, providedthey are inner nodes) is the requirement that for each path v0 v1 . . . vn in (the underlyinggraph of) B we have vi ∈ VI for 1 i < n andvar(v0 ) <℘ var(v1 ) <℘ . . . <℘ var(vn ),where for the drains we put var(v) = ⊥ (undefined) and extend <℘ by z <℘ ⊥ for allvariables z ∈ Var.
That is, we regard <℘ as a total order on Var ∪ {⊥} and considerthe variable labeling function as a function var : V → Var ∪ {⊥}. This yields that theunderlying graph of an OBDD is acyclic. In particular, v = succb (v) for all inner nodes vand b ∈ {0, 1}.Examples of OBDDs are the binary decision trees and graphs shown in Figures 6.20, 6.21,and 6.22. All these OBDDs rely on the variable ordering ℘ = (z1 , z2 , z3 ).In the sequel, we often refer to an inner node v with var(v) = z as a z -node.
As the picturesfor OBDDs suggest, we may think of the node set V of an OBDD to be partitioned intolevels. Dealing with the ordering ℘ = (z1 , . . . , zm ), then the zi -nodes constitute the nodesat level i. The drains yields the bottom level, while the top level consists of the root node.Definition 6.64.Semantics of OBDDsLet B be an ℘-OBDD as in Definition 6.63. The semantics B is the switching function fBfor Var where fB([z1 = b1 , . . . , zm = bm ]) is the value of the drain that will be reached whentraversing the graph starting in the root v0 and branching according to the evaluation[z1 = b1 , .
. . , zm = bm ]. That is, if the current node v is a zi -node, then the traversalcontinues with the bi -successor of v.Definition 6.65.Sub-OBDD, Switching Function for the NodesLet B be a ℘-OBDD. If v is a node in B, then the sub-OBDD induced by v, denotedBv arises from B by declaring v as the root node and removing all nodes that are notreachable from v. The switching function for node, denoted fv , is the switching functionfor Var that is given by the sub-OBDD Bv .Clearly, at most the variables x with var(v) ℘ x can be essential for fv , since none of thevariables z with z <℘ var(v) appear in the sub-OBDD.
Hence, fv could also be viewedas a switching function for the whole variable set Var or as a switching function for thevariables x with var(v) ℘ x , but this is irrelevant here. In particular, if v is a z -node,then the order condition z = var(v) <℘ var(succb (v)) yields that fsuccb (v) |z =c = fsuccb (v) ,Symbolic CTL Model Checking397since variable z is not essential for fsuccb (v) . But then:fv |z =0 = (¬z ∧ fsucc0 (v) )|z =0 ∨ (z ∧ fsucc1 (v) )|z =0=0= fsucc0 (v) |z =0 = fsucc0 (v)and, similarly, fv |z =1 = fsucc1 (v) . Thus, the Shannon expansion yields the followingbottom-up characterization of the functions fv :Lemma 6.66.Bottom-up Characterization of the Functions fvLet B be a ℘-OBDD.
The switching functions fv for the nodes v ∈ V are given as follows:• If v is a drain, then fv is the constant switching function with value val(v).• If v is a z -node, then fv = (¬z ∧ fsucc0 (v) ) ∧ (z ∧ fsucc1 (v) ).Furthermore, fB = fv0 for the root v0 of B.This yields that fv = fB|z1 =b1 ,...,zi =bi where [z1 = b1 , . . . , zi = bi ] is an evaluation whichleads from the root v0 of B to node v. In fact, all concepts of OBDD-based approachesrely on the decomposition of switching functions into their cofactors. However, only thecofactors are relevant that arise from f by assigning values to the first i variables of ℘ forsome i.Notation 6.67.℘-Consistent CofactorLet f be a switching function for Var and ℘ = (z1 , .
. . , zm ) a variable ordering for Var.A switching function f for Var is called a ℘-consistent cofactor of f if there exists somei ∈ {0, 1, . . . , m} such that f = f |z1 =b1 ,...,zi =bi . (Including the case i = 0 means that weregard f as a cofactor of itself.)For instance, if f = z1 ∧ (z2 ∨ ¬z3 ) and ℘ = (z1 , z2 , z3 ), then the ℘-consistent cofactors off are the switching functions f , f |z1 =1 = z2 ∨ ¬z3 , f |z1 =1,z2 =0 = ¬z3 and the constants0 and 1. The cofactors f |z3 =0 = z1 and f |z2 =0 = z1 ∧ ¬z3 are not ℘-consistent. Sinceit is possible that some cofactors of f arise by several evaluations, it is possible thatcofactors f |zi1 =b1 ,...,zik =bk are ℘-consistent for the variable ordering ℘ = (z1 , .
. . , zm ), evenif (zi1 , . . . , zik ) is not a permutation of (z1 , . . . , zk ). For example, for f = z1 ∧ (z2 ∨ ¬z3 )and ℘ = (z1 , z2 , z3 ) the cofactor f |z2 =0,z3 =1 is ℘-consistent as it agrees with the cofactorsfz1 =0 or f |z1 =1,z2 =0,z3 =1 . (They all agree with the constant function 0.)398Computation Tree LogicThe observation made above can now be rephrased as follows:Lemma 6.68.Nodes in OBDDs and ℘-Consistent CofactorsFor each node v of an ℘-OBDD B, the switching function fv is a ℘-consistent cofactor offB. Vice versa, for each ℘-consistent cofactor f of fB there is at least one node v in Bsuch that fv = f .However, given a ℘-OBDD B and a ℘-consistent cofactor f of fB there could be morethan one node in B representing f .
This, for instance, applies to the binary decision treeshown in Figure 6.20 on page 385, viewed as ℘-OBDD for ℘ = (z1 , z2 , z3 ), where we havefB = z1 ∧ (¬z2 ∨ z3 ) and the ℘-consistent cofactors represented by the nodes in the leftsubtree of the root agree as we havef |z1 =0 = f |z1 =0,z2 =b = f |z1 =0,z2 =b,z3 =c = 0for all b, c ∈ {0, 1}. For the ℘-OBDD shown on the left of Figure 6.21 on page 393, allinner nodes represent different switching functions.
However, the two drains with value0 represent the same cofactors of fB. The same holds for the two drains with value 1.However, in the ℘-OBDD shown on the right of Figure 6.21, every ℘-conistent cofactoris represented by a single node. In this sense, this ℘-OBDD is free of redundancies, andtherefore called reduced:Definition 6.69.Reduced OBDDLet B be a ℘-OBDD. B is called reduced if for every pair (v, w) of nodes in B: v = wimplies fv = fw . Let ℘-ROBDD denote a reduced ℘-OBDD.Thus, in reduced ℘-OBDDs any ℘-consistent cofactor is represented by exactly one node.This is the key property to prove that reduced OBDDs yield a universal and canonicaldata structure for switching functions. Universality means that any switching functioncan be represented by an OBDD.
Canonicity means that any two ℘-OBDDs for the samefunction agree up to isomorphism, i.e., renaming of the nodes.Theorem 6.70.Universality and Canonicity of ROBDDsLet Var be a finite set of Boolean variables and ℘ a variable ordering for Var. Then:(a) For each switching function f for Var there exists a ℘-ROBDD B with fB = f .(b) Given two ℘-ROBDDs B and C with fB = fC, then B and C are isomorphic, i.e.,agree up to renaming of the nodes.Symbolic CTL Model Checking399Proof: ad (a).
Clearly, the constant functions 0 and 1 can be represented by a ℘-ROBDDconsisting of a single drain. Given a nonconstant switching function f for Var and avariable ordering ℘ for Var, we construct a reduced ℘-OBDD B for f as follows. Let Vbe the set of ℘-consistent cofactors of f . The root of B is f . The constant cofactors are/ {0, 1}, letthe drains with the obvious values. For f ∈ V , f ∈var(f ) = min{ z ∈ Var | z is essential for f }be the first essential variable where the minimum is taken according to the total order <℘induced by ℘. (We use here the trivial fact that any nonconstant switching function hasat least one essential variable.) The successor functions are given bysucc0 (f ) = f |z =0 , succ1 (f ) = f |z =1where z = var(f ).
The definition of var(·) yields that B is a ℘-OBDD. By the Shannonexpansion we get that the semantics of f ∈ V (i.e., the switching function of f as a nodeof B) is f . In particular, this yields that fB = f (the function for the root f ) and thereducedness of B (as any two nodes represent different cofactors of f ).To prove the statement in (b), it suffices to show that any reduced ℘-OBDD C with fC = fis isomorphic to the ℘-ROBDD B constructed above.
Let V C be the node set of C, v0CCthe root of C, varC the variable labeling function, and succC0 , succ1 the successor functionsin C. Let function ı : V C → V be given by ı(v) = fv . (Recall that the functions fv are℘-consistent cofactors of fC = f . This ensures that fv ∈ V .) Since C is reduced, ı is abijection.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
