Verification Conditions for $\omega$-Automata and Applications to Fairness

Abstract

We present sound and complete verification conditions for proving that a program satisfies a specification definied by a deterministic Rabin automaton. Our verification conditions yield a simple method for proving that a program terminates under general fairness constraints. As opposed to previous approaches, our method is syntax-independent and does not require recursive applications of proof rules. Moreover using a result by Safra, we obtain the first direct method for proving that a program satisfies a Buchi automaton specification. Finally, we show that our method generalized two earlier methods.