Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories

• TCTL model checker for (dense-)timed Kripke structures in a pointwise semantics.
• Reduce TCTL model checking from continuous semantics to pointwise semantics.
• Sound and complete TCTL model checker for time-robust Real-Time Maude models.

In this paper we show that the satisfaction of timed CTL (TCTL) formulas under the natural continuous semantics for both discrete-time and dense-time timed Kripke structures can be reduced to a model-checking problem in the pointwise semantics for a large class of timed Kripke structures, which includes many discrete-event systems. We then present a TCTL model checking algorithm for the pointwise case. An important consequence of our results is that they together describe a sound and complete TCTL model checking procedure for time-robust real-time rewrite theories also for dense time domains. We have implemented such a TCTL model checker for Real-Time Maude. Our model checker provides for free a sound and complete TCTL model checker for subsets of modeling languages, such as Ptolemy II and (Synchronous) AADL, which have Real-Time Maude analysis integrated into their tool environments.