Streett automaton

A Streett automaton is one of the many types of finite automata on infinite strings. It is of the form $$mathcal{A} = (Q,~Sigma,~q_0,~delta,~Omega) where $$Q,~q_0 and $$Sigma are defined as for Büchi automata. $$delta: Q imes Sigma ightarrow Q is the transition function, and $$Omega is a set of pairs $$(E_j,~F_j) with $$E_j, F_j subset Q. $$mathcal{A} accepts the input word $$alpha if for the run $$ho in Q^omega of $$mathcal{A} on $$alpha, for every index $$i, $$inf( ho)cap E_j eempty o inf( ho)cap F_j eempty (where $$inf( ho) is the group of states in $$Q that the run $$ho visits infinitely often).

Less formally, a Streett acceptance condition defines a set of ordered pairs $$(E,~F) of finite sets of states taken from the automaton's graph. A pair is satisfied by any run $$~ ho that either does not contain infinitely many $$E states, or contains infinitely many $$E states and infinitely many $$F states. The Streett acceptance condition is met if all pairs are satisfied. The automaton may be nondeterministic, so an input word (which is infinite) may produce innumerable runs; the word is accepted if at least one run is accepted.

The acceptance condition is dual to the Rabin acceptance condition: The Streett condition is the logical negation of the Rabin condition, and therefore, if a language $$L can be recognized by a deterministic Streett automaton, then its complement $$ar{L} can be recognized by some deterministic Rabin automaton, and vice versa.

ee also

Rabin automaton - A closely related automaton with the same components but a different acceptance condition.