Completing the temporal picture

The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves on previous temporal systems, 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 appropriate proof rules for the classes of safety, response, and reactivity properties.

Authors

• Zohar Manna
• Amir Pnueli

Keywords

No keywords are indexed for this paper.