CJTCS Volume 1995 Article 3

Rabin Measures

Nils Klarlund ( University of Aarhus ) and Dexter Kozen ( Cornell University ) 20 September, 1995

Abstract

Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure , which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition.

We show that these measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. This property is used in [Kla94a(JPL)] to establish an exponential upper bound for the complementation of automata on infinite trees.

When applied to termination problems under fairness constraints, Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules.

• Preformatted versions of the article
  • DVI (127,808 bytes)
  • PostScript (315,634 bytes)
  • PDF (331,739 bytes)
  • Audio by AsTeR (to appear)
• Source materials for custom formatting
  • LaTeX ( cj95-03.tex , 61,539 bytes)
  • BIBTeX ( cj95-03.bib , 10,026 bytes)
  • Parameter settings for custom formatting ( cjropts.tex , 197 bytes)
  • Self citation in BIBTeX (241 bytes)
• Online discussion
• Instructions for Readers

---

Article 2 Article 4
Volume 1995 Published articles

Last modified: 24 March 1997