5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 90
Текст из файла (страница 90)
These results provide us with the tools to simplify establishing TS |= ϕ, for CTL(or CTL∗ ) formula ϕ by checking whether TS |= ϕ.This provides the theoretical underpinning of exploiting bisimulation and simulation relations for the purpose of abstraction. The remaining issue is how to obtain the moreabstract TS from the (larger, and more concrete) transition system TS . This chapter willtreat polynomial-time algorithms for several notions of (bi)simulation. These algorithmsallow checking whether two given transition systems are (bi)similar, and can be used togenerate an abstract transition system from a more concrete one in an automated manner.As in the previous chapters, we will follow the state-based approach. This means thatwe consider branching-time relations that refer to the state labels, i.e., the atomic propositions that hold in the states.
Action labels of the transitions are not considered. Allconcepts (definitions, theorems, algorithms) treated in this chapter can, however, easilybe reformulated for the approach that is focused on action labels rather than state labels.This connection is discussed in Section 7.1.2.Throughout this chapter, the transition systems under consideration may have terminalstates, and hence, may exhibit both finite and infinite paths and traces. When consideringtemporal logics, though, transition systems without terminal states (thus only havinginfinite behaviors) are assumed.Bisimulation7.1451BisimulationBisimulation equivalence aims to identify transition systems with the same branchingstructure, and which thus can simulate each other in a stepwise manner.
Roughly speaking, a transition system TS can simulate transition system TS if every step of TS canbe matched by one (or more) steps in TS . Bisimulation equivalence denotes the possibility of mutual, stepwise simulation. We first introduce bisimulation equivalence as abinary relation between transition systems (over the same set of atomic propositions);later on, bisimulation is also treated as a relation between states of a single transitionsystem. Bisimulation is defined coinductively, i.e., as the largest relation satisfying certainproperties.Definition 7.1.Bisimulation EquivalenceLet TSi = (Si , Acti , →i , Ii , AP, Li ), i = 1, 2, be transition systems over AP. A bisimulationfor (TS1 , TS2 ) is a binary relation R ⊆ S1 × S2 such that(A) ∀s1 ∈ I1 (∃s2 ∈ I2 .
(s1 , s2 ) ∈ R) and ∀s2 ∈ I2 (∃s1 ∈ I1 . (s1 , s2 ) ∈ R)(B) for all (s1 , s2 ) ∈ R it holds:(1) L1 (s1 ) = L2 (s2 )(2) if s1 ∈ Post(s1 ) then there exists s2 ∈ Post(s2 ) with (s1 , s2 ) ∈ R(3) if s2 ∈ Post(s2 ) then there exsist s1 ∈ Post(s1 ) with (s1 , s2 ) ∈ R.TS1 and TS2 are bisimulation-equivalent (bisimilar, for short), denoted TS1 ∼ TS2 , ifthere exists a bisimulation R for (TS1 , TS2 ).Condition (A) asserts that every initial state of TS1 is related to an initial state of TS2 ,and vice versa. According to condition (B.1), the states s1 and s2 are equally labeled.This can be considered as ensuring the “local” equivalence of s1 and s2 . Condition (B.2)states that every outgoing transition of s1 must be matched by an outgoing transition ofs2 ; the reverse is stated by (B.3).
Figure 7.1 summarises the latter two conditions.Example 7.2.Two Beverage Vending MachinesLet AP = { pay, beer, soda }. Consider the transition systems depicted in Figure 7.2.These model a beverage vending machine, but differ in the number of possibilities forsupplying beer. The fact that the right-hand transition system (TS2 ) has an additionaloption to deliver beer is not observable by a user.
This suggests an equivalence between452Equivalences and Abstractions1 R s2↓s1s1 R s2↓s2can be complemented tos1 R s2↓↓s1 R s2can be complemented tos1 R s2↓↓s1 R s2Figure 7.1: Conditions (B.2) and (B.3) of bisimulation equivalence.s0{ pay }s1∅{ beer }t0{ pay }t1∅t2{ beer } s2s3{ soda }{ beer } t3t4{ soda }Figure 7.2: Two bisimilar beverage vending machinesthe transition systems.
Indeed, the equivalence of TS1 and TS2 follows from the fact thatthe relationR = {(s0 , t0 ), (s1 , t1 ), (s2 , t2 ), (s2 , t3 ), (s3 , t4 )}is a bisimulation for (TS1 , TS2 ). It can easily be verified that R indeed satisfies all requirements of Definition 7.1.Now consider an alternative model (TS3 ) of the vending machine where the user selectsthe drink on inserting a coin, see Figure 7.3, depicting TS1 (left) and TS3 (right). APis as before. It follows that TS1 and TS3 are not bisimilar, since the state s1 in TS1cannot be mimicked by a state in TS3 . This can be seen as follows. Due to the labelingcondition (B.1), the only candidates for mimicking state s1 are the states u1 and u2 inTS3 .
However, neither of these states can mimic all transitions of s1 in TS1 : either thepossibility for soda or for beer is missing. Thus, TS1 ∼ TS3 for AP = { pay, beer, soda }.Bisimulation{ beer }453s2s0{ pay }s1∅u0∅s3{ soda }{ beer }u3u1{ pay }u2∅u4 { soda }Figure 7.3: Nonbisimulation-equivalent beverage vending machines.As a final example, reconsider TS1 and TS3 for AP = { pay, drink }. The labelings of thetransition systems are obvious: L(s0 ) = L(u0 ) = { pay }, L(s1 ) = L(u1 ) = L(u2 ) = ∅, andall remaining states are labeled with { drink }. It can now be established that the relation{ (s0 , u0 ), (s1 , u1 ), (s1 , u2 ), (s2 , u3 ), (s2 , u4 ), (s3 , u3 ), (s3 , u4 ) }is a bisimulation for (TS1 , TS3 ).
Henceforth, TS1 ∼ TS3 for AP = { pay, drink }.Remark 7.3.The Relevant Set of Atomic PropositionsThe fixed set AP plays a crucial role in comparing transition systems using bisimulation.Intuitively, AP stands for the set of all “relevant” atomic propositions. All other atomicpropositions are understood as negligible and are ignored in the comparison. In case TS isa refinement of TS , e.g., TS is obtained from TS by incorporating some implementationdetails, then the set AP of atomic propositions of TS generally is a proper superset ofthe set AP of propositions of TS .
To compare TS and TS , the set of common atomicpropositions, AP , is a reasonable choice. In this way, it is possible to check whetherthe branching structure of TS agrees with that of TS when considering all observableinformation in AP . If we are only interested in checking the equivalence of TS and TSwith respect to the satisfaction of a temporal logic formula Φ, it suffices to consider APas the atomic propositions that occur in Φ.Lemma 7.4.Reflexivity, Transitivity, and Symmetry of ∼For a fixed set AP of atomic propositions, the relation ∼ is an equivalence relation.Proof: Let AP be a set of atomic propositions.
We show reflexivity, symmetry, andtransitivity of ∼:454Equivalences and Abstraction• Reflexivity: For transition system TS with state space S, the identity relation R ={ (s, s) | s ∈ S } is a bisimulation for (TS, TS).• Symmetry: Sssume that R is a bisimulation for (TS1 , TS2 ). ConsiderR−1 = {(s2 , s1 ) | (s1 , s2 ) ∈ R}that is obtained by swapping the states in any pair in R.
Clearly, relation R−1satisfies conditions (A) and (B.1). By symmetry of (B.2) and (B.3), we immediatelyconclude that R−1 is a bisimulation for (TS2 , TS1 ).• Transitivity: Let R1,2 and R2,3 be bisimulations for (TS1 , TS2 ) and (TS2 , TS3 ),respectively. The relation R = R1,2 ◦ R2,3 , given byR = {(s1 , s3 ) | ∃s2 ∈ S2 . (s1 , s2 ) ∈ R1,2 ∧ (s2 , s3 ) ∈ R2,3 },is a bisimulation for (TS1 , TS3 ) where S2 denotes the set of states in TS2 . This canbe seen by checking all conditions for a bisimulation.(A) Consider the initial state s1 of TS1 . Since R1,2 is a bisimulation, there is aninitial state s2 of TS2 with (s1 , s2 ) ∈ R1,2 .
As R2,3 is a bisimulation, there isan initial state s3 of TS3 with (s2 , s3 ) ∈ R2,3 . Thus, (s1 , s3 ) ∈ R. In the sameway we can check that for any initial state s3 of TS3 , there is an initial states1 of TS1 with (s1 , s3 ) ∈ R.(B.1) By definition of R, there is a state s2 in TS2 with (s1 , s2 ) ∈ R1,2 and (s2 , s3 ) ∈R2,3 . Then, L1 (s1 ) = L2 (s2 ) = L3 (s3 ).(B.2) Assume (s1 , s3 ) ∈ R.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
