---
res:
  bibo_abstract:
  - We extend the specification language of temporal logic, the corresponding verification
    framework, and the underlying computational model to deal with real-time properties
    of reactive systems. Semantics We introduce the abstract computational model of
    timed transition systems as a conservative extension of traditional transition
    systems qualitative fairness requirements are superseded by quantitative real-time
    constraints on the transitions. Digital clocks are introduced as observers of
    continuous real-time behavior. We justify our semantical abstractions by demonstrating
    that a wide variety of concrete real-time systems can be modeled adequately. Specification
    We present two conservative extensions of temporal logic that allow for the specification
    of timing constraints while timed temporal logic provides access to time through
    a novel kind of time quantifier, metric temporal logic refers to time through
    time-bounded versions of the temporal operators. We justify our choice of specification
    languages by developing a general framework for the classification of real-time
    logics according to their complexity and expressive power. Verification We develop
    tools for determining if a real-time system that is modeled as a timed transition
    system meets a specification that is given in timed temporal logic or in metric
    temporal logic. We present both model-checking algorithms for the automatic verification
    of finite-state real-time systems and proof methods for the deductive verification
    of real-time systems.@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
  dct_date: 1991^xs_gYear
  dct_language: eng
  dct_publisher: Stanford University@
  dct_title: The temporal specification and verification of real-time systems @
...
