---
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. For this purpose, we introduce a μ-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 μ-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.1006/inco.1994.1045
  bibo_issue: '2'
  bibo_volume: 111
  dct_date: 1994^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0890-5401
  dct_language: eng
  dct_publisher: Elsevier@
  dct_title: Symbolic model checking for real-time systems@
...