Published by MIT Press. Copyright 1995 Massachusetts Institute of Technology.
Your institution may already be a subscriber to CJTCS. If not, please subscribe for legitimate access to all journal articles.
Rabin conditions are a general class of properties of infinite sequences 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 these measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. This property is used in [Kla94a(JPL)] to establish an exponential upper bound for the complementation of automata on infinite trees.
When applied to termination problems under fairness constraints, Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules.