5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 28
Текст из файла (страница 28)
Stated differently, P is a liveness propertyif and only if for all finite words w ∈ (2AP )∗ there exists an infinite word σ ∈ (2AP )ωsatisfying wσ ∈ P .Example 3.34.Repeated Eventually and Starvation FreedomIn the context of mutual exclusion algorithms the natural safety property that is requiredensures the mutual exclusion property stating that the processes are never simultaneouslyin their critical sections. (This is even an invariant.) Typical liveness properties that aredesired assert that• (eventually) each process will eventually enter its critical section;• (repeated eventually) each process will enter its critical section infinitely often;• (starvation freedom) each waiting process will eventually enter its critical section.Let’s see how these liveness properties are formalized as LT properties and let us check that122Linear-Time Propertiesthey are liveness properties.
As in Example 3.14, we will deal with the atomic propositionswait1 , crit1 , wait2 , crit2 where waiti characterizes the states where process Pi has requestedaccess to its critical section and is in its waiting phase, while criti serves as a label forthe states where Pi has entered its critical section. We now formalize the three propertiesby LT properties over AP = {wait1 , crit1 , wait2 , crit2 }. The first property (eventually)consists of all infinite words A0 A1 . .
. with Aj ⊆ AP such that(∃j 0. crit1 ∈ Aj ) ∧ (∃j 0. crit2 ∈ Aj )which requires that P1 and P2 are in their critical sections at least once. The secondproperty (repeated eventually) poses the condition(∀k 0. ∃j k. crit1 ∈ Aj ) ∧ (∀k 0. ∃j k. crit2 ∈ Aj )stating that P1 and P2 are infinitely often in their critical sections. This formula is oftenabbreviated by∞∞j0.critj0.crit∈A∈A∧∃∃1j2j .The third property (starvation freedom) requires that∀j 0. (wait1 ∈ Aj ⇒ (∃k > j. crit1 ∈ Ak )) ∧∀j 0. (wait2 ∈ Aj ⇒ (∃k > j. crit2 ∈ Ak )) .It expresses that each process that is waiting will acquire access to the critical sectionat some later time point.
Note that here we implicitly assume that a process that startswaiting to acquire access to the critical section does not “give up” waiting, i.e., it continueswaiting until it is granted access.All aforementioned properties are liveness properties, as any finite word over AP is a prefixof an infinite word where the corresponding condition holds. For instance, for starvationfreedom, a finite trace in which a process is waiting but never acquires access to its criticalsection can always be extended to an infinite trace that satisfies the starvation freedomproperty (by, e.g., providing access in an strictly alternating fashion from a certain pointon).3.4.2Safety vs.
Liveness PropertiesThis section studies the relationship between liveness and safety properties. In particular,it provides answers to the following questions:• Are safety and liveness properties disjoint?, andLiveness Properties123• Is any linear-time property a safety or liveness property?As we will see, the first question will be answered affirmatively while the second questionwill result in a negative answer. Interestingly enough, though, for any LT property P anequivalent LT property P does exist which is a combination (i.e., intersection) of a safetyand a liveness property.
All in all, one could say that the identification of safety andliveness properties thus provides an essential characterization of linear-time properties.The first result states that safety and liveness properties are indeed almost disjoint. Moreprecisely, it states that the only property that is both a safety and a liveness property isnonrestrictive, i.e., allows all possible behaviors. Logically speaking, this is the equivalentof “true”.Lemma 3.35.Intersection of Safety and Liveness PropertiesThe only LT property over AP that is both a safety and a liveness property is (2AP )ω .Proof: Assume P is a liveness property over AP. By definition, pref(P ) = (2AP )∗ . Itfollows that closure(P ) = (2AP )ω . If P is a safety property too, closure(P ) = P , andhence P = (2AP )ω .Recall that the closure of property P (over AP) is the set of infinite words (over 2AP )for which all prefixes are also prefixes of P .
In order to show that an LT property canbe considered as a conjunction of a liveness and a safety property, the following result ishelpful. It states that the closure of the union of two properties equals the union of theirclosures.Lemma 3.36.Distributivity of Union over ClosureFor any LT properties P and P :closure(P ) ∪ closure(P ) = closure(P ∪ P ).Proof: ⊆: As P ⊆ P implies closure(P ) ⊆ closure(P ), we have P ⊆ P ∪ P impliesclosure(P ) ⊆ closure(P ∪P ). In a similar way it follows that closure(P ) ⊆ closure(P ∪P ).Thus, closure(P ) ∪ closure(P ) ⊆ closure(P ∪ P ).⊇: Let σ ∈ closure(P ∪ P ).
By definition of closure, pref(σ) ⊆ pref(P ∪ P ). As pref(P ∪P ) = pref(P ) ∪ pref(P ), any finite prefix of σ is in pref(P ) or in pref(P ) (or in both).124Linear-Time PropertiesAs σ ∈ (2AP )ω , σ has infinitely many prefixes. Thus, infinitely many finite prefixesof σ belong to pref(P ) or to pref(P ) (or to both). W.l.o.g., assume pref(σ) ∩ pref(P )to be infinite.
Then pref(σ) ⊆ pref(P ), which yields σ ∈ closure(P ), and thus σ ∈closure(P ) ∪ closure(P ). The fact that pref(σ) ⊆ pref(P ) can be shown by contraposition.Assume σ ∈ pref(σ) \ pref(P ). Let |σ | = k. As pref(σ) ∩ pref(P ) is infinite, there existsσ ∈ pref(σ) ∩ pref(P ) with length larger than k. But then, there exists σ ∈ P with ∈ pref(σ ) (as both σ and σ are prefixes of σ) and asσ ∈ pref(σ ).
It then follows that σ ∈ pref(P ). This contradicts σ ∈ pref(σ) \ pref(P ).pref(σ ) ⊆ pref(P ), it follows that σConsider the beverage vending machine of Figure 3.5 (on page 97), and the followingproperty:“the machine provides beer infinitely oftenafter initially providing soda three times in a row”In fact, this property consists of two parts.
On the one hand, it requires beer to beprovided infinitely often. As any finite trace can be extended to an infinite trace thatenjoys this property it is a liveness property. On the other hand, the first three drinks itprovides should all be soda. This is a safety property, since any finite trace in which oneof the first three drinks provided is beer violates it. The property is thus a combination(in fact, a conjunction) of a safety and a liveness property. The following result showsthat every LT property can be decomposed in this way.Theorem 3.37.Decomposition TheoremFor any LT property P over AP there exists a safety property Psafe and a liveness propertyPlive (both over AP) such thatP = Psafe ∩ Plive .Proof: Let P be an LT property over AP.
It is easy to see that P ⊆ closure(P ). Thus:P = closure(P ) ∩ P , which by set calculus can be rewritten into:P = closure(P ) ∩ P ∪ (2AP )ω \ closure(P ) =Psafe=PliveBy definition,Psafe = closure(P) is a safety property. It remains to prove that Plive =ωAPP ∪ (2 ) \ closure(P ) is a liveness property. By definition, Plive is a liveness propertywhenever pref(Plive ) = (2AP )∗ . This is equivalent to closure(Plive ) = (2AP )ω . As for anyLiveness Properties125LT property P , closure(P ) ⊆ (2AP )ω holds true, it suffices to showing that (2AP )ω ⊆closure(Plive ).
This goes as follows:closure(Plive )⊇closure P ∪ ((2AP )ω \ closure(P ))closure(P ) ∪ closure (2AP )ω \ closure(P )closure(P ) ∪ (2AP )ω \ closure(P )=(2AP )ω=Lemma 3.36=where in the one-but-last step in the derivation, we exploit the fact that closure(P ) ⊇ P for all LT properties P .The proof of Theorem 3.37 shows that Psafe = closure(P ) is a safety property andPlive = P ∪ ((2AP )ω \ closure(P )) a liveness property with P = Psafe ∩ Plive . In fact,this decomposition is the ”sharpest” one for P since Psafe is the strongest safety propertyand Plive the weakest liveness property that can serve for a decomposition of P :Lemma 3.38.Sharpest DecompositionLet P be an LT property and P = Psafe ∩ Plive where Psafe is a safety property and Plivea liveness property.
We then have1. closure(P ) ⊆ Psafe ,2. Plive ⊆ P ∪ ((2AP )ω \ closure(P )).Proof: See Exercise 3.12, page 147.A summary of the classification of LT properties is depicted as a Venn diagram in Figure 3.11. The circle denotes the set of all LT properties over a given set of atomic propositions.Remark 3.39.Topological Characterizations of Safety and LivenessLet us conclude this section with a remark for readers who are familiar with basic notionsof topological spaces. The set (2AP )ω can be equipped with the distance function given byd(σ1 , σ2 ) = 1/2n if σ1 , σ2 are two distinct infinite words σ1 = A1 A2 . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
