---
_id: '4505'
abstract:
- lang: eng
  text: "We describe finite-state programs over real-numbered time in a guarded-command
    language with real-valued clocks or, equivalently, as finite automata with real-valued
    clocks. Model checking answers the question which states of a real-time program
    satisfy a branching-time specification (given in an extension of CTL with clock
    variables). We develop an algorithm that computes this set of states symbolically
    as a fixpoint of a functional on state predicates, without constructing the state
    space.\r\n\r\nFor this purpose, we introduce a mu-calculus on computation trees
    over real-numbered time. Unfortunately, many standard program properties, such
    as response for all nonzeno execution sequences (during which time diverges),
    cannot be characterized by fixpoints: we show that the expressiveness of the timed
    mu-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this
    result does not impair the symbolic verification of "implementable"
    real-time programs--those whose safety constraints are machine-closed with respect
    to diverging time and whose fairness constraints are restricted to finite upper
    bounds on clock values. All timed CTL properties of such programs are shown to
    be computable as finitely approximable fixpoints in a simple decidable theory."
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: Xavier
  full_name: Nicollin, Xavier
  last_name: Nicollin
- first_name: Joseph
  full_name: Sifakis, Joseph
  last_name: Sifakis
- first_name: Sergio
  full_name: Yovine, Sergio
  last_name: Yovine
citation:
  ama: 'Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for
    real-time systems. In: <i>Proceedings of the 7th Annual IEEE Symposium on Logic
    in Computer Science</i>. IEEE; 1992:394-406. doi:<a href="https://doi.org/10.1109/LICS.1992.185551">10.1109/LICS.1992.185551</a>'
  apa: 'Henzinger, T. A., Nicollin, X., Sifakis, J., &#38; Yovine, S. (1992). Symbolic
    model checking for real-time systems. In <i>Proceedings of the 7th Annual IEEE
    Symposium on Logic in Computer Science</i> (pp. 394–406). Santa Cruz, CA, United
    States of America: IEEE. <a href="https://doi.org/10.1109/LICS.1992.185551">https://doi.org/10.1109/LICS.1992.185551</a>'
  chicago: Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
    “Symbolic Model Checking for Real-Time Systems.” In <i>Proceedings of the 7th
    Annual IEEE Symposium on Logic in Computer Science</i>, 394–406. IEEE, 1992. <a
    href="https://doi.org/10.1109/LICS.1992.185551">https://doi.org/10.1109/LICS.1992.185551</a>.
  ieee: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking
    for real-time systems,” in <i>Proceedings of the 7th Annual IEEE Symposium on
    Logic in Computer Science</i>, Santa Cruz, CA, United States of America, 1992,
    pp. 394–406.
  ista: 'Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1992. Symbolic model checking
    for real-time systems. Proceedings of the 7th Annual IEEE Symposium on Logic in
    Computer Science. LICS: Logic in Computer Science, 394–406.'
  mla: Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.”
    <i>Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science</i>,
    IEEE, 1992, pp. 394–406, doi:<a href="https://doi.org/10.1109/LICS.1992.185551">10.1109/LICS.1992.185551</a>.
  short: T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, in:, Proceedings of the
    7th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1992, pp. 394–406.
conference:
  end_date: 1992-06-25
  location: Santa Cruz, CA, United States of America
  name: 'LICS: Logic in Computer Science'
  start_date: 1992-06-22
date_created: 2018-12-11T12:09:12Z
date_published: 1992-01-01T00:00:00Z
date_updated: 2022-03-14T13:20:50Z
day: '01'
doi: 10.1109/LICS.1992.185551
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/185551
month: '01'
oa_version: None
page: 394 - 406
publication: Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
  isbn:
  - 0-8186-2735-2
publication_status: published
publisher: IEEE
publist_id: '224'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for real-time systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1992'
...