---
_id: '4590'
abstract:
- lang: eng
  text: 'We introduce a temporal logic for the specification of real-time systems.
    Our logic, TPTL, employs a novel quantifier construct for referencing time: the
    "freeze" quantifier binds a variable to the time of the local temporal
    context. TPTL is both a natural language for specification and a suitable formalism
    for verification. We present a tableau-based decision procedure and a model-checking
    algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.'
acknowledgement: The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter
  Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.
alternative_title:
- AMAST Series in Computing
article_processing_charge: No
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 system = discrete system + clock variables.
    In: Rus T, Rattray C, eds. <i>Theories and Experiences for Real-Time System Development</i>.
    Vol 2. AMAST Series in Computing. World Scientific Publishing; 1994:1-29. doi:<a
    href="https://doi.org/10.1142/9789812831583_0001">10.1142/9789812831583_0001</a>'
  apa: Alur, R., &#38; Henzinger, T. A. (1994). Real-time system = discrete system
    + clock variables. In T. Rus &#38; C. Rattray (Eds.), <i>Theories and Experiences
    for Real-Time System Development</i> (Vol. 2, pp. 1–29). World Scientific Publishing.
    <a href="https://doi.org/10.1142/9789812831583_0001">https://doi.org/10.1142/9789812831583_0001</a>
  chicago: Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System
    + Clock Variables.” In <i>Theories and Experiences for Real-Time System Development</i>,
    edited by Teodor Rus and Charles Rattray, 2:1–29. AMAST Series in Computing. World
    Scientific Publishing, 1994. <a href="https://doi.org/10.1142/9789812831583_0001">https://doi.org/10.1142/9789812831583_0001</a>.
  ieee: R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,”
    in <i>Theories and Experiences for Real-Time System Development</i>, vol. 2, T.
    Rus and C. Rattray, Eds. World Scientific Publishing, 1994, pp. 1–29.
  ista: 'Alur R, Henzinger TA. 1994.Real-time system = discrete system + clock variables.
    In: Theories and Experiences for Real-Time System Development. AMAST Series in
    Computing, vol. 2, 1–29.'
  mla: Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System
    + Clock Variables.” <i>Theories and Experiences for Real-Time System Development</i>,
    edited by Teodor Rus and Charles Rattray, vol. 2, World Scientific Publishing,
    1994, pp. 1–29, doi:<a href="https://doi.org/10.1142/9789812831583_0001">10.1142/9789812831583_0001</a>.
  short: R. Alur, T.A. Henzinger, in:, T. Rus, C. Rattray (Eds.), Theories and Experiences
    for Real-Time System Development, World Scientific Publishing, 1994, pp. 1–29.
date_created: 2018-12-11T12:09:38Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T08:07:57Z
day: '01'
doi: 10.1142/9789812831583_0001
editor:
- first_name: Teodor
  full_name: Rus, Teodor
  last_name: Rus
- first_name: Charles
  full_name: Rattray, Charles
  last_name: Rattray
extern: '1'
intvolume: '         2'
keyword:
- real-time systems
- clock variables
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/article/10.1007/s100090050007
month: '01'
oa_version: None
page: 1 - 29
publication: Theories and Experiences for Real-Time System Development
publication_identifier:
  isbn:
  - ' 9789810219239'
publication_status: published
publisher: World Scientific Publishing
publist_id: '117'
quality_controlled: '1'
series_title: AMAST Series in Computing
status: public
title: Real-time system = discrete system + clock variables
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2
year: '1994'
...