T5: Stochastic games (CANCELLED!)
Stochastic Games: A Tutorial
Marcin Jurdzinski
(Univ. of Warwick, UK)
Unfortunately, this tutorial is cancelled!
Stochastic games are repeated games with probabilistic transitions and with payoffs that are functions of the whole play, i.e., the history of the players' interaction. The theory of stochastic games is surveyed as a basis for formal specification and algorithmic analysis of quantitative properties of systems. Potential applications include design, verification, and performance evaluation of computational systems, and formalization and analysis of models used in evolutionary and population biology, and in economics. A general framework of games with Borel measurable payoff functions is presented, as well as important special cases of discounted, limiting average, and omega-regular payoffs. Algorithmic methods for solving stochastic games are surveyed, including value iteration, strategy improvement, mathematical programming, and graph theoretic algorithms. Important subclasses of the general stochastic game model are discussed, including Markov decision processes, perfect-information games, and non-stochastic 2-player games. Finally, the quantitative mu-calculus is presented as a unifying formalism for the quantitative temporal specification and verification, and it is given a stochastic games semantics. This allows to apply the rich theory of stochastic games to the semantic study and to the algorithmic applications of the quantitative mu-calculus in automated quantitative model checking.
Web Maintenance Person.