5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 104
Текст из файла (страница 104)
As for the initial algorithmto compute ,TS , we deal with countersδ(s1 , s) = |Post(s) ∩ Sim(s1 )|.Using Algorithm 29 (page 479), the initial simulator sets Sim(s1 ) = {s2 ∈ S | L(s1 ) =L(s2 )} can be obtained in time O(|S| · |AP|). We then compute the sets Remove(s1 ) andthe counters δ(s1 , s) in time O(M ·|S|). In each iteration the counters δ(s1 , s) need tobe updated. This is done as follows. On removing s2 from Sim(s1 ), the list Pre(s2 ) istraversed and we setδ(s1 , s) := δ(s1 , s) − 1for every s ∈ Pre(s1 ).The check Post(s) ∩ Sim(s1 ) = ∅ boils down to δ(s1 , s) = 0 and can be performed inconstant time.
The total costs of the outermost iteration can be estimated as follows. For528Equivalences and Abstractioneach state s2 and each edge s → s2 , the condition ”s2 ∈ Remove(s1 ) ∧ s2 ∈ Sim(s1 )” issatisfied at most once. Therefore, the code fragmentif s2 ∈ Sim(s1 ) thenSim(s1 ) := Sim(s1 ) \ { s2 };for all s ∈ Pre(s2 ) doif Post(s) ∩ Sim(s1 ) = ∅ thenRemove(s1 ) := Remove(s1 ) ∪ { s };fiodficauses the cost:O s ∈S2|Pre(s2 )| ·M1= O(M · |S|),s ∈S 1 |S|where we add up the costs over all iterations for which s2 ∈ Sim(s1 ).
The conditions2 ∈ Remove(s1 ) of the outermost for-loop is fulfilled at most once (see Lemma 7.82).Thus, the total costs for all inner loopsfor all s2 ∈ Remove(s1 ) dofor all s1 ∈ Pre(s2 ) do...ododis bounded by O(M ). Under the assumption that M |S|, we thus obtain:Theorem 7.83.Complexity of Algorithm 36The simulation order , of finite transition system TS = (S, Act, →, I, AP, L) can be computed with Algorithm 36 in time O(M ·|S| + |S|·|AP|).The simulation equivalence -TS and the simulation quotient system TS/ - can be computed with the same complexity.Stutter Linear-Time Relations7.7529Stutter Linear-Time RelationsThe equivalence and preorder relations considered so far require that each outgoing transition of state s is mimicked by an outgoing transition of the related state s .
We nowconsider variants of trace equivalence and bisimulation that relax this requirement. Ratherthan considering all transitions as “visible”, it is allowed to mimic an outgoing transitions by a sequence of transitions starting from s . Such sequences of transitions need to be“invisible”, that is to say, all state changes (except the last state change) in such sequencesshould not change the truth value of the atomic propositions that hold in s . Such statechanges are called stutter steps.
Equivalences and preorders that abstract from these stutter steps, also referred to as internal or nonobservable steps, are called weak. In contrast,trace equivalence, ∼, ,, and - are strong implementation relations as these relationsconsider stutter steps as any other transition. Weak implementation relations are important for system synthesis as well as system analysis. To compare transition systemsthat model a given system at different abstraction levels, it is often too demanding torequire a statewise equivalence.
Instead, an action in a transition system at a high levelof abstraction can be modeled by a sequence of actions in the more concrete transitionsystem. Establishing, e.g., trace equivalence is then simply impossible. This is illustratedby the following example.Example 7.84.Abstraction of Internal MovesConsider the abstract program fragment x := y!, and let TSabs be its underlying transitionsystem. Let TSconc model the concrete program fragmenti := y; z := 1;while i > 1 doz := z ∗ i; i := i − 1;odx := z;that computes the factorial of y iteratively.
Clearly, TSabs and TSconc are not traceequivalent. They, however, are related after abstracting from the iteration (and initialassignments) in the concrete program under the assumption that the iteration (plus initialassignments) does not affect the truth value of atomic propositions. This is guaranteedwhen restricting to atomic propositions that only refer to the values of x and y, and, e.g.,not to the individual program locations.Secondly, by abstracting from internal steps, quotient transition systems are obtained thatmay be significantly smaller than the quotient under the corresponding strong implementation relation.
This is due to the fact that quotienting with respect to a weak relation530Equivalences and Abstractionallows for abstracting from sequences of transitions such that all states on such paths canbe aggregated. Interestingly, though, still a rather rich set of properties is preserved undersuch abstractions.This section is concerned with a weak version of trace inclusion and trace equivalence.Section 7.8 (from page 536 onward) deals with weak versions of bisimulation.7.7.1Stutter Trace EquivalenceInternal steps are transitions that do not affect the state labels of successive states.
Thus,intuitively, an internal step operates on program or control variables that are either notvisible from the outside or viewed to be irrelevant at a certain abstraction level. Suchtransitions are called stutter steps.Definition 7.85.Transition s →L(s) = L(s ).sStutter Stepin transition system TS = (S, Act, →, I, AP, L) is a stutter step ifThe notion of stuttering is lifted to paths as follows.
Two paths are called stutterequivalent if their traces only differ in their stutter steps, i.e., if there is a sequenceA0 A1 A2 . . . of sets of atomic propositions Ai ⊆ AP such that the traces of both paths+ +have the form A+0 A1 A2 . . ..Definition 7.86.Stutter-Equivalence of PathsLet TSi = (Si , Acti , →i , Ii , AP, Li ) be transition systems without terminal states andπi ∈ Paths(TSi ), i = 1, 2. π1 and π2 are stutter-equivalent, denoted π1 π2 , if thereexists an infinite sequence A0 A1 A2 .
. . with Ai ⊆ AP and natural numbers n0 , n1 , n2 , . . .,m0 , m1 , m2 , . . . 1 such thattrace(π1 ) = A0 . . . A0 A1 . . . A1 A2 . . . A2 . . . n0 -times n1 -times n2 -timestrace(π2 ) = A0 . . . A0 A1 . . . A1 A2 . . . A2 . . . m0 -times m1 -times m2 -times2 in TS2 are stutter equivalent, denoted π1 π2 ,Finite path fragments π1 in TS1 and π+APπ1 ) and trace(π2 ) areif there exists a finite sequence A0 . .
. An ∈ (2 ) such that trace(++A...A.contained in the language given by the regular expression A+n0 1Stutter Linear-Time Relations531Note that it is not required that A0 , A1 , A2 , . . . are distinct. The notion of stutter equivalence can be applied to (finite or infinite) path fragments of transition system TS bysetting TS1 = TS2 = TS.Example 7.87.Stutter-Equivalent PathsConsider the transition system TSSem depicted in Figure 7.29 and let AP = { crit1 , crit2 }.n1 , n2 , y=1w1 , n2 , y=1c1 , n2 , y=0n1 , w2 , y=1w1 , w2 , y=1c1 , w2 , y=0n1 , c2 , y=0w1 , c2 , y=0Figure 7.29: Transition system of semaphore-based mutual exclusion algorithm.All infinite paths in TSSem that agree on the first process acquiring access to the criticalsection, and in which the two processes acquire access in a strictly alternating fashion, arestutter-equivalent.
For the case that process P1 is the first to enter the critical section, allsuch paths have a trace of the form∅ . . . ∅ { crit1 } . . . { crit1 } ∅ . . . ∅ { crit2 } . . . { crit2 } ∅ . . . ∅ { crit1 } . . . { crit1 } . . .P1 in csP2 in csP1 in csConsider, for instance, the following two infinite paths in TSSem :π1 = n1 , n2 → w1 , n2 → w1 , w2 → c1 , w2 → n1 , w2 →n1 , c2 → n1 , n2 → w1 , n2 → w1 , w2 → c1 , w2 → . .
.π2 = n1 , n2 → w1 , n2 → c1 , n2 → c1 , w2 → n1 , w2 →w1 , w2 → w1 , c2 → w1 , n2 → c1 , n2 → . . .where for the sake of simplicity, we omitted the value of variable y in each state. Hence,532Equivalences and Abstractionπ1 π2 , since for AP = { crit1 , crit2 }trace(π1 ) = ∅3 { crit1 } ∅ { crit2 } ∅3 { crit1 } . . . andtrace(π2 ) = ∅2 ({ crit1 })2 ∅2 { crit2 } ∅ { crit1 } . . .Figure 7.30 indicates trace(π1 ) and trace(π2 ) and their stutter equivalence.n1 n2 w1 n2 w1 w2 c1 w2 n1 w2 n1 c2 n1 n2 w1 n2 w1 w20/0/0/c10/c20/0/0/n1 n2 w1 n2 c1 n2 c1 w2 n1 w2 w1 w2 w1 c2 w1 n2 c1 n20/0/c1c10/0/c20/c1Figure 7.30: Stutter-equivalent paths in TSSem .Notation 7.88.Stutter Equivalence for Executions and TracesThe notion of stutter equivalence can be adapted to execution fragments and words over2AP in the obvious way. Two execution fragments ρ1 and ρ2 of TS1 and TS2 are stutterequivalent, denoted ρ1 ρ2 , if the induced path fragments are stutter-equivalent.
Accordingly, traces σ1 and σ2 over 2AP are stutter-equivalent, denoted σ1 σ2 , if they are both+ +of the form A+0 A1 A2 . . . for A0 , A1 , A2 , . . . ⊆ AP.Transition systems TS1 and TS2 are stutter-equivalent whenever each trace of TS1 can bemimicked by a stutter equivalent trace in TS2 , and vice versa.Definition 7.89.Stutter Equivalence of Transition SystemsTransition systems TSi over AP, i=1, 2, are stutter trace equivalent, denoted TS1 TS2 ,if TS1 TS2 and TS2 TS1 , where is defined by:TS1 TS2iff∀σ1 ∈ Traces(TS1 )∃σ2 ∈ Traces(TS2 ).
σ1 σ2 .Evidently, it follows that Traces(TS1 ) ⊆ Traces(TS)2 implies TS1 TS2 .Stutter Linear-Time RelationsExample 7.90.533Stutter Trace InclusionConsider the transition systems TS1 (left), TS2 (middle) and TS3 (right) in Figure 7.31.It follows:Traces(TS1 ) = { (a∅)ω , (a∅)∗ aω }Traces(TS2 ) = { (a+ ∅)ω , (a+ ∅)∗ aω }Traces(TS3 ) = { aω , a+ (∅a)ω }.We have TS1 TS2 since Traces(TS1 ) ⊆ Traces(TS2 ), and TS2 TS1 as trace (a+ ∅)ωis stutter-equivalent to (a∅)ω and trace (a+ ∅)∗ aω is stutter-equivalent to (a∅)∗ aω . Accordingly,TS1 TS2 .Note that Traces(TS2 ) ⊆ Traces(TS1 ), as e.g., a2 ∅ . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
