---
res:
  bibo_abstract:
  - "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.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Xavier
      foaf_name: Nicollin, Xavier
      foaf_surname: Nicollin
  - foaf_Person:
      foaf_givenName: Joseph
      foaf_name: Sifakis, Joseph
      foaf_surname: Sifakis
  - foaf_Person:
      foaf_givenName: Sergio
      foaf_name: Yovine, Sergio
      foaf_surname: Yovine
  bibo_doi: 10.1109/LICS.1992.185551
  dct_date: 1992^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0-8186-2735-2
  dct_language: eng
  dct_publisher: IEEE@
  dct_title: Symbolic model checking for real-time systems@
...