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.