[{"publication_status":"published","volume":1790,"article_processing_charge":"No","_id":"4434","date_published":"2000-01-01T00:00:00Z","abstract":[{"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.","lang":"eng"}],"scopus_import":"1","date_updated":"2023-04-18T13:16:13Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9783540672593"]},"publist_id":"298","oa_version":"None","year":"2000","publisher":"Springer","publication":"Proceedings of the 3rd International Workshop on Hybrid Systems","quality_controlled":"1","status":"public","intvolume":"      1790","page":"145 - 159","month":"01","extern":"1","date_created":"2018-12-11T12:08:50Z","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. ","language":[{"iso":"eng"}],"doi":"10.1007/3-540-46430-1_15","citation":{"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>","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>","short":"T.A. Henzinger, J. Raskin, in:, Proceedings of the 3rd International Workshop on Hybrid Systems, Springer, 2000, pp. 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>.","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.","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.","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>."},"title":"Robust undecidability of timed and hybrid systems","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2000-03-25","start_date":"2000-03-23","location":"Pittsburgh, PA, USA"},"day":"01","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"}],"type":"conference","alternative_title":["LNCS"]},{"month":"01","extern":"1","date_created":"2018-12-11T12:09:04Z","page":"130 - 144","publication":"Proceedings of the 3rd International Workshop on Hybrid Systems","quality_controlled":"1","intvolume":"      1790","status":"public","publisher":"Springer","day":"01","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Benjamin","full_name":"Horowitz, Benjamin","last_name":"Horowitz"},{"full_name":"Majumdar, Ritankar","first_name":"Ritankar","last_name":"Majumdar"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}],"type":"conference","alternative_title":["LNCS"],"citation":{"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>.","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.","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.","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.","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>"},"title":"Beyond HyTech: Hybrid systems analysis using interval numerical methods","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2000-03-23","end_date":"2000-03-25","location":"Pittsburgh, PA, USA"},"language":[{"iso":"eng"}],"doi":"10.1007/3-540-46430-1_14","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.","date_published":"2000-01-01T00:00:00Z","_id":"4481","abstract":[{"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.","lang":"eng"}],"article_processing_charge":"No","volume":1790,"publication_status":"published","publist_id":"247","year":"2000","oa_version":"None","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2023-04-18T12:44:52Z","publication_identifier":{"isbn":["9783540672593"]}}]