---
_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. <i>Discrete &#38; Computational
    Geometry</i>. 1991;6(1):435-442. 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>
  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.
  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.
  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>.
  short: B. Aronov, B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, R. Wenger,
    Discrete &#38; 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: <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>'
  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>'
  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>.
  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.'
  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>.
  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). <i>The temporal specification and verification of
    real-time systems </i>. 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. <i>The Temporal Specification and Verification of Real-Time
    Systems </i>. 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. <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.
  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.
  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.” <i>SIGACT News</i>,
    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: <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>'
  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>'
  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>.
  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.
  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.” <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>.
  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'
...