Report Number: CS-TR-89-1296
Institution: Stanford University, Department of Computer Science
Title: Completing the temporal picture
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: December 1989
Abstract: The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves oll previous temporal systems, such as [MP83a] and [MP83b], in that it reduces the validity of program properties into pure assertional reasoning, not involving additional temporal reasoning. The proof system is based on the classification of temporal properties according to the Borel hierarchy, providing an appropriate proof rule for each of the main classes, such as safety, response, and progress properties.
http://i.stanford.edu/pub/cstr/reports/cs/tr/89/1296/CS-TR-89-1296.pdf