Streett automaton

A Streett automaton is an automaton on infinite words whose acceptance condition requires that for every pair (L, U) in its acceptance set, if some state from L is visited infinitely often, then some state from U is also visited infinitely often. Introduced by Robert Streett in 1982, the Streett condition is the logical dual of the Rabin condition: a language is Streett-recognizable if and only if its complement is Rabin-recognizable, and vice versa.\n\nStreett automata arise naturally in verification problems where fairness constraints matter. A fairness requirement — 'every request is eventually granted' — has the logical form of a Streett condition: if requests (L) occur infinitely often, then grants (U) must also occur infinitely often. This makes Streett automata the natural target for translating fairness-aware temporal logic specifications, though in practice most tools convert Streett conditions to Büchi automata to exploit better-known algorithms.\n\nThe Streett condition is more expressive than the Büchi condition but less compact: translating a Streett automaton to an equivalent Büchi automaton can require a quadratic blowup in the number of pairs. The trade-off between naturalness of specification and algorithmic efficiency is a recurring tension in formal verification, and Streett automata sit at one extreme of this spectrum.\n\nStreett automata are the fairness specialists of the automata world. They exist because some properties are easier to state than to check, and fairness is the canonical example. The fact that tools immediately translate them into Büchi automata is telling: the Streett condition is a specification convenience, not a computational primitive. This says something deep about the relationship between how humans specify requirements and what algorithms can efficiently verify.\n\n\n