5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 105

∈ Traces(TS2 ) but is not a trace ofTS1 . It follows thatTS1 TS3 and TS2 TS3 ,as TS1 and TS2 have traces of the form (a+ ∅)+ aω whereas there is no trace in TS3 thatcontains ∅ and ends with aω . Since Traces(TS3 ) ⊆ Traces(TS2 ), it follows TS3 TS2 .TS3 TS1 since aω is a trace of both transition systems, and a+ (∅a)ω of TS3 is stutterequivalent to (a∅)ω .s1 { a }u0 { a }t0 { a }s0 { a }u1 ∅t1 ∅s2 ∅u2 { a }Figure 7.31: Three transition systems.5347.7.2Equivalences and AbstractionStutter Trace and LTL\ EquivalenceIn analogy to the result stating that trace equivalence is finer than LTL equivalence, we nowconsider the fragment of LTL that is preserved by stutter trace equivalence. To that end,we first determine the properties that are preserved by stutter-equivalent paths and wordsover 2AP , respectively.

Let us discuss why a restriction to logics without the next operatoris necessary. Consider, e.g., the traces σ1 = A B B B . . . and σ2 = A A A B B B B . . . withA, B ⊆ AP and A = B. Clearly,σ1 σ2but σ1 |= band σ2 |= b for b ∈ B \ A.Stated in words: stutter equivalence does not preserve the truth value of formulae withthe next operator.

In fact, it turns out that this is the only modal operator that is notpreserved.Notation 7.91.LTL without Next StepLTL\ denotes the class of LTL formulae without the next step operator .Theorem 7.92.For σ1 , σ2 ∈Stutter Equivalence and LTL\ Equivalence(2AP )ω :σ1 σ2 ⇒ (σ1 |= ϕ if and only if σ2 |= ϕ)for any LTL\ formula ϕ over AP.Proof: The proof is by structural induction over the formula ϕ. Let A0 A1 A2 .

. . be aninfinite word over 2AP andσ1 = An0 0 An1 1 An2 2 . . .andm1 m20σ2 = Am0 A1 A2 . . .where n0 , n1 , n2 , . . . and m0 , m1 , m2 , . . . are positive natural numbers. Hence: σ1 σ2 .Basis: For ϕ = true the proposition is clear. For ϕ = a ∈ AP, we haveσ1 |= aiffa ∈ A0iffσ2 |= a.Induction step: For ϕ = ϕ1 ∧ ϕ2 or ϕ = ¬ϕ , the claim follows immediately from theinduction hypothesis applied to ϕ1 and ϕ2 or ϕ , respectively.

The remaining case isϕ = ϕ1 U ϕ2 . Assume σ1 |= ϕ. From the semantics of LTL\ , it follows that there existsa natural number j such thatStutter Linear-Time Relationsσ1 [j..] |= ϕ2535andσ1 [i..] |= ϕ1 for all 0 i < j.Recall that for σ = B0 B1 B2 . . . and h 0, the suffix Bh Bh+1 . . .

of σ is denoted by σ[h..].Let r 0 be such thatn0 + . . . + nr−1 < j n0 + . . . + nr−1 + nr .Stated in words, r is the index of the A-block in σ1 that contains σ1 [j]. Then, σ1 [j..] isnr−1 nobtained from σ1 by eliminating the prefix An0 0 . . . Ar−1Ar where n = n0 + . . . + nr−1 +++nr − j. Note that 0 n < nr . Thus, σ1 [j..] is of the form A+r Ar+1 Ar+2 .

. .. Since σ1 σ2 ,it follows that for:k = m0 + . . . + mr−1 + 1,++σ2 [k..] is of the form A+r Ar+1 Ar+2 . . .. More precisely, we have++1. σ1 [j..] σ2 [k..] since both words are of the form A+r Ar+1 Ar+2 . . ., and2. for all 0 h < k, there is an index 0 i < j such that σ1 [i..] σ2 [h..].As σ1 [j..] |= ϕ2 and σ1 [i..] |= ϕ1 , for all i < j, applying the induction hypothesis yieldsσ2 [k..] |= ϕ2 and σ2 [h..] |= ϕ1 , for h < k.

Hence, σ2 |= ϕ1 U ϕ2 .By symmetry, we get the equivalence of σ1 and σ2 for LTL\ .Corollary 7.93.Stutter Trace Relations and LTL\For transition systems TS1 , TS2 (over AP) without terminal states:(a) TS1 TS2 implies TS1 ≡LTL\ TS2 .(b) if TS1 TS2 , then for any LTL\ formula ϕ: TS2 |= ϕ implies TS1 |= ϕ.A slightly more general preservation result can be established for stutter trace equivalenceand inclusion.Definition 7.94.Stutter-Insensitive LT propertyLT property P is stutter-insensitive if [σ] ⊆ P , for any σ ∈ P .536Equivalences and AbstractionStated in words, P is stutter-insensitive if it is closed under stutter equivalence, i.e., forany σ ∈ P all stutter-equivalent words are also contained in P .

It follows immediatelythat stutter trace equivalent transition systems satisfy the same stutter-insensitive LTproperties. Moreover, for any stutter-insensitive LT property P :TS1 TS2 and TS2 |= PimpliesTS1 |= P.This is, in fact, a more general statement than Corollary 7.93 since for any LTL\ formulaϕ the induced LT property Words(ϕ) is stutter-insensitive. On the other hand, thereexist stutter-insensitive LT properties that cannot be expressed in LTL\ . For instance,consider the set P of words over { a, b } that contain an odd number of occurrences ofthe subword a b. The LT property that is stutter-insensitive and contains P , cannot beexpressed in LTL\ .

However, if ϕ is an LTL formula such that Words(ϕ) is stutterinsensitive, then ϕ is equivalent to some LTL\ formula ψ; see Exercise 7.20.7.8Stutter BisimulationThis section is concerned with stutter bisimulation. Stutter bisimulation is defined in acoinductive manner, as bisimulation. Whereas bisimulation requires for equivalent statess1 and s2 that each transition s1 → t1 (with s1 inequivalent to t1 ) is matched by sometransition s2 → t2 , stutter bisimulation allows s1 → t1 to be matched by a path fragments2 u1 u2 . . .

un t2 (for n 0) such that t1 and t2 are equivalent, and ui is equivalent to s2 .That is, single transitions may be matched by (suitable) path fragments.The following definition considers the notion of a stutter bisimulation for a single transitionsystem. Later on, this notion will be adapted for pairs of transition systems.Definition 7.95.Stutter BisimulationLet TS = (S, Act, →, I, AP, L) be a transition system. A stutter bisimulation for TS isa binary relation R on S such that for all (s1 , s2 ) ∈ R:1.

L(s1 ) = L(s2 ).2. If s1 ∈ Post(s1 ) with (s1 , s2 ) ∈ R, then there exists a finite path fragment s2 u1 . . . un s2with n 0 and (s1 , ui ) ∈ R, i = 1, . . . , n and (s1 , s2 ) ∈ R.3. If s2 ∈ Post(s2 ) with (s1 , s2 ) ∈ R, then there exists a finite path fragment s1 v1 . . . vn s1with n 0 and (vi , s2 ) ∈ R, i = 1, . . . , n and (s1 , s2 ) ∈ R.Stutter Bisimulation537s1 , s2 are stutter bisimulation equivalent (stutter-bisimilar, for short), denoted s1 ≈TS s2 ,if there exists a stutter bisimulation R for TS with (s1 , s2 ) ∈ R.Condition (1) is standard, and requires equivalent states to be equally labeled. Accordingto condition (2), every outgoing transition s1 → t1 (where s1 is not equivalent to t1 ) mustbe matched by a path fragment that leads from s2 to t2 such that t1 and t2 are equivalent,and all intermediate states in the path fragment are equivalent to s2 .

Roughly speaking,if s1 changes its equivalence class and moves to t1 , this must be mimicked by s2 , but onlyafter some transitions that are internal to the equivalence class of s2 . Condition (3) is thesymmetric counterpart of condition (2).Lemma 7.96.Coarsest Stutter BisimulationFor transition system TS with state space S:1. ≈TS is an equivalence relation on S.2. ≈TS is a stutter bisimulation for TS.3.

≈TS is the coarsest stutter bisimulation for TS and coincides with the union of allstutter bisimulations for TS.Proof: Similar to the case for bisimulation; see Exercise 7.26.(Note that ≈TS is an equivalence, but this does not hold for any stutter bisimulationrelation.) Since ≈TS is a stutter bisimulation, condition (2) of Definition 7.95 can berephrased by means of ≈TS , as illustrated in Figure 7.32.Example 7.97.Stutter Bisimulation in Semaphore-Based Mutual ExclusionConsider the semaphore-based solution to the mutual exclusion problem; see the transitionsystem TSSem in Figure 5.5 (page 239). Let AP = { crit1 , crit2 }.

Relation R that inducesthe following partitioning of the state space is a stutter bisimulation:{ { n1 , n2 , n1 , w2 , w1 , n2 , w1 , w2 }, { c1 , n2 , c1 , w2 }, { c2 , n1 , w1 , c2 } } .This can be checked by verifying the conditions in<b>Текст обрезан, так как является слишком большим</b>.