Games, Probability, and Mu-CalculusLuca de Alfaro (luca@ce.ucsc.edu) Abstract This talk overviews the solution of games using mu-calculus. First, we illustrate how games with omega-regular winning conditions can be solved using mu-calculus. The solution formulas were introduced by Emerson and Jutla in 1991 for games where the players play in turns. Such turn-based games are determined: from each state, either player 1 has a winning strategy, or player 2 has a spoiling strategy that prevents player 1 from winning. We show how the solution formulas can be extended to games in which the players choose their moves simultaleously and independently. Unlike turn-based games, these "concurrent" games are determined only in a probabilistic sense: a player may not be able to ensure victory from a state, but may nevertheless be able to ensure a certain probability of victory by playing with a randomized strategy. We show how the maximum winning probability can be computed using a quantitative extension of mu-calculus. Finally, we examine the relation between the mu-calculus formulas used to solve control (game) problems, as above, and those used to solve verification problems. In particular, we present necessary and sufficient conditions under which a mu-calculus formula can be used both for verifying an omega-regular property phi on a Kripke structure, and for solving a two-player game with winning objective phi. This talk is based on work done with Tom Henzinger, Orna Kupferman, and Rupak Majumdar. |