Büchi automaton

A Büchi automaton is the extension of a finite state automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi.

Automata on infinite words are useful for specifying behavior of nonterminating systems, such as hardware or operating systems. For such systems, you may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request which is not followed by an acknowledge". The latter is a property of infinite words: you cannot say of a finite sequence that it satisfies this property.

Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. A language defined by a Rabin automaton, Streett automaton, parity automaton, or Muller automaton is also omega-regular. These automata have more powerful acceptance conditions, and are therefore often more succinct (use fewer states to express the same language).

Generalized Büchi Automata

A minor variant of Büchi automata is the generalized Büchi automaton, which has more than one set of accepting states. A run is accepting if it passes through at least one state of every set of accepting states infinitely often. Multiple acceptance conditions can be gotten rid of with the help of the "counting construction". That is, a generalized Büchi automaton can be converted to a language equivalent Büchi automaton by simply considering the new set of States as the cross product between the set of states and a set of numbers from 1 to k, where k is the number of accepting states. This way, when a transition moves to an accepting state, it moves from (q,i) to (q,i+1) based on the above cross product. We go over all accepting states until finally returning to the first one. ie,

Q = $Q\; imes\{\; 1,2,3,4\; ldots\; \}$
-> if (q,q`) belongs to R and q belongs to the set of Final states

Labeled Generalized Büchi Automaton

A labeled Generalized Büchi automaton is one where the labels actually apply to the states rather than the edges. To obtain the non labeled version, the labels are moved from the nodes to the incoming arcs

Emptiness checking

Most model checking problems can be translated to "emptiness checking", i.e. finding a cycle from the initial state to an accepting state in the Büchi automaton. This is equivalent to the check whether the final state is actually reachable from the initial state in the case of a nondeterministic finite automaton. In the case of the nondeterministic finite automaton, we insert the initial state in a stack (and also create a hash map that records visited states) and check all reachable worlds. At the end of the run if we reach a final state we return the status that it is not empty. In the case of the nondeterministic Büchi automaton, the naive manner is to find the accepting states and see if there is a cycle. However, this reduces to a complexity of $O(n^2)$. A more complicated algorithm developed by Vardi et al. is as follows:
# Maintain 2 hash tables. One for reachable states and one for reachable states from the final state.
# Maintain 2 stacks. One is the current branch of reachable states and the other the current branch from the final state.
# Develop 2 Depth-first searches. Use the depth first search algorithm to find accepting states from the initial state (much alike the one described for NFA). Use another DFS to find cycles from the accepting state. A counter example ( non -empty status) is when you found a cycle by the second DFS and found a path from the initial state to this accepting state.

Deterministic Vs Nondeterministic Büchi automata

The class of deterministic Büchi automata does not accept all omega-regular languages. In particular, there is no deterministic Büchi automaton that accepts the language $(a+b)*a^\{omega\}$. (Any word that has an infinite suffix consisting of only a's.) This language is recognized by a two-state nondeterministic Büchi automaton.

Just like any automaton, Büchi automata can also be seen as tree automata.

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

From Kripke structures to Büchi Automata

Let the Kripke structure be defined by M = where Q is the set of states, I is the set of Initial states, R is a relation between 2 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 BA will have the following characteristics : $Q\_\{final\}\; =\; Q\; cup\; \{init\}$
$Sigma\; =\; 2^\{AP\}$
$I\; =\; \{init\}$
$F\; =\; Q\; cup\; \{init\}$
$delta\; =\; q\; overrightarrow\{a\}\; p$ if (q,p) belongs to R and L(p) = a
and init $overrightarrow\{a\}$ 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 explictily names every state variables polarity for every state, the latter just declares the current set of variables holding or not holding. It says absolutely nothing about the othervariables that could be present in the model.

From Fair Kripke structures to Büchi Automata

Let the Kripke structure be define by M = where Q is the set of states, I is the set of Initial states, R is a relation between 2 states also interpreted as an edge, L is the label for the state and AP are the set of atomic propositions that form L. FR is the set of states under the fair condition. The BA will have the following characteristics : $Q\_\{final\}\; =\; Q\; cup\; \{init\}$
$Sigma\; =\; 2^\{AP\}$
$I\; =\; \{init\}$
F = FR
$delta\; =\; q\; overrightarrow\{a\}\; p$ if (q,p) belongs to R and L(p) = a
and init $overrightarrow\{a\}$ q if q belongs to I and L(q) = a

See also

* Wolfgang Thomas, Automata on infinite objects, in Van Leeuwen, Ed., Handbook of Theoretical Computer Science, pp. 133-164, Elsevier, 1990.

External links

* [http://www.cmi.ac.in/~madhavan/papers/tcs-96-2.html Finite-state Automata on Infinite Inputs]