This paper presents a new method for model checking dense real-time systems. The dense real-time system is modeled by a timed automaton and the property is specified with the temporal logic TCTL. Specification of the TCTL property is reduced to CTL and its temporal constraints are captured in a new timed automaton. This timed automaton will be composed with the original timed automaton specifying the real-time system under analysis. Then, the product timed au- tomaton will be abstracted using partition refinement of state space based on strong bi-simulation. The result is an untimed automaton modulo the TCTL property which represents an equivalent finite state system to be model checked using existing CTL model checking tools. © 2005 Elsevier B.V. All rights reserved.
Bourahla, M., & Benmohamed, M. (2005). Analysis of real-time systems with CTL model checkers. In Electronic Notes in Theoretical Computer Science (Vol. 133, pp. 41–60). https://doi.org/10.1016/j.entcs.2004.08.057