---
_id: '4522'
abstract:
- lang: eng
  text: 'We introduce a novel extension of propositional modal logic that is interpreted
    over Kripke structures in which a value is associated with every possible world.
    These values are. however, not treated as full first-order objects: they can be
    accessed only by a very restricted form of quantification: the "freeze" quantifier
    binds a variable to the value of the current world. We present a complete proof
    system for this ("half-order") modal logic. As a special case, we obtain the real-time
    temporal logic TPTL of [AH891: the models are restricted to infinite sequences
    of states, whose values are monotonically increasing natural numbers. The ordering
    relation between states is interpreted as temporal precedence. while the value
    associated with a state is interpreted as its "rear time. We extend our proof
    system to be complete for TPTL. and demonstrate how it can be used to derive real-time
    properties. '
acknowledgement: Many thanks to Rajeev Alur, Adam Grove, Zohar Manna, and Amir Pnueli
  for their continuous discussions and support.
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. Half-order modal logic: How to prove real-time properties. In:
    <i>Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing</i>.
    ACM; 1990:281-296. doi:<a href="https://doi.org/10.1145/93385.93429">10.1145/93385.93429</a>'
  apa: 'Henzinger, T. A. (1990). Half-order modal logic: How to prove real-time properties.
    In <i>Proceedings of the 9th annual ACM symposium on Principles of distributed
    computing</i> (pp. 281–296). Quebec City, Canada: ACM. <a href="https://doi.org/10.1145/93385.93429">https://doi.org/10.1145/93385.93429</a>'
  chicago: 'Henzinger, Thomas A. “Half-Order Modal Logic: How to Prove Real-Time Properties.”
    In <i>Proceedings of the 9th Annual ACM Symposium on Principles of Distributed
    Computing</i>, 281–96. ACM, 1990. <a href="https://doi.org/10.1145/93385.93429">https://doi.org/10.1145/93385.93429</a>.'
  ieee: 'T. A. Henzinger, “Half-order modal logic: How to prove real-time properties,”
    in <i>Proceedings of the 9th annual ACM symposium on Principles of distributed
    computing</i>, Quebec City, Canada, 1990, pp. 281–296.'
  ista: 'Henzinger TA. 1990. Half-order modal logic: How to prove real-time properties.
    Proceedings of the 9th annual ACM symposium on Principles of distributed computing.
    PODC: Principles of Distributed Computing, 281–296.'
  mla: 'Henzinger, Thomas A. “Half-Order Modal Logic: How to Prove Real-Time Properties.”
    <i>Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing</i>,
    ACM, 1990, pp. 281–96, doi:<a href="https://doi.org/10.1145/93385.93429">10.1145/93385.93429</a>.'
  short: T.A. Henzinger, in:, Proceedings of the 9th Annual ACM Symposium on Principles
    of Distributed Computing, ACM, 1990, pp. 281–296.
conference:
  end_date: 1990-08-24
  location: Quebec City, Canada
  name: 'PODC: Principles of Distributed Computing'
  start_date: 1990-08-22
date_created: 2018-12-11T12:09:17Z
date_published: 1990-01-01T00:00:00Z
date_updated: 2022-02-15T15:11:03Z
day: '01'
doi: 10.1145/93385.93429
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/93385.93429
month: '01'
oa_version: None
page: 281 - 296
publication: Proceedings of the 9th annual ACM symposium on Principles of distributed
  computing
publication_identifier:
  isbn:
  - 978-0-89791-404-8
publication_status: published
publisher: ACM
publist_id: '209'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Half-order modal logic: How to prove real-time properties'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1990'
...