5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 98
Текст из файла (страница 98)
In thefollowing theorem, the problem which asks whether two finite transition systems are traceequivalent is shown to be complete for the complexity class PSPACE. This means thatthe trace equivalence problem belongs to PSPACE, i.e., is solvable by a polynomial spacebounded algorithm, and is PSPACE-hard.Theorem 7.46.Lower Bound on Checking Trace EquivalenceLet TS1 and TS2 be finite transition systems over AP.
Then:(a) The problem whether Tracesfin (TS1 ) = Tracesfin (TS2 ) is PSPACE-complete.(b) The problem whether Traces(TS1 ) = Traces(TS2 ) is PSPACE-complete.Proof: We first prove membership of PSPACE. We prove that problems (a) and (b) arein PSPACE by providing a polynomial reduction from these problems to the equivalenceproblem for nondeterministic finite automata (NFA).
As the latter problem is in PSPACE,the existence of this reduction implies that problems (a) and (b) are in PSPACE. Theequivalence problem for NFA A1 and A2 is whether L(A1 ) = L(A2 ).The main proof idea is to define NFA ATS for transition system TS such that L(ATS ) can beobtained from Traces(TS), and vice versa. For finite transition system TS = (S, Act, →,I, AP, L), let NFA ATS = (Q, Σ, δ, Q0 , F ) be defined as follows:• Q = S ∪ { t } with t ∈/ S (state t identifies terminal states in TS)• Σ = 2AP ∪ { τ } with τ ∈ 2APBisimulation-Quotienting Algorithms• The transition relation δ in ATS is⎧Post(s)⎪⎪⎪⎨{t}δ(s, A) =⎪⎪⎪⎩∅495given byif s ∈ S, Post(s) = ∅ and L(s) = Aif (s ∈ S ∧ Post(s) = ∅ ∧ L(s) = A)∨ (s = t ∧ A = τ )otherwise• Q0 = I• F =QIt now follows that Traces(TS) is the set consisting of all finite, nonempty words A0 A1 .
. . Anwhere A0 A1 . . . An τ ∈ L(ATS ) and all infinite words A0 A1 A2 . . . ∈ (2AP )ω where all prefixes A0 . . . An belong to L(ATS ). Hence, Traces(TS) can be derived from L(ATS ), and viceversa.For finite transition systems TS1 and TS2 we haveTraces(TS1 ) = Traces(TS2 )if and only ifL(ATS1 ) = L(ATS2 ).As the NFA ATS are obtained in polynomial time, this yields a polynomial reduction fromproblem (b) to the equivalence problem for NFA.A polynomial reduction from (a) to the equivalence problem for NFA is obtained byconsidering a similar transformation TS → ATS where ATS agrees with ATS , except that theself-loop at state t is omitted.
State t is thus the only terminal in ATS . Then, Tracesfin (TS)agrees with the set of all nonempty words accepted by ATS , i.e., Tracesfin (TS) = L(ATS ) \{ ε }. Thus:Tracesfin (TS1 ) = Tracesfin (TS2 )if and only ifL(ATS1 ) = L(ATS2 ).It remains to show the PSPACE-hardness. This is shown by a polynomial reductionfrom the language-equivalence problem for NFA, a problem that is PSPACE-complete.PSPACE-hardness of this problem follows from the fact that the (universality) problemwhether L(E) = Σ∗ for regular expression E over Σ is PSPACE-hard; see e.g. [383]. Sincethere are polynomial transformations from regular expressions to NFA and there is a singlestate NFA for Σ∗ , the universality problem is polynomial reducible to the equivalenceproblem for NFA.The main idea is to map an NFA A = (Q, Σ, δ, Q0 , F ) to a finite transition system TSA =(S, { τ }, →, I, AP, L) such that Traces(TSA ) encodes L(A).
As a preprocessing step wedelete all states q in A with δ∗ (q, w) ∩ F = ∅ for any w ∈ Σ∗ , as from these states it isimpossible to reach a final state. TSA is defined as496Equivalences and Abstraction• S = Q0 ∪ (Q × Σ) ∪ { accept } with Q0 ∩ (Q × Σ) = ∅ and accept ∈ Q ∪ (Q × Σ)• → is defined by the following rules:q0 ∈ Q0 ∧ p ∈ δ(q0 , A)τq0 −→p, Aandq ∈ Q ∧ B ∈ Σ ∧ p ∈ δ(q, A)τq, B −→p, Aq∈F ∧ B∈Στq, B −→acceptτaccept −→accept• I = Q0• AP = Σ ∪ { accept } with accept ∈/Σ• L(q0 ) = ∅ for any q0 ∈ Q0 , L(q, A) = { A }, and L(accept) = { accept }It is not difficult to establish that Tracesfin (TSA ) consists of all prefixes of words of theform ∅{ A1 } .
. . { An }{ accept }m with m 0 and A1 . . . An ∈ L(A). L(A) can be derivedfrom Traces(TSA ) as follows:A1 . . . An ∈ L(A)iff∅{ A1 } . . . { An }{ accept } ∈ Tracesfin (TSA )Thus, for NFA A1 and A2 over the alphabet Σ:L(A1 ) = L(A2 )iffTracesfin (TSA1 ) = Tracesfin (TSA2 )iffTraces(TSA1 ) = Traces(TSA2 )The equivalence of finite trace inclusion and trace inclusion follows from Theorem 3.30 onpage 117 as the transition systems TSAi are finite and do not have terminal states. SinceTSA is obtained in time O(|A|) from A, the above yields a polynomial reduction from theequivalence problem for NFA to problems (a) and (b).7.4Simulation RelationsBisimulation relations are equivalences requiring two bisimilar states to exhibit identicalstepwise behavior.
On the contrary, simulation relations are preorders on the state spacerequiring that whenever s , s (s simulates s), state s can mimic all stepwise behaviorSimulation Relations497of s; the reverse, i.e., s , s is not guaranteed, so state s may perform transitions thatcannot be matched by state s. Thus, if s simulates s then every successor of s hasa corresponding, i.e., related successor of s , but the reverse does not necessarily hold.Simulation can be lifted to entire transition systems by comparing (according to ,) theirinitial states.
Simulation relations are often used for verification purposes to show thatone system correctly implements another, more abstract system. One of the interestingaspects of simulation relations is that they allow a verification by “local” reasoning. Thetransitivity of , allows a stepwise verification in which the correctness is establishedvia several intermediate systems.
Simulation relations are therefore used as a basis forabstraction techniques where the rough idea is to replace the model to be verified by asmaller abstract model and to verify the latter instead of the original one.The simulation order , induces an equivalence which is coarser than bisimulation equivalence, and hence yields a better abstraction (i.e., a smaller quotient space), while stillpreserving a wide range of logical formulae in LTL and CTL.
As bisimulation equivalenceis the coarsest equivalence that preserves CTL and CTL∗ , the simulation order , preservesa fragment of these logics. The use of simulation thus relies on the preservation of certainclasses of formulae, not of all formulae. For instance, if s , s , then for any safety property∀ϕ it follows that s |= ∀ϕ implies s |= ∀ϕ, since any path starting in s is mimicked bya similar path that starts in s . The reverse, s |= ∀ϕ, cannot be used to deduce that ∀ϕdoes not hold in the simulated state s; the paths starting in s that violate ϕ might bebehaviors that s cannot perform at all.As for bisimulation relations, the formal definition of the simulation order relies on acoinductive approach which defines the simulation order as the greatest relation satisfyingcertain conditions:Definition 7.47.Simulation OrderLet TSi = (Si , Acti , →i , Ii , AP, Li ), i = 1, 2, be transition systems over AP.
A simulationfor (TS1 , TS2 ) is a binary relation R ⊆ S1 × S2 such that(A) ∀s1 ∈ I1 . (∃s2 ∈ I2 . (s1 , s2 ) ∈ R)(B) for all (s1 , s2 ) ∈ R it holds that:(1) L1 (s1 ) = L2 (s2 )(2) if s1 ∈ Post(s1 ), then there exists s2 ∈ Post(s2 ) with (s1 , s2 ) ∈ R.TS1 is simulated by TS2 (or, equivalently, TS2 simulates TS1 ), denoted TS1 , TS2 , ifthere exists a simulation R for (TS1 , TS2 ).498Equivalences and AbstractionCondition (A) requires that all initial states in TS1 are related to an initial state of TS2 .As the reverse is not required, there might be initial states of TS2 that are not matchedby an initial state of TS1 .
Conditions (B.1) and (B.2) are as for bisimulations; note thatthe symmetric counterpart of (B.2)—as for bisimulation—is not required.Example 7.48.Two Beverage Vending MachinesConsider the transition systems in Figure 7.17. Let AP = { pay, beer, soda } with theobvious labeling functions. The relationR = { (s0 , t0 ), (s1 , t1 ), (s2 , t1 ), (s3 , t2 ), (s4 , t3 ) }is a simulation for (TS1 , TS2 ). Since R contains the pair of initial states (s0 , t0 ), TS1 ,TS2 .
The reverse does not hold, i.e., TS2 , TS1 , since there is no state in TS1 that canmimic state t1 . This is due to the fact that the options “beer” and “soda” are possible instate t1 , but in no state in TS1 .t0 { pay }s0 { pay }∅ s1{ beer } s3t1 ∅s2 ∅s4 { soda }{ beer } t2t3 { soda }Figure 7.17: The vending machine on the right simulates the one on the left.Consider now AP = { pay, drink }, and assume states s3 , s4 , t2 and t3 equals { drink }.Relation R is again a simulation for (TS1 , TS2 ), and thus TS1 , TS2 . Its inverse,R−1 = { (t0 , s0 ), (t1 , s1 ), (t1 , s2 ), (t2 , s3 ), (t3 , s4 ) },is a simulation for (TS2 , TS1 ).
We thus also obtain TS2 , TS1 .The simulation relation , is a preorder, i.e., it is reflexive and transitive. As the conditionsof simulation relations are not symmetric, the simulation preorder is not an equivalence.Simulation RelationsLemma 7.49.499Reflexivity and Transitivity of ,For a fixed set AP of atomic propositions, the relation , is reflexive and transitive.Proof: Similar to the proof of reflexivity and transitivity of ∼; see Lemma 7.4 (page 453).TS1 , TS2 holds if TS1 originates from TS2 by deleting transitions from TS2 , e.g., incase of a nondeterministic choice in TS1 , only one alternative is retained.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
