Real-time symbolic model checking for hard real-time systems

We develop real-time symbolic model checking. Real-time systems can be described using timed automata. Although there exist model-checking algorithms for timed automata, the problem is intractable. In this paper, we propose a symbolic model-checking method as follows: Real-time systems can be expressed by BDDs. Symbolic computations are realized by approximations. The fixpoint computations of real-time temporal logic TCTL are realized by both forward and backward computations