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

Authors: 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}
  }