---
res:
  bibo_abstract:
  - 'Digital technology is increasingly deployed in safety-critical situations. This
    calls for systematic design and verification methodologies that can cope with
    three major sources of system complexity: concurrency, real time, and uncertainty.
    We advocate a two-step process: formal modeling followed by algorithmic analysis
    (or, “model building” followed by “model checking”). We model the concurrent components
    of a reactive system as potential collaborators or adversaries in a multi-player
    game with temporal objectives, such as system safety. The real-time aspect of
    embedded systems requires models that combine discrete state transitions and continuous
    state evolutions. Uncertainty in the environment is naturally modeled by probabilistic
    state changes. As a result, we obtain three orthogonal extensions of the basic
    state-transition graph model for reactive systems —game graphs, timed graphs,
    and stochastic graphs— as well as combinations thereof. In this short text, we
    provide a uniform exposition of the underlying definitions. For verification algorithms,
    we refer the reader to the literature.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Thomas Henzinger
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  bibo_doi: 10.1007/978-3-540-69507-3_7
  bibo_volume: 4362
  dct_date: 2007^xs_gYear
  dct_publisher: Springer@
  dct_title: 'Games, time, and probability: Graph models for system design and analysis@'
...