[{"date_published":"1991-12-01T00:00:00Z","page":"435 - 442","scopus_import":"1","publication_identifier":{"issn":["0179-5376"],"eissn":["1432-0444"]},"oa_version":"Published Version","type":"journal_article","date_updated":"2022-02-24T15:39:25Z","day":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","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","language":[{"iso":"eng"}],"doi":"10.1007/BF02574700","article_type":"original","publisher":"Springer","issue":"1","volume":6,"month":"12","date_created":"2018-12-11T12:06:43Z","status":"public","intvolume":"         6","publist_id":"2063","year":"1991","main_file_link":[{"url":"https://link.springer.com/article/10.1007/BF02574700","open_access":"1"}],"citation":{"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 &#38; Computational Geometry. 6(1), 435–442.","short":"B. Aronov, B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, R. Wenger, Discrete &#38; Computational Geometry 6 (1991) 435–442.","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.” <i>Discrete &#38; Computational Geometry</i>. Springer, 1991. <a href=\"https://doi.org/10.1007/BF02574700\">https://doi.org/10.1007/BF02574700</a>.","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,” <i>Discrete &#38; Computational Geometry</i>, vol. 6, no. 1. Springer, pp. 435–442, 1991.","ama":"Aronov B, Chazelle B, Edelsbrunner H, Guibas L, Sharir M, Wenger R. Points and triangles in the plane and halving planes in space. <i>Discrete &#38; Computational Geometry</i>. 1991;6(1):435-442. doi:<a href=\"https://doi.org/10.1007/BF02574700\">10.1007/BF02574700</a>","mla":"Aronov, Boris, et al. “Points and Triangles in the Plane and Halving Planes in Space.” <i>Discrete &#38; Computational Geometry</i>, vol. 6, no. 1, Springer, 1991, pp. 435–42, doi:<a href=\"https://doi.org/10.1007/BF02574700\">10.1007/BF02574700</a>.","apa":"Aronov, B., Chazelle, B., Edelsbrunner, H., Guibas, L., Sharir, M., &#38; Wenger, R. (1991). Points and triangles in the plane and halving planes in space. <i>Discrete &#38; Computational Geometry</i>. Springer. <a href=\"https://doi.org/10.1007/BF02574700\">https://doi.org/10.1007/BF02574700</a>"},"extern":"1","quality_controlled":"1","author":[{"last_name":"Aronov","first_name":"Boris","full_name":"Aronov, Boris"},{"last_name":"Chazelle","first_name":"Bernard","full_name":"Chazelle, Bernard"},{"last_name":"Edelsbrunner","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833","full_name":"Edelsbrunner, Herbert"},{"first_name":"Leonidas","last_name":"Guibas","full_name":"Guibas, Leonidas"},{"full_name":"Sharir, Micha","last_name":"Sharir","first_name":"Micha"},{"last_name":"Wenger","first_name":"Rephael","full_name":"Wenger, Rephael"}],"abstract":[{"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.","lang":"eng"}],"publication_status":"published","title":"Points and triangles in the plane and halving planes in space","publication":"Discrete & Computational Geometry","_id":"4062","oa":1},{"publist_id":"221","publication_identifier":{"isbn":["978-0-89791-419-2"]},"scopus_import":"1","status":"public","date_created":"2018-12-11T12:09:13Z","conference":{"name":"POPL: Principles of Programming Languages","end_date":"1991-01-23","start_date":"1991-01-21","location":"Orlando, FL, United States of America"},"month":"01","page":"353 - 366","date_published":"1991-01-01T00:00:00Z","publisher":"ACM","doi":"10.1145/99583.99629","language":[{"iso":"eng"}],"_id":"4508","title":"Temporal proof methodologies for real-time systems","publication":"Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","publication_status":"published","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. ","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Manna, Zohar","last_name":"Manna","first_name":"Zohar"},{"full_name":"Pnueli, Amir","first_name":"Amir","last_name":"Pnueli"}],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","quality_controlled":"1","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/99583.99629"}],"citation":{"ama":"Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for real-time systems. In: <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>. ACM; 1991:353-366. doi:<a href=\"https://doi.org/10.1145/99583.99629\">10.1145/99583.99629</a>","ieee":"T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for real-time systems,” in <i>Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i>, 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.","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.","chicago":"Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Real-Time Systems.” In <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, 353–66. ACM, 1991. <a href=\"https://doi.org/10.1145/99583.99629\">https://doi.org/10.1145/99583.99629</a>.","mla":"Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Real-Time Systems.” <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, ACM, 1991, pp. 353–66, doi:<a href=\"https://doi.org/10.1145/99583.99629\">10.1145/99583.99629</a>.","apa":"Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1991). Temporal proof methodologies for real-time systems. In <i>Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i> (pp. 353–366). Orlando, FL, United States of America: ACM. <a href=\"https://doi.org/10.1145/99583.99629\">https://doi.org/10.1145/99583.99629</a>"},"day":"01","year":"1991","type":"conference","date_updated":"2022-02-24T14:44:39Z","oa_version":"None"},{"publisher":"Stanford University","date_published":"1991-08-30T00:00:00Z","page":"295","month":"08","date_created":"2018-12-11T12:09:15Z","status":"public","degree_awarded":"PhD","publist_id":"210","oa_version":"None","date_updated":"2022-02-24T14:12:36Z","type":"dissertation","year":"1991","day":"30","citation":{"apa":"Henzinger, T. A. (1991). <i>The temporal specification and verification of real-time systems </i>. Stanford University.","mla":"Henzinger, Thomas A. <i>The Temporal Specification and Verification of Real-Time Systems </i>. Stanford University, 1991.","ama":"Henzinger TA. The temporal specification and verification of real-time systems . 1991.","ieee":"T. A. Henzinger, “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.","chicago":"Henzinger, Thomas A. “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."},"main_file_link":[{"url":"http://pub.ist.ac.at/~tah/Publications/the_temporal_specification_and_verification_of_real-time_systems.pdf"}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","extern":"1","abstract":[{"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.","lang":"eng"}],"publication_status":"published","title":"The temporal specification and verification of real-time systems ","_id":"4516","language":[{"iso":"eng"}]},{"status":"public","month":"01","date_created":"2018-12-11T12:09:39Z","publist_id":"113","publication_identifier":{"issn":["0163-5700"]},"intvolume":"        22","publisher":"ACM","article_type":"letter_note","issue":"3","volume":22,"page":"6 - 12","date_published":"1991-01-01T00:00:00Z","publication_status":"published","_id":"4592","language":[{"iso":"eng"}],"publication":"SIGACT News","title":"Time for logic","year":"1991","day":"01","oa_version":"None","date_updated":"2022-02-24T13:54:10Z","type":"journal_article","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","quality_controlled":"1","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"extern":"1","article_processing_charge":"No","main_file_link":[{"url":"https://dl.acm.org/toc/sigact/1991/22/1"}],"citation":{"ista":"Alur R, Henzinger TA. 1991. Time for logic. SIGACT News. 22(3), 6–12.","short":"R. Alur, T.A. Henzinger, SIGACT News 22 (1991) 6–12.","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Time for Logic.” <i>SIGACT News</i>. ACM, 1991.","ieee":"R. Alur and T. A. Henzinger, “Time for logic,” <i>SIGACT News</i>, vol. 22, no. 3. ACM, pp. 6–12, 1991.","ama":"Alur R, Henzinger TA. Time for logic. <i>SIGACT News</i>. 1991;22(3):6-12.","apa":"Alur, R., &#38; Henzinger, T. A. (1991). Time for logic. <i>SIGACT News</i>. ACM.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Time for Logic.” <i>SIGACT News</i>, vol. 22, no. 3, ACM, 1991, pp. 6–12."}},{"citation":{"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.","chicago":"Alur, Rajeev, Tomás Feder, and Thomas A Henzinger. “The Benefits of Relaxing Punctuality.” In <i>Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing</i>, 139–52. ACM, 1991. <a href=\"https://doi.org/10.1145/227595.227602\">https://doi.org/10.1145/227595.227602</a>.","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.","ieee":"R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,” in <i>Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing</i>, Montreal, Canada, 1991, pp. 139–152.","ama":"Alur R, Feder T, Henzinger TA. The benefits of relaxing punctuality. In: <i>Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing</i>. ACM; 1991:139-152. doi:<a href=\"https://doi.org/10.1145/227595.227602\">10.1145/227595.227602</a>","mla":"Alur, Rajeev, et al. “The Benefits of Relaxing Punctuality.” <i>Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing</i>, ACM, 1991, pp. 139–52, doi:<a href=\"https://doi.org/10.1145/227595.227602\">10.1145/227595.227602</a>.","apa":"Alur, R., Feder, T., &#38; Henzinger, T. A. (1991). The benefits of relaxing punctuality. In <i>Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing</i> (pp. 139–152). Montreal, Canada: ACM. <a href=\"https://doi.org/10.1145/227595.227602\">https://doi.org/10.1145/227595.227602</a>"},"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/227595.227602"}],"quality_controlled":"1","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"last_name":"Feder","first_name":"Tomás","full_name":"Feder, Tomás"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"None","date_updated":"2022-02-24T13:27:20Z","type":"conference","year":"1991","day":"01","title":"The benefits of relaxing punctuality","publication":"Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing","_id":"4621","doi":"10.1145/227595.227602","language":[{"iso":"eng"}],"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. ","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."}],"publication_status":"published","date_published":"1991-01-01T00:00:00Z","page":"139 - 152","publisher":"ACM","scopus_import":"1","publist_id":"86","publication_identifier":{"isbn":["978-0-89791-439-0"]},"month":"01","conference":{"start_date":"1991-08-19","location":"Montreal, Canada","end_date":"1991-08-21","name":"PODC: Principles of Distributed Computing"},"date_created":"2018-12-11T12:09:48Z","status":"public"}]