## Games, Time, and Probability:
Graph Models for System Design and Analysis

*Thomas A. Henzinger*

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.

*Proceedings of the 33rd International Conference on
Current Trends in Theory and Practice of Computer Science*
(SOFSEM),
Lecture Notes in Computer Science 4362,
Springer, 2007, pp. 103-110.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2007 Springer.