Progress measures for complementation ω-automata with applications to temporal logic

A new approach to complementing ω-automata, which are finite-state automata defining languages of infinite words, is given. Instead of using usual combinatorial or algebraic properties of transition relations, it is shown that a graph-theoretic approach based on the notion of progress measures is a potent tool for complementing ω-automata. Progress measures are applied to the classical problem of complementing Buchi automata, and a simple method is obtained. The technique applies to Streett automata, for which an optimal complementation method is also obtained. As a consequence, it is seen that the powerful temporal logic ETLS is much more tractable than previously thought.