--- _id: '4491' abstract: - lang: eng text: We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology article_processing_charge: No article_type: original 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. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. 1998;43(4):540-554. doi:10.1109/9.664156 apa: Henzinger, T. A., Ho, P., & Wong Toi, H. (1998). Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. IEEE. https://doi.org/10.1109/9.664156 chicago: Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “Algorithmic Analysis of Nonlinear Hybrid Systems.” IEEE Transactions on Automatic Control. IEEE, 1998. https://doi.org/10.1109/9.664156 . ieee: T. A. Henzinger, P. Ho, and H. Wong Toi, “Algorithmic analysis of nonlinear hybrid systems,” IEEE Transactions on Automatic Control, vol. 43, no. 4. IEEE, pp. 540–554, 1998. ista: Henzinger TA, Ho P, Wong Toi H. 1998. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. 43(4), 540–554. mla: Henzinger, Thomas A., et al. “Algorithmic Analysis of Nonlinear Hybrid Systems.” IEEE Transactions on Automatic Control, vol. 43, no. 4, IEEE, 1998, pp. 540–54, doi:10.1109/9.664156 . short: T.A. Henzinger, P. Ho, H. Wong Toi, IEEE Transactions on Automatic Control 43 (1998) 540–554. date_created: 2018-12-11T12:09:07Z date_published: 1998-01-01T00:00:00Z date_updated: 2022-08-23T14:34:35Z day: '01' doi: '10.1109/9.664156 ' extern: '1' intvolume: ' 43' issue: '4' language: - iso: eng month: '01' oa_version: None page: 540 - 554 publication: IEEE Transactions on Automatic Control publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '238' quality_controlled: '1' status: public title: Algorithmic analysis of nonlinear hybrid systems type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 43 year: '1998' ... --- _id: '4024' abstract: - lang: eng text: We have developed general modeling software for a Cave Automatic Virtual Environment (CAVE); one of its applications is modeling 3D protein structures, generating both outside-in and inside-out views of geometric models. An advantage of the CAVE over other virtual environments is that multiple viewers can observe the same scene at the same time and place. Our software is scalable-from high-end virtual environments such as the CAVE, to mid-range immersive desktop systems, down to low-end graphics workstations. In the current configuration, a parallel Silicon Graphics Power Challenge supercomputer architecture performs the computationally intensive construction of surface patches remotely, and sends the results through the I-WAY (Information Wide Area Year) using VBNS (Very-high-Bandwidth Network Systems) to the graphics machines that drive the CAVE and our graphics visualization software, Valvis (Virtual ALpha shapes VISualizer). article_processing_charge: No article_type: original author: - first_name: Nataraj full_name: Akkiraju, Nataraj last_name: Akkiraju - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: Ping full_name: Fu, Ping last_name: Fu - first_name: Jiang full_name: Qian, Jiang last_name: Qian citation: ama: Akkiraju N, Edelsbrunner H, Fu P, Qian J. Viewing geometric protein structures from inside a CAVE. IEEE Computer Graphics and Applications. 1996;16(4):58-61. doi:10.1109/38.511855 apa: Akkiraju, N., Edelsbrunner, H., Fu, P., & Qian, J. (1996). Viewing geometric protein structures from inside a CAVE. IEEE Computer Graphics and Applications. IEEE. https://doi.org/10.1109/38.511855 chicago: Akkiraju, Nataraj, Herbert Edelsbrunner, Ping Fu, and Jiang Qian. “Viewing Geometric Protein Structures from inside a CAVE.” IEEE Computer Graphics and Applications. IEEE, 1996. https://doi.org/10.1109/38.511855. ieee: N. Akkiraju, H. Edelsbrunner, P. Fu, and J. Qian, “Viewing geometric protein structures from inside a CAVE,” IEEE Computer Graphics and Applications, vol. 16, no. 4. IEEE, pp. 58–61, 1996. ista: Akkiraju N, Edelsbrunner H, Fu P, Qian J. 1996. Viewing geometric protein structures from inside a CAVE. IEEE Computer Graphics and Applications. 16(4), 58–61. mla: Akkiraju, Nataraj, et al. “Viewing Geometric Protein Structures from inside a CAVE.” IEEE Computer Graphics and Applications, vol. 16, no. 4, IEEE, 1996, pp. 58–61, doi:10.1109/38.511855. short: N. Akkiraju, H. Edelsbrunner, P. Fu, J. Qian, IEEE Computer Graphics and Applications 16 (1996) 58–61. date_created: 2018-12-11T12:06:30Z date_published: 1996-07-01T00:00:00Z date_updated: 2022-08-09T13:32:21Z day: '01' doi: 10.1109/38.511855 extern: '1' intvolume: ' 16' issue: '4' language: - iso: eng month: '07' oa_version: None page: 58 - 61 publication: IEEE Computer Graphics and Applications publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '2101' quality_controlled: '1' scopus_import: '1' status: public title: Viewing geometric protein structures from inside a CAVE type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 16 year: '1996' ... --- _id: '4588' abstract: - lang: eng text: 'We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise refinement) reasoning. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message passing' 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. Reactive modules. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE; 1996:207-218. doi:10.1109/LICS.1996.561320' apa: 'Alur, R., & Henzinger, T. A. (1996). Reactive modules. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science (pp. 207–218). New Brunswick, NJ, USA: IEEE. https://doi.org/10.1109/LICS.1996.561320' chicago: Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 207–18. IEEE, 1996. https://doi.org/10.1109/LICS.1996.561320. ieee: R. Alur and T. A. Henzinger, “Reactive modules,” in Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA, 1996, pp. 207–218. ista: 'Alur R, Henzinger TA. 1996. Reactive modules. Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 207–218.' mla: Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1996, pp. 207–18, doi:10.1109/LICS.1996.561320. short: R. Alur, T.A. Henzinger, in:, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1996, pp. 207–218. conference: end_date: 1996-07-30 location: New Brunswick, NJ, USA name: 'LICS: Logic in Computer Science' start_date: 1996-07-27 date_created: 2018-12-11T12:09:37Z date_published: 1996-01-01T00:00:00Z date_updated: 2022-07-04T14:51:40Z day: '01' doi: 10.1109/LICS.1996.561320 extern: '1' language: - iso: eng main_file_link: - url: https://ieeexplore.ieee.org/document/561320 month: '01' oa_version: None page: 207 - 218 publication: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '121' quality_controlled: '1' scopus_import: '1' status: public title: Reactive modules type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1996' ... --- _id: '4611' abstract: - lang: eng text: Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms acknowledgement: "We thank Costas Courcoubetis, Nicolas Halbwachs, Peter Kopke, Joseph Sifakis, and Howard Wong-Toi for helpful\r\ndiscussions and valuable comments. Thomas A. Henzinger's research was supported in part by the U.S. Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by National Science Foundation grants CCR-9200794 and CCR-9504469, by U.S. Air Force Office of Scientific Research contract F49620-93-1- 0056, and by Advanced Research Projects Agency grant NAG2-892. " article_processing_charge: No article_type: original 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 - first_name: Pei full_name: Ho, Pei last_name: Ho citation: ama: Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 1996;22(3):181-201. doi:10.1109/32.489079 apa: Alur, R., Henzinger, T. A., & Ho, P. (1996). Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. IEEE. https://doi.org/10.1109/32.489079 chicago: Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering. IEEE, 1996. https://doi.org/10.1109/32.489079. ieee: R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded systems,” IEEE Transactions on Software Engineering, vol. 22, no. 3. IEEE, pp. 181–201, 1996. ista: Alur R, Henzinger TA, Ho P. 1996. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering. 22(3), 181–201. mla: Alur, Rajeev, et al. “Automatic Symbolic Verification of Embedded Systems.” IEEE Transactions on Software Engineering, vol. 22, no. 3, IEEE, 1996, pp. 181–201, doi:10.1109/32.489079. short: R. Alur, T.A. Henzinger, P. Ho, IEEE Transactions on Software Engineering 22 (1996) 181–201. date_created: 2018-12-11T12:09:45Z date_published: 1996-03-01T00:00:00Z date_updated: 2022-07-04T12:47:05Z day: '01' doi: 10.1109/32.489079 extern: '1' intvolume: ' 22' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://ecommons.cornell.edu/handle/1813/7170 month: '03' oa: 1 oa_version: Published Version page: 181 - 201 publication: IEEE Transactions on Software Engineering publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '96' quality_controlled: '1' scopus_import: '1' status: public title: Automatic symbolic verification of embedded systems type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 22 year: '1996' ... --- _id: '4586' abstract: - lang: eng text: 'Fairness is a mathematical abstraction: in a multiprogramming environment, fairness abstracts the details of admissible (“fair”) schedulers; in a distributed environment, fairness abstracts the speeds of independent processors. We argue that the standard definition of fairness often is unnecessarily weak and can be replaced by the stronger, yet still abstract, notion of finitary fairness. While standard weak fairness requires that no enabled transition is postponed forever, finitary weak fairness requires that for every run of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. In general, the finitary restriction fin(F) of any given fairness assumption F is the union of all w-regular safety properties that are contained in F. The adequacy of the proposed abstraction is demonstrated in two ways. Suppose that we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors' 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. Finitary fairness. In: Proceedings 9th Annual IEEE Symposium on Logic in Computer Science. IEEE; 1994:52-61. doi:10.1109/LICS.1994.316087 ' apa: 'Alur, R., & Henzinger, T. A. (1994). Finitary fairness. In Proceedings 9th Annual IEEE Symposium on Logic in Computer Science (pp. 52–61). Paris, France: IEEE. https://doi.org/10.1109/LICS.1994.316087 ' chicago: Alur, Rajeev, and Thomas A Henzinger. “Finitary Fairness.” In Proceedings 9th Annual IEEE Symposium on Logic in Computer Science, 52–61. IEEE, 1994. https://doi.org/10.1109/LICS.1994.316087 . ieee: R. Alur and T. A. Henzinger, “Finitary fairness,” in Proceedings 9th Annual IEEE Symposium on Logic in Computer Science, Paris, France, 1994, pp. 52–61. ista: 'Alur R, Henzinger TA. 1994. Finitary fairness. Proceedings 9th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 52–61.' mla: Alur, Rajeev, and Thomas A. Henzinger. “Finitary Fairness.” Proceedings 9th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1994, pp. 52–61, doi:10.1109/LICS.1994.316087 . short: R. Alur, T.A. Henzinger, in:, Proceedings 9th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1994, pp. 52–61. conference: end_date: "\t1994-07-07" location: Paris, France name: 'LICS: Logic in Computer Science' start_date: 1994-07-04 date_created: 2018-12-11T12:09:37Z date_published: 1994-01-01T00:00:00Z date_updated: 2022-06-02T08:45:57Z day: '01' doi: '10.1109/LICS.1994.316087 ' extern: '1' language: - iso: eng main_file_link: - url: https://ieeexplore.ieee.org/document/316087 month: '01' oa_version: None page: 52 - 61 publication: Proceedings 9th Annual IEEE Symposium on Logic in Computer Science publication_identifier: issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '119' quality_controlled: '1' scopus_import: '1' status: public title: Finitary fairness type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1994' ... --- _id: '4596' abstract: - lang: eng text: A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. acknowledgement: 'We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance. Moshe Vardi and Joe Halpern gave us very helpful advice for refilling our undecidability results. ' 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. A really temporal logic. In: 30th Annual Symposium on Foundations of Computer Science. FCOS. IEEE; 1989:164-169. doi:10.1109/SFCS.1989.63473' apa: 'Alur, R., & Henzinger, T. A. (1989). A really temporal logic. In 30th Annual Symposium on Foundations of Computer Science (pp. 164–169). Research Triangle Park, NC, USA: IEEE. https://doi.org/10.1109/SFCS.1989.63473' chicago: Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” In 30th Annual Symposium on Foundations of Computer Science, 164–69. FCOS. IEEE, 1989. https://doi.org/10.1109/SFCS.1989.63473. ieee: R. Alur and T. A. Henzinger, “A really temporal logic,” in 30th Annual Symposium on Foundations of Computer Science, Research Triangle Park, NC, USA, 1989, pp. 164–169. ista: 'Alur R, Henzinger TA. 1989. A really temporal logic. 30th Annual Symposium on Foundations of Computer Science. FOCS: Foundations of Computer ScienceFCOS, 164–169.' mla: Alur, Rajeev, and Thomas A. Henzinger. “A Really Temporal Logic.” 30th Annual Symposium on Foundations of Computer Science, IEEE, 1989, pp. 164–69, doi:10.1109/SFCS.1989.63473. short: R. Alur, T.A. Henzinger, in:, 30th Annual Symposium on Foundations of Computer Science, IEEE, 1989, pp. 164–169. conference: end_date: 1989-11-01 location: Research Triangle Park, NC, USA name: 'FOCS: Foundations of Computer Science' start_date: 1989-10-30 date_created: 2018-12-11T12:09:40Z date_published: 1989-01-01T00:00:00Z date_updated: 2022-02-09T10:40:13Z day: '01' doi: 10.1109/SFCS.1989.63473 extern: '1' language: - iso: eng main_file_link: - url: https://ieeexplore.ieee.org/document/63473 month: '01' oa_version: None page: 164 - 169 publication: 30th Annual Symposium on Foundations of Computer Science publication_identifier: eissn: - 1558-0814 isbn: - 0-8186-1982-1 issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '111' quality_controlled: '1' series_title: FCOS status: public title: A really temporal logic type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1989' ... --- _id: '4128' abstract: - lang: eng text: A generalization of the convex hull of a finite set of points in the plane is introduced and analyzed. This generalization leads to a family of straight-line graphs, " \alpha -shapes," which seem to capture the intuitive notions of "fine shape" and "crude shape" of point sets. It is shown that a-shapes are subgraphs of the closest point or furthest point Delaunay triangulation. Relying on this result an optimal O(n \log n) algorithm that constructs \alpha -shapes is developed. acknowledgement: "The authors express their appreciation for numerous constructive suggestions, which led to improvements on\r\nvarious phases of the manuscript, to Dr. Marvin Simon of JPL and to Professor George L. Turin of University of\r\nCalifornia, Berkeley. The junior author also gratefully acknowledges the role of the latter as her M.S. research\r\nadvisor on the project which formed the nucleus of this work. \r\n" article_processing_charge: No article_type: original author: - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: David full_name: Kirkpatrick, David last_name: Kirkpatrick - first_name: Raimund full_name: Seidel, Raimund last_name: Seidel citation: ama: Edelsbrunner H, Kirkpatrick D, Seidel R. On the shape of a set of points in the plane. IEEE Transactions on Information Theory. 1983;29(4):551-559. doi:10.1109/TIT.1983.1056714 apa: Edelsbrunner, H., Kirkpatrick, D., & Seidel, R. (1983). On the shape of a set of points in the plane. IEEE Transactions on Information Theory. IEEE. https://doi.org/10.1109/TIT.1983.1056714 chicago: Edelsbrunner, Herbert, David Kirkpatrick, and Raimund Seidel. “On the Shape of a Set of Points in the Plane.” IEEE Transactions on Information Theory. IEEE, 1983. https://doi.org/10.1109/TIT.1983.1056714 . ieee: H. Edelsbrunner, D. Kirkpatrick, and R. Seidel, “On the shape of a set of points in the plane,” IEEE Transactions on Information Theory, vol. 29, no. 4. IEEE, pp. 551–559, 1983. ista: Edelsbrunner H, Kirkpatrick D, Seidel R. 1983. On the shape of a set of points in the plane. IEEE Transactions on Information Theory. 29(4), 551–559. mla: Edelsbrunner, Herbert, et al. “On the Shape of a Set of Points in the Plane.” IEEE Transactions on Information Theory, vol. 29, no. 4, IEEE, 1983, pp. 551–59, doi:10.1109/TIT.1983.1056714 . short: H. Edelsbrunner, D. Kirkpatrick, R. Seidel, IEEE Transactions on Information Theory 29 (1983) 551–559. date_created: 2018-12-11T12:07:06Z date_published: 1983-06-01T00:00:00Z date_updated: 2022-01-25T12:55:07Z day: '01' doi: '10.1109/TIT.1983.1056714 ' extern: '1' intvolume: ' 29' issue: '4' language: - iso: eng main_file_link: - url: https://ieeexplore.ieee.org/document/1056714 month: '06' oa_version: None page: 551 - 559 publication: IEEE Transactions on Information Theory publication_identifier: eissn: - 1558-0814 issn: - 0018-9162 publication_status: published publisher: IEEE publist_id: '1995' quality_controlled: '1' scopus_import: '1' status: public title: On the shape of a set of points in the plane type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 29 year: '1983' ...