5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 62
Текст из файла (страница 62)
Suppose wehave the following atomic propositions for Peter at our disposal:• Peter.request ::= indicates that Peter requests usage of the printer;• Peter.use ::= indicates that Peter uses the printer;• Peter.release ::= indicates that Peter releases the printer.For Betsy, similar predicates are defined. Specify in LTL the following properties:(a) Mutual exclusion, i.e., only one user at a time can use the printer.(b) Finite time of usage, i.e., a user can print only for a finite amount of time.(c) Absence of individual starvation, i.e., if a user wants to print something, he/she eventuallyis able to do so.(d) Absence of blocking, i.e., a user can always request to use the printer(e) Alternating access, i.e., users must strictly alternate in printing.Exercise 5.5.
Consider an elevator system that services N > 0 floors numbered 0 throughN −1. There is an elevator door at each floor with a call-button and an indicator light that signalswhether or not the elevator has been called. For simplicity consider N = 4. Present a set ofatomic propositions – try to minimize the number of propositions – that are needed to describethe following properties of the elevator system as LTL formulae and give the corresponding LTLformulae:(a) The doors are “safe”, i.e., a floor door is never open if the elevator is not present at the givenfloor.(b) A requested floor will be served sometime.Exercises303(c) Again and again the elevator returns to floor 0.(d) When the top floor is requested, the elevator serves it immediately and does not stop on theway there.Exercise 5.6. Which of the following equivalences are correct? Prove the equivalence or providea counterexample that illustrates that the formula on the left and the formula on the right are notequivalent.(a) ϕ → ♦ψ ≡ ϕ U (ψ ∨ ¬ϕ)(b) ♦ϕ → ♦ψ ≡ ϕ U (ψ ∨ ¬ϕ)(c) (ϕ ∨ ¬ψ) ≡ ¬♦(¬ϕ ∧ ψ)(d) ♦(ϕ ∧ ψ) ≡ ♦ϕ ∧ ♦ψ(e) ϕ ∧ ♦ϕ ≡ ϕ(f) ♦ϕ ∧ ϕ ≡ ♦ϕ(g) ♦ϕ → ♦ψ ≡ ϕ → ♦ψ(h) ¬(ϕ1 U ϕ2 ) ≡ ¬ϕ2 W (¬ϕ1 ∧ ¬ϕ2 )(i) ♦ ϕ1 ≡ ♦ ϕ2(j) (♦ ϕ1 ) ∧ (♦ ϕ2 ) ≡ ♦ ( ϕ1 ∧ ϕ2 )(k) (ϕ1 U ϕ2 ) U ϕ2 ≡ ϕ1 U ϕ2Exercise 5.7.
Let ϕ and ψ be LTL formulae. Consider the following new operators:(a) “At next” ϕ N ψ: at the next time where ψ holds, ϕ also holds.(b) “While” ϕ W ψ: ϕ holds as least as long as ψ does.(c) “Before” ϕ B ψ: if ψ holds sometime, ϕ does so before.Make the definitions of these informally explained operators precise by providing LTL formulaethat formalize their intuitive meanings.defExercise 5.8. We consider the release operator R which was defined by ϕ R ψ = ¬(¬ϕ U ¬ψ);see Section 5.1.5 on page 252 ff.(a) Prove the expansion law ϕ1 R ϕ2 ≡ ϕ2 ∧ (ϕ1 ∨ (ϕ1 ∧ ϕ2 )).304Linear Temporal Logic(b) Prove that ϕ R ψ ≡ (¬ϕ ∧ ψ) W (ϕ ∧ ψ).(c) Prove that ϕ1 W ϕ2 ≡ (¬ϕ1 ∨ ϕ2 ) R (ϕ1 ∨ ϕ2 ).(d) Prove that ϕ1 U ϕ2 ≡ ¬(¬ϕ1 R ¬ϕ2 ).Exercise 5.9. Consider the LTL formulaϕ = ¬ (a) → (a ∧ ¬c) U ¬( b) ∧ ¬(¬a ∨ ♦c).Transform ϕ into an equivalent LTL formula in PNF(a) using the weak-until operator W ,(b) using the release operator R .Exercise 5.10.
Provide an example for a sequence (ϕn ) of LTL formulae such that the LTLformula ψn is in weak-until PNF, ϕn ≡ ψn , and ψn is exponentially longer than ϕn . Use thetransformation rules in Section 5.1.5{ a, b }{b}s0s1s2{a}s5∅{b}{ a, b }s3s4Figure 5.25: Transition system for Exercise 5.11.Exercise 5.11. Consider the transition system TS in Figure 5.25 with the set AP = { a, b, c } ofatomic propositions.
Note that this is a single transition system with two initial states. Considerthe LTL fairness assumptionfair = ♦(a ∧ b) → ♦¬c ∧ ♦(a ∧ b) → ♦¬b .Questions:(a) Determine the fair paths in TS, i.e., the initial, infinite paths satisfying fair(b) For each of the following LTL formulae:ϕ1ϕ2ϕ3ϕ4ϕ5ϕ6======♦a ¬a −→ ♦aab U ¬bb W ¬b b U ¬bExercises305determine whether TS |=fair ϕi . In case TS |=fair ϕi , indicate a path π ∈ Paths(TS) forwhich π |= ϕi .Exercise 5.12.
Let ϕ = (a → ¬b) W (a ∧ b) and P = Words(ϕ) where AP = { a, b }.(a) Show that P is a safety property.(b) Define an NFA A with L(A) = BadPref(P ).(c) Now consider P = Words (a → ¬b) U (a ∧ b) . Decompose P into a safety property Psafeand a liveness property Plive such thatP = Psafe ∩ Plive .Show that Psafe is a safety and that Plive is a liveness property.{a}s2s0{ a, b }s3{a}s1∅Figure 5.26: Transition system for Exercise 5.14.Exercise 5.13.
Provide an NBA for each of the following LTL formulae:(a ∨ ¬ b) and ♦a ∨ ♦(a ↔ b) and (a ∨ ♦b).Exercise 5.14. Consider the transition system TS in Figure 5.26 with the atomic propositions{ a, b }. Sketch the main steps of the LTL model-checking algorithm applied to TS and the LTLformulaeϕ1 = ♦a → ♦b and ϕ2 = ♦(a ∧ a).To that end, carry out the following steps:(a) Depict an NBA Ai for ¬ϕi .(b) Depict the reachable fragment of the product transition system TS ⊗ Ai .(c) Explain the main steps of the nested DFS in TS ⊗ Ai by illustrating the order in which thestates are visited during the “outer” and “inner” DFS.306Linear Temporal Logictrueq0atruea∧bq1a∧bq2a∧b¬aq3aFigure 5.27: GNBA for Exercise 5.15.(d) If TS |= ϕi , provide the counterexample resulting from the nested DFS.{ a,b }Exerciseand the set 5.15.
Consider the GNBA G in Figure 5.27 with the alphabet Σ = 2F ={ q1 , q3 }, { q2 } of accepting sets.(a) Provide an LTL formula ϕ with Words(ϕ) = Lω (G). Justify your answer.(b) Depict the NBA A with Lω (A) = Lω (G).Exercise 5.16. Depict a GNBA G over the alphabet Σ = 2{ a,b,c } such thatLω (G) = Words (♦a → ♦b) ∧ ¬a ∧ (¬a W c) .Exercise 5.17. Let ψ = (a ↔ ¬a) and AP = { a }.(a) Show that ψ can be transformed into the following equivalent basic LTL formula#$ϕ = ¬ true U ¬ (a ∧ ¬a) ∧ ¬ (¬a ∧ ¬ ¬a) .The basic LTL syntax is given by the following context-free grammar:ϕ ::= true | a | ϕ1 ∧ ϕ2 | ¬ϕ | ϕ | ϕ1 U ϕ2 .(b) Compute all elementary sets with respect to closure(ϕ) (Hint: There are six elementarysets.)(c) Construct the GNBA Gϕ with Lω (Gϕ ) = Words(ϕ).
To that end:(i) Define its set of initial states and its acceptance component.(ii) For each elementary set B, define δ(B, B ∩ AP ).Exercise 5.18. Let AP = { a } and ϕ = (a ∧ a) U ¬a an LTL formula over AP.Exercises307(a) Compute all elementary sets with respect to ϕ.(Hint: There are five elementary sets.).(b) Construct the GNBA Gϕ such that Lω (Gϕ ) = Words(ϕ).Exercise 5.19. Consider the formula ϕ = a U (¬a ∧ b) and let G be the GNBA for ϕ thatis obtained through the construction explained in the proof of Theorem 4.56. What are theinitial states in G? What are the accept states in G? Provide an accepting run for the word{a}{a}{a, b}{b}ω. Explain why there are no accepting runs for the words {a}ω and {a}{a}{a, b}ω.(Hint: The answers to these questions can be given without depicting G.)Exercise 5.20.We consider the LTL formula ϕ = (a → (¬b U (a ∧ b))) over the setAP = { a, b } of atomic propositions and we want to check TS |= ϕ ∅for TS outlined on the right.s0(a) To check TS |= ϕ, convert ¬ϕ into an equivalent LTL formulaψ which is constructed according to the following grammar:Φ ::= true | false | a | b | Φ ∧ Φ | ¬Φ | Φ | Φ U Φ.s3{a}{b}s1s2{ a, b }Then construct closure(ψ).(b) Give the elementary sets w.r.t.
closure(ψ)!(c) Construct the GNBA Gψ .(d) Construct an NBA A¬ϕ directly from ¬ϕ, i.e., without relying on Gψ . (Hint: Four statessuffice.)(e) Construct TS ⊗ A¬ϕ .(f) Use the nested DFS algorithm to check TS |= ϕ. Therefore, sketch the algorithm’s mainsteps and interpret its outcome!Exercise 5.21.
The construction of a G from a given LTL formula in the proof of Theorem4.56 assumes an LTL formula that only uses the basic temporal modalities and U . Thederived operators ♦, , W and R can be treated by syntactic replacements of their definitions.Alternatively, and more efficient, is to treat them as basic modalities and to allow for formulae ♦ψ,ψ, ϕ1 W ϕ2 and ϕ1 R ϕ2 as elements of elementary sets of formulae and redefine the componentsof the constructed GNBA.Explain which modifications are necessary for such a ”direct” treatment of ♦ (eventually), (always), W (weak-until), and R (release). That is, which additional conditions do the elementarysets, the transition function δ, and the set F of accepting sets have to fulfill?308Linear Temporal LogicExercise 5.22. Let TS = (S, Act, →, S0 , AP, L) be a finite transition system without terminalstates and let wfair = ♦b1 → ♦b2 be a weak LTL fairness assumption with b1 , b2 ∈ AP.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
