Rabin measures and their applications to fairness and automata theory

Abstract

Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. It is shown how to determine whether a program satisfies a Rabin condition by reasoning about single transitions instead of infinite computations. A concept a Rabin measure, which in a precise sense expresses progress for each transition towards satisfaction of the Rabin condition, is introduced. 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 S. Safra (1988), the result gives a method for proving that a program satisfies a nondeterministic Buchi automaton specification.