--- _id: '4062' abstract: - lang: eng text: We prove that for any set S of n points in the plane and n3-α triangles spanned by the points in S there exists a point (not necessarily in S) contained in at least n3-3α/(c log5 n) of the triangles. This implies that any set of n points in three-dimensional space defines at most {Mathematical expression} halving planes. acknowledgement: "Work on this paper by Boris Aronov and Rephael Wenger has been supported by DIMACS under NSF Grant STC-88-09648. Work on this paper by Bernard Chazelle has been supported by NSF Grant CCR-87-00917. Work by Herbert Edelsbrunner has been supported by NSF Grant CCR-87-14565. Micha Sharir has been supported by ONR Grant N00014-87-K-0129, by NSF Grant CCR-89-01484, and by grants from the U.S.-Israeli Binational Science Foundation, the Israeli National Council for Research and Development, and the Fund for Basic Research administered by the Israeli\r\nAcademy of Sciences" article_processing_charge: No article_type: original author: - first_name: Boris full_name: Aronov, Boris last_name: Aronov - first_name: Bernard full_name: Chazelle, Bernard last_name: Chazelle - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: Leonidas full_name: Guibas, Leonidas last_name: Guibas - first_name: Micha full_name: Sharir, Micha last_name: Sharir - first_name: Rephael full_name: Wenger, Rephael last_name: Wenger citation: ama: Aronov B, Chazelle B, Edelsbrunner H, Guibas L, Sharir M, Wenger R. Points and triangles in the plane and halving planes in space. Discrete & Computational Geometry. 1991;6(1):435-442. doi:10.1007/BF02574700 apa: Aronov, B., Chazelle, B., Edelsbrunner, H., Guibas, L., Sharir, M., & Wenger, R. (1991). Points and triangles in the plane and halving planes in space. Discrete & Computational Geometry. Springer. https://doi.org/10.1007/BF02574700 chicago: Aronov, Boris, Bernard Chazelle, Herbert Edelsbrunner, Leonidas Guibas, Micha Sharir, and Rephael Wenger. “Points and Triangles in the Plane and Halving Planes in Space.” Discrete & Computational Geometry. Springer, 1991. https://doi.org/10.1007/BF02574700. ieee: B. Aronov, B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, and R. Wenger, “Points and triangles in the plane and halving planes in space,” Discrete & Computational Geometry, vol. 6, no. 1. Springer, pp. 435–442, 1991. ista: Aronov B, Chazelle B, Edelsbrunner H, Guibas L, Sharir M, Wenger R. 1991. Points and triangles in the plane and halving planes in space. Discrete & Computational Geometry. 6(1), 435–442. mla: Aronov, Boris, et al. “Points and Triangles in the Plane and Halving Planes in Space.” Discrete & Computational Geometry, vol. 6, no. 1, Springer, 1991, pp. 435–42, doi:10.1007/BF02574700. short: B. Aronov, B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, R. Wenger, Discrete & Computational Geometry 6 (1991) 435–442. date_created: 2018-12-11T12:06:43Z date_published: 1991-12-01T00:00:00Z date_updated: 2022-02-24T15:39:25Z day: '01' doi: 10.1007/BF02574700 extern: '1' intvolume: ' 6' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: https://link.springer.com/article/10.1007/BF02574700 month: '12' oa: 1 oa_version: Published Version page: 435 - 442 publication: Discrete & Computational Geometry publication_identifier: eissn: - 1432-0444 issn: - 0179-5376 publication_status: published publisher: Springer publist_id: '2063' quality_controlled: '1' scopus_import: '1' status: public title: Points and triangles in the plane and halving planes in space type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 6 year: '1991' ... --- _id: '4508' abstract: - lang: eng text: 'We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...' acknowledgement: 'This research was supported in part by an IBM graduate fellowship, by the National Science Foundation grants CCR-89-11512 and CC R-89-13641, by the Defense Advanced Re-search Projects Agency under contract NOO03%84C-0211, by the United States Air Force Office of Scientific Research un-der contract AFOSR-W-0057, and by the European Community ESPRIT Basic Research Action project 3096 (SPEC). We thank Rajeev Alur for many helpful discussions. ' 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: Zohar full_name: Manna, Zohar last_name: Manna - first_name: Amir full_name: Pnueli, Amir last_name: Pnueli citation: ama: 'Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for real-time systems. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM; 1991:353-366. doi:10.1145/99583.99629' apa: 'Henzinger, T. A., Manna, Z., & Pnueli, A. (1991). Temporal proof methodologies for real-time systems. In Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 353–366). Orlando, FL, United States of America: ACM. https://doi.org/10.1145/99583.99629' chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Real-Time Systems.” In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 353–66. ACM, 1991. https://doi.org/10.1145/99583.99629. ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for real-time systems,” in Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Orlando, FL, United States of America, 1991, pp. 353–366. ista: 'Henzinger TA, Manna Z, Pnueli A. 1991. Temporal proof methodologies for real-time systems. Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL: Principles of Programming Languages, 353–366.' mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Real-Time Systems.” Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 1991, pp. 353–66, doi:10.1145/99583.99629. short: T.A. Henzinger, Z. Manna, A. Pnueli, in:, Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 1991, pp. 353–366. conference: end_date: 1991-01-23 location: Orlando, FL, United States of America name: 'POPL: Principles of Programming Languages' start_date: 1991-01-21 date_created: 2018-12-11T12:09:13Z date_published: 1991-01-01T00:00:00Z date_updated: 2022-02-24T14:44:39Z day: '01' doi: 10.1145/99583.99629 extern: '1' language: - iso: eng main_file_link: - url: https://dl.acm.org/doi/10.1145/99583.99629 month: '01' oa_version: None page: 353 - 366 publication: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages publication_identifier: isbn: - 978-0-89791-419-2 publication_status: published publisher: ACM publist_id: '221' quality_controlled: '1' scopus_import: '1' status: public title: Temporal proof methodologies for real-time systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1991' ... --- _id: '4516' abstract: - lang: eng text: We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of reactive systems. Semantics We introduce the abstract computational model of timed transition systems as a conservative extension of traditional transition systems qualitative fairness requirements are superseded by quantitative real-time constraints on the transitions. Digital clocks are introduced as observers of continuous real-time behavior. We justify our semantical abstractions by demonstrating that a wide variety of concrete real-time systems can be modeled adequately. Specification We present two conservative extensions of temporal logic that allow for the specification of timing constraints while timed temporal logic provides access to time through a novel kind of time quantifier, metric temporal logic refers to time through time-bounded versions of the temporal operators. We justify our choice of specification languages by developing a general framework for the classification of real-time logics according to their complexity and expressive power. Verification We develop tools for determining if a real-time system that is modeled as a timed transition system meets a specification that is given in timed temporal logic or in metric temporal logic. We present both model-checking algorithms for the automatic verification of finite-state real-time systems and proof methods for the deductive verification of real-time systems. 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. The temporal specification and verification of real-time systems . 1991. apa: Henzinger, T. A. (1991). The temporal specification and verification of real-time systems . Stanford University. chicago: Henzinger, Thomas A. “The Temporal Specification and Verification of Real-Time Systems .” Stanford University, 1991. ieee: T. A. Henzinger, “The temporal specification and verification of real-time systems ,” Stanford University, 1991. ista: Henzinger TA. 1991. The temporal specification and verification of real-time systems . Stanford University. mla: Henzinger, Thomas A. The Temporal Specification and Verification of Real-Time Systems . Stanford University, 1991. short: T.A. Henzinger, The Temporal Specification and Verification of Real-Time Systems , Stanford University, 1991. date_created: 2018-12-11T12:09:15Z date_published: 1991-08-30T00:00:00Z date_updated: 2022-02-24T14:12:36Z day: '30' degree_awarded: PhD extern: '1' language: - iso: eng main_file_link: - url: http://pub.ist.ac.at/~tah/Publications/the_temporal_specification_and_verification_of_real-time_systems.pdf month: '08' oa_version: None page: '295' publication_status: published publisher: Stanford University publist_id: '210' status: public title: 'The temporal specification and verification of real-time systems ' type: dissertation user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1991' ... --- _id: '4592' article_processing_charge: No article_type: letter_note 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. Time for logic. SIGACT News. 1991;22(3):6-12. apa: Alur, R., & Henzinger, T. A. (1991). Time for logic. SIGACT News. ACM. chicago: Alur, Rajeev, and Thomas A Henzinger. “Time for Logic.” SIGACT News. ACM, 1991. ieee: R. Alur and T. A. Henzinger, “Time for logic,” SIGACT News, vol. 22, no. 3. ACM, pp. 6–12, 1991. ista: Alur R, Henzinger TA. 1991. Time for logic. SIGACT News. 22(3), 6–12. mla: Alur, Rajeev, and Thomas A. Henzinger. “Time for Logic.” SIGACT News, vol. 22, no. 3, ACM, 1991, pp. 6–12. short: R. Alur, T.A. Henzinger, SIGACT News 22 (1991) 6–12. date_created: 2018-12-11T12:09:39Z date_published: 1991-01-01T00:00:00Z date_updated: 2022-02-24T13:54:10Z day: '01' extern: '1' intvolume: ' 22' issue: '3' language: - iso: eng main_file_link: - url: https://dl.acm.org/toc/sigact/1991/22/1 month: '01' oa_version: None page: 6 - 12 publication: SIGACT News publication_identifier: issn: - 0163-5700 publication_status: published publisher: ACM publist_id: '113' quality_controlled: '1' status: public title: Time for logic type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 22 year: '1991' ... --- _id: '4621' abstract: - lang: eng text: The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics. acknowledgement: 'We wish to thank an anonymous referee for pointing out the PSPACE-fragment of Section 4.5. T. A. Henzinger was supported in part by the Office of Naval Research Young Investigator award NOOO14-95-l-0520, by the National Science Foundation CAREER award CCR 9501708, by the National Science Foundation grants CCR 92-00794 and CCR 9504469, by the Air Force Office of Scientific Research contract F49620-93-l-0056, and by the Advanced Research Projects Agency grant NAG2-892. ' article_processing_charge: No author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Tomás full_name: Feder, Tomás last_name: Feder - 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, Feder T, Henzinger TA. The benefits of relaxing punctuality. In: Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing. ACM; 1991:139-152. doi:10.1145/227595.227602' apa: 'Alur, R., Feder, T., & Henzinger, T. A. (1991). The benefits of relaxing punctuality. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing (pp. 139–152). Montreal, Canada: ACM. https://doi.org/10.1145/227595.227602' chicago: Alur, Rajeev, Tomás Feder, and Thomas A Henzinger. “The Benefits of Relaxing Punctuality.” In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, 139–52. ACM, 1991. https://doi.org/10.1145/227595.227602. ieee: R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,” in Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, Montreal, Canada, 1991, pp. 139–152. ista: 'Alur R, Feder T, Henzinger TA. 1991. The benefits of relaxing punctuality. Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing. PODC: Principles of Distributed Computing, 139–152.' mla: Alur, Rajeev, et al. “The Benefits of Relaxing Punctuality.” Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, ACM, 1991, pp. 139–52, doi:10.1145/227595.227602. short: R. Alur, T. Feder, T.A. Henzinger, in:, Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, ACM, 1991, pp. 139–152. conference: end_date: 1991-08-21 location: Montreal, Canada name: 'PODC: Principles of Distributed Computing' start_date: 1991-08-19 date_created: 2018-12-11T12:09:48Z date_published: 1991-01-01T00:00:00Z date_updated: 2022-02-24T13:27:20Z day: '01' doi: 10.1145/227595.227602 extern: '1' language: - iso: eng main_file_link: - url: https://dl.acm.org/doi/10.1145/227595.227602 month: '01' oa_version: None page: 139 - 152 publication: Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing publication_identifier: isbn: - 978-0-89791-439-0 publication_status: published publisher: ACM publist_id: '86' quality_controlled: '1' scopus_import: '1' status: public title: The benefits of relaxing punctuality type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 year: '1991' ...