Büchi automaton

In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs.

A non-deterministic Büchi automaton, later referred to just as a Büchi automaton, has a transition function which may have multiple outputs, leading to many possible paths for the same input; it accepts an infinite input if and only if some possible path is accepting.

They are named after the Swiss mathematician Julius Richard Büchi, who invented them in 1962.

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

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.

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.

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 ⁠

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 recognizes ⁠

the automaton will visit some state in F. Continuing with this construction the ω-word

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

Model checking of finite state systems can often be translated into various operations on Büchi automata.

Minimizing deterministic Büchi automata (i.e., given a deterministic Büchi automaton, finding a deterministic Büchi automaton recognizing the same language with a minimal number of states) is an NP-complete problem.

Existence of algorithms for this construction proves that the set of ω-regular languages is closed under complementation.

[4] Later, other constructions were developed that enabled efficient and optimal complementation.

[5][6][7][8][9] Büchi presented[4] a doubly exponential complement construction in a logical form.

Here, we have his construction in the modern notation used in automata theory.

Let ~A be an equivalence relation over elements of Σ+ such that for each v,w ∈ Σ+, v ~A w if and only if for all p,q ∈ Q, A has a run from p to q over v if and only if this is possible over w and furthermore A has a run via F from p to q over v if and only if this is possible over w. Each class of ~A defines a map f:Q → 2Q × 2Q in the following way: for each state p ∈ Q, we have (Q1,Q2)= f(p), where Q1 = {q ∈ Q | w can move automaton A from p to q} and Q2 = {q ∈ Q | w can move automaton A from p to q via a state in F}.

The following three theorems provide a construction of the complement of A using the equivalence classes of ~A.

Consider the set of natural numbers N. Let equivalence classes of ~A be the colors of subsets of N of size 2.

Let f be a defining map of an equivalence class such that w(0,i0) ∈ Lf.

Let g be a defining map of an equivalence class such that for each j>0,w(ij-1,ij) ∈ Lg.

Proof: Suppose there is a word w ∈ L(A) ∩ Lf(Lg)ω, otherwise the theorem holds trivially.

Let r be an accepting run of A over input w. We need to show that each word w' ∈ Lf(Lg)ω is also in L(A), i.e., there exists a run r' of A over input w' such that a state in F occurs in r' infinitely often.

Let the first state of r' be same as r. By definition of Lf, we can choose a run segment on word w'0 to reach s0.

By definition of Lg, we can extend the run along the word segment w'i+1 such that the extension reaches si+1 and visits a state in F if i ∈ I.

By the above theorems, we can represent Σω-L(A) as finite union of ω-regular languages of the form Lf(Lg)ω, where Lf and Lg are equivalence classes of ~A.

This construction is doubly exponential in terms of size of A.