A Linear Temporal Logic with Clocks for Verification of Real-Time Systems

In order to specify real-time systems, many temporal logics such as Timed Computation Tree Logic, Metric Interval Temporal Logic and Real-Time Temporal Logic have been proposed. Although these logics are good at specifying properties of real-time systems, they are not suitable for describing the implementations of such systems. Thus, the specifications and the implementations are usually described by different languages for real-time systems. In this paper, a new linear temporal logic with clocks, called LTLC, is introduced. It is an extension of Manna and Pnueli抯 linear temporal logic. It can express both the properties and the implementations of real-time systems. With LTLC, systems can be described at many levels of abstraction, from high-level requirement specifications to low-level implementation models, and the conformance between different descriptions can be expressed by logical implication. This aspect of LTLC will be beneficial to the verification and the stepwise refinements of real-time systems.