Büchi automaton

In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence if there exists a run of the automaton that visits (at least) one of the final states infinitely often. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962.[1]

Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic.

Formal definition

Formally, a deterministic Büchi automaton is a tuple A = (Q,Σ,δ,q0,F) that consists of the following components:

In a non-deterministic Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states, and the single initial state q0 is replaced by a set I of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata.

For more comprehensive formalism see also ω-automaton.

Closure properties

The set of Büchi automata is closed under the following operations.

Let A=(QA,Σ,ΔA,IA,FA) and B=(QB,Σ,ΔB,IB,FB) be Büchi automata and C=(QC,Σ,ΔC,IC,FC) be a finite automaton.

Proof: If we assume, w.l.o.g., QA∩QB is empty then L(A)∪L(B) is recognized by the Büchi automaton (QA∪QB, Σ, ΔA∪ΔB, IA∪IB, FA∪FB).
Proof: The Büchi automaton A'=(Q',Σ,Δ',I',F') recognizes L(A)∩L(B), where
  • Q' = QA × QB × {1,2}
  • Δ' = Δ1 ∪ Δ2
    • Δ1 = {( (qA,qB,1), a, (q'A,q'B,i) ) | (qA,a,q'A)∈ΔA and (qB,a,q'B)∈ΔB and if qA∈FA then i=2 else i=1 }
    • Δ2 = {( (qA,qB,2), a, (q'A,q'B,i) ) | (qA,a,q'A)∈ΔA and (qB,a,q'B)∈ΔB and if qB∈FB then i=1 else i=2 }
  • I' = IA × IB × {1}
  • F' = { (qA,qB,2) | qB∈FB }
By construction, r'=(qA0,qB0,i0),(qA1,qB1,i1),... is a run of automaton A' on input word w iff rA=qA0,qA1,... is run of A on w and rB=qB0,qB1,... is run of B on w. rA is accepting and rB is accepting iff r' is concatenation of an infinite series of finite segments of 1-states(states with third component 1) and 2-states(states with third component 2) alternatively. There is such a series of segments of r' iff r' is accepted by A'.
Proof: If we assume, w.l.o.g., QC∩QA is empty then the Büchi automaton A'=(QC∪QA,Σ,Δ',I',FA) recognizes L(C)⋅L(A), where
  • Δ' = ΔA ∪ ΔC ∪ { (q,a,q') | q'∈IA and ∃f∈FC. (q,a,f)∈ΔC }
  • if IC∩FC is empty then I' = IC otherwise I' = IC ∪ IA
Proof: The Büchi automaton that recognizes L(C)ω is constructed in two stages. First, we construct a finite automaton A' such that A' also recognizes L(C) but there are no incoming transitions to initial states of A'. So, A'=(QC ∪ {qnew},Σ,Δ',{qnew},FC), where Δ' = ΔC ∪ { (qnew,a,q') | ∃q∈IC. (q,a,q')∈ΔC}. Note that L(C)=L(A') because L(C) does not contain the empty string. Second, we will construct the Büchi automaton A" that recognize L(C)ω by adding a loop back to the initial state of A'. So, A"=(QC ∪ {qnew},Σ,Δ",{qnew},{qnew}), where Δ" = Δ' ∪ { (q,a,qnew) | ∃q'∈FC. (q,a,q')∈Δ'}.
Proof: The proof is presented here.

Recognizable languages

Büchi automata recognize the ω-regular languages. Using the definition of ω-regular language and the above closure properties of Büchi automata, it can be easily shown that a Büchi automaton can be constructed such that it recognizes any given ω-regular language. For converse, see construction of a ω-regular language for a Büchi automaton.

Deterministic versus non-deterministic Büchi automata
A non-deterministic büchi automaton that recognizes (0∪1)*0ω

The class of deterministic Büchi automata does not suffice to encompass all omega-regular languages. In particular, there is no deterministic Büchi automaton that recognizes the language (0∪1)*0ω, which contains exactly words in which 1 occurs only finitely many times. We can demonstrate it by contradiction that no such deterministic Büchi automaton exists. Let us suppose A is a deterministic Büchi automaton that recognize (0∪1)*0ω with final state set F. A accepts 0ω. So, A will visit some state in F after reading some finite prefix of 0ω, say after the i0th letter. A also accepts the ω-word 0i010ω. Therefore, for some i1, after the prefix 0i010i1 the automaton will visit some state in F. Continuing with this construction the ω-word 0i010i110i2... is generated which causes A to visit some state in F infinitely often and the word is not in (0∪1)*0ω. Contradiction.

The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma.

Lemma: An ω-language is recognizable by a deterministic Büchi automaton iff it is the limit language of some regular language.
Proof: Any deterministic Büchi automaton A can be viewed as a deterministic finite automaton A' and vice versa, since both types of automaton are defined as 5-tuple of the same components, only the interpretation of acceptance condition is different. We will show that L(A) is the limit language of L(A'). An ω-word is accepted by A iff it will force A to visit final states infinitely often. Iff, infinitely many finite prefixes of this ω-word will be accepted by A'. Hence, L(A) is a limit language of L(A').

Algorithms

Model checking of finite state systems can often be translated into various operations on Büchi automata. In addition to the closure operations presented above, the following are some useful operations for the applications of Büchi automata.

Determinization

Since deterministic Büchi automata are strictly less expressive than non-deterministic automata, there can not be an algorithm for determinization of Büchi automata. But, McNaughton's Theorem and Safra's construction provide algorithms that can translate a Büchi automaton into a deterministic Muller automaton or deterministic Rabin automaton.[2]

Emptiness checking

The language recognized by a Büchi automaton is non-empty if and only if there is a final state that is both reachable from the initial state, and lies on a cycle.

An effective algorithm that can check emptiness of a Büchi automaton:

  1. Consider the automaton as a directed graph and decompose it into strongly connected components (SCCs).
  2. Run a search (e.g., the depth-first search) to find which SCCs are reachable from the initial state.
  3. Check whether there is a non-trivial SCC that is reachable and contains a final state.

Each of the steps of this algorithm can be done in time linear in the automaton size, hence the algorithm is clearly optimal.

Minimization

The algorithm for minimizing nondeterministic finite automaton also correctly minimizes a Büchi automaton. The algorithm does not guarantee minimum Büchi automaton. However, the algorithms for minimizing deterministic finite automaton does not work for deterministic Büchi automaton.

Variants

Transforming from other models of description to non-deterministic Büchi automata

From generalized Büchi automata (GBA)
Multiple sets of states in acceptance condition can be translated into one set of states by an automata construction, which is known as "counting construction". Let's say A = (Q,Σ,∆,q0,{F1,...,Fn}) is a GBA, where F1,...,Fn are sets of accepting states then the equivalent Büchi automaton is A' = (Q', Σ, ∆',q'0,F'), where
  • Q' = Q × {1,...,n}
  • q'0 = ( q0,1 )
  • ∆' = { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆ and if q ∈ Fi then j=((i+1) mod n) else j=i }
  • F'=F1× {1}
From Linear temporal logic formula
A translation from a Linear temporal logic formula to a generalized Büchi automaton is given here. And, a translation from a generalized Büchi automaton to a Büchi automaton is presented above.
From Muller automata
A given Muller automaton can be transformed into an equivalent Büchi automaton with following automata construction. Let's suppose A = (Q,Σ,∆,Q0,{F0,...,Fn}) is a Muller automaton, where F0,...,Fn are sets of accepting states. An equivalent Büchi automaton is A' = (Q', Σ, ∆',Q0,F'), where
  • Q' = Q ∪  ∪ni=0 {i} × Fi × 2Fi
  • ∆'= ∆ ∪ ∆1 ∪ ∆2, where
    • ∆1 ={ ( q, a, (i,q',∅) ) | (q, a, q') ∈ ∆ and q' ∈ Fi }
    • ∆2={ ( (i,q,R), a, (i,q',R') ) | (q,a,q')∈∆ and q,q' ∈ Fi and if R=Fi then R'= ∅ otherwise R'=R∪{q} }
  • F'=∪ni=0 {i} × Fi × {Fi}
A' keeps original set of states from A and adds extra states on them. The Büchi automaton A' simulates the Muller automaton A as follows: At the beginning of the input word, the execution of A' follows the execution of A, since initial states are same and ∆' contains ∆. At some non-deterministically chosen position in the input word, A' decides of jump into newly added states via a transition in ∆1. Then, the transitions in ∆2 try to visit all the states of Fi and keep growing R. Once R becomes equal to Fi then it is reset to the empty set and ∆2 try to visit all the states of Fi states again and again. So, if the states R=Fi are visited infinitely often then A' accepts corresponding input and so does A. This construction closely follows the first part of the proof of McNaughton's Theorem.
From Kripke structures
Let the given Kripke structure be defined by M = <Q, I, R, L, AP> where Q is the set of states, I is the set of initial states, R is a relation between two states also interpreted as an edge, L is the label for the state and AP are the set of atomic propositions that form L.
The Büchi automaton will have the following characteristics:
if (q, p) belongs to R and L(p) = a
and init q if q belongs to I and L(q) = a.
Note however that there is a difference in the interpretation between Kripke structures and Büchi automata. While the former explicitly names every state variable's polarity for every state, the latter just declares the current set of variables holding or not holding true. It says absolutely nothing about the other variables that could be present in the model.

References

  1. ↑ Büchi, J.R. (1962). "On a decision method in restricted second order arithmetic". Proc. International Congress on Logic, Method, and Philosophy of Science. 1960. Stanford: Stanford University Press: 1–12.
  2. ↑ Safra, S. (1988), "On the complexity of ω-automata", Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS '88), Washington, DC, USA: IEEE Computer Society, pp. 319–327, doi:10.1109/SFCS.1988.21948.

External links

Chomsky hierarchyGrammarsLanguagesAbstract machines
  • Type-0
  • —
  • Type-1
  • —
  • —
  • —
  • —
  • —
  • Type-2
  • —
  • —
  • Type-3
  • —
  • —
Each category of languages, except those marked by a *, is a proper subset of the category directly above it. Any language in each category is generated by a grammar and by an automaton in the category in the same line.

This article is issued from Wikipedia - version of the 11/2/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.