--- _id: '4450' abstract: - lang: eng 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." 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. 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: Pei full_name: Ho, Pei last_name: Ho citation: 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' 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' 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. 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. 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.' 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. short: T.A. Henzinger, P. Ho, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 225–238. conference: end_date: 1995-07-05 location: Liege, Belgium name: 'CAV: Computer Aided Verification' start_date: 1995-07-03 date_created: 2018-12-11T12:08:55Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-10T09:48:52Z day: '01' doi: 10.1007/3-540-60045-0_53 extern: '1' intvolume: ' 939' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60045-0_53 month: '01' oa_version: None page: 225 - 238 publication: 7th International Conference on Computer Aided Verification publication_identifier: isbn: - '9783540494133' publication_status: published publisher: Springer publist_id: '280' quality_controlled: '1' scopus_import: '1' status: public title: Algorithmic analysis of nonlinear hybrid systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 939 year: '1995' ... --- _id: '4448' 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. 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.' 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: Pei full_name: Ho, Pei last_name: Ho citation: 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. 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. 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. 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. 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. conference: end_date: 1994-10-30 location: Ithaca, NY, United States of America name: Hybrid Systems II start_date: 1994-10-28 date_created: 2018-12-11T12:08:54Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-10T11:48:59Z day: '01' doi: 10.1007/3-540-60472-3_13 editor: - first_name: Antsaklis full_name: Panos, Antsaklis last_name: Panos - first_name: Wolf full_name: Kohn, Wolf last_name: Kohn - first_name: Anil full_name: Nerode, Anil last_name: Nerode - first_name: Shankar full_name: Sastry, Shankar last_name: Sastry extern: '1' intvolume: ' 999' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60472-3_13 month: '01' oa_version: None page: 252 - 264 publication: 3rd International Hybrid Systems Workshop publication_identifier: isbn: - '9783540604723' publication_status: published publisher: Springer publist_id: '282' quality_controlled: '1' status: public title: A note on abstract-interpretation strategies for hybrid automata type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 999 year: '1995' ... --- _id: '4447' 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. 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. 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: Pei full_name: Ho, Pei last_name: Ho citation: 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' 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.' 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.' 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.' 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. conference: end_date: 1955-10-25 location: ' New Brunswick, NJ, United States of America' name: Hybrid Systems III start_date: 1995-10-22 date_created: 2018-12-11T12:08:54Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-10T11:24:15Z day: '01' doi: 10.1007/3-540-60472-3_14 editor: - first_name: Antsaklis full_name: Panos, Antsaklis last_name: Panos - first_name: Wolf full_name: Kohn, Wolf last_name: Kohn - first_name: Anil full_name: Nerode, Anil last_name: Nerode - first_name: Shankar full_name: Sastry, Shankar last_name: Sastry extern: '1' intvolume: ' 999' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60472-3_14 month: '01' oa_version: None page: 265 - 293 publication: 4th International Hybrid Systems Workshop publication_identifier: isbn: - '9783540683346' publication_status: published publisher: Springer publist_id: '281' quality_controlled: '1' series_title: LNCS status: public title: 'HyTech: The Cornell Hybrid Technology Tool' type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 999 year: '1995' ... --- _id: '4497' abstract: - lang: eng 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." 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. 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: Pei full_name: Ho, Pei last_name: Ho - first_name: Howard full_name: Wong Toi, Howard last_name: Wong Toi citation: 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' 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. 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. 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.' 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. 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. conference: end_date: 1995-05-20 location: Aarhus, Denmark name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 1995-05-19 date_created: 2018-12-11T12:09:09Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-10T09:00:05Z day: '01' doi: 10.1007/3-540-60630-0_3 extern: '1' intvolume: ' 1019' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60630-0_3 month: '01' oa_version: None page: 41 - 71 publication: 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems publication_identifier: isbn: - '9783540606307' publication_status: published publisher: Springer publist_id: '230' quality_controlled: '1' scopus_import: '1' status: public title: A user guide to HyTech type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 1019 year: '1995' ... --- _id: '4499' 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 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: Pei full_name: Ho, Pei last_name: Ho - first_name: Howard full_name: Wong Toi, Howard last_name: Wong Toi citation: 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 ' 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 ' 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 .' 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.' 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.' 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 .' short: T.A. Henzinger, P. Ho, H. Wong Toi, in:, Proceedings 16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65. conference: end_date: 1995-12-07 location: Pisa, Italy name: 'RTSS: Real-Time Systems Symposium' start_date: 1995-12-05 date_created: 2018-12-11T12:09:10Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-10T09:33:19Z day: '01' doi: '10.1109/REAL.1995.495196 ' extern: '1' language: - iso: eng main_file_link: - url: https://ieeexplore.ieee.org/document/495196 month: '01' oa_version: None page: 56 - 65 publication: Proceedings 16th IEEE Real-Time Systems Symposium publication_identifier: isbn: - '0818673370' publication_status: published publisher: IEEE publist_id: '232' quality_controlled: '1' scopus_import: '1' status: public title: 'HyTech: The next generation' type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1995' ... --- _id: '4498' abstract: - lang: eng text: We present algorithms for computing similarity relations of labeled graphs. Similarity relations have applications for the refinement and verification of reactive systems. For finite graphs, we present an O(mn) algorithm for computing the similarity relation of a graph with n vertices and m edges (assuming m⩾n). For effectively presented infinite graphs, we present a symbolic similarity-checking procedure that terminates if a finite similarity relation exists. We show that 2D rectangular automata, which model discrete reactive systems with continuous environments, define effectively presented infinite graphs with finite similarity relations. It follows that the refinement problem and the ∀CTL* model-checking problem are decidable for 2D rectangular automata article_processing_charge: No author: - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - 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: Peter full_name: Kopke, Peter last_name: Kopke citation: ama: 'Henzinger MH, Henzinger TA, Kopke P. Computing simulations on finite and infinite graphs. In: Proceedings of IEEE 36th Annual Foundations of Computer Science. IEEE; 1995:453-462. doi:10.1109/SFCS.1995.492576' apa: 'Henzinger, M. H., Henzinger, T. A., & Kopke, P. (1995). Computing simulations on finite and infinite graphs. In Proceedings of IEEE 36th Annual Foundations of Computer Science (pp. 453–462). Milwaukee, WI, United States of America: IEEE. https://doi.org/10.1109/SFCS.1995.492576' chicago: Henzinger, Monika H, Thomas A Henzinger, and Peter Kopke. “Computing Simulations on Finite and Infinite Graphs.” In Proceedings of IEEE 36th Annual Foundations of Computer Science, 453–62. IEEE, 1995. https://doi.org/10.1109/SFCS.1995.492576. ieee: M. H. Henzinger, T. A. Henzinger, and P. Kopke, “Computing simulations on finite and infinite graphs,” in Proceedings of IEEE 36th Annual Foundations of Computer Science, Milwaukee, WI, United States of America, 1995, pp. 453–462. ista: 'Henzinger MH, Henzinger TA, Kopke P. 1995. Computing simulations on finite and infinite graphs. Proceedings of IEEE 36th Annual Foundations of Computer Science. FOCS: Foundations of Computer Science, 453–462.' mla: Henzinger, Monika H., et al. “Computing Simulations on Finite and Infinite Graphs.” Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 453–62, doi:10.1109/SFCS.1995.492576. short: M.H. Henzinger, T.A. Henzinger, P. Kopke, in:, Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 453–462. conference: end_date: 1995-10-25 location: Milwaukee, WI, United States of America name: 'FOCS: Foundations of Computer Science' start_date: 1995-10-23 date_created: 2018-12-11T12:09:10Z date_published: 1995-11-01T00:00:00Z date_updated: 2023-02-09T08:43:48Z day: '01' doi: 10.1109/SFCS.1995.492576 extern: '1' language: - iso: eng month: '11' oa_version: None page: 453 - 462 publication: Proceedings of IEEE 36th Annual Foundations of Computer Science publication_identifier: isbn: - '0818671831' issn: - 0272-5428 publication_status: published publisher: IEEE publist_id: '231' quality_controlled: '1' scopus_import: '1' status: public title: Computing simulations on finite and infinite graphs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '1995' ... --- _id: '4502' abstract: - lang: eng text: "Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify the precise boundary between decidability and undecidability of the reachability problem for hybrid automata.\r\n\r\nOn the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the omega-languages of initialized rectangular automata with bounded nondeterminism.\r\n\r\nOn the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch." acknowledgement: "We thank Howard Wong-Toi for a careful reading.\r\n" 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: Peter full_name: Kopke, Peter last_name: Kopke - first_name: Anuj full_name: Puri, Anuj last_name: Puri - first_name: P. full_name: Varaiya, P. last_name: Varaiya citation: ama: 'Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Proceedings of the 27th Annual ACM Symposium on Theory of Computing. ACM; 1995:373-382. doi:10.1145/225058.225162' apa: 'Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1995). What’s decidable about hybrid automata? In Proceedings of the 27th annual ACM symposium on Theory of computing (pp. 373–382). Las Vegas, NV, United States of America: ACM. https://doi.org/10.1145/225058.225162' chicago: Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” In Proceedings of the 27th Annual ACM Symposium on Theory of Computing, 373–82. ACM, 1995. https://doi.org/10.1145/225058.225162. ieee: T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” in Proceedings of the 27th annual ACM symposium on Theory of computing, Las Vegas, NV, United States of America, 1995, pp. 373–382. ista: 'Henzinger TA, Kopke P, Puri A, Varaiya P. 1995. What’s decidable about hybrid automata? Proceedings of the 27th annual ACM symposium on Theory of computing. STOC: Symposium on the Theory of Computing, 373–382.' mla: Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” Proceedings of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–82, doi:10.1145/225058.225162. short: T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, in:, Proceedings of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–382. conference: end_date: 1995-06-01 location: Las Vegas, NV, United States of America name: 'STOC: Symposium on the Theory of Computing' start_date: 1995-05-29 date_created: 2018-12-11T12:09:11Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-09T14:40:29Z day: '01' doi: 10.1145/225058.225162 extern: '1' language: - iso: eng main_file_link: - open_access: '1' url: https://dl.acm.org/doi/10.1145/225058.225162 month: '01' oa: 1 oa_version: Published Version page: 373 - 382 publication: Proceedings of the 27th annual ACM symposium on Theory of computing publication_identifier: isbn: - '9780897917186' publication_status: published publisher: ACM publist_id: '228' quality_controlled: '1' status: public title: What's decidable about hybrid automata? type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1995' ... --- _id: '4500' abstract: - lang: eng text: 'We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition—the divergence of time—can express Büchi, Muller, Streett, Rabin, and weak and strong fairness conditions on a given labeled transition system. We then consider the effect, on both timed and time-abstract expressiveness, of varying the following parameters: time domain (discrete or dense), number of clocks, number of states, and size of constants used in timing restrictions.' acknowledgement: "This research was supported in part by the National Science Foundation under grant CCR-9200794, by the United States Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Defense Advanced Research Projects Agency under grant NAG2-892, and by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University, Contract Number DAAL03-91-C-0027.\r\nThe full version of this paper is available from the Department of Computer Science, Cornell University, Ithaca, NY 14853, as Technical Report TR95-1496." 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: Peter full_name: Kopke, Peter last_name: Kopke - first_name: Howard full_name: Wong Toi, Howard last_name: Wong Toi citation: ama: 'Henzinger TA, Kopke P, Wong Toi H. The expressive power of clocks. In: 22nd International Colloquium on Automata, Languages and Programming . Vol 944. Springer; 1995:417-428. doi:10.1007/3-540-60084-1_93' apa: 'Henzinger, T. A., Kopke, P., & Wong Toi, H. (1995). The expressive power of clocks. In 22nd International Colloquium on Automata, Languages and Programming (Vol. 944, pp. 417–428). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_93' chicago: Henzinger, Thomas A, Peter Kopke, and Howard Wong Toi. “The Expressive Power of Clocks.” In 22nd International Colloquium on Automata, Languages and Programming , 944:417–28. Springer, 1995. https://doi.org/10.1007/3-540-60084-1_93. ieee: T. A. Henzinger, P. Kopke, and H. Wong Toi, “The expressive power of clocks,” in 22nd International Colloquium on Automata, Languages and Programming , Szeged, Hungary, 1995, vol. 944, pp. 417–428. ista: 'Henzinger TA, Kopke P, Wong Toi H. 1995. The expressive power of clocks. 22nd International Colloquium on Automata, Languages and Programming . ICALP: Automata, Languages and Programming, LNCS, vol. 944, 417–428.' mla: Henzinger, Thomas A., et al. “The Expressive Power of Clocks.” 22nd International Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995, pp. 417–28, doi:10.1007/3-540-60084-1_93. short: T.A. Henzinger, P. Kopke, H. Wong Toi, in:, 22nd International Colloquium on Automata, Languages and Programming , Springer, 1995, pp. 417–428. conference: end_date: 1995-07-14 location: Szeged, Hungary name: 'ICALP: Automata, Languages and Programming' start_date: 1995-07-10 date_created: 2018-12-11T12:09:10Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-09T14:58:31Z day: '01' doi: 10.1007/3-540-60084-1_93 extern: '1' intvolume: ' 944' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60084-1_93 month: '01' oa_version: None page: 417 - 428 publication: '22nd International Colloquium on Automata, Languages and Programming ' publication_identifier: isbn: - '9783540600848' publication_status: published publisher: Springer publist_id: '229' quality_controlled: '1' status: public title: The expressive power of clocks type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 944 year: '1995' ... --- _id: '4518' abstract: - lang: eng text: The analysis, verification, and control of hybrid automata with finite bisimulations can be reduced to finite-state problems. We advocate a time-abstract, phase-based methodology for checking if a given hybrid automaton has a finite bisimulation. First, we factor the automaton into two components, a boolean automaton with a discrete dynamics on the finite state space B m and a euclidean automaton with a continuous dynamics on the infinite state space n . Second, we investigate the phase portrait of the euclidean component. In this fashion, we obtain new decidability results for hybrid systems as well as new, uniform proofs of known decidability results. 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.\r\n" 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 citation: ama: 'Henzinger TA. Hybrid automata with finite bisimulations. In: 22nd International Colloquium on Automata, Languages and Programming . Vol 944. Springer; 1995:324-335. doi:10.1007/3-540-60084-1_85' apa: 'Henzinger, T. A. (1995). Hybrid automata with finite bisimulations. In 22nd International Colloquium on Automata, Languages and Programming (Vol. 944, pp. 324–335). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_85' chicago: Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” In 22nd International Colloquium on Automata, Languages and Programming , 944:324–35. Springer, 1995. https://doi.org/10.1007/3-540-60084-1_85. ieee: T. A. Henzinger, “Hybrid automata with finite bisimulations,” in 22nd International Colloquium on Automata, Languages and Programming , Szeged, Hungary, 1995, vol. 944, pp. 324–335. ista: 'Henzinger TA. 1995. Hybrid automata with finite bisimulations. 22nd International Colloquium on Automata, Languages and Programming . ICALP: Automata, Languages and Programming, LNCS, vol. 944, 324–335.' mla: Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” 22nd International Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995, pp. 324–35, doi:10.1007/3-540-60084-1_85. short: T.A. Henzinger, in:, 22nd International Colloquium on Automata, Languages and Programming , Springer, 1995, pp. 324–335. conference: end_date: 1995-07-14 location: Szeged, Hungary name: 'ICALP: Automata, Languages and Programming' start_date: 1995-07-10 date_created: 2018-12-11T12:09:16Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-09T14:21:08Z day: '01' doi: 10.1007/3-540-60084-1_85 extern: '1' intvolume: ' 944' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60084-1_85 month: '01' oa_version: None page: 324 - 335 publication: '22nd International Colloquium on Automata, Languages and Programming ' publication_identifier: isbn: - '9783540600848' publication_status: published publisher: Springer publist_id: '212' quality_controlled: '1' status: public title: Hybrid automata with finite bisimulations type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 944 year: '1995' ... --- _id: '4587' abstract: - lang: eng text: We argue that the standard constraints on liveness conditions in nonblocking trace models—machine closure for closed systems, and receptiveness for open systems—are unnecessarily weak and complex, and that liveness should, instead, be specified by augmenting transition systems with acceptance conditions that satisfy a locality constraint. First, locality implies machine closure and receptiveness, and thus permits the composition and modular verification of live transition systems. Second, while machine closure and receptiveness are based on infinite games, locality is based on repeated finite games, and thus easier to check. Third, no expressive power is lost by the restriction to local liveness conditions. We illustrate the appeal of local liveness using the model of Fair Reactive Systems, a nonblocking trace model of communicating processes. acknowledgement: Supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892. alternative_title: - LNCS article_processing_charge: No author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Alur R, Henzinger TA. Local liveness for compositional modeling of fair reactive systems. In: 7th International Conference on Computer Aided Verification. Vol 939. Springer; 1995:166-179. doi:10.1007/3-540-60045-0_49' apa: 'Alur, R., & Henzinger, T. A. (1995). Local liveness for compositional modeling of fair reactive systems. In 7th International Conference on Computer Aided Verification (Vol. 939, pp. 166–179). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_49' chicago: Alur, Rajeev, and Thomas A Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” In 7th International Conference on Computer Aided Verification, 939:166–79. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_49. ieee: R. Alur and T. A. Henzinger, “Local liveness for compositional modeling of fair reactive systems,” in 7th International Conference on Computer Aided Verification, Liege, Belgium, 1995, vol. 939, pp. 166–179. ista: 'Alur R, Henzinger TA. 1995. Local liveness for compositional modeling of fair reactive systems. 7th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 939, 166–179.' mla: Alur, Rajeev, and Thomas A. Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” 7th International Conference on Computer Aided Verification, vol. 939, Springer, 1995, pp. 166–79, doi:10.1007/3-540-60045-0_49. short: R. Alur, T.A. Henzinger, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 166–179. conference: end_date: 1995-07-05 location: Liege, Belgium name: 'CAV: Computer Aided Verification' start_date: 1995-07-03 date_created: 2018-12-11T12:09:37Z date_published: 1995-01-01T00:00:00Z date_updated: 2022-06-09T14:05:04Z day: '01' doi: 10.1007/3-540-60045-0_49 extern: '1' intvolume: ' 939' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-60045-0_49 month: '01' oa_version: None page: 166 - 179 publication: 7th International Conference on Computer Aided Verification publication_identifier: isbn: - 978-3-540-60045-9 publication_status: published publisher: Springer publist_id: '120' quality_controlled: '1' status: public title: Local liveness for compositional modeling of fair reactive systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 939 year: '1995' ... --- _id: '4613' abstract: - lang: eng text: We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge. article_processing_charge: No article_type: original author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Costas full_name: Courcoubetis, Costas last_name: Courcoubetis - first_name: Nicolas full_name: Halbwachs, Nicolas last_name: Halbwachs - 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: Pei full_name: Ho, Pei last_name: Ho - first_name: Xavier full_name: Nicollin, Xavier last_name: Nicollin - first_name: Alfredo full_name: Olivero, Alfredo last_name: Olivero - first_name: Joseph full_name: Sifakis, Joseph last_name: Sifakis - first_name: Sergio full_name: Yovine, Sergio last_name: Yovine citation: ama: Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 1995;138(1):3-34. doi:10.1016/0304-3975(94)00202-T apa: Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin, X., … Yovine, S. (1995). The algorithmic analysis of hybrid systems. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/0304-3975(94)00202-T chicago: Alur, Rajeev, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, Pei Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis of Hybrid Systems.” Theoretical Computer Science. Elsevier, 1995. https://doi.org/10.1016/0304-3975(94)00202-T. ieee: R. Alur et al., “The algorithmic analysis of hybrid systems,” Theoretical Computer Science, vol. 138, no. 1. Elsevier, pp. 3–34, 1995. ista: Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis J, Yovine S. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 138(1), 3–34. mla: Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” Theoretical Computer Science, vol. 138, no. 1, Elsevier, 1995, pp. 3–34, doi:10.1016/0304-3975(94)00202-T. short: R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, Theoretical Computer Science 138 (1995) 3–34. date_created: 2018-12-11T12:09:45Z date_published: 1995-02-06T00:00:00Z date_updated: 2022-06-09T13:40:48Z day: '06' doi: 10.1016/0304-3975(94)00202-T extern: '1' intvolume: ' 138' issue: '1' language: - iso: eng main_file_link: - url: https://www.sciencedirect.com/science/article/pii/030439759400202T?via%3Dihub month: '02' oa_version: None page: 3 - 34 publication: Theoretical Computer Science publication_identifier: issn: - 0304-3975 publication_status: published publisher: Elsevier publist_id: '94' quality_controlled: '1' status: public title: The algorithmic analysis of hybrid systems type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 138 year: '1995' ... --- _id: '6162' abstract: - lang: eng text: 'The tra-1 gene is the terminal global selector of somatic sex in Caenorhabditis elegans: High tra-1 activity elicits female somatic development while low tra-1 activity elicits male development. Previous genetic studies defined a cascade of negatively interacting genes that regulates tra-1 activity in response to the primary sex-determining signal. Here, we investigate the last step in this regulatory cascade, by studying rare gain-of-function (gf) mutations of tra-1 that direct female somatic development irrespective of the upstream sex-determining signal. These mutations appear to abolish negative regulation of tra-1 in male tissues. We identify the lesions associated with 29 of these mutations and find that all affect a short stretch of amino acid residues present in both protein products of the tra-1 gene. Twenty-six alleles are associated with single nonconservative amino acid substitutions. Two alleles affect tra-1 RNA splicing and generate messages that omit part or all of the exon encoding this short stretch. These results suggest that sexual regulation of tra-1 is achieved post-translationally, by an inhibitory protein-protein interaction. The amino acid stretch altered by the tra-1(gf) mutations may define a site of interaction for negative regulators of tra-1. The stretch includes a potential phosphorylation site for glycogen synthase kinase 3 and may be conserved in the human gene GLI3, a homolog of tra-1 identified previously.' author: - first_name: Mario full_name: de Bono, Mario id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87 last_name: de Bono orcid: 0000-0001-8347-0443 - first_name: D. full_name: Zarkower, D. last_name: Zarkower - first_name: J. full_name: Hodgkin, J. last_name: Hodgkin citation: ama: de Bono M, Zarkower D, Hodgkin J. Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1. Genes and Development. 1995;9(2):155-167. doi:10.1101/gad.9.2.155 apa: de Bono, M., Zarkower, D., & Hodgkin, J. (1995). Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1. Genes and Development. CSH Press. https://doi.org/10.1101/gad.9.2.155 chicago: Bono, Mario de, D. Zarkower, and J. Hodgkin. “Dominant Feminizing Mutations Implicate Protein-Protein Interactions as the Main Mode of Regulation of the Nematode Sex-Determining Gene Tra-1.” Genes and Development. CSH Press, 1995. https://doi.org/10.1101/gad.9.2.155. ieee: M. de Bono, D. Zarkower, and J. Hodgkin, “Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1,” Genes and Development, vol. 9, no. 2. CSH Press, pp. 155–167, 1995. ista: de Bono M, Zarkower D, Hodgkin J. 1995. Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1. Genes and Development. 9(2), 155–167. mla: de Bono, Mario, et al. “Dominant Feminizing Mutations Implicate Protein-Protein Interactions as the Main Mode of Regulation of the Nematode Sex-Determining Gene Tra-1.” Genes and Development, vol. 9, no. 2, CSH Press, 1995, pp. 155–67, doi:10.1101/gad.9.2.155. short: M. de Bono, D. Zarkower, J. Hodgkin, Genes and Development 9 (1995) 155–167. date_created: 2019-03-21T11:57:40Z date_published: 1995-01-15T00:00:00Z date_updated: 2021-01-12T08:06:29Z day: '15' doi: 10.1101/gad.9.2.155 extern: '1' external_id: pmid: - '7851791' intvolume: ' 9' issue: '2' language: - iso: eng month: '01' oa_version: None page: 155-167 pmid: 1 publication: Genes and Development publication_identifier: issn: - '08909369' publication_status: published publisher: CSH Press quality_controlled: '1' status: public title: Dominant feminizing mutations implicate protein-protein interactions as the main mode of regulation of the nematode sex-determining gene tra-1 type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 9 year: '1995' ...