Thomas A. Henzinger and Jean-Francois Raskin

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-99-1073
October 1999

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/CSD-99-1073.pdf

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

BibTeX citation:

@techreport{Henzinger:CSD-99-1073,
    Author = {Henzinger, Thomas A. and Raskin, Jean-Francois},
    Title = {Robust Undecidability of Timed and Hybrid Systems},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1999},
    Month = {Oct},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5716.html},
    Number = {UCB/CSD-99-1073},
    Abstract = {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 conclusively 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.}
}

EndNote citation:

%0 Report
%A Henzinger, Thomas A.
%A Raskin, Jean-Francois
%T Robust Undecidability of Timed and Hybrid Systems
%I EECS Department, University of California, Berkeley
%D 1999
%@ UCB/CSD-99-1073
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5716.html
%F Henzinger:CSD-99-1073