|
Abstract : |
Abstract. The theory of timed automata provides a formal framework to model and to verify the correct functioning of real-time systems. Among the di erent veri cation problems that have been investigated within this theory, the so-called reachability problem has been the most throughly studied. This problem is stated as follows. Given two statesof the system, is there an execution starting at one of them that reaches the other? The rst 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 anincorrect 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 di erent algorithms, data-structures and tools that have been proposed in the literature to solve this problem. 1, |
