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.*