## Paper: Rabin measures and their applications to fairness and automata theory (at LICS 1991)

**Nils Klarlund Dexter C. Kozen**

### 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

### BibTeX

@InProceedings{KlarlundKozen-Rabinmeasuresandthe, author = {Nils Klarlund and Dexter C. Kozen}, title = {Rabin measures and their applications to fairness and automata theory }, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {256--265}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }