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 $w$ if there exists a run, such that all the states occurring infinitely often in the run are in the final state set $F$ . In contrast, 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$ .

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

Formal definition

Formally, a deterministic co-Büchi automaton is a tuple ${\mathcal {A}}=(Q,\Sigma ,\delta ,q_{0},F)$ that consists of the following components:

$Q$ is a finite set. The elements of $Q$ are called the states of ${\mathcal {A}}$ .
$\Sigma$ is a finite set called the alphabet of ${\mathcal {A}}$ .
$\delta :Q\times \Sigma \rightarrow Q$ is the transition function of ${\mathcal {A}}$ .
$q_0$ is an element of $Q$ , called the initial state.
$F\subseteq Q$ is the final state set. ${\mathcal {A}}$ accepts exactly those words $w$ with the run $\rho (w)$ , in which all of the infinitely often occurring states in $\rho (w)$ are in $F$ .

In a non-deterministic co-Büchi automaton, the transition function $\delta$ is replaced with a transition relation $\Delta$ . The initial state $q_0$ is replaced with an initial state set $Q_{0}$ . Generally, the term co-Büchi automaton refers to the non-deterministic co-Büchi Büchi automaton.

For more comprehensive formalism see also ω-automaton.

Acceptance Condition

The acceptance condition of a co-Büchi automaton is formally

$\exists i\forall j:\;j\geq i\quad \rho (w_{j})\in F.$

The Büchi acceptance condition is the complement of the co-Büchi acceptance condition:

$\forall i\exists j:\;j\geq i\quad \rho (w_{j})\in F.$

Properties

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

This article is issued from Wikipedia - version of the 10/23/2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.