Model checking timed automata

Abstract

The theory of timed automata provides a formal framework to model and to verify the correct functioning of real-time systems. Among the different verification problems that have been investigated within this theory, the so-called teachability problem has been the most throughly studied. This problem is stated as follows. Given two states of the system, is there an execution starting at one of them that reaches the other? The first reason for studying such problem is that safety properties can expressed as the non-reachability of a set of states where the system is consider to show an incorrect or unsafe functioning. Second, the algorithms developed for analyzing other classes of properties are essentially based on the algorithms developed for solving the reachability question. In this paper we survey the different algorithms, data-structures and tools that have been proposed in the literature to solve this problem.