5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 48
Текст из файла (страница 48)
Let AP = { a, b, c }. Consider the following NFA A (over the alphabet 2AP ) andthe following transition system TS:ExercisesA:221¬a¬b ∧ ¬caq0b ∧ ¬ccTS :cq1∅q3b ∧ ¬cq2αs1β¬b ∧ ¬cγ{b} s4γ{b, c}s2βγs3{a}αConstruct the product TS ⊗ A of the transition system and the NFA.Exercise 4.6. Consider the following transition system TSs0{ a, b }αs3{ a, c }βγ{ a, b, c }s1αγs4{ a, c }γ{ b, c }s2ββαs5{ a, b }and the regular safety propertyPsafe =“always if a is valid and b ∧ ¬c was valid somewhere before,then a and b do not hold thereafter at least until c holds”As an example, it holds:{ b }∅{ a, b }{ a, b, c }{ a, b }{ a, b }∅{ b, c }{ b }{ a, c }{ a }{ a, b, c }{ b }{ a, c }{ a, c }{ a }∈ pref(Psafe )∈ pref(Psafe )∈ BadPref(Psafe )∈ BadPref(Psafe )Questions:(a) Define an NFA A such that L(A) = MinBadPref(Psaf e ).(b) Decide whether T S |= Psaf e using the TS ⊗ A construction.Provide a counterexample if TS |= Psaf e .Exercise 4.7.
Prove or disprove the following equivalences for ω-regular expressions:222Regular Properties(a) (E1 + E2 ).Fω≡ E1 .Fω + E2 .Fω(b) E.(F1 + F2 )ωω≡ E.Fω1 + E.F2(c) E.(F.F∗ )ω(d) (E∗ .F)ω≡ E.Fω≡ E∗ .Fωwhere E, E1 , E2 , F, F1 , F2 are arbitrary regular expressions with ε ∈/ L(F) ∪ L(F1 ) ∪ L(F2 ).Exercise 4.8. Generalized ω-regular expressions are built from the symbols ∅ (to denote theempty language), ε (to denote the language {ε} consisting of the empty word), the symbols A forA ∈ Σ (for the singleton sets {A}) and the language operators “+” (union), “.” (concatenation),“∗” (Kleene star, finite repetition), and “ω”(infinite repetition).
The semantics of a generalizedω-regular expression G is a language Lg (G) ⊆ Σ∗ ∪ Σω , which is defined by• Lg (∅) = ∅, Lg (ε) = {ε}, Lg (A) = {A},• Lg (G1 + G2 ) = Lg (G1 ) ∪ Lg (G2 ) and Lg (G1 .G2 ) = Lg (G1 ).Lg (G2 ),• Lg (G∗ ) = Lg (G)∗ , and Lg (Gω ) = Lg (G)ω .Two generalized ω-regular expressions G and G are called equivalent iff Lg (G) = Lg (G ).Show that for each generalized ω-regular expression G there exists an equivalent generalized ωregular expression G of the formωG = E + E1 .Fω1 + . .
. En .Fnwhere E, E1 , . . . , En , F1 , . . . , Fn are regular expressions and ε ∈/ L(Fi ), i = 1, . . . , n.Exercise 4.9. Let Σ = { A, B }. Construct an NBA A that accepts the set of infinite words σover Σ such that A occurs infinitely many times in σ and between any two successive A’s an oddnumber of B’s occur.Exercise 4.10. Let Σ = { A, B, C } be an alphabet.(a) Construct an NBA A that accepts exactly the infinite words σ over Σ such that A occursinfinitely many times in σ and between any two successive A’s an odd number of B’s or anodd number of C’s occur. Moreover, between any two successive A’s either only B’s or onlyC’s are allowed.
That is, the accepted words should have the formwAv1 Av2 Av3 . . .where w ∈ { B, C }∗ , vi ∈ { B2k+1 | k 0 } ∪ { C2k+1 | k 0 } for all i > 0. Give also anω-regular expression for this language.Exercises223(b) Repeat the previous exercise such that any accepting word contains only finitely many C’s.(c) Change your automaton from part (a) such that between any two successive A’s an oddnumber of symbols from the set { B, C } may occur.(d) Same exercise as in (c), except that now an odd number of B’s and an odd number of C’smust occur between any two successive A symbols.Exercise 4.11. Depict an NBA for the language described by the ω-regular expression(AB + C)∗ ((AA + B)C)ω + (A∗ C)ω .224Regular PropertiesExercise 4.12.
Consider the following NBA A1 and A2 over the alphabet { A, B, C }:A2 :A1 :ACq1q0q2AAq1q2BB, C BCA, B, CBq0Cq3A, B, CAFind ω-regular expressions for the languages accepted by A1 and A2 .Exercise 4.13. Consider the NFA A1 and A2 :p4A1 :Ap3CABBAp0CAA2 :q0p1q2CCBq1BACq3Bq4p2A, BωConstruct an NBA for the language L(A1 ).L (A2 ) .Exercise 4.14. Let AP = { a, b }. Give an NBA for the LT property consisting of the infiniteωwords A0 A1 A2 .
. . 2AP such that∞/ Aj ).∃ j 0. (a ∈ Aj ∧ b ∈ Aj ) and ∃j 0. (a ∈ Aj ∧ b ∈Provide an ω-regular expression for Lω (A).Exercise 4.15. Let AP = {a, b, c}. Depict an NBA for the LT property consisting of the infiniteωwords A0 A1 A2 . . . 2AP such that∀j 0. A2j |= (a ∨ (b ∧ c))Exercises225Recall that A |= (a ∨ (b ∧ c)) means a ∈ A or {b, c} ⊆ A, i.e., A ∈ { { a }, { b, c }, { a, b, c } }.Exercise 4.16.
Consider NBA A1 and A2 depicted in Figure 4.26. Show that the powersetconstruction applied to A1 and A2 (viewed as NFA) yields the same deterministic automaton,while Lω (A1 ) = Lω (A2 ). (This exercise is taken from [408].)AAAAA(a)(b)Figure 4.26: NBA A1 (a) and A2 (b).Exercise 4.17.Consider the following NBA A with the alphabet Σ = 2AP where AP ={ a1 , . . . , an } for n > 0.¬ananq0qntrue¬a1q2an−1a1q1¬a2a2(a) Determine the accepted language Lω (A).(b) Show that there is no NBA A with Lω (A) = Lω (A ) and less than n states.(This exercise is inspired by [149].)226Regular PropertiesExercise 4.18. Provide an example for a regular safety property Psafe over AP and an NFA Afor its minimal bad prefixes such thatLω (A) = AP ω2\ Psafewhen A is viewed as an NBA.Exercise 4.19.answer.Provide an example for a liveness property that is not ω-regular.
Justify yourExercise 4.20. Is there a DBA that accepts the language described by the ω-regular expression(A + B)∗ (AB + BA)ω ? Justify your answer.Exercise 4.21. Provide an example for an ω-regular language L = Lk that is recognizable for aDBA such that the following two conditions are satisfied:(a) There exists an NBA A with |A| = O(k) and Lω (A) = L.(b) Each DBA A for L is of the size |A | = Ω(2k ).Hint: There is a simple answer to this question that uses the result that the regular language forthe expression (A + B)∗ B(A + B)k is recognizable by an NFA of size O(k), while any DFA hasΩ(2k ) states.Exercise 4.22.
Show that the class of languages that are accepted by DBAs is not closed undercomplementation.Exercise 4.23. Show that the class of languages that are accepted by DBAs is closed underunion. To do so, prove the following stronger statement:Let A1 and A2 be two DBAs both over the alphabet Σ. Show that there exists a DBA A with|A| = O(|A1 | · |A2 |) and Lω (A) = Lω (A1 ) ∪ Lω (A2 ).Exercise 4.24.Consider the GNBA outlined on the right with acceptancesets F1 = { q1 } and F2 = { q2 }.
Construct an equivalentNBA.BAq0q1BBBq2Exercises227Exercise 4.25. Provide NBA A1 and A2 for the languages given by the expressions (AC+B)∗ Bωand (B∗ AC)ω and apply the product construction to obtain a GNBA G with Lω (G) = Lω (A1 ) ∩Lω (A2 ). Justify that Lω (G) = ∅.Exercise 4.26.A nondeterministic Muller automaton is a quintuple A = (Q, Σ, δ, Q0 , F )whereQ,Σ,δ,Qareas for N BA and F ⊆ 2Q .
For an infinite run ρ of A, let lim(ρ) :=0∞q ∈ Q | ∃ i ≥ 0. ρ[i] = q . Let α ∈ Σω .A accepts α ⇐⇒ ex. infinite run ρ of A on α s.t. lim(ρ) ∈ F(a) Consider the following Muller automaton A with F = {{q2 , q3 }, {q1 , q3 }, {q0 , q2 }}:Bq1Cq0Aq2q3BCADefine the language accepted by A by means of an ω-regular expression.(b) Show that every GNBA G can be transformed into a nondeterministic Muller automaton Asuch that Lω (A) = Lω (G) by defining the corresponding transformation.Exercise 4.27.
Consider the transition systems TSSem and TSPet for mutual exclusion with asemaphore and the Peterson algorithm, respectively. Let Plive be the following ω-regular propertyover AP = { wait1 , crit1 }:“whenever process 1 is in its waiting location then it will eventually enter its critical section”ω(a) Depict an NBA for Plive and an NBA Ā for the complement property P̄live = 2AP \ Plive .(b) Show that TSSem |= Plive by applying the techniques explained in Section 4.4:(i) Depict the reachable fragment of the product TSSem ⊗ Ā(ii) Sketch the main steps of the nested depth-first search applied to TSSem ⊗ Ā for thepersistence property “eventually forever ¬F ” where F is the acceptance set of Ā.Which counterexample is returned by Algorithm ?8(c) Apply now the same techniques (product construction, nested DFS) to show that TSPet |=Plive .Exercise 4.28.
The nested depth-first search approach can also be reformulated for an emptinesscheck for NBA. The path fragment returned by Algorithm 8 in case of a negative answer then yieldsa prefix of an accepting run.228Regular PropertiesConsider the automaton shown in Exercise 4.24 as an NBA, i.e., the acceptance set is F = { q1 , q2 }.Apply the nested depth-first search approach to verify that Lω (A) = ∅.Chapter 5Linear Temporal LogicThis chapter introduces (propositional) linear temporal logic (LTL), a logical formalismthat is suited for specifying LT properties. The syntax and semantics of linear temporallogic are defined.
Various examples are provided that show how linear temporal logiccan be used to specify important system properties. The second part of the chapter isconcerned with a model-checking algorithm—based on Büchi automata—for LTL. Thisalgorithm can be used to answer the question: given a transition system TS and LTLformula ϕ, how to check whether ϕ holds in TS?5.1Linear Temporal LogicFor reactive systems, correctness depends on the executions of the system—not only onthe input and output of a computation—and on fairness issues.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
