---
_id: '4434'
abstract:
- lang: eng
  text: '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.'
acknowledgement: 'This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341,
  and the NSF CAREER award CCR-9501708. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: 'Henzinger TA, Raskin J. Robust undecidability of timed and hybrid systems.
    In: <i>Proceedings of the 3rd International Workshop on Hybrid Systems</i>. Vol
    1790. Springer; 2000:145-159. doi:<a href="https://doi.org/10.1007/3-540-46430-1_15">10.1007/3-540-46430-1_15</a>'
  apa: 'Henzinger, T. A., &#38; Raskin, J. (2000). Robust undecidability of timed
    and hybrid systems. In <i>Proceedings of the 3rd International Workshop on Hybrid
    Systems</i> (Vol. 1790, pp. 145–159). Pittsburgh, PA, USA: Springer. <a href="https://doi.org/10.1007/3-540-46430-1_15">https://doi.org/10.1007/3-540-46430-1_15</a>'
  chicago: Henzinger, Thomas A, and Jean Raskin. “Robust Undecidability of Timed and
    Hybrid Systems.” In <i>Proceedings of the 3rd International Workshop on Hybrid
    Systems</i>, 1790:145–59. Springer, 2000. <a href="https://doi.org/10.1007/3-540-46430-1_15">https://doi.org/10.1007/3-540-46430-1_15</a>.
  ieee: T. A. Henzinger and J. Raskin, “Robust undecidability of timed and hybrid
    systems,” in <i>Proceedings of the 3rd International Workshop on Hybrid Systems</i>,
    Pittsburgh, PA, USA, 2000, vol. 1790, pp. 145–159.
  ista: 'Henzinger TA, Raskin J. 2000. Robust undecidability of timed and hybrid systems.
    Proceedings of the 3rd International Workshop on Hybrid Systems. HSCC: Hybrid
    Systems - Computation and Control, LNCS, vol. 1790, 145–159.'
  mla: Henzinger, Thomas A., and Jean Raskin. “Robust Undecidability of Timed and
    Hybrid Systems.” <i>Proceedings of the 3rd International Workshop on Hybrid Systems</i>,
    vol. 1790, Springer, 2000, pp. 145–59, doi:<a href="https://doi.org/10.1007/3-540-46430-1_15">10.1007/3-540-46430-1_15</a>.
  short: T.A. Henzinger, J. Raskin, in:, Proceedings of the 3rd International Workshop
    on Hybrid Systems, Springer, 2000, pp. 145–159.
conference:
  end_date: 2000-03-25
  location: Pittsburgh, PA, USA
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 2000-03-23
date_created: 2018-12-11T12:08:50Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:16:13Z
day: '01'
doi: 10.1007/3-540-46430-1_15
extern: '1'
intvolume: '      1790'
language:
- iso: eng
month: '01'
oa_version: None
page: 145 - 159
publication: Proceedings of the 3rd International Workshop on Hybrid Systems
publication_identifier:
  isbn:
  - '9783540672593'
publication_status: published
publisher: Springer
publist_id: '298'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Robust undecidability of timed and hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1790
year: '2000'
...
---
_id: '4481'
abstract:
- lang: eng
  text: 'Since hybrid embedded systems are pervasive and often safety-critical, guarantees
    about their correct performance are desirable. The hybrid systems model checker
    HyTech provides such guarantees and has successfully verified some systems. However,
    HyTech severely restricts the continuous dynamics of the system being analyzed
    and, therefore, often forces the use of prohibitively expensive discrete and polyhedral
    abstractions. We have designed a new algorithm, which is capable of directly verifying
    hybrid systems with general continuous dynamics, such as linear and nonlinear
    differential equations. The new algorithm conservatively overapproximates the
    reachable states of a hybrid automaton by using interval numerical methods. Interval
    numerical methods return sets of points that enclose the true result of numerical
    computation and, thus, avoid distortions due to the accumulation of round-off
    errors. We have implemented the new algorithm in a successor tool to HyTech called
    HyperTech. We consider three examples: a thermostat with delay, a two-tank water
    system, and an air-traffic collision avoidance protocol. HyperTech enables the
    direct, fully automatic analysis of these systems, which is also more accurate
    than the use of polyhedral abstractions.'
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341,
  and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Benjamin
  full_name: Horowitz, Benjamin
  last_name: Horowitz
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Howard
  full_name: Wong Toi, Howard
  last_name: Wong Toi
citation:
  ama: 'Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. Beyond HyTech: Hybrid systems
    analysis using interval numerical methods. In: <i>Proceedings of the 3rd International
    Workshop on Hybrid Systems</i>. Vol 1790. Springer; 2000:130-144. doi:<a href="https://doi.org/10.1007/3-540-46430-1_14">10.1007/3-540-46430-1_14</a>'
  apa: 'Henzinger, T. A., Horowitz, B., Majumdar, R., &#38; Wong Toi, H. (2000). Beyond
    HyTech: Hybrid systems analysis using interval numerical methods. In <i>Proceedings
    of the 3rd International Workshop on Hybrid Systems</i> (Vol. 1790, pp. 130–144).
    Pittsburgh, PA, USA: Springer. <a href="https://doi.org/10.1007/3-540-46430-1_14">https://doi.org/10.1007/3-540-46430-1_14</a>'
  chicago: 'Henzinger, Thomas A, Benjamin Horowitz, Ritankar Majumdar, and Howard
    Wong Toi. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.”
    In <i>Proceedings of the 3rd International Workshop on Hybrid Systems</i>, 1790:130–44.
    Springer, 2000. <a href="https://doi.org/10.1007/3-540-46430-1_14">https://doi.org/10.1007/3-540-46430-1_14</a>.'
  ieee: 'T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong Toi, “Beyond HyTech:
    Hybrid systems analysis using interval numerical methods,” in <i>Proceedings of
    the 3rd International Workshop on Hybrid Systems</i>, Pittsburgh, PA, USA, 2000,
    vol. 1790, pp. 130–144.'
  ista: 'Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. 2000. Beyond HyTech: Hybrid
    systems analysis using interval numerical methods. Proceedings of the 3rd International
    Workshop on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, LNCS,
    vol. 1790, 130–144.'
  mla: 'Henzinger, Thomas A., et al. “Beyond HyTech: Hybrid Systems Analysis Using
    Interval Numerical Methods.” <i>Proceedings of the 3rd International Workshop
    on Hybrid Systems</i>, vol. 1790, Springer, 2000, pp. 130–44, doi:<a href="https://doi.org/10.1007/3-540-46430-1_14">10.1007/3-540-46430-1_14</a>.'
  short: T.A. Henzinger, B. Horowitz, R. Majumdar, H. Wong Toi, in:, Proceedings of
    the 3rd International Workshop on Hybrid Systems, Springer, 2000, pp. 130–144.
conference:
  end_date: 2000-03-25
  location: Pittsburgh, PA, USA
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 2000-03-23
date_created: 2018-12-11T12:09:04Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:44:52Z
day: '01'
doi: 10.1007/3-540-46430-1_14
extern: '1'
intvolume: '      1790'
language:
- iso: eng
month: '01'
oa_version: None
page: 130 - 144
publication: Proceedings of the 3rd International Workshop on Hybrid Systems
publication_identifier:
  isbn:
  - '9783540672593'
publication_status: published
publisher: Springer
publist_id: '247'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Beyond HyTech: Hybrid systems analysis using interval numerical methods'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1790
year: '2000'
...