Dynamical properties of timed automata

Timed automata are an important model for specifying and analyzing real-tim e systems. The main analysis performed on timed automata is the reachabilit y 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 automat a is as follows: we define the set R*(T,Z(0)) = boolean AND(epsilon>0)reach (T-epsilon,Z(0)) where T-epsilon is obtained from timed automaton T by allo wing 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) whe n the clocks drift by an infinitesimally small amount. We present an algori thm for computing R*(T,Z(0)) and provide a proof of its correctness. We sho w that R*(T,Z(0)) is robust with respect to various types of modeling error s. To prove the correctness of our algorithm, we need to understand the dyn amics of timed automata-in particular, the structure of the limit cycles of timed automata.