• CMPE 248 Syllabus

Syllabus for CMPE 248: Games in Design and Verification

• Note that this syllabus, even though detailed, is somewhat approximate, since this is the first year that I am teaching this class.

Main Topics

1. Preliminaries.
   • Partial orders and mu-calculus.
   • Recall of some basic notions about Markov chains.
2. Two-person zero-sum games and Markov decision processes.
   • Definitions.
   • Classes of games (turn-based, concurrent, perfect and partialinformation, stochastic) and of strategies (memoryless, history-dependent, deterministic, randomized).
   • Markov decision processes (MDPs) as a special case of games.
   • Examples drawn from control and scheduling problems.
3. Structural properties of MDPs: end components, maximal end-component decomposition.
4. The sure-winning case: guaranteed winning of games with respect to safety and reachability goals.
   • Solution algorithms and the mu-calculus.
   • Properties of the winning strategies.
   • Applications: control of nondeterministic systems, scheduling, component-based design, system verification.
   • Algorithmic techniques: BDDs, QBF, and their complexity analysis.
   • Almost-sure (probability 1) winning for reachability goals.
5. Quantitative solution of MDPs with respect to safety, reachability, and total reward goals.
   • From the boolean to the quantitative mu-calculus.
   • Computation of the maximal probability of winning with respect to safety and reachability goals via value iteration and the mu-calculus.
   • Policy iteration algorithms, and properties of the winning strategies.
   • Relationship between the mu-calculus algorithms and Bellman equations; polynomial-time algorithms via linear programming.
   • Applications: safe control, optimal control.
   • Corollary: solution of MDPs with respect to omega-regular goals.
6. Quantitative solution of safety and reachability games.
   • The quantitative mu-calculus for games.
   • Matrix games and minimax theorem; linear-programming solution of matrix games.
   • Computing the maximal probability of winning a safety or reachability game via the quantitative mu-calculus.
   • Structural properties of the winning strategies.
   • Applications: optimal control of nondeterministic systems.
7. Omega-regular games via the mu-calculus.
   • Computing the maximal probability of winning via the boolean mu-calculus (turn-based games), and via the quantitative mu-calculus (concurrent games).
   • Structural properties of the winning strategies.
   • Applications: scheduling, control of nondeterministic systems.
8. Game relations.
   • A brief recall: simulation, bisimulation, and trace relations.
   • Qualitative game relations (alternating simulation and bisimulation).
   • Preservation theorems for game logics (ATL).
   • Applications: approximate analysis, system design.
9. The average reward case.
   • MDPs with average reward goals via linear programming and maximal end-component decomposition.
   • Turn-based games with average reward, their correspondence to finite games, and complexity issues.
   • Applications: optimal control, scheduling.

Optional Topics

• Advanced optional topic: partial information and team games.
  • Decidability and complexity results.
  • Partially observable MDPs: complexity results.
• Advanced optional topic: Real-time games.
  • Models for real-time games.
  • The time-progress requirement.
  • Algorithms for the solution of real-time games wrt. omega-regular conditions.
• Advanced optional topic: non-zero sum games.
  • Nash equilibrium.
  • Existence theorem via Kakutani's fixpoint theorem.
• Advanced optional topic: discounting.
  • MDPs with discounted total or average reward via the mu-calculus.
  • Games with discounted total or average reward via the mu-calculus.
  • Discounting omega-regular conditions.