5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 52
Текст из файла (страница 52)
For asynchronoussystems (for which the transition system representation is time-abstract), the next-stepoperator cannot be interpreted as a real-time modality. In fact, for asynchronous systemsthe next-step operator should be used with care. The phase changes of a traffic light, forexample, can be described byϕ = (green → yellow) ∧ (yellow → red) ∧ . .
.Linear Temporal Logic247For the interleaving of two independent traffic lights (Example 2.17 on page 36) and theformulae ϕ1 , ϕ2 (where the indexed atomic propositions greeni , yellowi , etc., are used),TrLight1 ||| TrLight2 |= ϕ1 ∧ ϕ2 .This stems from the fact that, e.g., the first traffic light does not change its location whenthe second traffic light changes its phase. To avoid this problem, the until operator canbe used instead, e.g.,ϕ = (green → (green U yellow)) ∧ (yellow → (yellow U red)) ∧ .
. .This differs from the synchronous product operator ⊗, whereTrLight1 ⊗ TrLight2 |= ϕ.Remark 5.16.Other Notations and Variants of LTLMany variants and notations have been introduced for LTL. Alternative notations forthe temporal modalities are X for (neXt), F for ♦ (Finally), and G for (Globally).All operators from LTL refer to the future (including the current state). Consequently,operators are known as future operators. LTL can, however, also be extended with pastoperators.
This can be useful for specifying some properties more easily (and succinctly)in terms of the past than in terms of the future. For instance, −1 a (“always in the past”)means that a is valid now and in any state in the past. ♦−1 a (“sometime in the past”)means that either a is valid in the current state or in some state in the past and −1 ameans that a holds in the previous state, provided such state exists.
For example, theproperty “every red light phase is preceded by a yellow one” can be described by(red → −1 yellow).The main reason for introducing past operators is to simplify the specification of severalproperties. The expressive power of the logic is, however, not affected by the addition ofpast operators when a discrete notion of time is taken (as we do). Thus, for any propertywhich contains one or more past operators, an LTL-formula with only future temporaloperators exists expressing the same thing. More information is described in Section 5.4.5.1.4Equivalence of LTL FormulaeFor any type of logic, a clear separation between syntax and semantics is an essentialaspect.
On the other hand, two formulae are intuitively identified whenever they have the248Linear Temporal Logicduality lawidempotency law¬ ϕ ≡ ¬ϕ♦♦ϕ ≡ ♦ϕ¬♦ϕ ≡ ¬ϕ ϕ ≡ ϕ¬ϕ ≡ ♦¬ϕϕ U (ϕ U ψ) ≡ ϕ U ψ(ϕ U ψ) U ψ ≡ ϕ U ψabsorption lawexpansion law♦ ♦ϕ ≡ ♦ϕϕ U ψ ≡ ψ ∨ (ϕ ∧ (ϕ U ψ)) ♦ ϕ ≡ ♦ ϕ♦ψ ≡ ψ ∨ ♦ψψ ≡ ψ ∧ ψdistributive law (ϕ U ψ) ≡ ( ϕ) U ( ψ)♦(ϕ ∨ ψ) ≡ ♦ϕ ∨ ♦ψ(ϕ ∧ ψ) ≡ ϕ ∧ ψFigure 5.7: Some equivalence rules for LTL.same truth-value under all interpretations. For example, it seems useless to distinguishbetween ¬¬a and a, although both formulae are syntactically different.Definition 5.17.Equivalence of LTL FormulaeLTL formulae ϕ1 , ϕ2 are equivalent, denoted ϕ1 ≡ ϕ2 , if Words(ϕ1 ) = Words(ϕ2 ).As LTL subsumes propositional logic, equivalences of propositional logic also hold for LTL,e.g., ¬¬ϕ ≡ ϕ and ϕ ∧ ϕ ≡ ϕ.
In addition, there exist a number of equivalence rules fortemporal modalities. They include the equivalence laws indicated in Figure 5.7.Weexplain some of these equivalence laws. The duality rule ¬ ϕ ≡ ¬ϕ shows that thenext-step operator is dual to itself. It results from the observation thatA0 A1 A2 . . . |= ¬ ϕiffA0 A1 A2 . . . |= ϕiffA1 A2 . .
. |= ϕiffA1 A2 . . . |= ¬ϕiffA0 A1 A2 . . . |= ¬ϕ.The first absorption law is explained by the fact that “infinitely often ϕ” is equal to “fromLinear Temporal Logic249a certain point of time on, ϕ is true infinitely often”.The distributive laws for ♦ and disjunction, or and conjunction, respectively, are dualto each other. They can be regarded as the temporal logic analogon to the distributivelaws for ∃ and ∨ or ∀ and ∧ in predicate logic. It should be noted, however, that ♦ doesnot distribute over conjunction (as existential quantification), and does not distributeover disjunction (like universal quantification):♦(a ∧ b) ≡ ♦a ∧ ♦band (a ∨ b) ≡ a ∨ b.The formula ♦(a ∧ b) ensures that a state will be reached for which a and b hold, while♦a ∧ ♦b ensures that eventually an a-state and eventually a b-state will be reached. According to the latter formula, a and b need not to be satisfied at the same time.
Figure5.8 depicts a transition system that satisfies ♦a ∧ ♦b, but not ♦(a ∧ b).{b}{a}Figure 5.8: TS |= ♦(a ∧ b) and TS |= ♦a ∧ ♦b.The expansion laws play an important role. They describe the temporal modalities U , ♦,and by means of a recursive equivalence. These equivalences all have the same globalstructure: they assert something about the current state, and about the direct successorstate. The assertion about the current state is done without the need to use temporalmodalities whereas the assertion about the next state is done using the operator.
Theexpansion law for until, for instance, can be considered as follows. Formula φ U ψ is asolution of the equivalenceκ ≡ ψ ∨ (ϕ ∧ κ). ↑current statefirst suffixLet us explain the expansion law for the until operator in more detail. Let A0 A1 A2 . . . bean infinite word over the alphabet 2AP , such that A0 A1 A2 .
. . |= ϕ U ψ. By the definitionof “until”, there exists a k 0, such thatAi Ai+1 Ai+2 . . . |= ϕ,for all 0 i < kandAk Ak+1 Ak+2 . . . |= ψ.Distinguish between k = 0 and k > 0. If k = 0, then A0 A1 A2 . . . |= ψ and thusA0 A1 A2 . .
. |= ψ ∨ . . .. If k > 0, then250Linear Temporal LogicA0 A1 A2 . . . |= ϕA1 A2 . . . |= ϕ U ψ.andFrom this it immediately follows thatA0 A1 A2 . . . |= ϕ ∧ (ϕ U ψ).Gathering the results for k = 0 and k > 0 yieldsA0 A1 A2 . . . |= ψ ∨ (ϕ ∧ (ϕ U ψ)).For the reverse direction, a similar argument can be provided.The expansion law for ♦ψ is a special case of the expansion law for until:♦ψ = true U ψ ≡ ψ ∨ (true ∧ (true U ψ)) ≡ ψ ∨ ♦ψ.≡ (true U ψ) = ♦ψThe expansion law for ψ now results from the duality of ♦ and , the duality of ∨ and∧ (i.e., de Morgan’s law) and from the duality law for ψ=≡≡≡≡¬♦¬ψ¬(¬ψ ∨ ♦¬ψ)(* definition of *)(* expansion law for ♦*)(* de Morgan’s law *)¬¬ψ ∧ ¬ ♦¬ψψ ∧ ¬♦¬ψψ ∧ ψ(* self-duality of *)(* definition of *)It is important to realize that none of the indicated expansion laws represents a completerecursive characterization of the temporal operator at hand.
For example, the formulaeϕ = false and ϕ = a both satisfy the recursive “equation” ϕ ≡ a ∧ ϕ since false ≡a ∧ false and a ≡ a ∧ a. However, ϕ U ψ and ♦ϕ are the least solutions ofthe expansion law indicated for “until” and“eventually”, respectively. Similarly, ϕ isthe greatest solution of the expansion law for “always”.
The precise meaning of thesestatements will be explained by considering the until operator as example:Linear Temporal LogicLemma 5.18.251Until is the Least Solution of the Expansion LawFor LTL formulae ϕ and ψ, Words(ϕ U ψ) is the least LT property P ⊆ (2AP )ω such that:Words(ψ) ∪ {A0 A1 A2 .
. . ∈ Words(ϕ) | A1 A2 . . . ∈ P } ⊆ P(*)Moreover, Words(ϕ U ψ) agrees with the setWords(ψ) ∪ {A0 A1 A2 . . . ∈ Words(ϕ) | A1 A2 . . . ∈ Words(ϕ U ψ)}.The formulation “least LT property satisfying condition (*)” means that the followingconditions hold:(1) P = Words(ϕ U ψ) satisfies (*).(2) Words(ϕ U ψ) ⊆ P for all LT properties P satisfying condition (*).Proof: Condition (1) follows immediately from the expansion law ϕ U ψ ≡ ψ ∨ (ϕ ∧ (ϕ U ψ)). In fact, the expansion law even yields that ⊆ in (*) can be replaced byequality, i.e., Words(ϕ U ψ) agrees withWords(ψ) ∪ {A0 A1 A2 .
. . ∈ Words(ϕ) | A1 A2 . . . ∈ Words(ϕ U ψ)}.To prove condition (2), P is assumed to be an LT property that satisfies (*). We showthat Words(ϕ U ψ) ⊆ P . Since P fulfills (*), we have:(i) Words(ψ) ⊆ P ,(ii) If B0 B1 B2 . . . ∈ Words(ϕ) and B1 B2 . . . ∈ P then B0 B1 B2 . . . ∈ P.Let A0 A1 A2 . . . ∈ Words(ϕ U ψ). Then, there exists an index k 0 such that(iii) Ai Ai+1 Ai+2 . . . ∈ Words(ϕ),(iv) Ak Ak+1 Ak+2 . . . ∈ Words(ψ).We now derivefor all 0 i < k,2525.1.5Linear Temporal Logic=⇒=⇒Ak Ak+1 Ak+2 Ak+3 . . . ∈ PAk−1 Ak Ak+1 Ak+2 . . . ∈ PAk−2 Ak−1 Ak Ak+1 .
. . ∈ P...due to (iv) and (i)due to (ii) and (iii)due to (ii) and (iii)=⇒A0 A1 A2 A3 . . . ∈ Pdue to (ii) and (iii).Weak Until, Release, and Positive Normal FormAny LTL formula can be transformed into a canonical form, the so-called positive normalform (PNF). This canonical form is characterized by the fact that negations only occuradjacent to atomic propositions. PNF formulae in propositional logic are constructed fromthe constants true and false, the literals a and ¬a, and the operators ∧ and ∨. For instance,¬a ∧ ((¬b ∧ c) ∨ ¬a) is in PNF, while ¬(a ∧ ¬b) is not.
The well-known disjunctive andconjunctive normal forms are special cases of the PNF for propositional logic.In order to transform any LTL formula into PNF, for each operator a dual operator needsto be incorporated into the syntax of PNF formulae. The propositional logical primitives ofthe positive normal form for LTL are the constant true and its dual constant false = ¬true,as well as conjunction ∧ and its dual, ∨. De Morgan’s rules ¬(ϕ ∨ ψ) ≡ ¬ϕ ∧ ¬ψ and¬(ϕ ∧ ψ) ≡ ¬ϕ ∨ ¬ψ yield the duality of conjunction and disjunction. According to theduality rule ¬ ϕ ≡ ¬ϕ, the next-step operator is a dual of itself.
Therefore, noextra operator is necessary for . Now consider the until operator. First we observe that¬(ϕ U ψ) ≡ ((ϕ ∧ ¬ψ) U (¬ϕ ∧ ¬ψ)) ∨ (ϕ ∧ ¬ψ).The first disjunct on the right-hand side asserts that ϕ stops to hold “too early”, i.e.,before ψ becomes valid. The second disjunct states that ϕ always holds but never ψ.Clearly, in both cases, ¬(ϕ U ψ) holds.This observation provides the motivation to introduce the operator W (called weak untilor unless) as the dual of U .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
