Neha Patil (Editor)

Co Büchi automaton

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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 .

Contents

(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 A = ( Q , Σ , δ , q 0 , 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 the transition function of A .
  • q 0 is an element of Q , called the initial state.
  • F ⊆ Q is the final state set. A accepts exactly those words w with the run ρ ( w ) , in which all of the infinitely often occurring states in ρ ( w ) are in F .

    • In a non-deterministic co-Büchi automaton, the transition function δ is replaced with a transition relation Δ . 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 automaton.

    For more comprehensive formalism see also ω-automaton.

    Acceptance Condition

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

    ∃ i ∀ j : j ≥ i ρ ( w j ) ∈ F .

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

    ∀ i ∃ j : j ≥ i ρ ( w j ) ∈ F .

    Properties

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

    References

    Co-Büchi automaton Wikipedia
    (Text) CC BY-SA