Analysis of real-time systems with CTL model checkers

Citations of this article
Mendeley users who have this article in their library.


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).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free