---
_id: '4495'
abstract:
- lang: eng
  text: In temporal-logic model checking, we verify the correctness of a program with
    respect to a desired behavior by checking whether a structure that models the
    program satisfies a temporal-logic formula that specifies the behavior. The main
    practical limitation of model checking is caused by the size of the state space
    of the program, which grows exponentially with the number of concurrent components.
    This problem, known as the state-explosion problem, becomes more difficult when
    we consider real-time model checking, where the program and the specification
    involve quantitative references to time. In particular, when use timed automata
    to describe real-time programs and we specify timed behaviors in the logic TCTL,
    a real-time extension of the temporal logic CTL with clock variables, then the
    state space under consideration grows exponentially not only with the number of
    concurrent components, but also with the number of clocks and the length of the
    clock constraints used in the program and the specification. Two powerful methods
    for coping with the state-explosion problem are on-the-fly and space-efficient
    model checking. In on-the-fly model checking, we explore only the portion of the
    state space of the program whose exploration is essential for determining the
    satisfaction of the specification. In space-efficient model checking, we store
    in memory the minimal information required, preferring to spend time on reconstructing
    information rather than spend space on storing it. In this work we develop an
    automata-theoretic approach to TCTL model checking that combines both methods.
    We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for
    TCTL.
acknowledgement: Supported in part by the ONR YIP award N00014-95-1-0520, by the NSF
  CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056,
  and by the ARPA grant NAG2-892.
alternative_title:
- LNCS
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
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Moshe
  full_name: Vardi, Moshe
  last_name: Vardi
citation:
  ama: 'Henzinger TA, Kupferman O, Vardi M. A space-efficient on-the-fly algorithm
    for real-time model checking. In: <i>7th International Conference on Concurrency
    Theory</i>. Vol 1119. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1996:514-529.
    doi:<a href="https://doi.org/10.1007/3-540-61604-7_73">10.1007/3-540-61604-7_73</a>'
  apa: 'Henzinger, T. A., Kupferman, O., &#38; Vardi, M. (1996). A space-efficient
    on-the-fly algorithm for real-time model checking. In <i>7th International Conference
    on Concurrency Theory</i> (Vol. 1119, pp. 514–529). Pisa, Italy: Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/3-540-61604-7_73">https://doi.org/10.1007/3-540-61604-7_73</a>'
  chicago: Henzinger, Thomas A, Orna Kupferman, and Moshe Vardi. “A Space-Efficient
    on-the-Fly Algorithm for Real-Time Model Checking.” In <i>7th International Conference
    on Concurrency Theory</i>, 1119:514–29. Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik, 1996. <a href="https://doi.org/10.1007/3-540-61604-7_73">https://doi.org/10.1007/3-540-61604-7_73</a>.
  ieee: T. A. Henzinger, O. Kupferman, and M. Vardi, “A space-efficient on-the-fly
    algorithm for real-time model checking,” in <i>7th International Conference on
    Concurrency Theory</i>, Pisa, Italy, 1996, vol. 1119, pp. 514–529.
  ista: 'Henzinger TA, Kupferman O, Vardi M. 1996. A space-efficient on-the-fly algorithm
    for real-time model checking. 7th International Conference on Concurrency Theory.
    CONCUR: Concurrency Theory, LNCS, vol. 1119, 514–529.'
  mla: Henzinger, Thomas A., et al. “A Space-Efficient on-the-Fly Algorithm for Real-Time
    Model Checking.” <i>7th International Conference on Concurrency Theory</i>, vol.
    1119, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 514–29, doi:<a
    href="https://doi.org/10.1007/3-540-61604-7_73">10.1007/3-540-61604-7_73</a>.
  short: T.A. Henzinger, O. Kupferman, M. Vardi, in:, 7th International Conference
    on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996,
    pp. 514–529.
conference:
  end_date: 1996-08-29
  location: Pisa, Italy
  name: 'CONCUR: Concurrency Theory'
  start_date: 1996-08-26
date_created: 2018-12-11T12:09:08Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T08:21:20Z
day: '01'
doi: 10.1007/3-540-61604-7_73
extern: '1'
intvolume: '      1119'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-61604-7_73
month: '01'
oa_version: None
page: 514 - 529
publication: 7th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - 978-3-540-70625-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '233'
quality_controlled: '1'
status: public
title: A space-efficient on-the-fly algorithm for real-time model checking
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1119
year: '1996'
...