Abstract: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 anextension of Manna and Pnueli's linear temporal logic.It can express both the properties and the implementaions ofreal-time system.With LTLC,systems can be described at many at many levels of abstraction,from high-level requirement specificatons to low-level implementation models,and the conformance between different descriptions can be expressed by logical implication.This aspect of LTLC will be beneficil to the verification and the stepwise refinements of real-time systems.