Temporal Proof Methodology for Reactive Systems

摘要

The paper presents a minimal proof theory which is adequate for proving the mainimportant temporal properties of reactive programs. The properties we consider consist of the classes of invariance, response, and precedence properties. For each of these classes we present a small set of rules that is complete for verifying properties belonging to this class. We illustrate the application of these rules on several examples. We discuss concise presentations of complex proofs using the devices of transition tables and proof diagrams.... Mathematical theory of computation.