5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 24
Текст из файла (страница 24)
. . is not in P as it contains onlyfinitely many occurrences of green1 .As a second LT property, consider P :“The traffic lights are never both green simultaneously”.This property is formalized by the set of infinite words of the form A0 A1 A2 . . . such that/ Ai or green2 ∈/ Ai , for all i 0. For example, the following infinite wordseither green1 ∈are in P :{ red1 , green2 } { green1 , red2 } { red1 , green2 } { green1 , red2 } . . . ,∅ { green1 } ∅ { green1 } ∅ { green1 } ∅ { green1 } ∅ . . .and{ red1 , green1 } { red1 , green1 } { red1 , green1 } { red1 , green1 } . . .
,whereas the infinite word { red1 green2 } { green1 , green2 }, . . . is not in P .The traffic lights depicted in Figure 3.7 are at intersecting roads and their switching issynchronized, i.e., if one light switches from red to green, the other switches from green to102Linear-Time Propertiesred. In this way, the lights always have complementary colors. Clearly, these traffic lightssatisfy both P and P . Traffic lights that switch completely autonomously will neithersatisfy P —there is no guarantee that the first traffic light is green infinitely often—norP .Often, an LT property does not refer to all atomic propositions occurring in a transitionsystem, but just to a relatively small subset thereof.
For a property P over a set of be a finite pathpropositions AP ⊆ AP, only the labels in AP are relevant. Let ππ ) to denote the finite trace of π where only thefragment of TS. We write traceAP (atomic propositions in AP are considered.
Accordingly, traceAP (π) denotes the trace ofan infinite path fragment π by focusing on propositions in AP Thus, for π = s0 s1 s2 . . .,we havetraceAP (π) = L (s0 ) L (s1 ) . . . = (L(s0 ) ∩ AP ) (L(s1 ) ∩ AP ) . . .Let TracesAP (TS) denote the set of traces traceAP (Paths(TS)). Whenever the set AP ofatomic propositions is clear from the context, the subscript AP is omitted. In the rest ofthis chapter, the restriction to a relevant subset of atomic propositions is often implicitlymade.Example 3.13.The Mutual Exclusion PropertyIn Chapter 2, several mutual exclusion algorithms have been considered. For specifying themutual exclusion property—always at most one process is in its critical section—it sufficesto only consider the atomic propositions crit1 and crit2 .
Other atomic propositions arenot of any relevance for this property. The formalization of the mutual exclusion propertyis given by the LT propertyPmutex = set of infinite words A0 A1 A2 . . . with { crit1 , crit2 } ⊆ Ai for all 0 i.For example, the infinite words{ crit1 } { crit2 } { crit1 } { crit2 } { crit1 } { crit2 } . . . ,and{ crit1 } { crit1 } { crit1 } { crit1 } { crit1 } { crit1 } . .
. ,and∅∅∅∅∅∅∅...are all contained in Pmutex . However, this does not apply to words of the form{ crit1 } ∅ { crit1 , crit2 } . . .The transition system TSArb = (TS1 ||| TS2 ) Arbiter described in Example 2.28 (page 50)fulfills the mutex property, i.e.,TSArb |= Pmutex .Linear-Time Behavior103It is left to the reader to check that the mutex property is also fulfilled by the semaphorebased mutual exclusion algorithm (see Figure 3.6 on page 99) and Peterson’s algorithm(see Example 2.25 on page 45).Example 3.14.Starvation FreedomGuaranteeing mutual exclusion is a significant property of mutual exclusion algorithms,but is not the only relevant property. An algorithm that never allows a process to enterits critical section will do, but is certainly not intended.
Besides, a property is imposedthat requires a process that wants to enter the critical section to be able to eventually doso. This property prevents a process from waiting ad infinitum and is formally specifiedas the LT property Pfinwait = set of infinite words A0 A1 A2 . . . such that∀j.lwaiti ∈ Aj ⇒ ∃k j.waiti ∈ Ak for each i ∈ { 1, 2 }.Here, we assumed the set of propositions to be:AP = { wait1 , crit1 , wait2 , crit2 }.Property Pfinwait expresses that each of the two processes enters its critical section eventually if they are waiting.
That is, a process has to wait some finite amount before enteringthe critical section. It does not express that a process that waits often, is often enteringthe critical section.Consider the following variant. The LT property Pnostarve = set of infinite words A0 A1 A2 . . .such that:(∀k 0. ∃j k. waiti ∈ Aj ) ⇒ (∀k 0. ∃j k. criti ∈ Aj )In abbreviated form we write:∞∞⇒ ∃ j. criti ∈ Aj∃ j. waiti ∈ Ajfor each i ∈ { 1, 2 }.for each i ∈ { 1, 2 }∞where ∃ stands for “there are infinitely many”.Property Pnostarve expresses that each of the two processes enters its critical section infinitely often if they are waiting infinitely often.
This natural requirement is, however, notsatisfied for the semaphore-based solution, since∅ ({ wait2 } { wait1 , wait2 } { crit1 , wait2 } )ωis a possible trace of the transition system but does not belong to Pnostarve . This tracerepresents an execution in which only the first process enters its critical section infinitelyoften. In fact, the second process waits infinitely long to enter its critical section.It is left to the reader to check that the transition system modeling Peterson’s algorithm(see Example 2.25, page 45) does indeed satisfy Pnostarve .1043.2.4Linear-Time PropertiesTrace Equivalence and Linear-Time PropertiesLT properties specify the (infinite) traces that a transition system should exhibit. Iftransition systems TS and TS have the same traces, one would expect that they satisfythe same LT properties. Clearly, if TS |= P , then all traces of TS are contained in P , andwhen Traces(TS) = Traces(TS ), the traces of TS are also contained in P .
Otherwise,whenever TS |= P , there is a trace in Traces(TS) that is prohibited by P , i.e., not includedin the set P of traces. As Traces(TS) = Traces(TS ), also TS exhibits this prohibited trace,and thus TS |= P . The precise relationship between trace equivalence, trace inclusion,and the satisfaction of LT properties is the subject of this section.We start by considering trace inclusion and its importance in concurrent system design.Trace inclusion between transition systems TS and TS requires that all traces exhibitedby TS can also be exhibited by TS , i.e., Traces(TS) ⊆ Traces(TS ). Note that transitionsystem TS may exhibit more traces, i.e., may have some (linear-time) behavior that TSdoes not have. In stepwise system design, where designs are successively refined, traceinclusion is often viewed as an implementation relation in the sense thatTraces(TS) ⊆ Traces(TS ) means TS “is a correct implementation of” TS .For example, let TS be a (more abstract) design where parallel composition is modeled byinterleaving, and TS its realization where (some of) the interleaving is resolved by meansof some scheduling mechanism.
TS may thus be viewed as an “implementation” of TS ,and clearly, Traces(TS) ⊆ Traces(TS ).What does trace inclusion have to do with LT properties? The following theorem showsthat trace inclusion is compatible with requirement specifications represented as LT properties.Theorem 3.15.Trace Inclusion and LT PropertiesLet TS and TS be transition systems without terminal states and with the same set ofpropositions AP. Then the following statements are equivalent:(a) Traces(TS) ⊆ Traces(TS )(b) For any LT property P : TS |= P implies TS |= P .Proof: (a) =⇒ (b): Assume Traces(TS) ⊆ Traces(TS ), and let P be an LT property suchthat TS |= P .
From Definition 3.11 it follows that Traces(TS ) ⊆ P . Given Traces(TS) ⊆Linear-Time Behavior105Traces(TS ), it now follows that Traces(TS) ⊆ P . By Definition 3.11 it follows thatTS |= P .(b) =⇒ (a): Assume that for all LT properties it holds that: TS |= P implies TS |= P .Let P = Traces(TS ). Obviously, TS |= P , as Traces(TS ) ⊆ Traces(TS ). By assumption,TS |= P . Hence, Traces(TS) ⊆ Traces(TS ).This simple observation plays a decisive role for the design by means of successive refinement. If TS is the transition system representing a preliminary design and TSis a transition system originating from a refinement of TS (i.e., a more detailed design), then it can immediately—without explicit proof—be concluded from the relationTraces(TS) ⊆ Traces(TS ) that any LT property that holds in TS also holds for TS.Example 3.16.Refining the Semaphore-Based Mutual Exclusion AlgorithmLet TS = TSSem , the transition system representing the semaphore-based mutual exclusion algorithm (see Figure 3.6 on page 99) and let TS be the transition system obtainedfrom TS by removing the transition→ wait1 , crit2 , y = 0.wait1 , wait2 , y = 1 −Stated in words, from the situation in which both processes are waiting, it is no longerpossible that the second process (P2 ) acquires access to the critical section.
This thus yieldsa model that assigns higher priority to process P1 than to process P2 when both processesare competing to access the critical section. As a transition is removed, it immediatelyfollows that Traces(TS) ⊆ Traces(TS ). Consequently, by the fact that TS ensures mutualexclusion, i.e., TS |= Pmutex , it follows by Theorem 3.15 that TS |= Pmutex .Transition systems are said to be trace-equivalent if they have the same set of traces:Definition 3.17.Trace EquivalenceTransition systems TS and TS are trace-equivalent with respect to the set of propositionsAP if TracesAP (TS) = TracesAP (TS ). 4Theorem 3.15 implies equivalence of two trace-equivalent transition systems with respectto requirements formulated as LT properties.4Here, we assume two transition systems with sets of propositions that include AP.106Linear-Time PropertiesCorollary 3.18.Trace Equivalence and LT PropertiesLet TS and TS be transition systems without terminal states and with the same set ofatomic propositions.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
