5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 27
Текст из файла (страница 27)
Hence, (b) yieldsTS |= Psafe , i.e.,Traces(TS) ⊆ closure(Traces(TS )).From this, we may deriveTracesfin (TS) =⊆==pref(Traces(TS))pref(closure(Traces(TS ))pref(Traces(TS ))Tracesfin (TS ).Here we use the property that for any P it holds that pref(closure(P )) = pref(P ) (seeExercise 3.10, page 147).Safety Properties and Invariants117Theorem 3.28 is of relevance for the gradual design of concurrent systems. If a preliminarydesign (i.e., a transition system) TS is refined to a design TS such thatTraces(TS) ⊆ Traces(TS ),then the LT properties of TS cannot be carried over to TS.
However, if the finite tracesof TS are finite traces of TS (which is a weaker requirement than full trace inclusion ofTS and TS ), i.e.,Tracesfin (TS) ⊆ Tracesfin (TS ),then all safety properties that have been established for TS also hold for TS. Otherrequirements for TS, i.e., LT properties that fall outside the scope of safety properties,need to be checked using different techniques.Corollary 3.29.Finite Trace Equivalence and Safety PropertiesLet TS and TS be transition systems without terminal states and with the same set APof atomic propositions. Then, the following statements are equivalent:(a) Tracesfin (TS) = Tracesfin (TS ),(b) For any safety property Psafe over AP: TS |= Psafe ⇐⇒ TS |= Psafe .A few remarks on the difference between finite trace inclusion and trace inclusion are inorder.
Since we assume transition systems without terminal states, there is only a slightdifference between trace inclusion and finite trace inclusion. For finite transition systemsTS and TS without terminal states, trace inclusion and finite trace inclusion coincide.This can be derived from the following theorem.Theorem 3.30.Relating Finite Trace and Trace InclusionLet TS and TS be transition systems with the same set AP of atomic propositions suchthat TS has no terminal states and TS is finite. Then:Traces(TS) ⊆ Traces(TS ) ⇐⇒ Tracesfin (TS) ⊆ Tracesfin (TS ).Proof: The implication from left to right follows from the monotonicity of pref(·) and thefact that Tracesfin (TS) = pref(Traces(TS)) for any transition system TS.It remains to consider the proof for the implication ⇐=. Let us assume that Tracesfin (TS) ⊆Tracesfin (TS ).
As TS has no terminal states, all traces of TS are infinite. Let A0 A1 . . . ∈118Linear-Time PropertiesTraces(TS). To prove that A0 A1 . . . ∈ Traces(TS ) we have to show that there exists apath in TS , say s0 s1 . . ., that generates this trace, i.e., trace(s0 s1 . . .) = A0 A1 . . ..Any finite prefix A0 A1 . . . Am of the infinite trace A0 A1 . . . is in Tracesfin (TS), and asTracesfin (TS) ⊆ Tracesfin (TS ), also in Tracesfin (TS ). Thus, for any natural number m,mmthere exists a finite path π m = sm0 s1 .
. . sm in TS such thatmmtrace(π m ) = L(sm0 )L(s1 ) . . . L(sm ) = A0 A1 . . . Amwhere L denotes the labeling function of TS . Thus, L(smj ) = Aj for all 0 j m.Although A0 . . . Am is a prefix of A0 . . . Am+1 , it is not guaranteed that path π m is aprefix of π m+1 .
Due to the finiteness of TS , however, there is an infinite subsequenceπ m0 π m1 π m2 . . . of π 0 π 1 π 2 . . . such that π mi and π mi+1 agree on the first i states. Thus,π m0 π m1 π m2 . . . induces an infinite path π in TS with the desired property.This is formally proven using a so-called diagonalization technique.
This goes as follows.Let I0 , I1 , I2 , . . . be an infinite series of infinite sets of indices (i.e., natural numbers) withIn ⊆ { m ∈ IN | m n } and s0 , s1 , . . . be states in TS such that for all natural numbersn it holds that(1) n 1 implies In−1 ⊇ In ,(2) s0 s1 s2 . . . sn is an initial, finite path fragment in TS ,m(3) for all m ∈ In it holds that s0 .
. . sn = sm0 . . . sn .The definition of the sets In and states sn is by induction on n.Base case (n = 0): As { sm0 | m ∈ IN } is finite (since it is a subset of the finite set of initialstates of TS ), there exists an initial state s0 in TS and an infinite index set I0 such thats0 = sm0 for all m ∈ I0 .Induction step n =⇒ n+1.
Assume that the index sets I0 , . . . , In and states s0 , . . . , sn aredefined. Since TS is finite, Post(sn ) is finite. Furthermore, by the induction hypothesissn = smn for all m ∈ In , and thus{ smn+1 | m ∈ In , m n+1 } ⊆ Post(sn ).Since In is infinite, there exists an infinite subset In+1 ⊆ { m ∈ In | m n+1 } and astate sn+1 ∈ Post(sn ) such that smn+1 = sn+1 for all m ∈ In+1 . It follows directly that theabove properties (1) through (3) are fulfilled.Safety Properties and Invariants119We now consider the state sequence s0 s1 . .
. in TS . Obviously, this state sequence is apath in TS satisfying trace(s0 s1 . . .) = A0 A1 . . .. Consequently, A0 A1 . . . ∈ Traces(TS ).Remark 3.31.Image-Finite Transition SystemsThe result stated in Theorem 3.30 also holds under slightly weaker conditions: it sufficesto require that TS has no terminal states (as in Theorem 3.30) and that TS is AP imagefinite (rather than being finite).Let TS = (S, Act, →, I, AP, L). Then, TS is called AP image-finite (or briefly imagefinite) if(i) for all A ⊆ AP, the set { s0 ∈ I | L(s0 ) = A } is finite and(ii) for all states s in TS and all A ⊆ AP, the set of successors { s ∈ Post(s) | L(s ) = A }is finite.Thus, any finite transition system is image-finite.
Moreover, any transition system that isAP-deterministic is image-finite. (Recall that AP-determinism requires { s0 ∈ I | L(s0 ) =A } and { s ∈ Post(s) | L(s ) = A } to be either singletons or empty sets; see Definition2.5, page 24.)In fact, a careful inspection of the proof of Theorem 3.30 shows that (i) and (ii) forTS are used in the construction of the index sets In and states sn . Hence, we haveTraces(TS) ⊆ Traces(TS ) iff Tracesfin (TS) ⊆ Tracesfin (TS ), provided TS has no terminalstates and TS is image-finite.Trace and finite trace inclusion, however, coincide neither for infinite transition systemsnor for finite ones which have terminal states.Example 3.32.Finite vs. Infinite Transition SystemConsider the transition systems sketched in Figure 3.10, where b stands for an atomicproposition.
Transition system TS (on the left) is finite, whereas TS (depicted on theright) is infinite and not image-finite, because of the infinite branching in the initial state.It is not difficult to observe thatTraces(TS) ⊆ Traces(TS )andTracesfin (TS) ⊆ Tracesfin (TS ).This stems from the fact that TS can take the self-loop infinitely often and never reachesa b-state, whereas TS does not exhibit such behavior.
Moreover, any finite trace of TS is120Linear-Time Propertiesof the form (∅)n for n 0 and is also a finite trace of TS . Consequently, LT properties ofTS do not carry over to TS (and those of TS may not hold for TS ). For example, the LTproperty “eventually b” holds for TS , but not for TS. Similarly, the LT property “neverb” holds for TS, but not for TS .Although these transition systems might seem rather artificial, this is not the case: TScould result from an infinite loop in a program, whereas TS could model the semanticsof a program fragment that nondeterministically chooses a natural number k and thenperforms k steps.{b}{b}{b}{b}Figure 3.10: Distinguishing trace inclusion from finite trace inclusion.3.4Liveness PropertiesInformally speaking, safety properties specify that “something bad never happens”. Forthe mutual exclusion algorithm, the “bad” thing is that more than one process is in itscritical section, while for the traffic light the “bad” situation is whenever a red light phaseis not preceded by a yellow light phase.
An algorithm can easily fulfill a safety propertyby simply doing nothing as this will never lead to a “bad” situation. As this is usuallyundesired, safety properties are complemented by properties that require some progress.Such properties are called “liveness” properties (or sometimes “progress” properties). Intuitively, they state that ”something good” will happen in the future. Whereas safetyproperties are violated in finite time, i.e., by a finite system run, liveness properties areviolated in infinite time, i.e., by infinite system runs.Liveness Properties3.4.1121Liveness PropertiesSeveral (nonequivalent) notions of liveness properties have been defined in the literature.We follow here the approach of Alpern and Schneider [5, 6, 7].
They provided a formalnotion of liveness properties which relies on the view that liveness properties do not constrain the finite behaviors, but require a certain condition on the infinite behaviors. Atypical example for a liveness property is the requirement that certain events occur infinitely often. In this sense, the ”good event” of a liveness property is a condition on theinfinite behaviors, while the ”bad event” for a safety property occurs in a finite amountof time, if it occurs at all.In our approach, a liveness property (over AP) is defined as an LT property that does notrule out any prefix.
This entails that the set of finite traces of a system are of no use atall to decide whether a liveness property holds or not. Intuitively speaking, it means thatany finite prefix can be extended such that the resulting infinite trace satisfies the livenessproperty under consideration. This is in contrast to safety properties where it suffices tohave one finite trace (the “bad prefix”) to conclude that a safety property is refuted.Definition 3.33.Liveness PropertyLT property Plive over AP is a liveness property whenever pref(Plive ) = (2AP )∗ .Thus, a liveness property (over AP) is an LT property P such that each finite word can beextended to an infinite word that satisfies P .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
