5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 76
Текст из файла (страница 76)
The remainder of this section is concerned with explanations on this approach.Section 6.7.1 summarizes our notations for switching functions and operations on them.The encoding of transition systems by switching functions and a corresponding reformulation of the CTL model-checking algorithm will be presented in Section 6.7.2. The mainconcepts of (ordered) binary decision diagrams are summarized in Section 6.7.3.6.7.1Switching FunctionsFor technical reasons, it is more appropriate to consider switching functions as mappingsfrom evaluations for certain Boolean variables to the values 0 or 1 rather than functions{0, 1}n → {0, 1}.
This permits simpler definitions of composition operators as we justhave to identify the common variables, rather than refer to common arguments via theirpositions in bit tuples. Furthermore, the reference of the arguments of a switching functionby means of variable names is also central for binary decision diagrams.Let z1 . . . , zm be Boolean variables and Var = {z1 , . . .
, zm }. Let Eval(z1 , . . . , zm ) denotethe set of evaluations for z1 , . . . , zm , i.e., functions η : Var → {0, 1}. Evaluations arewritten as [z1 = b1 , . . . , zm = bm ]. We often use tuple-notations such as z for the variabletuple (z1 , . . . , zm ), b for a bit tuple (b1 , . . . , bm ) ∈ {0, 1}m , and [z = b] as a shorthand forthe evaluation [z1 = b1 , . . . , zm = bm ].Symbolic CTL Model CheckingNotation 6.49.383Switching FunctionA switching function for Var = {z1 , . . . , zm } is a function f : Eval(Var) → {0, 1}.
Thespecial case m = 0 (i.e., Var = ∅) is allowed. The switching functions for the emptyvariable set are just constants 0 or 1.To indicate the underlying set of variables of a switching function we often write f (z ) orf (z1 , . . . , zm ) rather than f . When an enumeration of the variables in Var is clear fromthe context, say z1 , . . . , zm , then we often simply write f (b1 , . . .
, bm ) or f (b) instead off ([z1 = b1 , . . . , zm = bm ]) (or f ([z = b])).Disjunction, conjunction, negation and other Boolean connectives are defined for switchingfunctions in the obvious way. For example, if f1 is a switching function for {z1 , .
. . , zn , . . . zm }and f2 a switching function for {zn , . . . zm , . . . , zk }, where the zi ’s are supposed to be pairwise distinct and 0 n m k, then f1 ∨ f2 is a switching function for {z1 , . . . , zk } andthe values of f1 ∨ f2 are given by(f1 ∨ f2 )([z1 = b1 , . . .
, zk = bk ])= max{ f1 ([z1 = b1 , . . . , zm = bm ]), f2 ([zn = bn , . . . , zk = bk ]) }.We often simply write zi for the projection function przi : Eval(z ) → {0, 1}, przi ([z = b]) =bi and 0 or 1 for the constant switching functions. With these notations, switching functions can be represented by Boolean connections of the variables zi (viewed as projectionfunctions) and constants. For instance, z1 ∨ (z2 ∧ ¬z3 ) stands for a switching function.Notation 6.50.Cofactor and Essential VariableLet f : Eval(z , y1 , . . . , ym ) → {0, 1} be a switching function. The positive cofactor of f forvariable z is the switching function f |z =1 : Eval(z , y1 , .
. . , ym ) → {0, 1} given byf |z =1 (c, b1 , . . . , bm ) = f (1, b1 , . . . , bm )where the bit tuple (c, b1 , . . . , bm ) ∈ {0, 1}m+1 is short for the evaluation [z = c, y1 =b1 , . . . , ym = bm ]. Similarly, the negative cofactor of f for variable z is the switching function f |z =0 : Eval(z , y1 , . . . , ym ) → {0, 1} given by f |z =0 (c, b1 , . . . , bm ) = f (0, b1 , . . . , bm ).If f is a switching function for {z1 , . .
. , zk , y1 , . . . , ym }, then we write f |z1 =b1 ,...,zk =bk forthe iterated cofactor, also simply called cofactor of f , given byf |z1 =b1 ,...,zk =bk = (. . . (f |z1 =b1 )|z2 =b2 . . .)|zk =bk .Variable z is called essential for f if f |z =0 = f |z =1 .The values of f |z1 =b1 ,...,zk =bk for f = f (z1 , . . . , zk , y1 , . . . , ym ) are given byf |z1 =b1 ,...,zk =bk (c1 , . . . , ck , a1 , . .
. , am ) = f (b1 , . . . , bk , a1 , . . . , am )384Computation Tree Logicwhere (c1 , . . . , ck , a1 , . . . , am ) is identified with the evaluation [z1 = c1 , . . . , zk = ck , y1 =a1 , . . . , ym = am ]. As a consequence, the definition of (iterated) cofactors does not dependon the order in which the cofactors for single variables are considered, i.e.:f |z1 =b1 ,...,zk =bk = (. . . (f |zi1 =bi1 )|zi2 =bi2 . . .)|zik =bikfor each permutation (i1 , . . . , ik ) of (1, .
. . , k).Obviously, variable z is not essential for the cofactors f |z =0 and f |z =1 . Thus, at most thevariables in Var\{z1 , . . . , zk } are essential for f |z1 =b1 ,...,zk =bk , provided that f is a switchingfunction for Var.Example 6.51.Cofactors and Essential VariablesConsider the switching function f (z1 , z2 , z3 ) given by (z1 ∨ ¬z2 ) ∧ z3 . Then, f |z1 =1 = z3and f |z1 =0 = ¬z2 ∧ z3 . In particular, variable z1 is essential for f .When we fix the variable set {z1 , z2 , z3 }, then variables z2 and z3 are not essential for theprojection function prz1 = z1 .
In fact, we have z1 |z2 =0 = z1 |z2 =1 = z1 . On the other hand,z1 is essential for the projection function z1 as we have z1 |z1 =1 = 1 = 0 = z1 |z1 =0 .For another example, variables z1 and z2 are essential for f (z1 , z2 , z3 ) = z1 ∨ ¬z2 ∨ (z1 ∧ z2 ∧¬z3 ), while variable z3 is not, as f |z3 =1 = z1 ∨ ¬z2 agrees with f |z3 =0 = z1 ∨ ¬z2 ∨ (z1 ∧ z2 ).The following lemma yields a decomposition of f into its cofactors. This simple observationrelies on the fact that for any evaluation where z is assigned to 0 the value of f (z , y) agreeswith the value of f |z =0 under the same evaluation for y. And similarly, f ([z = 1, y = b]) =f |z =1 ([y = b]).Lemma 6.52.Shannon ExpansionIf f is a switching function for Var , then for each variable z ∈ Var:f = (¬z ∧ f |z =0 ) ∨ (z ∧ f |z =1 ).A simple consequence of the Shannon expansion is that z is not essential for f if and onlyif f = f |z =0 = f |z =1 .Symbolic CTL Model Checking385z1z2z2z31z301z310z3000Figure 6.20: Binary decision tree for z1 ∧ (¬z2 ∨ z3 ).Remark 6.53.Binary Decision TreesThe Shannon expansion is inherent in the representation of switching functions by binarydecision trees.
Given a switching function f for some variable set Var, one first fixes anarbitrary enumeration z1 , . . . , zm for the variables in Var and then represents f by a binarytree of height m such that the two outgoing edges of the inner nodes at level i stand forthe cases zi = 0 (depicted by a dashed line) and zi = 1 (depicted by a solid line). Thus, thepaths from the root to a leaf in that tree represent the evaluations and the correspondingvalue. The leaves stand for the function values 0 or 1 of f . That is, given the evaluations = [z1 = b1 , .
. . , zm = bm ], then f (s) is the value of the terminal node that is reachedby traversing the tree from the root using the branch zi = bi for the node at level i. Thesubtree of node v of the binary decision tree for f and the variable ordering z1 , . . . , zmyields a representation of the iterated cofactor f |z1 =b1 ,...,zi−1 =bi−1 (viewed as a switchingfunction for {zi , . . . , zm }) where z1 = b1 , . .
., zi−1 = bi−1 is the sequence of decisions madealong the path from the root to node v.An example of a binary decision tree for f (z1 , z2 , z3 ) = z1 ∧ (¬z2 ∨ z3 ) is given in Figure6.20. We use dashed lines for the edges from an inner node for variable z representing thecase z = 0 and solid edges for the case z = 1.Further operators on switching functions that will be needed later are existential quantification over variables and renaming of variables.Notation 6.54.Existential and Universal QuantificationLet f be a switching function for Var and z ∈ Var.
Then, ∃z .f is the switching functiongiven by:∃z .f = f |z =0 ∨ f |z =1 .386Computation Tree LogicIf z = (z1 , . . . , zk ) and zi ∈ Var for 1 i k, then ∃z .f is a short-form notation for∃z1 .∃z2 . . . . ∃zk .f . Similarly, universal quantification is defined by∀z .f = f |z =0 ∧ f |z =1and ∀z .f = ∀z1 .∀z2 . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
