---
_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'
...