5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 53
Текст из файла (страница 53)
It is defined by:ϕ W ψ = (ϕ U ψ) ∨ ϕ.defThe semantics of ϕ W ψ is similar to that of ϕ U ψ, except that ϕ U ψ requires a state tobe reached for which ψ holds, whereas this is not required for ϕ W ψ. Until U and weakuntil W are dual in the following sense:¬(ϕ U ψ)≡ (ϕ ∧ ¬ψ) W (¬ϕ ∧ ¬ψ)¬(ϕ W ψ) ≡ (ϕ ∧ ¬ψ) U (¬ϕ ∧ ¬ψ)Linear Temporal Logic253The reason that weak until is not a standard operator for LTL is that U and W have thesame expressiveness, sinceψ≡ ψ W false,ϕ U ψ ≡ (ϕ W ψ) ∧♦ψ .≡ ¬¬ψThat is to say, weak until is relevant only if restrictions are imposed on the occurrenceof negation (as in PNF).
It is interesting to observe that W and U satisfy the sameexpansion law:ϕ W ψ ≡ ψ ∨ (ϕ ∧ (ϕ W ψ)).For ψ = false this results in the expansion law for ϕ:ϕ = ϕ W false ≡ false ∨ (ϕ ∧ (ϕ W false)) ≡ ϕ ∧ ϕ.The semantic difference between U and W is shown by the fact that ϕ W ψ is the greatestsolution ofκ ≡ ψ ∨ (ϕ ∧ κ).This result is proven below. Recall ϕ U ψ is the least solution of this equivalence, seeLemma 5.18 on page 251.Lemma 5.19.Weak-Until is the Greatest Solution of the Expansion LawFor LTL formulae ϕ and ψ, Words(ϕ W ψ) is the greatest LT property P ⊆ (2AP )ω suchthat:Words(ψ) ∪ {A0 A1 A2 . . . ∈ Words(ϕ) | A1 A2 .
. . ∈ P } ⊇ P(*)Moreover, Words(ϕ W ψ) agrees with the LT propertyWords(ψ) ∪ {A0 A1 A2 . . . ∈ Words(ϕ) | A1 A2 . . . ∈ Words(ϕ W ψ)}.The formulation “greatest LT property with the indicated condition (*) is to be understoodin the following sense:(1) P ⊇ Words(ϕ W ψ) satisfies (*).(2) Words(ϕ W ψ) ⊇ P for all LT properties P satisfying condition (*).254Linear Temporal LogicProof: The fact that condition (1) is satisfied, even with equality rather than ⊇, i.e.,Words(ϕ W ψ) agrees withWords(ψ) ∪ {A0 A1 A2 . .
. ∈ Words(ϕ) | A1 A2 . . . ∈ Words(ϕ W ψ)},is an immediate conclusion from the expansion law ϕ W ψ ≡ ψ ∨ (ϕ ∧ (ϕ W ψ)).For proving condition (2), P is assumed to be an LT property satisfying (*). In particular,for all words B0 B1 B2 B3 . . . ∈ (2AP )ω \ Words(ψ) we have:/ Words(ϕ), then B0 B1 B2 B3 . . . ∈/ P.(i) If B0 B1 B2 B3 .
. . ∈/ P , then B0 B1 B2 B3 . . . ∈/ P.(ii) If B1 B2 B3 . . . ∈Now we demonstrate that(2AP )ω \ Words(ϕ W ψ) ⊆ (2AP )ω \ P.Let A0 A1 A2 . . . ∈ (2AP )ω \ Words(ϕ W ψ). Then A0 A1 A2 . . . |= ϕ W ψ and thusA0 A1 A2 . . . |= ¬(ϕ W ψ) ≡ (ϕ ∧ ¬ψ) U (¬ϕ ∧ ¬ψ).Thus there exists k 0, such that:(iii) Ai Ai+1 Ai+2 . . . |= ϕ ∧ ¬ψ,for all 0 i < k,(iv) Ak Ak+1 Ak+2 . . . |= ¬ϕ ∧ ¬ψ.In particular, none of the words Ai Ai+1 Ai+2 .
. . belongs to Words(ψ) for 0 i k. Weobtain:=⇒=⇒/PAk Ak+1 Ak+2 Ak+3 . . . ∈/PAk−1 Ak Ak+1 Ak+2 . . . ∈/PAk−2 Ak−1 Ak Ak+1 . . . ∈...due to (i) and (iv)due to (ii) and (iii)due to (ii) and (iii)=⇒/PA0 A1 A2 A3 . . . ∈due to (ii) and (iii) .Thus, (2AP )ω \ Words(ϕ W ψ) ⊆ (2AP )ω \ P , or equivalently, Words(ϕ W ψ) ⊇ P .We are now ready to introduce the positive normal form for LTL which permits negationonly on the level of literals and – to ensure the full expressiveness of LTL – uses the dualBoolean connectors ∧ and ∨, the self-dual next-step operator , and U and W :Linear Temporal LogicDefinition 5.20.255Positive Normal Form for LTL (Weak-Until PNF)For a ∈ AP, the set of LTL formulae in weak-until positive normal form (weak-until PNF,for short, or simply PNF) is given by:ϕ ::= true falsea¬a ϕ1 ∧ ϕ2ϕ1 ∨ ϕ2ϕϕ1 U ϕ2ϕ1 W ϕ2 .Due to the law ϕ ≡ ϕ W false, can also be considered as permitted operator of theW -positive normal form.
As before, ♦ϕ = true U ϕ. An example LTL formula in PNF is♦(a U b) ∨ (a ∧ ¬c) W (♦(¬a U b)).The LTL formulae ¬(a U b) and c ∨ ¬(a ∧ ♦b) are not in weak-until PNF.The previous considerations were aimed to rewrite any LTL formula into weak-until PNF.This is done by successively “pushing” negations “inside” the formula at hand. This isfacilitated by the following transformations:¬true¬false¬¬ϕ¬(ϕ ∧ ψ)¬ ϕ¬(ϕ U ψ)falsetrueϕ¬ϕ ∨ ¬ψ ¬ϕ(ϕ ∧ ¬ψ) W (¬ϕ ∧ ¬ψ).These rewrite rules are lifted to the derived operators as follows:¬(ϕ ∨ ψ) ¬ϕ ∧ ¬ψExample 5.21.and¬♦ϕ ¬ϕ and ¬ϕ ♦¬ϕ.Positive Normal FormConsider the LTL formula ¬((a U b) ∨ c).
This formula is not in PNF, but can betransformed into an equivalent LTL formula in weak-until PNF as follows:¬((a U b) ∨ c)≡ ♦¬((a U b) ∨ c)≡ ♦(¬(a U b) ∧ ¬ c)≡ ♦((a ∧ ¬b) W (¬a ∧ ¬b) ∧ ¬c)256Linear Temporal LogicTheorem 5.22.Existence of Equivalent Weak-Until PNF FormulaeFor each LTL formula there exists an equivalent LTL formula in weak-until PNF.The main drawback of the rewrite rules introduced above is that the length of the resultingLTL formula (in weak-until PNF) may be exponential in the length of the original nonPNFLTL formula.
This is due to the rewrite rule for until where ϕ and ψ are duplicated.Although this can be slightly improved by adopting the law:¬(ϕ U ψ) ≡ (¬ψ) W (¬ϕ ∧ ¬ψ)an exponential growth in length is not avoided here too due to the duplication of ψ in theright-hand side.To avoid this exponential blowup in transforming an LTL formula in PNF, another temporal modality is used that is dual to the until operator: the so-called binary release-operator,denoted R . It is defined byϕRψ= ¬(¬ϕ U ¬ψ).defIts intuitive interpretation is as follows.
Formula ϕ R ψ holds for a word if ψ always holds,a requirement that is released as soon as ϕ becomes valid. Thus, the formula false R ϕ isvalid if ϕ always holds, since the release condition (false) is a contradiction. Formally, fora given word σ = A0 A1 . . . ∈ (2AP )ω :σ |= ϕ R ψiffiffiff(* definition of R *)¬∃j 0. (σ[j..] |= ¬ψ ∧ ∀i < j. σ[i..] |= ¬ϕ)(* semantics of negation *)¬∃j 0. (σ[j..] |= ψ ∧ ∀i < j. σ[i..] |= ϕ)(* duality of ∃ and ∀ *)∀j 0.
¬ σ[j..] |= ψ ∧ ∀i < j. σ[i..] |= ϕiff(*de Morgan’s law *)∀j 0. ¬(σ[j..] |= ψ) ∨ ¬∀i < j. σ[i..] |= ϕiff(*semantics of negation *)∀j 0. σ[j..] |= ψ ∨ ∃i < j. σ[i..] |= ϕiff∀j 0. σ[j..] |= ψor∃i 0. (σ[i..] |= ϕ) ∧ ∀k i. σ[k..] |= ψ).The always operator is obtained from the release operator by:ϕ ≡ false R ϕ.Linear Temporal Logic257The weak-until and the until operator are obtained by:ϕ W ψ ≡ (¬ϕ ∨ ψ) R (ϕ ∨ ψ),ϕ U ψ ≡ ¬(¬ϕ R ¬ψ).Vice versa, ϕ R ψ ≡ (¬ϕ ∧ ψ) W (ϕ ∧ ψ). The expansion law (see Exercise 5.8) for releasereads as follows:ϕ R ψ ≡ ψ ∧ (ϕ ∨ (ϕ R ψ)).We now revisit the notion of PNF, which is defined using the R -operator rather than W :Definition 5.23.Positive Normal Form (release PNF)For a ∈ AP , LTL formulae in release positive normal form (release PNF, or simply PNF)are given byϕ ::= true false a¬aϕ1 ∧ ϕ2ϕ1 ∨ ϕ2 ϕ ϕ1 U ϕ2ϕ1 R ϕ2 .The following transformation rules push negations inside and serve to transform a givenLTL formula into an equivalent LTL formula in PNF:¬true¬¬ϕ¬(ϕ ∧ ψ)¬ ϕ¬(ϕ U ψ)falseϕ¬ϕ ∨ ¬ψ ¬ϕ¬ϕ R ¬ψIn each rewrite rule the size of the resulting formula increases at most by an additiveconstant.Theorem 5.24.Existence of Equivalent Release PNF FormulaeFor any LTL formula ϕ there exists an equivalent LTL formula ϕ in release PNF with|ϕ | = O(|ϕ|).5.1.6Fairness in LTLIn Chapter 3, we have seen that typically some fairness constraints are needed to verifyliveness properties.
Three types of fairness constraints (for sets of actions) have been distinguished, namely unconditional, strong, and weak fairness. Accordingly, the satisfaction258Linear Temporal Logicrelation for LT properties (denoted |=) has been adapted to the fairness assumption F(denoted |=F ), where F is a triple of (sets of) fairness constraints.
This entails that onlyfair paths are considered while determining the satisfaction of a property. In this section,this approach is adopted in the context of LTL. That is to say, rather than determining fortransition system TS and LTL formula ϕ whether TS |= ϕ, we focus on the fair executionsof TS.
The main difference with the action-based fairness assumptions (and constraints)is that we now focus on state-based fairness.Definition 5.25.LTL Fairness Constraints and AssumptionsLet Φ and Ψ be propositional logic formulae over AP.1. An unconditional LTL fairness constraint is an LTL formula of the formufair = ♦Ψ.2. A strong LTL fairness condition is an LTL formula of the formsfair = ♦Φ −→ ♦Ψ.3. A weak LTL fairness constraint is an LTL formula of the formwfair = ♦Φ −→ ♦Ψ.An LTL fairness assumption is a conjunction of LTL fairness constraints (of any arbitrarytype).For instance, a strong LTL fairness assumption denotes a conjunction of strong LTLfairness constraints, i.e., a formula of the form(♦Φi −→ ♦Ψi )sfair =0<ikfor propositional logical formulae Φi and Ψi over AP.
Weak and unconditional LTL fairnessassumptions are defined in a similar way.Linear Temporal Logic259In their most general form, LTL fairness assumptions are (as in Definition 3.46, page 133)a conjunction of unconditional, strong, and weak fairness assumptions:fair = ufair ∧ sfair ∧ wfair .where ufair, sfair, and wfair are unconditional, strong, and weak LTL fairness assumptions, respectively. As in the case of action-based fairness assumptions, the rule of thumbfor imposing fairness assumptions is: strong (or unconditional) fairness assumptions areuseful for solving contentions, and weak fairness is often sufficient for resolving the nondeterminism that results from interleaving.In the sequel, we adopt the same notations as for action-based fairness assumptions.
LetFairPaths(s) denote the set of all fair paths starting in s and FairTraces(s) the set of alltraces induced by fair paths starting in s. Formally, for fixed formula fair ,FairPaths(s)= { π ∈ Paths(s) | π |= fair },FairTraces(s) = { trace(π) | π ∈ FairPaths(s) }.These notions can be lifted to transition systems in the obvious way yielding FairPaths(TS)and FairTraces(TS). To identify the fairness assumption fair, we may write FairPathsfair (·)or FairTracesfair (·).Definition 5.26.Satisfaction Relation for LTL with FairnessFor state s in transition system TS (over AP) without terminal states, LTL formula ϕ,and LTL fairness assumption fair lets |=fair ϕ iff ∀π ∈ FairPaths(s). π |= ϕ andTS |=fair ϕ iff ∀s0 ∈ I. s0 |=fair ϕ.TS satisfies ϕ under the LTL fairness assumption fair if ϕ holds for all fair paths thatoriginate from some initial state.Example 5.27.Mutual Exclusion with Randomized Arbiter (Fairness)Consider the following approach to two-process mutual exclusion.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
