[{"acknowledgement":"This research was supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.","quality_controlled":"1","publisher":"Springer","day":"01","publication":"7th International Conference on Computer Aided Verification","year":"1995","doi":"10.1007/3-540-60045-0_53","date_published":"1995-01-01T00:00:00Z","date_created":"2018-12-11T12:08:55Z","page":"225 - 238","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"mla":"Henzinger, Thomas A., and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” 7th International Conference on Computer Aided Verification, vol. 939, Springer, 1995, pp. 225–38, doi:10.1007/3-540-60045-0_53.","apa":"Henzinger, T. A., & Ho, P. (1995). Algorithmic analysis of nonlinear hybrid systems. In 7th International Conference on Computer Aided Verification (Vol. 939, pp. 225–238). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_53","ama":"Henzinger TA, Ho P. Algorithmic analysis of nonlinear hybrid systems. In: 7th International Conference on Computer Aided Verification. Vol 939. Springer; 1995:225-238. doi:10.1007/3-540-60045-0_53","ieee":"T. A. Henzinger and P. Ho, “Algorithmic analysis of nonlinear hybrid systems,” in 7th International Conference on Computer Aided Verification, Liege, Belgium, 1995, vol. 939, pp. 225–238.","short":"T.A. Henzinger, P. Ho, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 225–238.","chicago":"Henzinger, Thomas A, and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” In 7th International Conference on Computer Aided Verification, 939:225–38. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_53.","ista":"Henzinger TA, Ho P. 1995. Algorithmic analysis of nonlinear hybrid systems. 7th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 939, 225–238."},"title":"Algorithmic analysis of nonlinear hybrid systems","publist_id":"280","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Pei","last_name":"Ho","full_name":"Ho, Pei"}],"article_processing_charge":"No","oa_version":"None","abstract":[{"text":"Hybrid systems model discrete programs that are embedded in continuous environments. Model-checking tools are available for the analysis of linear hybrid systems, whose continuous variables are bounded by piecewise-linear trajectories. Most embedded programs, however, operate in nonlinear environments. We present, analyze, and apply two algorithms for translating nonlinear hybrid systems into linear hybrid systems.\r\nThe clock translation replaces nonlinear variables by clock variables; the rate translation approximates nonlinear variables by piecewise-linear envelopes. Both translations are sound for reachability; that is, if we establish a safety property of the translated linear system, we may conclude that the original nonlinear system satisfies the property. The clock translation is also complete for reachability; that is, the original system and the translated system satisfy the same safety properties. The two translations apply to incomparable classes of nonlinear hybrid systems. From the clock translation we obtain a new decidability result for hybrid systems.\r\nWith the help of Hytech, a symbolic model checker for linear hybrid systems, we automatically verify a nonlinear railroad gate control program using the clock translation, and a nonlinear temperature control program using the rate translation.","lang":"eng"}],"month":"01","intvolume":" 939","scopus_import":"1","alternative_title":["LNCS"],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60045-0_53"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783540494133"]},"publication_status":"published","volume":939,"_id":"4450","status":"public","type":"conference","conference":{"name":"CAV: Computer Aided Verification","end_date":"1995-07-05","location":"Liege, Belgium","start_date":"1995-07-03"},"extern":"1","date_updated":"2022-06-10T09:48:52Z"},{"date_updated":"2022-06-10T11:48:59Z","extern":"1","_id":"4448","type":"conference","conference":{"name":"Hybrid Systems II","location":"Ithaca, NY, United States of America","end_date":"1994-10-30","start_date":"1994-10-28"},"status":"public","publication_identifier":{"isbn":["9783540604723"]},"publication_status":"published","language":[{"iso":"eng"}],"volume":999,"abstract":[{"lang":"eng","text":"We report on several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems. We (1) simultaneously compute the target region from different directions, (2) conservatively approximate the target region by dropping constraints, and (3) iteratively refine the approximation until sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator."}],"oa_version":"None","alternative_title":["LNCS"],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60472-3_13"}],"month":"01","intvolume":" 999","citation":{"mla":"Henzinger, Thomas A., and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” 3rd International Hybrid Systems Workshop, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 252–64, doi:10.1007/3-540-60472-3_13.","ieee":"T. A. Henzinger and P. Ho, “A note on abstract-interpretation strategies for hybrid automata,” in 3rd International Hybrid Systems Workshop, Ithaca, NY, United States of America, 1995, vol. 999, pp. 252–264.","short":"T.A. Henzinger, P. Ho, in:, A. Panos, W. Kohn, A. Nerode, S. Sastry (Eds.), 3rd International Hybrid Systems Workshop, Springer, 1995, pp. 252–264.","ama":"Henzinger TA, Ho P. A note on abstract-interpretation strategies for hybrid automata. In: Panos A, Kohn W, Nerode A, Sastry S, eds. 3rd International Hybrid Systems Workshop. Vol 999. Springer; 1995:252-264. doi:10.1007/3-540-60472-3_13","apa":"Henzinger, T. A., & Ho, P. (1995). A note on abstract-interpretation strategies for hybrid automata. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.), 3rd International Hybrid Systems Workshop (Vol. 999, pp. 252–264). Ithaca, NY, United States of America: Springer. https://doi.org/10.1007/3-540-60472-3_13","chicago":"Henzinger, Thomas A, and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” In 3rd International Hybrid Systems Workshop, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:252–64. Springer, 1995. https://doi.org/10.1007/3-540-60472-3_13.","ista":"Henzinger TA, Ho P. 1995. A note on abstract-interpretation strategies for hybrid automata. 3rd International Hybrid Systems Workshop. Hybrid Systems II, LNCS, vol. 999, 252–264."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"282","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"}],"article_processing_charge":"No","editor":[{"full_name":"Panos, Antsaklis","last_name":"Panos","first_name":"Antsaklis"},{"last_name":"Kohn","full_name":"Kohn, Wolf","first_name":"Wolf"},{"full_name":"Nerode, Anil","last_name":"Nerode","first_name":"Anil"},{"last_name":"Sastry","full_name":"Sastry, Shankar","first_name":"Shankar"}],"title":"A note on abstract-interpretation strategies for hybrid automata","year":"1995","day":"01","publication":"3rd International Hybrid Systems Workshop","page":"252 - 264","date_published":"1995-01-01T00:00:00Z","doi":"10.1007/3-540-60472-3_13","date_created":"2018-12-11T12:08:54Z","acknowledgement":" National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","quality_controlled":"1","publisher":"Springer"},{"title":"HyTech: The Cornell Hybrid Technology Tool","editor":[{"full_name":"Panos, Antsaklis","last_name":"Panos","first_name":"Antsaklis"},{"first_name":"Wolf","full_name":"Kohn, Wolf","last_name":"Kohn"},{"last_name":"Nerode","full_name":"Nerode, Anil","first_name":"Anil"},{"last_name":"Sastry","full_name":"Sastry, Shankar","first_name":"Shankar"}],"author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Pei","last_name":"Ho","full_name":"Ho, Pei"}],"publist_id":"281","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"ista":"Henzinger TA, Ho P. 1995. HyTech: The Cornell Hybrid Technology Tool. 4th International Hybrid Systems Workshop. Hybrid Systems IIILNCS, LNCS, vol. 999, 265–293.","chicago":"Henzinger, Thomas A, and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” In 4th International Hybrid Systems Workshop, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:265–93. LNCS. Springer, 1995. https://doi.org/10.1007/3-540-60472-3_14.","ieee":"T. A. Henzinger and P. Ho, “HyTech: The Cornell Hybrid Technology Tool,” in 4th International Hybrid Systems Workshop, New Brunswick, NJ, United States of America, 1995, vol. 999, pp. 265–293.","short":"T.A. Henzinger, P. Ho, in:, A. Panos, W. Kohn, A. Nerode, S. Sastry (Eds.), 4th International Hybrid Systems Workshop, Springer, 1995, pp. 265–293.","ama":"Henzinger TA, Ho P. HyTech: The Cornell Hybrid Technology Tool. In: Panos A, Kohn W, Nerode A, Sastry S, eds. 4th International Hybrid Systems Workshop. Vol 999. LNCS. Springer; 1995:265-293. doi:10.1007/3-540-60472-3_14","apa":"Henzinger, T. A., & Ho, P. (1995). HyTech: The Cornell Hybrid Technology Tool. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.), 4th International Hybrid Systems Workshop (Vol. 999, pp. 265–293). New Brunswick, NJ, United States of America: Springer. https://doi.org/10.1007/3-540-60472-3_14","mla":"Henzinger, Thomas A., and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” 4th International Hybrid Systems Workshop, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 265–93, doi:10.1007/3-540-60472-3_14."},"quality_controlled":"1","publisher":"Springer","acknowledgement":"This research was supported in part by the National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","doi":"10.1007/3-540-60472-3_14","date_published":"1995-01-01T00:00:00Z","date_created":"2018-12-11T12:08:54Z","page":"265 - 293","day":"01","publication":"4th International Hybrid Systems Workshop","year":"1995","status":"public","type":"conference","conference":{"name":"Hybrid Systems III","end_date":"1955-10-25","location":" New Brunswick, NJ, United States of America","start_date":"1995-10-22"},"_id":"4447","series_title":"LNCS","extern":"1","date_updated":"2022-06-10T11:24:15Z","month":"01","intvolume":" 999","alternative_title":["LNCS"],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60472-3_14"}],"oa_version":"None","abstract":[{"lang":"eng","text":"This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies that have been incorporated into HyTech, and we illustrate the use of HyTech with three nontrivial case studies."}],"volume":999,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783540683346"]},"publication_status":"published"},{"abstract":[{"text":"HyTech is a tool for the automated analysis of embedded systems. This document, designed for the first-time user of HyTech, guides the reader through the underlying system model, and through the input language for describing and analyzing systems. The guide gives several examples of usage, and some hints for gaining maximal computational efficiency from the tool.\r\nThe version of HyTech described in this guide was released in August 1995, and is available through anonymous ftp from ftp.cs.cornell.edu in the directory pub/tah/HyTech, and through the World-Wide Web via HyTech's home page http:/www.cs.cornell.edu/Info/People/tah/hytech.html.","lang":"eng"}],"oa_version":"None","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60630-0_3"}],"alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 1019","month":"01","publication_status":"published","publication_identifier":{"isbn":["9783540606307"]},"language":[{"iso":"eng"}],"volume":1019,"_id":"4497","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"1995-05-20","location":"Aarhus, Denmark","start_date":"1995-05-19"},"type":"conference","status":"public","date_updated":"2022-06-10T09:00:05Z","extern":"1","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892.","publisher":"Springer","quality_controlled":"1","year":"1995","publication":"1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems","day":"01","page":"41 - 71","date_created":"2018-12-11T12:09:09Z","date_published":"1995-01-01T00:00:00Z","doi":"10.1007/3-540-60630-0_3","citation":{"ista":"Henzinger TA, Ho P, Wong Toi H. 1995. A user guide to HyTech. 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1019, 41–71.","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “A User Guide to HyTech.” In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1019:41–71. Springer, 1995. https://doi.org/10.1007/3-540-60630-0_3.","ama":"Henzinger TA, Ho P, Wong Toi H. A user guide to HyTech. In: 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Vol 1019. Springer; 1995:41-71. doi:10.1007/3-540-60630-0_3","apa":"Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). A user guide to HyTech. In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 1019, pp. 41–71). Aarhus, Denmark: Springer. https://doi.org/10.1007/3-540-60630-0_3","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1995, pp. 41–71.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “A user guide to HyTech,” in 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, 1995, vol. 1019, pp. 41–71.","mla":"Henzinger, Thomas A., et al. “A User Guide to HyTech.” 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1019, Springer, 1995, pp. 41–71, doi:10.1007/3-540-60630-0_3."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publist_id":"230","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Ho, Pei","last_name":"Ho","first_name":"Pei"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"title":"A user guide to HyTech"},{"abstract":[{"lang":"eng","text":"We describe a new implementation of HYTECH, a symbolic model checker for hybrid systems. Given a parametric description of an embedded system as a collection of communicating automata, HYTECH automatically computes the conditions on the parameters under which the system satisfies its safety and timing requirements. While the original HYTECH prototype was based on the symbolic algebra tool Mathematica, the new implementation is written in C++ and builds on geometric algorithms instead of formula manipulation. The new HYTECH offers a cleaner and more expressive input language, greater portability, superior performance (typically two to three orders of magnitude), and new features such as diagnostic error-trace generation. We illustrate the effectiveness of the new implementation by applying HYTECH to the automatic parametric analysis of the generic railroad crossing benchmark problem and to an active structure control algorithm"}],"oa_version":"None","scopus_import":"1","quality_controlled":"1","publisher":"IEEE","main_file_link":[{"url":"https://ieeexplore.ieee.org/document/495196"}],"month":"01","publication_identifier":{"isbn":["0818673370"]},"publication_status":"published","year":"1995","day":"01","publication":"Proceedings 16th IEEE Real-Time Systems Symposium","language":[{"iso":"eng"}],"page":"56 - 65","doi":"10.1109/REAL.1995.495196 ","date_published":"1995-01-01T00:00:00Z","date_created":"2018-12-11T12:09:10Z","_id":"4499","type":"conference","conference":{"location":"Pisa, Italy","end_date":"1995-12-07","start_date":"1995-12-05","name":"RTSS: Real-Time Systems Symposium"},"status":"public","citation":{"mla":"Henzinger, Thomas A., et al. “HyTech: The next Generation.” Proceedings 16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65, doi:10.1109/REAL.1995.495196 .","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: The next generation,” in Proceedings 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 1995, pp. 56–65.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, Proceedings 16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65.","apa":"Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). HyTech: The next generation. In Proceedings 16th IEEE Real-Time Systems Symposium (pp. 56–65). Pisa, Italy: IEEE. https://doi.org/10.1109/REAL.1995.495196 ","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: The next generation. In: Proceedings 16th IEEE Real-Time Systems Symposium. IEEE; 1995:56-65. doi:10.1109/REAL.1995.495196 ","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: The next Generation.” In Proceedings 16th IEEE Real-Time Systems Symposium, 56–65. IEEE, 1995. https://doi.org/10.1109/REAL.1995.495196 .","ista":"Henzinger TA, Ho P, Wong Toi H. 1995. HyTech: The next generation. Proceedings 16th IEEE Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium, 56–65."},"date_updated":"2022-06-10T09:33:19Z","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"232","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Ho, Pei","last_name":"Ho","first_name":"Pei"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}],"article_processing_charge":"No","title":"HyTech: The next generation"}]