5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 40
Текст из файла (страница 40)
In order to obtain an NBA recognizing (A∗ B)ω , we first apply the transformationAutomata on Infinite Words181Aq0ABq1qnewAq0Bq1BBqnewAAq0Bq1BBFigure 4.12: From an NFA accepting A∗ B to an NBA accepting (A∗ B)ω .as described in the proof of Lemma 4.34 to remove initial states that have an incomingtransition. This yields the NFA depicted in the right upper part of Figure 4.12. Thisautomaton can now be used to apply the construction of the required NBA as detailed inthe proof of Lemma 4.34.
This yields the NBA depicted in the lower part of Figure 4.12.It remains to provide a construction for task (3) above. Assume that we have NFA A forthe regular language L(A) and a given NBA A at our disposal. The proof of the followinglemma will describe a procedure to obtain an NBA for the ω-language L(A).Lω (A ).Lemma 4.36.Concatenation of an NFA and an NBAFor NFA A and NBA A (both over the alphabet Σ), there exists an NBA A withLω (A ) = L(A).Lω (A )and|A | = O(|A| + |A |).Proof: Let A = (Q, Σ, δ, Q0 , F ) be an NFA and A = (Q , Σ, δ , Q0 , F ) an NBA withQ ∩ Q = ∅. Let A = (Q , Σ, δ , Q0 , F ) be the following NBA. The state space isQ = Q ∪ Q .
The set of initial and accept states are given byQ0if Q0 ∩ F = ∅Q0 =otherwise,Q0 ∪ Q0182Regular Propertiesand F = F (set of accept state in the NBA A ). The transition function δ is given by⎧if q ∈ Q and δ(q, A) ∩ F = ∅⎨ δ(q, A)δ(q, A) ∪ Q0if q ∈ Q and δ(q, A) ∩ F = ∅δ (q, A) =⎩ if q ∈ Qδ (q, A)It is now easy to check that A fulfills the desired conditions.Example 4.37.Concatenation of an NFA and an NBAConsider the NFA A and the NBA A depicted in the left and right upper part of Figure 4.13, respectively. We have L(A) = (AB)∗ and L(A ) = (A+B)∗ BAω . Applying thetransformation as described in Lemma 4.36 yields the NBA depicted in the lower part ofFigure 4.13.
It is not difficult to assess that this NBA accepts indeed the concatenatedlanguage (AB)∗ (A+B)∗ BAω .AABBABBABBAABFigure 4.13: Concatenation of an NFA and an NBA.By Lemmas 4.33, 4.34, and 4.36 we obtain the first part for the proof of Theorem 4.32:Corollary 4.38.NBA for ω-Regular LanguagesFor any ω-regular language L there exists an NBA A with Lω (A) = L.Automata on Infinite Words183The proof of the following lemma shows that the languages accepted by NBA can bedescribed by an ω-regular expression.Lemma 4.39.NBAs Accept ω-Regular LanguagesFor each NBA A, the accepted language Lω (A) is ω-regular.Proof: Let A = (Q, Σ, δ, Q0 , F ) be an NBA. For states q, p ∈ Q, let Aqp be the NFA(Q, Σ, δ, { q }, { p }). Then, Aqp recognizes the regular language consisting of all finitewords w ∈ Σ∗ that have a run in A leading from q to p, that is,defLqp = L(Aqp ) = { w ∈ Σ∗ | p ∈ δ∗ (q, w) }.Consider a word σ ∈ Lω (A) and an accepting run q0 q1 .
. . for σ in A. Some accept stateq ∈ F appears infinitely often in this run. Hence, we may split σ into nonempty finitesubwords w0 , w1 , w2 , w3 , . . . ∈ Σ∗ such that w0 ∈ Lq0q and wk ∈ Lqq for all k 1 andσ =w0 w1 w2 w3 . . . . . . ∈Lq0 q ∈Lqq ∈Lqq ∈LqqOn the other hand, any infinite word σ which has the form σ = w0 w1 w2 . . . wherethe wk ’s are nonempty finite words with w0 ∈ Lq0q for some initial state q0 ∈ Q0 and{w1 , w2 , w3 , . . .} ⊆ Lqq for some accept state q ∈ F has an accepting run in A. This yieldsσ ∈ Lω (A) if and only if ∃q0 ∈ Q0 ∃q ∈ F. σ ∈ Lq0 q (Lqq \ {ε})ω .Hence, Lω (A) agrees with the languageLq0q .
(Lqq \ {ε})ωq0 ∈Q0 ,q∈Fwhich is ω-regular.Example 4.40.From NBA to ω-Regular ExpressionFor the NBA A shown in Figure 4.7 on page 175, a corresponding ω-regular expression isobtained byLq1 q3 .(Lq3 q3 \ {ε})ωsince q1 is the unique initial state and q3 the unique accept state in A.
The regularlanguage Lq3 q3 \ {ε} can be described by the expression (B+ + BC∗ AB)+ , while Lq1 q3 isgiven by (C∗ AB(B∗ +BC∗ AB)∗ B)∗ C∗ AB. Hence, Lω (A) = Lω (G) where G is the ω-regularexpression:G = (C∗ AB(B∗ + BC∗ AB)∗ B)∗ C∗ AB ((B+ + BC∗ AB)+ )ω .Lq1 q3(Lq3 q3 \{ε})ω184Regular PropertiesThe thus obtained expression G can be simplified to the equivalent expression:C∗ AB(B+ + BC∗ AB)ω .The above lemma, together with Corollary 4.38, completes the proof of Theorem 4.32stating the equivalence of the class of languages accepted by NBAs and the class of allω-regular languages.
Thus, NBAs and ω-regular languages are equally expressive.A fundamental question for any type of automata model is the question whether for a givenautomaton A the accepted language is empty. For nondeterministic Büchi automata,an analysis of the underlying directed graph by means of standard graph algorithms issufficient, as we will show now.Lemma 4.41.Criterion for the Nonemptiness of an NBALet A = (Q, Σ, δ, Q0 , F ) be an NBA. Then, the following two statements are equivalent:(a) Lω (A) = ∅,(b) There exists a reachable accept state q that belongs to a cycle in A.
Formally,∃q0 ∈ Q0 ∃q ∈ F ∃w ∈ Σ∗ ∃v ∈ Σ+ . q ∈ δ∗ (q0 , w) ∩ δ∗ (q, v).Proof: (a) =⇒ (b): Let σ = A0 A1 A2 . . . ∈ Lω (A) and let q0 q1 q2 . . . be an acceptingrun for σ in A. Let q ∈ F be an accept state with q = qi for infinitely many indicesi. Let i and j be two indices with 0 i < j and qi = qj = q.
We consider the finitewords w = A0 A1 . . . Ai−1 and v = Ai Ai+1 . . . Aj−1 and obtain q = qi ∈ δ∗ (q0 , w) andq = qj ∈ δ∗ (qi , v) = δ∗ (q, v). Hence, (b) holds.(b) =⇒ (a): Let q0 , q, w, v be as in statement (b). Then, the infinite word σ = wvω has arun of the form q0 . . . q . . . q . . . q . . . that infinitely often contains q. Since q ∈ F this runis accepting which yields σ ∈ Lω (A), and thus, Lω (A) = ∅.By the above lemma, the emptiness problem for NBAs can be solved by means of graphalgorithms that explore all reachable states and check whether they belong to a cycle. Onepossibility to do so is to calculate the strongly connected components of the underlyingdirected graph of A and to check whether there is at least one nontrivial strongly con-Automata on Infinite Words185nected component3 that is reachable (from at least one of the initial states) and containsan accept state.
Since the strongly connected components of a (finite) directed graph canbe computed in time linear in the number of states and edges, the time complexity of thisalgorithm for the emptiness check of NBA A is linear in the size of A. An alternativealgorithm that also runs in time linear in the size of A, but avoids the explicit computation of the strongly connected components, can be derived from the results stated inSection 4.4.2.Theorem 4.42.Checking Emptiness for NBAThe emptiness problem for NBA A can be solved in time O(|A|).Since NBAs serve as a formalism for ω-regular languages, we may identify two Büchiautomata for the same language:Definition 4.43.Equivalence of NBALet A1 and A2 be two NBAs with the same alphabet.
A1 and A2 are called equivalent,denoted A1 ≡ A2 , if Lω (A1 ) = Lω (A2 ).Example 4.44.Equivalent NBAAs for other finite automata, equivalent NBAs can have a totally different structure. Forexample, consider the NBA shown in Figure 4.14 over the alphabet 2AP where AP ={ a, b }. Both NBAs represent the liveness property “infinitely often a and infinitely oftenb”, and thus, they are equivalent.Remark 4.45.NFA vs. NBA EquivalenceIt is interesting to consider more carefully the relationship between the notions of equivalence of NFAs and NBAs. Let A1 and A2 be two automata that we can regard as eitherNFA or as NBA. To distinguish the equivalence symbol ≡ for NFAs from that for NBAs wewill write in this example ≡NFA to denote the equivalence relation for NFA and the symbol≡NBA to denote the equivalence relation for NBA, i.e., A1 ≡NFA A2 iff L(A1 ) = L(A2 )and A1 ≡NBA A2 iff Lω (A1 ) = Lω (A2 ).1.
If A1 and A2 accept the same finite words, i.e., A1 ≡NFA A2 , then this does notmean that they also accept the same infinite words. The following two automataexamples show this:3A strongly connected component is nontrivial if it contains at least one edge. In fact, any cycle iscontained in a nontrivial strongly connected component, and vice versa, any nontrivial strongly connectedcomponent contains a cycle that goes through all its states.186Regular Propertiestrueq0truebq2ap0trueq1ap1truep3p2b¬a¬btrueFigure 4.14: Two equivalent NBA.AAAAA2A1We have L(A1 ) = L(A2 ) = { An | n 1 }, but Lω (A1 ) = { Aω } and Lω (A2 ) = ∅.Thus, A1 ≡NFA A2 but A1 ≡NBA A2 .2. If A1 and A2 accept the same infinite words, i.e., A1 ≡NBA A2 , then one mightexpect that they would also accept the same finite words.
This also turns out notto be true. The following example shows this:AAA1AAA2We have Lω (A1 ) = Lω (A2 ) = { Aω }, but L(A1 ) = { A2n | n 0 } and L(A2 ) ={ A2n+1 | n 0 }.3. If A1 and A2 are both deterministic (see Definition 4.9 on page 156), then A1 ≡NFAA2 implies A1 ≡NBA A2 . The reverse is, however, not true, as illustrated by theprevious example.Automata on Infinite Words187For technical reasons, it is often comfortable to assume for an NBA that for each state qand for each input symbol A, there is a possible transition. Such an NBA can be seen to benonblocking since no matter how the nondeterministic choices are resolved, the automatoncannot fail to consume the current input symbol.Definition 4.46.Nonblocking NBALet A = (Q, Σ, δ, Q0 , F ) be an NBA.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
