5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 41
Текст из файла (страница 41)
A is called nonblocking if δ(q, A) = ∅ for all statesq and all symbols A ∈ Σ.Note that for a given nonblocking NBA A and input word σ ∈ Σω , there is at least one(infinite) possibly nonaccepting run for σ in A. The following remark demonstrates thatit is not a restriction to assume a nonblocking NBA.Remark 4.47.Nonblocking NBAFor each NBA A there exists a nonblocking NBA trap(A) with |trap(A)| = O(|A|) andA ≡ trap(A).Let us see how such a nonblocking NBA can be derived from A.
NBA trap(A) is obtainedfrom A by inserting a nonaccept trapping state qtrap equipped with a self-loop for eachsymbol in the alphabet Σ. For every symbol A ∈ Σ for which state q in A does not havean outgoing transition, a transition to qtrap is added. Formally, if A = (Q, Σ, δ, Q0 , F ),then trap(A) = (Q , Σ, δ , Q0 , F ) as follows. Here, Q = Q ∪ { qtrap } where qtrap is a newstate (not in Q) that will be reached in A whenever A does not have a correspondingtransition. Formally, the transition relation δ of trap(A) is defined by:δ(q, A)if q ∈ Q and δ(q, A) = ∅δ (q, A) =otherwise{ qtrap }The initial and accept states are unchanged, i.e., Q0 = Q0 and F = F .
By definition,trap(A) is nonblocking and – since the new trap state is nonaccepting – is equivalent toA.We conclude this subsection on automata over infinite words with a few more commentson Büchi automata and ω-regular languages. We first study the subclass of deterministicBüchi automata (Section 4.3.3 below) and then in Section 4.3.4 the class of NBA with amore general acceptance condition consisting of several acceptance sets that have to bevisited infinitely often.1884.3.3Regular PropertiesDeterministic Büchi AutomataAn important difference between finite-state automata and Büchi automata is the expressive power of deterministic and nondeterministic automata. While for languages offinite words, DFAs and NFAs have the same expressiveness, this does not hold for Büchiautomata.The definition of a deterministic Büchi automaton is the same as for a DFA:Definition 4.48.Deterministic Büchi Automaton (DBA)Let A = (Q, Σ, δ, Q0 , F ) be an NBA.
A is called deterministic, if|Q0 | 1 and|δ(q, A)| 1for all q ∈ Q and A ∈ Σ. A is total if |Q0 | = 1 and |δ(q, A)| = 1 for all q ∈ Q and A ∈ Σ.Obviously, the behavior of a DBA for a given input word is deterministic: either eventuallythe DBA will get stuck in some state as it fails to consume the current input symbol orthere is a unique (infinite) run for the given input word. Total DBAs rule out the firstalternative and ensure the existence of a unique run for every input word σ ∈ Σω .Example 4.49.DBA for LT PropertiesFigure 4.15 shows the DBA A (on the left) and the NBA A (on the right) over the alphabetΣ = 2AP where AP = { a, b }.
These automata are equivalent since both represent the LTproperty ”always b and infinitely often a”. Let δ be the transition function of A and δ¬a ∧ ba∧b¬a ∧ bq0a∧ba∧bba∧bq1r0r1bFigure 4.15: An equivalent DBA A (left) and NBA A (right).the transition function of A . The NBA A is not deterministic since for all input symbolscontaining a b, there is the possibility to move to either state r0 or r1 . The DBA A isAutomata on Infinite Words189deterministic.
Note that both A and A are blocking, e.g., any state is blocking on aninput symbol containing ¬b.As for deterministic finite automata, the usual notation is q = δ(q, A) (instead of {q } =δ(q, A)) and δ(q, A) = ⊥ (undefined), if δ(q, A) = ∅. Thus, the transition relation of aDBA is understood as partial function δ : Q × Σ → Q. Total DBAs are often writtenin the form (Q, Σ, δ, q0 , F ) where q0 is the unique initial state and δ is viewed as a totalfunction Q × Σ → Q. Since DBA can always be extended by a nonaccept trapping statewithout changing the accepting language, it can be assumed without restriction that thetransition relation is total. For instance, Figure 4.16 shows an equivalent total DBA forthe DBA A in Figure 4.15 that is obtained by adding such a trapping state.¬a ∧ ba∧b¬a ∧ bq0a∧bq1¬b¬bqtraptrueFigure 4.16: A total DBA for ”always b and infinitely often a”.The transition function δ of a total DBA can be expanded to a total function δ∗ : Q×Σ∗ →Q in the obvious way; see also page 157 for the transition function of a total DFA.
Thatis, let δ∗ (q, ε) = q, δ∗ (q, A) = δ(q, A) andδ∗ (q, A1 A2 . . . An ) = δ∗ ( δ(q, A1 ), A2 . . . An ).Then, for every infinite word σ = A0 A1 A2 . . . ∈ Σω , the run q0 q1 q2 . . . in A belonging toσ is given by qi+1 = δ∗ (q0 , A0 . . . Ai ) for all i 0, where q0 is the unique initial state of A.In particular, for total DBA A = (Q, Σ, δ, q0 , F ) the accepted language is given byLω (A) = { A0 A1 A2 . . . ∈ Σω | δ∗ (q0 , A0 . .
. Ai ) ∈ F for infinitely many i }As we have seen before, NFAs are as expressive as deterministic ones. However, NBAsare more expressive than deterministic ones. That is, there do exist NBA for which there190Regular Propertiesdoes not exist an equivalent deterministic one. Stated differently, while any ω-languageaccepted by a DBA is ω-regular, there do exist ω-regular languages for which there doesnot exist a DBA accepting it.
An example of such ω-regular language is the languagegiven by the expression (A+B)∗ Bω .Aq0Bq1BBFigure 4.17: NBA for the ω-regular expression (A + B)∗ Bω .In fact, the language Lω ( (A+B)∗ Bω ) is accepted by a rather simple NBA, shown in Figure4.17. The idea of this NBA is that given an input word σ = wBω where w ∈ {A, B}∗ theautomaton may stay in q0 and guess nondeterministically when the suffix consisting of B’sstarts and then moves to the accept state q1 .
This behavior, however, cannot be simulatedby a DBA as formally shown in the following theorem.Theorem 4.50.NBAs are More Powerful than DBAsThere does not exist a DBA A such that Lω (A) = Lω ((A + B)∗ Bω ).Proof: By contradiction. Assume that Lω ((A + B)∗ Bω ) = Lω (A) for some DBA A =(Q, Σ, δ, q0 , F ) with Σ = { A, B }. Note that since A is deterministic, δ∗ can be consideredas a function of type Q × Σ∗ → Q.Since the word σ1 = Bω belongs to Lω ((A + B)∗ Bω ) = Lω (A), there exists an acceptingstate q1 ∈ F and a n1 ∈ IN1 such that(1)δ∗ (q0 , Bn1 ) = q1 ∈ F.(Since A is deterministic, q1 is uniquely determined.) Now consider the word σ2 =Bn1 ABω ∈ Lω ((A + B)∗ Bω ) = Lω (A). Since σ2 is accepted by A, there exists an accepting state q2 ∈ F and n2 ∈ IN1 , such that(2)δ∗ (q0 , Bn1 ABn2 ) = q2 ∈ F.The word Bn1 ABn2 ABω is in Lω ((A + B)∗ Bω ), and, thus, is accepted by A.
So, there isan accepting state q3 ∈ F and n3 ∈ IN1 withAutomata on Infinite Words(3)191δ∗ (q0 , Bn1 ABn2 ABn3 ) = q3 ∈ F.Continuing this process, we obtain a sequence n1 , n2 , n3 , . . . of natural numbers 1 anda sequence q1 , q2 , q3 , . . . of accepting states such thatδ∗ (q0 , Bn1 ABn2 A .
. . Bni−1 ABni ) = qi ∈ F,i 1...Since there are only finitely many states, there exist i < j such thatδ∗ (q0 , Bn1 A . . . ABni ) = δ∗ (q0 , Bn1 A . . . ABni . . . ABnj )Thus A has an accepting run onBn1 A . . . ABni (ABni+1 A . . . ABnj )ω .But this word has infinitely many occurrences of A, and thus does not belong to Lω ((A +B)∗ Bω ). Contradiction.Example 4.51.The Need for NondeterminismIn Examples 4.29 and 4.30, we provided DBAs for LT properties. To represent livenessproperties of the form “eventually forever”, the concept of nondeterminism is, however,necessary.
Consider the property “eventually forever a”, where a is some atomic proposition. Let { a } = AP, i.e., 2AP = {A, B} where A = {} and B = {a}. Then, the linear-timeproperty ”eventually forever a” is given by the ω-regular expression(A + B)∗ Bω = ({} + {a})∗ {a}ω .By Theorem 4.50, there is no DBA for ”eventually forever a”. On the other hand, thisproperty can be described by the NBA A depicted in Figure 4.18.
(Note that state q2could be omitted, as there is no accepting run that starts in q2 .) Intuitively, A nondeterministically decides (by means of an omniscient oracle) from which instant the propositiona is continuously true. This behavior cannot be mimicked by a DBA.q0trueaq1a¬aq2trueFigure 4.18: An NBA accepting “eventually forever a”.The reader might wonder why the powerset construction known for finite automata (seepage 157) fails for Büchi automata. The deterministic automaton Adet obtained through192Regular Propertiesthe powerset construction allows simulating the given nondeterministic automaton A bykeeping track of the set Q of states that are reachable in A for any finite prefix of the giveninput word. (This set Q is a state in Adet .) What is problematic here is the acceptancecondition: while for NFAs the information whether an accept state is reachable is sufficient,for infinite words we need one single run that passes an accept state infinitely often.
Thelatter is not equivalent to the requirement that a state Q with Q ∩ F = ∅ is visitedinfinitely often, since there might be infinitely many possibilities (runs) to enter F atdifferent time points, i.e., for different prefixes of the input word. This, in fact, is thecase for the NBA in Figure 4.17. For the input word σ = ABABA . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
