---
_id: '4589'
abstract:
- lang: eng
  text: "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.\r\n\r\nCopyright © 1993
    Academic Press. All rights reserved."
acknowledgement: We thank David Dill, Zohar Manna, and Amir Pnueli for helpful discussion.
article_processing_charge: No
article_type: original
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. Real-time logics: Complexity and expressiveness. <i>Information
    and Computation</i>. 1993;104(1):35-77. doi:<a href="https://doi.org/10.1006/inco.1993.1025">10.1006/inco.1993.1025</a>'
  apa: 'Alur, R., &#38; Henzinger, T. A. (1993). Real-time logics: Complexity and
    expressiveness. <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1006/inco.1993.1025">https://doi.org/10.1006/inco.1993.1025</a>'
  chicago: 'Alur, Rajeev, and Thomas A Henzinger. “Real-Time Logics: Complexity and
    Expressiveness.” <i>Information and Computation</i>. Elsevier, 1993. <a href="https://doi.org/10.1006/inco.1993.1025">https://doi.org/10.1006/inco.1993.1025</a>.'
  ieee: 'R. Alur and T. A. Henzinger, “Real-time logics: Complexity and expressiveness,”
    <i>Information and Computation</i>, vol. 104, no. 1. Elsevier, pp. 35–77, 1993.'
  ista: 'Alur R, Henzinger TA. 1993. Real-time logics: Complexity and expressiveness.
    Information and Computation. 104(1), 35–77.'
  mla: 'Alur, Rajeev, and Thomas A. Henzinger. “Real-Time Logics: Complexity and Expressiveness.”
    <i>Information and Computation</i>, vol. 104, no. 1, Elsevier, 1993, pp. 35–77,
    doi:<a href="https://doi.org/10.1006/inco.1993.1025">10.1006/inco.1993.1025</a>.'
  short: R. Alur, T.A. Henzinger, Information and Computation 104 (1993) 35–77.
date_created: 2018-12-11T12:09:38Z
date_published: 1993-05-01T00:00:00Z
date_updated: 2022-03-23T13:08:27Z
day: '01'
doi: 10.1006/inco.1993.1025
extern: '1'
intvolume: '       104'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/S0890540183710254?via%3Dihub
month: '05'
oa: 1
oa_version: Published Version
page: 35 - 77
publication: Information and Computation
publication_identifier:
  eissn:
  - 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '116'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Real-time logics: Complexity and expressiveness'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 104
year: '1993'
...
---
_id: '4090'
abstract:
- lang: eng
  text: 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.
acknowledgement: Research of the first author is supported by Amoco Fnd. Fat. Dev.
  Comput. Sci. l-6-44862; research of the second author is supported by NSF Grant
  ECS 84-10902.
article_processing_charge: No
article_type: original
author:
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Franco
  full_name: Preparata, Franco
  last_name: Preparata
citation:
  ama: Edelsbrunner H, Preparata F. Minimum polygonal separation. <i>Information and
    Computation</i>. 1988;77(3):218-232. doi:<a href="https://doi.org/10.1016/0890-5401(88)90049-1">10.1016/0890-5401(88)90049-1</a>
  apa: Edelsbrunner, H., &#38; Preparata, F. (1988). Minimum polygonal separation.
    <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1016/0890-5401(88)90049-1">https://doi.org/10.1016/0890-5401(88)90049-1</a>
  chicago: Edelsbrunner, Herbert, and Franco Preparata. “Minimum Polygonal Separation.”
    <i>Information and Computation</i>. Elsevier, 1988. <a href="https://doi.org/10.1016/0890-5401(88)90049-1">https://doi.org/10.1016/0890-5401(88)90049-1</a>.
  ieee: H. Edelsbrunner and F. Preparata, “Minimum polygonal separation,” <i>Information
    and Computation</i>, vol. 77, no. 3. Elsevier, pp. 218–232, 1988.
  ista: Edelsbrunner H, Preparata F. 1988. Minimum polygonal separation. Information
    and Computation. 77(3), 218–232.
  mla: Edelsbrunner, Herbert, and Franco Preparata. “Minimum Polygonal Separation.”
    <i>Information and Computation</i>, vol. 77, no. 3, Elsevier, 1988, pp. 218–32,
    doi:<a href="https://doi.org/10.1016/0890-5401(88)90049-1">10.1016/0890-5401(88)90049-1</a>.
  short: H. Edelsbrunner, F. Preparata, Information and Computation 77 (1988) 218–232.
date_created: 2018-12-11T12:06:53Z
date_published: 1988-06-01T00:00:00Z
date_updated: 2022-02-08T10:36:30Z
day: '01'
doi: 10.1016/0890-5401(88)90049-1
extern: '1'
intvolume: '        77'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/0890540188900491?via%3Dihub
month: '06'
oa: 1
oa_version: None
page: 218 - 232
publication: Information and Computation
publication_identifier:
  eissn:
  - 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '2029'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Minimum polygonal separation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 77
year: '1988'
...