Formal Specification of Real-time Systems

Abstract

This paper presents the formal syntax and semantics of Real Time Logic (RTL), a logic for the specification of real-time systems. An example illustrating the specification of a system in RTL is presented, and natural deduction is used to verify that the system satisfies a given safety property. RTL is shown to be undecidable by a reduction from the acceptance problem for two-counter machines. Decidable subclasses of the logic are also discussed.