5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 77
Текст из файла (страница 77)
. ∀zk .f .For example, if f (z , y1 , y2 ) is given by (z ∨ y1 ) ∧ (¬z ∨ y2 ), then∃z .f = f |z =0 ∨ f |z =1 = y1 ∨ y2and ∀z .f = f |z =0 ∧ f |z =1 = y1 ∧ y2 .The rename operator simply replaces certain variables with other ones. E.g., renamingvariable z into y in f (z , x ) = ¬z ∨ x yields the switching function ¬y ∨ x . Formally:Notation 6.55.Rename OperatorLet z = (z1 , . . . , zm ), y = (y1 , . . .
, ym ) be variable tuples of the same length and let x =(x1 , . . . , xk ) be a variable tuple such that none of the variables yi or zi is contained in x . Forthe evaluation s = [y = b] ∈ Eval(y, x ), s{y ← z } denotes the evaluation in Eval(z , x ) thatis obtained by composing the variable renaming function yi → zi , for 1 i m with theevaluation s.
That is, s{y ← z } agrees with s for the variables in x and s{y ← z } assignsthe same value b ∈ {0, 1} to variable zi as s to variable yi . Given a switching functionf : Eval(z , x ) → {0, 1}, then the switching function f {z ← y} : Eval(y, x ) → {0, 1} isgiven byf {z ← y}(s) = f ( s{y ← z } ),i.e., f {z ← y}([y = b, x = c]) = f ([z = b, x = c]). If it is clear from the context whichvariables have to be renamed, then we simply write f (y, x ) rather than f {z ← y}.6.7.2Encoding Transition Systems by Switching FunctionsAfter this excursus on switching functions, we return to the question of a symbolicrepresentation of a transition system TS = (S, →, I, AP, L).
As mentioned above (seepage 382), the action set is irrelevant for our purposes and therefore omitted. For theencoding of the states s ∈ S we use n Boolean variables x1 , . . . , xn and identify anyevaluation [x1 = b1 , . . . , xn = bn ] ∈ Eval(x ) with the unique state s ∈ S such thatenc(s) = (b1 , . . . , bn ).
In the sequel, we suppose S = Eval(x ). Given a subset B ofS, then the characteristic function χB : S → {0, 1} of B assigns 1 to all states s ∈ BSymbolic CTL Model Checking387and 0 to all states s ∈/ B. As we assume S = Eval(x ), the characteristic function is theswitching function given by1if s ∈ BχB : Eval(x ) → {0, 1}, χB (s) =0otherwise.In particular, for any atomic proposition a ∈ AP, the satisfaction set Sat(a) = {s ∈ S |s |= a} can be represented by the switching function fa = χSat(a) for x . This yields asymbolic representation of the labeling function by means of a family (fa )a∈AP of switchingfunctions for x .The symbolic representation of the transition relation → ⊆ S×S relies on the same idea: weidentify → with its characteristic function S × S → {0, 1} where truth-value 1 is assignedto the state pair (s, t) if and only if s → t.
Formally, we deal with the variable tuplex = (x1 , . . . , xn ) to encode the starting state s of a transition and a copy x = (x1 , . . . , xn )of x to encode the target state. That is, for each of the variables xi we introduce a newvariable xi . The original (unprimed) variables xi serve to encode the current state, whilethe primed variables xi are used to encode the next state. Then, we identify the transitionrelation → of TS with the switching function1if s → tΔ : Eval(x , x ) → {0, 1}, Δ(s, t{x ← x }) =0otherwisewhere s and t are elements of the state space S = Eval(x ) and the second argumentt{x ← x } in Δ(s, t{x /x }) is the evaluation for x that assigns the same value (1 or 0) tovariable xi as t assigns to variable xi (cf.
Notation 6.55).Example 6.56.Symbolic Representation of Transition RelationSuppose that TS has two states s0 and s1 and the transitions s0 → s0 , s0 → s1 ands1 → s0 , then we need a single Boolean variable x1 = x for the encoding. Say we identifystate s0 by 0 and state s1 by 1. The transition relation → is represented by the switchingfunction Δ : Eval(x , x ) → {0, 1},Δ = ¬x ∨ ¬x .Let us check why. The satisfying assignments for Δ are [x = 0, x = 0], [x = 0, x = 1] and[x = 1, x = 0]. The first two evaluations (where x = 0 = 0) represent the two outgoingtransitions from state s0 = 0, while [x = 1, x = 0] stands for the transition s1 → s0 .Example 6.57.Symbolic Representation of a RingConsider a transition system TS with states {s0 , .
. . , sk−1 } where k = 2n that are organizedin a ring, i.e., TS has the transitionssi → s(i + 1) mod k388Computation Tree Logicfor 0 i < k. We use the encoding that identifies any state si with the binary encodingof its index i. E.g., if k = 16, then n = 4 and state s1 is identified with 0001, state s10with 1010, and state s15 with 1111. We use the Boolean variables x1 , . . . , xn where xnrepresents the most significant bit (i.e., the evaluation [xn = bn , . . .
, x1 = b1 ] stands forstate 1in bi 2i−1 ). Then, Δ is a function with 2n variables, namely x1 , x2 , . . . , xn andtheir copies x1 , x2 , . . . xn . The values of the switching function Δ(x , x ) are given by ∧(xj ↔ xj )x1 ∧ . . . ∧ xi ∧ ¬xi+1 → x ∧ . . . ∧ xi ∧ xi+11i<n∧ (x1 ∧ .
. . ∧ xn → ¬x1 ∧ . . . ∧ ¬xn ).j<inThe set B = { s2i | 0 i < 2n−1 } is given by the switching function χB (x ) = x1 .Given the switching function Δ and a state s ∈ S = Eval(x ), then the successor setPost(s) = {s ∈ S | s → s } arises from Δ by fixing evaluation s for x .
More precisely, ifs = [x1 = b1 , . . . , xn = bn ], then a switching function χPost(s) for Post(s) is obtained fromΔ by building the cofactor for the variables x1 , . . . , xn and the values b1 , . . . , bn :χPost(s) = Δ|s {x ← x }where Δ|s stands for the iterated cofactor Δ|x1 =b1 ,...,xn =bn . As Δ|s is a switching functionfor {x1 , . . . , xn }, the renaming operator {x ← x } yields a representation of Post(s) by thevariables x1 , . . . , xn .Example 6.58.The successor set Post(s0 ) = { s0 , s1 } for the simple system in Example 6.56 is obtainedsymbolically byΔ|x=0 {x ← x } = (¬x ∨ ¬x )|x=0 {x ← x } = 1,=1which reflects the fact that after identifying state s0 with the evaluation [x = 0] and states1 with [x = 1] the successor set of s0 is Eval(x) = {s0 , s1 }, and its characteristic functionis the constant 1.
For state s1 = [x = 1], a symbolic representation of the successor setPost(s1 ) = {s0 } = {[x = 0]} is obtained byΔ|x=1 {x ← x } = (¬x ∨ ¬x )|x=1 {x ← x } = ¬x=¬xSymbolic CTL Model CheckingRemark 6.59.389Symbolic Composition OperatorsAs we explained in Chapter 2, a crucial aspect for the feasibility of any algorithmic verification technique is the automatic construction of “large” transition systems to be analyzedby means of operators that compose several “small” transition systems TS1 , .
. . , TSmrepresenting the processes to be executed in parallel. Let us suppose that we have appropriate representations for the switching functions Δ1 , . . . , Δm for transition systemsTS1 , . . . , TSm at our disposal. If TS arises by TS1 , . . . , TSm through the synchronousproduct operator of TS, then the transition relation of TS is given byΔi (x i , x i )Δ(x 1 , . . . , x m , x 1 , . .
. , x m ) =1inwhere x i denotes the variable tuple that is used to encode the states in TSi . The justification for the above equation is that each transition s1 , . . . , sm → s1 , . . . , sm ofTS = TS1 ⊗ . . . ⊗ TSm is composed of individual transitions si → si in TSi for each ofthe transition systems TSi . For the other extreme, suppose that TS = TS1 ||| . . .
||| TSmarises by the interleaving operator of the TSi ’s (without any synchronization or communication). Then,! x j = x jΔi (x i , x i ) ∧Δ(x 1 , . . . , x m , x 1 , . . . , x m ) =1in1jmi=j , . . . , xwhere for x j = (x1,j , . . . , xnj ,j ) and x j = (x1,jnj ,j ) notation x j = x j abbreviates1knj ( xk,j ↔ xk,j ). The justification for the above equation for Δ is that each transitionin TS has the forms1 , . . . , si−1 , si , si+1 , . . .
, sm → s1 , . . . , si−1 , si , si+1 , . . . , sm where exactly one transition system makes a move si → si , while the others do not changetheir local state. For the parallel operator H which relies on an interleaving semantics foractions outside H and synchronization over the actions in H, we need a combination ofthe above formulae for Δ.
Here, in fact, we need a refined representation of the transitionrelation in TSi with actions for the transitions by means of a switching function Δi (x i , z , x i )where the variable tuple z serves to encode the action names. In case m = 2, the switchingfunction Δ(x 1 , x 2 , x 1 , x 2 ) for the transition relation in TS = TS1 H TS2 is given by(χH (z ) ∧ Δ1 (x 1 , z , x 1 ) ∧ Δ2 (x 1 , z , x 2 ) ) ∨∃z .( ¬χH (z ) ∧ Δ1 (x 1 , z , x 1 ) ∧ x 2 = x 2( ¬χH (z ) ∧Δ2 (x 2 , z , x 2 )∧ x1 =x 1) ∨).In case TS is the transition system of a program graph or channel system then the Booleanvariables xi serve to encode the locations, the potential values of the variables, and the390Computation Tree Logicchannel contents. The effect of the actions has then to be rewritten in terms of thesevariables.Given the switching function Δ(x , x ) and the characteristic function χB (x ) for some set Bof states, we can now describe the backward BFS-based reachability analysis to computeall states in Pre∗ (B) = {s ∈ S | s |= ∃♦B} on the basis of switching functions.
Initially,we start with the switching function f0 = χB that characterizes the set T0 = B. Then, wesuccessively compute the characteristic functions fj+1 = χTj+1 ofTj+1 = Tj ∪ {s ∈ S | ∃s ∈ S s.t. s ∈ Post(s) ∧ s ∈ Tj }The set of states s where the condition ∃s ∈ S s.t. s ∈ Post(s) and s ∈ Tj holds is givenby the switching function:∃x . ( Δ(x , x ) ∧ fj (x ) ). s ∈ Post(s)s ∈TjRecall that fj (x ) is just a short notation for fj {x ← x }, i.e., arises from fj by renamingthe unprimed variables xi into their primed copies xi for 1 i n. This BFS-basedtechnique can easily be adapted to treat constrained reachability properties ∃(C U B) forsubsets B, C of S, as shown in Algorithm 20 on page 390.Algorithm 20 Symbolic computation of Sat(∃(C U B))f0 (x ) := χB (x );j := 0;repeatfj+1 (x ) := fj+1 (x ) ∨ ( χC (x ) ∧ ∃x .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
