Citation
Tom Henzinger. "Games, time, and probability: Graph models for system design and analysis". Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), Lecture Notes in Computer Science, Springer, 2007.

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.

Electronic downloads

• http://mtc.epfl.ch/%7Etah/Publications/games_time_and_probability.pdf

• HTML

  Tom Henzinger. <a
  href="http://chess.eecs.berkeley.edu/pubs/265.html"
  >Games, time, and probability: Graph models for system
  design and analysis</a>, Proceedings of the 33rd
  International Conference on Current Trends in Theory and
  Practice of Computer Science (SOFSEM), Lecture Notes in
  Computer Science, Springer, 2007.

• Plain text

  Tom Henzinger. "Games, time, and probability: Graph
  models for system design and analysis". Proceedings of
  the 33rd International Conference on Current Trends in
  Theory and Practice of Computer Science (SOFSEM), Lecture
  Notes in Computer Science, Springer, 2007.

• BibTeX

  @inproceedings{Henzinger07_GamesTimeProbabilityGraphModelsForSystemDesignAnalysis,
      author = {Tom Henzinger},
      title = {Games, time, and probability: Graph models for
                system design and analysis},
      booktitle = {Proceedings of the 33rd International Conference
                on Current Trends in Theory and Practice of
                Computer Science (SOFSEM), Lecture Notes in
                Computer Science},
      organization = {Springer},
      year = {2007},
      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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/265.html}
  }
  

Posted by Tom Henzinger on 21 May 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.