@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},
}