Buchi

buchi auto

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.

For more comprehensive formalism see also ω-automaton.