@article{4589,
  abstract     = {The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.

Copyright © 1993 Academic Press. All rights reserved.},
  author       = {Alur, Rajeev and Henzinger, Thomas A},
  issn         = {0890-5401},
  journal      = {Information and Computation},
  number       = {1},
  pages        = {35 -- 77},
  publisher    = {Elsevier},
  title        = {{Real-time logics: Complexity and expressiveness}},
  doi          = {10.1006/inco.1993.1025},
  volume       = {104},
  year         = {1993},
}

@article{4090,
  abstract     = {In this paper we study the problem of polygonal separation in the plane, i.e., finding a convex polygon with minimum number k of sides separating two given finite point sets (k-separator), if it exists. We show that for k = Θ(n),  is a lower bound to the running time of any algorithm for this problem, and exhibit two algorithms of distinctly different flavors. The first relies on an O(n log n)-time preprocessing task, which constructs the convex hull of the internal set and a nested star-shaped polygon determined by the external set; the k-separator is contained in the annulus between the boundaries of these two polygons and is constructed in additional linear time. The second algorithm adapts the prune-and-search approach, and constructs, in each iteration, one side of the separator; its running time is O(kn), but the separator may have one more side than the minimum.},
  author       = {Edelsbrunner, Herbert and Preparata, Franco},
  issn         = {0890-5401},
  journal      = {Information and Computation},
  number       = {3},
  pages        = {218 -- 232},
  publisher    = {Elsevier},
  title        = {{Minimum polygonal separation}},
  doi          = {10.1016/0890-5401(88)90049-1},
  volume       = {77},
  year         = {1988},
}