5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 42
Текст из файла (страница 42)
= (AB)ω , theautomaton in Figure 4.17 can enter the accept state q1 after the second, fourth, sixth,etc., symbol by staying in q0 for the first 2n−1 symbols and moving with the nth B tostate q1 (for n = 1, 2, . . .). Thus, at infinitely many positions there is the possibility toenter F , although there is no run that visits q1 infinitely often, since whenever q1 hasbeen entered the automaton A rejects when reading the next A. In fact, the powersetconstruction applied to the NBA A in Figure 4.17 yields a DBA Adet with two reachablestates (namely {q0 } and {q0 , q1 }) for the language consisting of all infinite words withinfinitely many B’s, but not for the language given by (A + B)∗ Bω .Another example that illustrates why the powerset construction fails for Büchi automatais provided in Exercise 4.16 (page 225).4.3.4Generalized Büchi AutomataIn several applications, other ω-automata types are useful as automata models for ωregular languages.
In fact, there are several variants of ω-automata that are equallyexpressive as nondeterministic Büchi automata, although they use more general acceptanceconditions than the Büchi acceptance condition ”visit infinitely often the acceptance setF ”. For some of these ω-automata types, the deterministic version has the full power ofω-regular languages. These automata types are not relevant for the remaining chapters ofthis monograph and will not be treated here. 4For the purposes of this monograph, it suffices to consider a slight variant of nondeterministic Büchi automata, called generalized nondeterministic Büchi automata, or GNBAfor short.
The difference between an NBA and a GNBA is that the acceptance conditionfor a GNBA requires to visit several sets F1 , . . . , Fk infinitely often. Formally, the syntaxof a GNBA is as for an NBA, except that the acceptance condition is a set F consistingof finitely many acceptance sets F1 , .
. . , Fk with Fi ⊆ Q. That is, if Q is the state space ofQthe automaton then the acceptance condition of a GNBA is an element F of 22 . Recall4In Chapter 10, deterministic Rabin automata will be used for representing ω-regular properties.Automata on Infinite Words193that for an NBA, it is an element F ∈ 2Q . The accepted language of a GNBA G consistsof all infinite words which have an infinite run in G that visits all sets Fi ∈ F infinitelyoften. Thus, the acceptance criterion in a generalized Büchi automaton can be understoodas the conjunction of a number of Büchi acceptance conditions.Definition 4.52.Generalized NBA (GNBA)A generalized NBA is a tuple G = (Q, Σ, δ, Q0 , F) where Q, Σ, δ, Q0 are defined as for anNBA (see Definition 4.27 on page 174) and F is a (possibly empty) subset of 2Q .The elements F ∈ F are called acceptance sets.
Runs in a GNBA are defined as for anNBA. That is, a run in G for the infinite word A0 A1 . . . ∈ Σω is an infinite state sequenceq0 q1 q2 . . . ∈ Qω such that q0 ∈ Q0 and qi+1 ∈ δ(qi , Ai ) for all i 0.The infinite run q0 q1 q2 . . . is called accepting if∞∀ F ∈ F. ∃ j ∈ IN. qj ∈ F .The accepted language of G is:Lω (G) = { σ ∈ Σω | there exists an accepting run for σ in G }.Equivalence of GNBAs and the size of a GNBA are defined as for NBAs. Thus, GNBA Gand G are equivalent if Lω (G) = Lω (G ). The size of GNBA G, denoted |G|, equals thenumber of states and transitions in G.Example 4.53.GNBAFigure 4.19 shows a GNBA G over the alphabet 2AP where AP = { crit1 , crit2 } with theacceptance sets F1 = { q1 } and F2 = { q2 }. That is, F = {{ q1 }, { q2 }}. The acceptedlanguage is the LT property Plive consisting of all infinite words A0 A1 A2 .
. . ∈ (2AP )ωsuch that the atomic propositions crit1 and crit2 hold infinitely often (possibly at differentpositions), i.e.,∞∃ j 0. crit1 ∈ Ajand∞∃ j 0. crit2 ∈ Aj .Thus, Plive formalizes the property ”both processes are infinitely often in their criticalsection”. Let us justify that indeed Lω (G) = Plive . This goes as follows.”⊆”: Each accepting run has to pass infinitely often through the edges (labeled with crit1or crit2 ) leading to the states q1 and q2 .
Thus, in every accepted word σ = A0 A1 A2 . . . ∈194Regular Propertiescrit2trueq1q0q2truecrit1trueFigure 4.19: GNBA for “infinitely often processes 1 and 2 are in their critical section”.Lω (G) the atomic propositions crit1 and crit2 occur infinitely often as elements of the setsAi ∈ 2AP . Thus, σ ∈ Plive .”⊇”: Let σ = A0 A1 A2 . . . ∈ Plive .
Since both propositions crit1 and crit2 occur infinitelyoften in the symbols Ai , the GNBA G can behave for the input word σ as follows. G remainsin state q0 until the first input symbol Ai with crit1 ∈ Ai appears. The automaton thenmoves to state q1 .
From there, G consumes the next input symbol Ai+1 and returns to q0 .It then waits in q0 until a symbol Aj with crit2 ∈ Aj occurs, in which case the automatonmoves to state q2 for the symbol Aj and returns to q0 on the next symbol Aj+1 . Now thewhole procedure restarts, i.e., G stays in q0 while reading the symbols Aj+1 , . . . , A−1 andmoves to q1 as soon as the current input symbol A contains crit1 .
And so on. In thisway, G generates an accepting run of the formq0k1 q1 q0k2 q2 q0k3 q1 q0k4 q2 q0k5 . . .for the input word σ. These considerations show that Plive ⊆ Lω (G).Remark 4.54.No Acceptance SetThe set F of acceptance sets of a GNBA may be empty. If F = ∅ then σ ∈ Lω (G) ifand only if there exists an infinite run for σ in G. We like to stress the difference withNBA with an empty set of accepting states. For an NBA A = (Q, Σ, δ, Q0 , ∅) there are noaccepting runs. Therefore, the language Lω (A) is empty. Contrary to that, every infiniterun of a GNBA G = (Q, Σ, δ, Q0 , ∅) is accepting.In fact, every GNBA G is equivalent to a GNBA G having at least one acceptance set.This is due to the fact that the state space Q can always be added to the set F of theacceptance sets without affecting the accepted language of the GNBA.
Formally, for GNBAG = (Q, Σ, δ, Q0 , F) let GNBA G = (Q, Σ, δ, Q0 , F ∪ {Q}). Then it easily follows that:Lω (G) = Lω (G ).Automata on Infinite WordsRemark 4.55.195Nonblocking GNBAAs for NBAs, each GNBA G can be replaced with an equivalent GNBA G , in which allpossible behaviors for a given infinite input word yield an infinite run. Such a GNBAG can be constructed by inserting a nonaccept trapping state, as we did for NBA in theremark on page 187.Obviously, every NBA can be understood as a GNBA with exactly one acceptance set.Conversely, every GNBA can be transformed into an equivalent NBA:Theorem 4.56.From GNBA to NBAFor each GNBA G there exists an NBA A with Lω (G) = Lω (A) and |A| = O(|G| · |F|)where F denotes the set of acceptance sets in G.Proof: Let G = (Q, Σ, δ, Q0 , F) be a GNBA. According to the remark on page 194, we mayassume without loss of generality that F = ∅.
Let F = {F1 , . . . , Fk } where k 1. Thebasic idea of the construction of A is to create k copies of G such that the acceptance set Fiof the ith copy is connected to the corresponding states of the (i+1)th copy. The acceptingQ0...F2FkF1Figure 4.20: Idea for transforming a GNBA into an NBA.condition for A consists of the requirement that an accepting state of the first copy is visitedinfinitely often. This ensures that all other accepting sets Fi of the k copies are visitedinfinitely often too, see Figure 4.20 on page 195. Formally, let A = (Q , Σ, δ , Q0 , F )where:Q = Q × { 1, . .
. , k },Q0 = Q0 × { 1 } = { q0 , 1 | q0 ∈ Q0 }, andF = F1 × { 1 } = { qF , 1 | qF ∈ F1 }.196Regular PropertiesThe transition function δ is given by { q , i | q ∈ δ(q, A) }if q ∈ Fiδ (q, i, A) ={ q , i+1 | q ∈ δ(q, A) } otherwise.We thereby identify q, k+1 and q, 1. It is not difficult to check that A can be constructed in time and space O(|G| · |F|) where |F| = k is the number of acceptance sets inG. The fact Lω (G) = Lω (A) can be seen as follows.⊇: For a run of A to be accepting it has to visit some state q, 1 infinitely often, whereq ∈ F1 .
As soon as a run reaches q, 1, the NBA A moves to the second copy. From thesecond copy the next copy can be reached by visiting q , 2 with q ∈ F2 . NBA A can onlyreturn to q, 1 if it goes through all k copies. This is only possible if it reaches an acceptstate in each copy since that is the only opportunity to move to the next copy. So, for arun to visit q, 1 infinitely often it has to visit some accept state in each copy infinitelyoften.⊆: By a similar reasoning it can be deduced that every word in Lω (G) is also acceptingin A.Example 4.57.Transformation of a GNBA into an NBAConsider the GNBA G described in Example 4.53 on page 193.
The construction indicatedin the proof of Theorem 4.56 provides an NBA consisting of two copies (as there are twoaccept sets) of G, see Figure 4.21. For example,δ (q0 , 1, { crit1 }) = { q0 , 1, q1 , 1 },/ F1 = { q1 } and δ (q2 , 2, A) = { q0 , 1 }, since F2 = { q2 }.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
