A Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks

Model checking is an algorithmic technique for checking if a concurrent system satisfies a given property expressed in an appropriate temporal logic. LTLC(linear temporal logic with clocks) is a continuous-time temporal logic proposed for the specification of real-time systems. It is a real-time extension of the temporal logic LTL. In this paper, the model checking problem for LTLC is discrssed and a reduction from LTLC model checking to LTL model checking is presented. This reduction will enable us to use the existing LTL model checking tools for LTLC model checking. Owing to the fact that LTLC can express both the properties and the implementations of real-time systems, the LTLC model checking procedures can be used for both the property verification and the refinement verification for real-time systems with finite locations.