Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Rabin Measures and Their Applications to Fairness and Automata Theory

Rabin Measures and Their Applications to Fairness and Automata Theory

File(s)
91-1201.ps (319.03 KB)
91-1201.pdf (1.32 MB)
Permanent Link(s)
https://hdl.handle.net/1813/7041
Collections
Computer Science Technical Reports
Author
Klarlund, Nils
Kozen, Dexter
Abstract

Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to determine whether a program satisfies a Rabin condition by reasoning about single transitions instead of infinite computations. We introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition. 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 Safra, our result gives a method for proving that a program satisfies a nondeterministic Buchi automaton specification.

Date Issued
1991-04
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR91-1201
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance