---
_id: '4514'
abstract:
- lang: eng
text: '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.'
acknowledgement: This research was supported in part by the Swiss National Science
Foundation, and by the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Games, time, and probability: Graph models for system design
and analysis. In: Vol 4362. Springer; 2007:103-110. doi:10.1007/978-3-540-69507-3_7'
apa: 'Henzinger, T. A. (2007). Games, time, and probability: Graph models for system
design and analysis (Vol. 4362, pp. 103–110). Presented at the SOFSEM: Current
Trends in Theory and Practice of Computer Science, Springer. https://doi.org/10.1007/978-3-540-69507-3_7'
chicago: 'Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System
Design and Analysis,” 4362:103–10. Springer, 2007. https://doi.org/10.1007/978-3-540-69507-3_7.'
ieee: 'T. A. Henzinger, “Games, time, and probability: Graph models for system design
and analysis,” presented at the SOFSEM: Current Trends in Theory and Practice
of Computer Science, 2007, vol. 4362, pp. 103–110.'
ista: 'Henzinger TA. 2007. Games, time, and probability: Graph models for system
design and analysis. SOFSEM: Current Trends in Theory and Practice of Computer
Science, LNCS, vol. 4362, 103–110.'
mla: 'Henzinger, Thomas A. Games, Time, and Probability: Graph Models for System
Design and Analysis. Vol. 4362, Springer, 2007, pp. 103–10, doi:10.1007/978-3-540-69507-3_7.'
short: T.A. Henzinger, in:, Springer, 2007, pp. 103–110.
conference:
name: 'SOFSEM: Current Trends in Theory and Practice of Computer Science'
date_created: 2018-12-11T12:09:15Z
date_published: 2007-01-04T00:00:00Z
date_updated: 2021-01-12T07:59:22Z
day: '04'
doi: 10.1007/978-3-540-69507-3_7
extern: 1
intvolume: ' 4362'
month: '01'
page: 103 - 110
publication_status: published
publisher: Springer
publist_id: '217'
quality_controlled: 0
status: public
title: 'Games, time, and probability: Graph models for system design and analysis'
type: conference
volume: 4362
year: '2007'
...