Co-Büchi automaton
Encyclopedia
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 w if there exist a run, such that all the states occurring infinitely often in the run are not in the acceptance condition. In contrast, a Büchi automaton
accepts a word if there exists a run, such that at least one state occurring infinitely often in its acceptance condition.
Co-Büchi automata are strictly weaker than Büchi automata.
In a non-deterministic co-Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states and initial state is q0 is replaced by a set of initial states Q0. Generally, co-Büchi automaton refers to non-deterministic co-Büchi Büchi automaton.
For more comprehensive formalism see also ω-automaton
.
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
, a co-Büchi automaton is a variant of Büchi automaton
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 iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
. The only difference is the accepting condition: a Co-Büchi automaton accepts an infinite word w if there exist a run, such that all the states occurring infinitely often in the run are not in the acceptance condition. In contrast, a Büchi automaton
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 iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
accepts a word if there exists a run, such that at least one state occurring infinitely often in its acceptance condition.
Co-Büchi automata are strictly weaker than Büchi automata.
Formal definition
Formally, a deterministic co-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.
- F⊆Q is the acceptance condition. A accepts exactly those runs r, in which all of the infinitely often occurring states in r are not in F.
In a non-deterministic co-Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states and initial state is q0 is replaced by a set of initial states Q0. Generally, co-Büchi automaton refers to non-deterministic co-Büchi Büchi automaton.
For more comprehensive formalism see also ω-automaton
Ω-automaton
In automata theory, a branch of theoretical computer science, an ω-automaton is a deterministic or nondeterministic automaton that runs on infinite, rather than finite, strings as input...
.