Timed automata are an improtant model for specifying and analyzing real-time systems. The main analysis performed on timed automata is the reachability analysis. In this paper we show that the standard approach for performing reachability analysis is not correct when the clocks drift even by a very small amount. Our formulation of the reachability problem for timed automata is as follows: we define the set R~* (T,Z_0)= intersect_(#epsilon#)>0 Reach (T_(#epsilon#, Z_0) where T_(#epsilon#) is obtained from timed automatin T by allowing an #epsilon# drift in the clocks. R~* (T, Z_0) is the set of states which can be reached in the timed automaton T from the initial states in Z_0 when the clocks drift by an infinitesimally small amount. We present an algorithm for computing R~*(T, Z_0) and provide a proof of its correctness. We show that R~*(T,Z_0) is robust with respect to various types of modeling erros. To prove the correctness of our algorithm, we need to understand the dynamics of timed automata - in particular, the structure of the limit cycles of timed automata.
展开▼
