5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 38
Текст из файла (страница 38)
Variants of nondeterministic Büchi automata will be discussed in Sections 4.3.3 and 4.3.4.4.3.1ω-Regular Languages and PropertiesInfinite words over the alphabet Σ are infinite sequences A0 A1 A2 . . . of symbols Ai ∈ Σ.Σω denotes the set of all infinite words over Σ. As before, the Greek letter σ will beused for infinite words, while w, v, u range over finite words. Any subset of Σω is called alanguage of infinite words, sometimes also called an ω-language. In the sequel, the notionof a language will be used for any subset of Σ∗ ∪ Σω .
Languages will be denoted by thesymbol L.Automata on Infinite Words171To reason about languages of infinite words, the basic operations of regular expressions(union, concatenation, and finite repetition) are extended by infinite repetition, denotedby the Greek letter ω.2 For instance, the infinite repetition of the finite word AB yieldsthe infinite word ABABABABAB . . . (ad infinitum) and is denoted by (AB)ω .
For thespecial case of the empty word, we have εω = ε. For an infinite word, infinite repetitionhas no effect, that is, σ ω = σ if σ ∈ Σω . Note that the finite repetition of a word resultsin a language of finite words, i.e., a subset of Σ∗ , whereas infinite repetition of a (finite orinfinite) word results in a single word.Infinite repetition can be lifted to languages as follows. For language L ⊆ Σ∗ , let Lω bethe set of words in Σ∗ ∪ Σω that arise from the infinite concatenation of (arbitrary) wordsin Σ, i.e.,Lω = {w1 w2 w3 . . .
| wi ∈ L, i 1}.The result is an ω-language, provided that L ⊆ Σ+ , i.e., L does not contain the emptyword ε. However, in the sequel, we only need the ω-operator applied to languages offinite words that do not contain the empty word. In this case, i.e., for L ⊆ Σ+ , we haveLω ⊆ Σ ω .In the following definition, the concatenation operator L1 .L2 is used that combines alanguage L1 of finite words with a language L2 of infinite words.
It is defined by L1 .L2 ={wσ | w ∈ L1 , σ ∈ L2 }.Definition 4.23.ω-Regular ExpressionAn ω-regular expression G over the alphabet Σ has the formG = E1 .Fω1 + . . . + En .Fωnwhere n 1 and E1 , . . . , En , F1 , . . . , Fn are regular expressions over Σ such that ε ∈/ L(Fi ),for all 1 i n.The semantics of the ω-regular expression G is a language of infinite words, defined byLω (G) = L(E1 ).L(F1 )ω ∪ . . .
∪ L(En ).L(Fn )ωwhere L(E) ⊆ Σ∗ denotes the language (of finite words) induced by the regular expressionE (see page 914).Two ω-regular expressions G1 and G2 are equivalent, denoted G1 ≡ G2 , if Lω (G1 ) = Lω (G2 ).The symbol ω denotes the first infinite ordinal. It already appeared in the notation Σω for the set ofinfinite words over the alphabet Σ.2172Regular PropertiesExamples for ω-regular expressions over the alphabet Σ = { A, B, C } are(A + B)∗ A(AAB + C)ωorA(B + C)∗ Aω + B(A + C)ω .If E is a regular expression with ε ∈/ L(E), then also Eω can be viewed as an ω-regularexpression since it can be identified with E.Eω or ε.Eω . Note that we have L(E)ω =L(E.Eω ) = L(ε.Eω ).Definition 4.24.ω-Regular LanguageA language L ⊆Σ.is called ω-regular if L = Lω (G) for some ω-regular expression G overΣωFor instance, the language consisting of all infinite words over {A, B} that contain infinitelymany A’s is ω-regular since it is given by the ω-regular expression (B∗ A)ω .
The languageconsisting of all infinite words over {A, B} that contain only finitely many A’s is ω-regulartoo. A corresponding ω-regular expression is (A+ B)∗ Bω . The empty set is ω-regular sinceit is obtained, e.g., by the ω-regular expression ∅ω . More generally, if L ⊆ Σ∗ is regularand L is ω-regular, then Lω and L.L are ω-regular.ω-Regular languages possess several closure properties: they are closed under union, intersection, and complementation. The argument for union is obvious from the definition byω-regular expressions. The proof for the intersection will be provided later; see Corollary4.60 on page 198. The more advanced proof for complementation is not provided in thismonograph.
We refer the interested reader to [174] that covers also other properties ofω-regular languages and various other automata models.The concepts of ω-regular languages play an important role in verification since mostrelevant LT properties are ω-regular:ω-Regular PropertiesDefinition 4.25.LT property P over AP is called ω-regular if P is an ω-regular language over the alphabet2AP .For instance, for AP = { a, b }, the invariant Pinv induced by the proposition Φ = a ∨ ¬bis an ω-regular property sinceA0 A1 A2 .
. . ∈ (2AP )ω | ∀i 0. (a ∈ Ai or b ∈/ Ai )Pinv ==A0 A1 A2 . . . ∈ (2AP )ω | ∀i 0. (Ai ∈ {{}, {a}, {a, b}}Automata on Infinite Words173is given by the ω-regular expression E = ({} + {a} + {a, b})ω over the alphabet Σ = 2AP ={{}, {a}, {b}, {a, b}}. In fact, any invariant over AP is ω-regular (the set AP of atomicpropositions is arbitrary) as it can be described by the ω-regular expression Φω where Φdenotes the underlying propositional formula (that has to hold for all reachable states)and is identified with the regular expression given by the sum of all A ⊆ AP with A |= Φ.Also, any regular safety property Psafe is an ω-regular property. This follows from the factthat the complement language(2AP )ω \ Psafe = BadPref(Psafe ) .(2AP )ωregularis an ω-regular language.
The result that ω-regular languages are closed under complementation (stated above, in the end of Section 4.3.1 on page 172) yields the claim.Example 4.26.Mutual ExclusionAnother example of an ω-regular property is the property given by the informal statement“process P visits its critical section infinitely often” which, for AP = { wait, crit }, can beformalized by the ω-regular expression:(( {} + { wait } )∗ .({ crit } + { wait, crit }))ω .negative literal ¬critpositive literal critWhen allowing a somewhat sloppy notation using propositional formulae, the above expression may be rewritten into ((¬crit)∗ .crit)ω .Starvation freedom in the sense of “whenever process P is waiting then it will enter itscritical section eventually later” is an ω-regular property as it can be described by((¬wait)∗ .wait.true∗ .crit)ω + ((¬wait)∗ .wait.true∗ .crit)∗ .(¬wait)ωwhich is a short form for the ω-regular expression over AP = { wait, crit } that results byreplacing ¬wait with {} + {crit}, wait with {wait} + {wait, crit}, true with {} + {crit} +{wait} + {wait, crit}, and crit with {crit} + {wait, crit}.
Intuitively, the first summand inthe above expression stands for the case where P requests and enters its critical sectioninfinitely often, while the second summand stands for the case where P is in its waitingphase only finitely many times.4.3.2Nondeterministic Büchi AutomataThe issue now is to provide a kind of automaton that is suited for accepting ω-regularlanguages. Finite automata are not adequate for this purpose as they operate on finite174Regular Propertieswords, while we need an acceptor for infinite words.
Automata models that recognizelanguages of infinite words are called ω-automata. The accepting runs of an ω-automatonhave to “check” the entire input word (and not just a finite prefix thereof), and thus haveto be infinite. This implies that acceptance criteria for infinite runs are needed.In this monograph, the simplest variant of ω-automata, called nondeterministic Büchiautomata (NBAs), suffices. The syntax of NBAs is exactly the same as for nondeterministicfinite automata (NFAs). NBAs and NFAs differ, however, in their semantics: the acceptedlanguage of an NFA A is a language of finite words, i.e., L(A) ⊆ Σ∗ , whereas the acceptedlanguage of NBA A (denoted Lω (A) is an ω-language, i.e., Lω (A) ⊆ Σω . The intuitivemeaning of the acceptance criterion named after Büchi is that the accept set of A (i.e., theset of accept states in A) has to be visited infinitely often.
Thus, the accepted languageLω (A) consists of all infinite words that have a run in which some accept state is visitedinfinitely often.Definition 4.27.Nondeterministic Büchi Automaton (NBA)A nondeterministic Büchi automaton (NBA) A is a tuple A = (Q, Σ, δ, Q0 , F ) where• Q is a finite set of states,• Σ is an alphabet,• δ : Q × Σ → 2Q is a transition function,• Q0 ⊆ Q is a set of initial states, and• F ⊆ Q is a set of accept (or: final) states, called the acceptance set.A run for σ = A0 A1 A2 .
. . ∈ Σω denotes an infinite sequence q0 q1 q2 . . . of states in A suchAi→ qi+1 for i 0. Run q0 q1 q2 . . . is accepting if qi ∈ F for infinitelythat q0 ∈ Q0 and qi −−many indices i ∈ IN. The accepted language of A isLω (A) = { σ ∈ Σω | there exists an accepting run for σ in A }.The size of A, denoted |A|, is defined as the number of states and transitions in A.As for an NFA, we identify the transition function δ with the induced transition relation→ ⊆ Q × Σ × Q which is given byA→ p if and only if p ∈ δ(q, A).q −−Automata on Infinite Words175Since the state space Q of an NBA A is finite, each run for an infinite word σ ∈ Σω isinfinite, and hence visits some state q ∈ Q infinitely often.
Acceptance of a run dependson whether or not the set of all states that appear infinitely often in the given run containsan accept state. The definition of an NBA allows for the special case where F = ∅, whichmeans that there are no accept states. Clearly, in this case, no run is accepting. ThusLω (A) = ∅ if F = ∅. There are also no accepting runs whenever, Q0 = ∅ as in this case,no word has a run.Example 4.28.Consider the NBA of Figure 4.7 with the alphabet Σ = {A, B, C}.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
