Buchi Automation

What is 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. Such a machine has a set of states and a transition function, which determines which state the machine should move to from its current state when it reads the next input character. Some states are accepting states and one state is the start state. The machine accepts an input if and only if it will pass through an accepting state infinitely many times as it reads the input.

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. Deterministic and non-deterministic Büchi automata generalize deterministic finite automata and non-deterministic finite automaton to infinite inputs. Each are types of ω-automata. Büchi automata recognize the ω-regular languages, the infinite word version of regular languages. They are named after the Swiss mathematician Julius Richard Büchi, who invented them in 1962.

Formal Definition

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

· Q is a finite set. The elements of Q are called the states of A.

· Σ is a finite set called the alphabet of A.

· δ: Q × Σ → Q is a function, called the transition function of A.

· q₀ is an element of Q, called the initial state of A.

· F⊆Q is the acceptance condition. A accepts exactly those runs in which at least one of the infinitely often occurring states is in F.

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 q₀ is replaced by a set I of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata.

Example of Büchi automaton

1.Accepts all words over {a,b} that have infinitely many a’s

It is a deterministic Büchi Automata

2.Accepts all words {a,b} that have Only finitely many a’s.

It is a non-deterministic Büchi automata.

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

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\cup 1)^{*}0^{\omega }$ , 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 recognizes $(0\cup 1)^{*}0^{\omega }$ with final state set F. A accepts $0^{\omega }$ . So, A will visit some state in F after reading some finite prefix of $0^{\omega }$ , say after the $i_{0}$ th letter. A also accepts the ω-word $0^{i_{0}}10^{\omega }.$ Therefore, for some $i_{1}$ , after the prefix $0^{i_{0}}10^{i_{1}}$ the automaton will visit some state in F. Continuing with this construction the ω-word $0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots$ is generated which causes A to visit some state in F infinitely often and the word is not in $(0\cup 1)^{*}0^{\omega }.$ 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 if 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$ if it will force $A$ to visit final states infinitely often. if, 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.

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

1.Co-Büchi automaton:

In automata theory, a co-Büchi automaton is a variant of Büchi automaton. The only difference is the accepting condition: a Co-Büchi automaton accepts an infinite word if there exists a run, such that all the states occurring infinitely often in the run are in the final state set . In contrast, a Büchi automaton accepts a word if there exists a run, such that at least one state occurring infinitely often in the final state set .

(Deterministic) Co-Büchi automata are strictly weaker than (nondeterministic) Büchi automata.

Co-Büchi automata are closed under union, intersection, projection and determinization.

2.Weak Büchi automaton:

In computer science and automata theory, a Weak Büchi automaton is a formalism which represents a set of infinite words. A Weak Büchi automaton is a modification of Büchi automaton such that for all pair of states

q

and

q'

belonging to the same strongly connected component,

q

is accepting if and only if

q'

is accepting.

A Büchi automaton accepts a word $w$ if there exists a run, such that at least one state occurring infinitely often in the final state set $F$ . For Weak Büchi automata, this condition is equivalent to the existence of a run which ultimately stays in the set of accepting states.

Weak Büchi automata are strictly less-expressive than Büchi automaton and than Co-Büchi automaton.

The deterministic Weak Büchi automata can be minimized in time $O(n\log(n))$ .

The languages accepted by Weak Büchi automata are closed under union, intersection and complementation.

Non-deterministic Weak Büchi automata are more expressive than Weak Büchi automata. As an example, the language $(a+b)^{*}b^{\omega }$ can be decided by a weak Büchi automaton but by no deterministic Büchi automaton.

3.Semi-Deterministic Büchi automaton:

In automata theory, a semi-deterministic Büchi automaton (also known as Büchi automaton deterministic in the limit or limit-deterministic Büchi automaton) is a special type of Büchi automaton. In such an automaton, the set of states can be partitioned into two subsets: one subset forms a deterministic automaton and also contains all the accepting states.

For every Büchi automaton, a semi-deterministic Büchi automaton can be constructed such that both recognize the same ω-language. But, a deterministic Büchi automaton may not exist for the same ω-language.

In standard model checking against Linear Temporal Logic (LTL) properties, it is sufficient to translate a LTL formula into a non-deterministic Büchi automaton. But, in probabilistic model checking, LTL formulae are typically translated into Deterministic Rabin Automata (DRA), as for instance in the PRISM tool. However, not a full deterministic automaton is needed. Indeed, semi-deterministic Büchi automata are sufficient in probabilistic model checking.

4.Generalized Büchi automaton:

In automata theory, generalized Büchi automaton is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely often. Generalized büchi automata is equivalent in expressive power with Büchi automata.

In formal verification, the model checking method needs to obtain an automaton from a LTL formula that specifies the program property. There are algorithms that translate a LTL formula into a generalized Büchi automaton, for this purpose. The notion of generalized Büchi automaton was introduced specifically for this translation.

Conclusion

Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machine should move to from its current state when it reads the next input character.

Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic. Büchi automata recognize the languages, the infinite word version of regular languages

Thank You for reading this post

Authors:

Vaishnavi Gawale

Pankaj Gujar

Ankur Jadhav

Sonal Kharde

Search This Blog