@article{4062, abstract = {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.}, author = {Aronov, Boris and Chazelle, Bernard and Edelsbrunner, Herbert and Guibas, Leonidas and Sharir, Micha and Wenger, Rephael}, issn = {1432-0444}, journal = {Discrete & Computational Geometry}, number = {1}, pages = {435 -- 442}, publisher = {Springer}, title = {{Points and triangles in the plane and halving planes in space}}, doi = {10.1007/BF02574700}, volume = {6}, year = {1991}, } @inproceedings{4508, abstract = {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 ...}, author = {Henzinger, Thomas A and Manna, Zohar and Pnueli, Amir}, booktitle = {Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, isbn = {978-0-89791-419-2}, location = {Orlando, FL, United States of America}, pages = {353 -- 366}, publisher = {ACM}, title = {{Temporal proof methodologies for real-time systems}}, doi = {10.1145/99583.99629}, year = {1991}, } @phdthesis{4516, abstract = {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.}, author = {Henzinger, Thomas A}, pages = {295}, publisher = {Stanford University}, title = {{The temporal specification and verification of real-time systems }}, year = {1991}, } @article{4592, author = {Alur, Rajeev and Henzinger, Thomas A}, issn = {0163-5700}, journal = {SIGACT News}, number = {3}, pages = {6 -- 12}, publisher = {ACM}, title = {{Time for logic}}, volume = {22}, year = {1991}, } @inproceedings{4621, abstract = {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.}, author = {Alur, Rajeev and Feder, Tomás and Henzinger, Thomas A}, booktitle = {Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing}, isbn = {978-0-89791-439-0}, location = {Montreal, Canada}, pages = {139 -- 152}, publisher = {ACM}, title = {{The benefits of relaxing punctuality}}, doi = {10.1145/227595.227602}, year = {1991}, }