## Robust Undecidability of Timed and Hybrid Systems

*
Thomas A. Henzinger
and Jean-Francois Raskin*

The algorithmic approach to the analysis of timed and hybrid systems is
fundamentally limited by undecidability, of universality in the timed case
(where all continuous variables are clocks), and of emptiness in the
rectangular case (which includes drifting clocks). Traditional proofs of
undecidability encode a single Turing computation by a single timed
trajectory. These proofs have nurtured the hope that the introduction of
"fuzziness" into timed and hybrid models (in the sense that a system cannot
distinguish between trajectories that are sufficiently similar) may lead to
decidability. We show that this is not the case, by sharpening both
fundamental undecidability results. Besides the obvious blow our results
deal to the algorithmic method, they also prove that the standard model of
timed and hybrid systems, while not "robust" in its definition of trajectory
acceptance (which is affected by tiny perturbations in the timing of events),
is quite robust in its mathematical properties: the undecidability barriers
are not affected by reasonable perturbations of the model.

*Proceedings of the
Third International Workshop on Hybrid Systems: Computation and Control*
(HSCC),
Lecture Notes in Computer Science 1790,
Springer, 2000, pp. 145-159.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2000 Springer.