About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
LICS 1991
Conference paper
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.