Timed Automata Reachability Detection Methods

Timed-automata is the finite-state transition system with timed constrains. In the process of the formal verification of real-time systems, we first use it to model systems, and then to check whether some unsafe state is reachable or not. We should mainly study its reachability problem when study timed-automata and its verification technique. Computing timed-automata's reachability relation is complex because of its infinite state in its semantics.It's difficult to computing its reachability relation because of its real-value timers. In this article, we transform timer's value from real to integer through equivalent transform based on R.Alur and D.L.Dill's through, then analysis its influence to the two kind transition in timed-automata and its equivalent proof.The key to computing timed-automata's reachability relation is to manage its time constrains relation of each timer. The method to construct region automata put forward by R.Alur and D.L.Dill is to construct the finite automata through of the equivalent partition of state space, and then analysis the reachability relation through region automata. Johan Bengtsson come up the method to compute the relation for thetimed-automata including the constrains like x—y～n(～~∈{<,>,=,≤,≥}). Oneapproximate method comed up by Felice Balarin is to computing a superset of reachable states. The superset of reachable states occasionally causes a correct system to be declared incorrect, but can never cause an incorrect system to be declared correct. Catalin Dima applies the reset points semantics to timed-automata, and computing the reachability relation through the union, composition and star of atomic relation.This article has a though study of these methods. Because it is not correct when applying the equivalent operate for time constraints under the symbolic semantics of timed-automata, we come up a method to solve this problem. The main idea of this method is to regard of different timer's constraints as one timer. Before applying the equivalent operation. we compute the maximal matrix of all of the arbitrary different constraints, and then when we compute the reachability sets using this matrix we will get the right answers. In this article we analysis of its feasibility and correctness. Its virtues lies in not only it considers of all the maximum of different constrains but also it is utility.