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

Digital technology, from medical implants to drive-by-wire systems, is increasingly deployed in safety-critical situations. calls for systematic design and verification methodologies that can cope with three major sources of system complexity: concurrency, real time, and uncertainty. advocate a two-step process: formal modeling followed by algorithmic analysis (or, model building followed by model checking). model the components of a concurrent system as potential collaborators or adversaries in a multi-player game with temporal objectives, such as system safety. real-time aspects of embedded software are modeled by hybrid dynamical systems that combine both discrete state transitions and continuous state evolutions. Uncertainty in the environment is naturally modeled by stochastic behavior. a result, we obtain three orthogonal extensions of basic state-transition graph models of systems

• game graphs,
• timed graphs,
• Markov decision processes

and all combinations thereof.

While the model checking of finite, boolean systems is now standard practice in hardware verification, recently much progress has been made also in model checking software and embedded systems. These algorithms must cope with the infinite, quantitative aspects of the models outlined above, including an unbounded number of concurrent processes, recursive data structures, and real numbers for representing time and probabilities. present a couple of common ingredients for constructing such model checkers: the use of fixed-point computations on symbolic constraints for exploring non-boolean state spaces; and the use of lazy abstraction refinement for automatically adjusting the precision of the algorithm.