Rabin Measures and Their Applications to Fairness and Automata Theory

Abstract

Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to determine whether a program satisfies a Rabin condition by reasoning about single transitions instead of infinite computations. We introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition. When applied to termination problems under fairness constraints, Rabin measures constitute a simpler verification method than previous approaches, which often are syntax-dependent and require recursive applications of proof rules to syntactically transformed programs. Rabin measures also generalize earlier automata-theoretic verification methods. Combined with a result by Safra, our result gives a method for proving that a program satisfies a nondeterministic Buchi automaton specification.