Dynamical properties of timed automata revisited

We investigate the reachability problem for timed automata with drifting clocks. In our automata, transition guards are not restricted to closed, as in a previous work of Puri. The reachability problem is the following: given a zone in the clock-valuation space, does there exist a constant $\Delta$ for which all accepting trajectories in the timed automaton with clock drifts smaller than $\Delta$ avoid the zone?
We show that open guards pose certain specific problems which cannot be handled by Puri's algorithm, and propose a new algorithm, based on the idea of ``boundary clock regions'' of Alur, LaTorre and Pappas. We also propose a symbolic algorithm for solving the reachability problem.

"Proceedings of 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2007)", Salzburg, Austria, 3-5 October 2007, Springer Verlag, Lecture Notes in Computer Science volume 4763, pages 130-146, 2007.

 gzipped postscript file.
 
See also the Technical Report, LACL, 2006.