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 nondeterministic finite automata 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. 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: 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. q0 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 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.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (6)

Related lectures (15)

Ω-automaton

In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automata that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. ω-automata are useful for specifying behavior of systems that are not expected to terminate, such as hardware, operating systems and control systems.

Büchi automaton

Powerset construction

In the theory of computation and automata theory, the powerset construction or subset construction is a standard method for converting a nondeterministic finite automaton (NFA) into a deterministic finite automaton (DFA) which recognizes the same formal language. It is important in theory because it establishes that NFAs, despite their additional flexibility, are unable to recognize any language that cannot be recognized by some DFA. It is also important in practice for converting easier-to-construct NFAs into more efficiently executable DFAs.

History of the First Robot MOOC: Thymio: un robot pour se former à l'informatique

Explores the history of robots, from automatons to the first practical robot, Electric Dog, showcasing the significance of bio-inspiration in robotics.

History of the First Robot MOOC: Il robot Thymio come strumento di scoperta delle scienze digitali

Explores the history of automatons, leading to the emergence of robots.

The History of the First Robot

Delves into the history of robots, from ancient automatons to the first electric robot.