5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 39
Текст из файла (страница 39)
The word Cω has onlyBCq1Aq2Bq3BFigure 4.7: An example of an NBA.one run in A, namely q1 q1 q1 q1 . . ., or in short, q1ω . Some other runs are q1 q2 q3ω for theword ABω , (q1 q1 q2 q3 )ω for the word (CABB)ω , and (q1 q2 q3 )n q1ω for the word (ABB)n Cωwhere n 0.The runs that go infinitely often through the accept state q3 are accepting. For instance,q1 q2 q3ω and (q1 q1 q2 q3 )ω are accepting runs. q1ω is not an accepting run as it never visitsthe accept state q3 , while runs of the form (q1 q2 q3 )n q1ω are not accepting as they visit theaccept state q3 only finitely many times. The language accepted by this NBA is given bythe ω-regular expression:ωC∗ AB B+ + BC∗ ABLater in this chapter (page 198 ff.), NBAs are used for the verification of ω-regular properties – in the same vein as NFAs were exploited for the verification of regular safetyproperties. In that case, Σ is of the form Σ = 2AP .
As explained on page 159, propositional logic formulae are used as a shorthand notation for the transitions of such NBAs.For instance, if AP = { a, b }, then the label a ∨ b for an edge from q to p means that thereare three transitions from q to p: one for the symbol { a }, one for the symbol { b }, andone for the symbol { a, b }.176Example 4.29.Regular PropertiesInfinitely Often GreenLet AP = { green, red } or any other set containing the proposition green.
The language ofwords σ = A0 A1 . . . ∈ 2AP satisfying the LT property “infinitely often green” is acceptedby the NBA A depicted in Figure 4.8.greenq0¬greenq1¬greengreenFigure 4.8: An NBA accepting “infinitely often green”.The automaton A is in the accept state q1 if and only if the last input set of symbols(i.e., the last set Ai ) contains the propositional symbol green. Therefore, Lω (A) is exactlythe set of all infinite words A0 A1 .
. . with infinitely many sets Ai with green ∈ Ai . Forexample, for the input wordσ = { green } { } { green } { } { green } { } . . .we obtain the accepting run q0 q1 q0 q1 . . .. The same run q0 q1 q0 q1 . . . is obtained for thewordσ = ({ green, red } { } { green } { red })ωor any other word A0 A1 A2 .
. . ∈ (2AP )ω with green ∈ A2j and green ∈/ A2j+1 for allj 0.Example 4.30.Request ResponseMany liveness properties are of the form“Whenever some event a occurs,some event b will eventually occur in the future”For example, the property “once a request is provided, eventually a response occurs” is ofthis form. An associated NBA with propositions req and resp is indicated in Figure 4.9.It is assumed that { req, resp } ⊆ AP, i.e., we assume the NBA to have alphabet 2AP withAP containing at least req and resp.
It is not difficult to see that this NBA accepts exactlythose sequences in which each request is always eventually followed by a response. Notethat an infinite trace in which only responses occur, but never a request (or finitely manyrequests) is also accepting.Automata on Infinite Words177req ∧ ¬respq0¬req ∨ respq1resp¬respFigure 4.9: An NBA accepting “on each request, eventually a response is provided”.Remark 4.31.NBA and Regular Safety PropertiesIn Section 4.2, we have seen that there is a strong relationship between bad prefixes ofregular safety properties and NFAs. In fact, there is also a strong relationship betweenNBAs and regular safety properties. This can be seen as follows. Let Psafe be a regularsafety property over AP and A = (Q, 2AP , δ, Q0 , F ) an NFA recognizing the language ofall bad prefixes of Psafe .
Each accept state qF ∈ F may be assumed to be a trapping state,A→ qF for all A ⊆ AP. This assumption is justified since each extension of a badi.e., qF −−prefix is a bad prefix. (As a bad prefix contains a ”bad” event that causes the violationof Psafe , each extension of this prefix contains this event.)When interpreting A as an NBA, it accepts exactly the infinite words σ ∈ (2AP )ω thatviolate Psafe , i.e.,Lω (A) = (2AP )ω \ Psafe .Here, it is important that A accepts all bad prefixes, and not just the minimal ones (seeExercise 4.18).If A is a total deterministic automaton, i.e., in each state there is a single possible transitionfor each input symbol, then the NBA obtained byA = Q, 2AP , δ, Q0 , Q \ F accepts the language Lω A = Psafe .This is exemplified by means of a concrete case.
Consider again the property “a redlight phase should be immediately preceded by a yellow light phase” for a traffic lightsystem. We have seen before (see Example 4.13 on page 161) that the bad prefixes ofthis safety property constitute a regular language and are accepted by the NFA shownin Figure 4.10. Note that this NFA is total. Applying the procedure described justabove to this automaton yields the NBA depicted in Figure 4.11. It is easy to see thatthe infinite language accepted by this NBA consists exactly of all sequences of the formσ = A0 A1 A2 . .
. such that red ∈ Aj implies j > 0 and yellow ∈ Aj−1 .The accepted languages of the NBA examples have so far been ω-regular. It is now shown178Regular Propertiesq1yellow¬yellow¬red ∧ yellowq0red¬red ∧ ¬yellowq2trueFigure 4.10: An NFA for the set of all bad prefixes of Psafe .q1yellow¬yellow¬red ∧ yellowq0¬red ∧ ¬yellowredq2trueFigure 4.11: An NBA for the LT property “red should be preceded by yellow”.that this holds for any NBA. Moreover, it will be shown that any ω-regular language canbe described by an NBA. Thus, NBAs are as expressive as ω-regular languages. Thisresult is analogous to the fact that NFAs are as expressive as regular languages, and thusmay act as an alternative formalism to describe regular languages.
In the same spirit,NBAs are an alternative formalism for describing ω-regular languages. This is capturedby the following theorem.Theorem 4.32.NBAs and ω-Regular LanguagesThe class of languages accepted by NBAs agrees with the class of ω-regular languages.The proof of Theorem 4.32 amounts to showing that (1) any ω-regular language is recognized by an NBA (see Corollary 4.38 on page 182) and (2) that the language Lω (A)accepted by the NBA A is ω-regular (see Lemma 4.39 on page 183).We first consider the statement that ω-regular languages are contained in the class oflanguages recognized by an NBA. The proof of this fact is divided into the followingthree steps that rely on operations for NBAs to mimic the building blocks of ω-regularexpressions:(1) For any NBA A1 and A2 there exists an NBA accepting Lω (A1 ) ∪ Lω (A2 ).(2) For any regular language L (of finite words) with ε ∈/ L there exists an NBA acceptingLω .Automata on Infinite Words179(3) For regular language L and NBA A there exists an NBA accepting L.Lω (A ).These three results that are proven below form the basic ingredients to construct anNBA for a given ω-regular expression G = E1 .Fω1 + .
. . + En .Fωn with ε ∈ Fi . This works asfollows. As an initial step, (2) is exploited to construct NBA A1 , . . . , An for the expressionsFω1 , . . . , Fωn . Then, (3) is used to construct an NBA for the expressions Ei .Fωi , for 1 i n.Finally, these NBA are combined using (1) to obtain an NBA for G.Let us start with the union operator on two NBAs. Let A1 = (Q1 , Σ, δ1 , Q0,1 , F1 ) andA2 = (Q2 , Σ, δ2 , Q0,2 , F2 ) be NBAs over the same alphabet Σ. Without loss of generality,it may be assumed that the state spaces Q1 and Q2 of A1 and A2 are disjoint, i.e.,Q1 ∩ Q2 = ∅.
Let A1 + A2 be the NBA with the joint state spaces of A1 and A2 , andwith all transitions in A1 and A2 . The initial states of A are the initial states of A1 andA2 , and similarly, the accept states of A are the accept states of A1 and A2 . That is,A1 + A2 = (Q1 ∪ Q2 , Σ, δ, Q0,1 ∪ Q0,2 , F1 ∪ F2 )where δ(q, A) = δi (q, A) if q ∈ Qi for i=1, 2. Clearly, any accepting run in Ai is also anaccepting run in A1 + A2 , and vice versa, each accepting run in A1 + A2 is an acceptingrun in either A1 or A2 . This yields Lω (A1 + A2 ) = Lω (A1 ) ∪ Lω (A2 ). We thus obtain:Lemma 4.33.Union Operator on NBAFor NBA A1 and A2 (both over the alphabet Σ) there exists an NBA A such that:Lω (A) = Lω (A1 ) ∪ Lω (A2 )and|A| = O(|A1 | + |A2 |).Now consider (2).
We will show that for any regular language L ⊆ Σ∗ there exists an NBAover the alphabet Σ that accepts the ω-regular language Lω . To do so, we start with arepresentation of L by an NFA A.Lemma 4.34.ω-Operator for NFAFor each NFA A with ε ∈/ L(A) there exists an NBA A such thatLω (A ) = L(A)ωand|A | = O(|A|)./ L(A). Without loss of generality, weProof: Let A = (Q, Σ, δ, Q0 , F ) be an NFA with ε ∈may assume that all initial states in A have no incoming transitions and are not accepting.180Regular PropertiesAny A that does not possess this property, can be modified into an equivalent NFA asA→ q iffollows. Add a new initial (nonaccept) state qnew to Q with the transitions qnew −−Aand only if q0 −−→ q for some initial state q0 ∈ Q0 .
All other transitions, as well as theaccept states, remain unchanged. The state qnew is the single initial state of the modifiedNFA, is not accept, and, clearly, has no incoming transitions. This modification neitheraffects the accepted language nor the asymptotic size of A.In the sequel, we assume that A = (Q, Σ, δ, Q0 , F ) is an NFA such that the states inQ0 do not have any incoming transitions and Q0 ∩ F = ∅. We now construct an NBAA = (Q, Σ, δ , Q0 , F ) with Lω (A ) = L(A)ω . The basic idea of the construction of A isto add for any transition in A that leads to an accept state new transitions leading to theinitial states of A. Formally, the transition relation δ in the NBA A is given byδ(q, A)if δ(q, A) ∩ F = ∅δ (q, A) =δ(q, A) ∪ Q0 otherwise.The initial states in the NBA A agree with the initial states in A, i.e., Q0 = Q0 .
Theseare also the accept states in A , i.e., F = Q0 .Let us check that Lω (A ) = L(A)ω . This is proven as follows.⊆: Assume that σ ∈ Lω (A ) and let q0 q1 q2 . . . be an accepting run for σ in A . Hence,qi ∈ F = Q0 for infinitely many indices i. Let i0 = 0 < i1 < i2 < . . . be the strictly/ Q0 for allincreasing sequence of natural numbers with { qi0 , qi1 , qi2 , . . . } ⊆ Q0 and qj ∈j ∈ IN \ { i0 , i1 , i2 , . . . }. The word σ can be divided into infinitely many nonempty finitesubwords wi ∈ Σ∗ yielding σ = w1 w2 w3 . .
. such that qik ∈ δ ∗ (qik−1 , wk ) for all k 1.(The extension of δ to a function δ ∗ : Q × Σ∗ → 2Q is as for an NFA, see page 154.) Bydefinition of A and since the states qik ∈ Q0 do not have any predecessor in A, we getδ ∗ (qik−1 , wk ) ∩ F = ∅. This yields wk ∈ L(A) for all k 1, which gives us σ ∈ L(A)ω .⊇: Let σ = w1 w2 w3 . . . ∈ Σω such that wk ∈ L(A) for all k 1. For each k, we choose anaccepting run q0k q1k . .
. qnk k for wk in A. Hence, q0k ∈ Q0 and qnk k ∈ F . By definition of A ,we have q0k+1 ∈ δ ∗ (q0k , wk ) for all k 1. Thus,q01 . . . qn1 1 −1 q02 . . . qn2 2 −1 q03 . . . qn3 3 −1 . . .is an accepting run for σ in A . Hence, σ ∈ Lω (A ).Example 4.35.ω-Operator for an NFAConsider the NFA depicted in the left upper part of Figure 4.12. It accepts the languageA∗ B.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
