RABIN MEASURES

Rabin conditions are a general class of properties of infinite sequenc es that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition. We show that t hese measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. This property is used in [Kla94b] to establish an e xponential upper bound for the complementation of automata on infinite trees. When applied to termination problems under fairness constraint s. Rabin measures eliminate the need for syntax-dependent, recursive a pplications of proof rules.