Game thoeretic methods provide the mathematical background for formal analysis of several important problems in computer science, such as formally proving correctness of dynamic systems, automatically designing a correct system from specifications, auction theory, controller synthesis, etc. Game theoretic methods are central in formal verification of open reactive systems (systems that interact with an environment), embedded systems, and many other applications in formal verification. In this course we will study the basic game models in formal verification with all the commonly used specifications in verification, such as safety, reachability, liveness and fairness specifications.
The course will not be taught from any specific book. There will be references to research papers.
This PhD-level course is introduction to basic game theoretic methods in formal verification, algorithmic analysis of the games, and formal-mathematical analysis of the games. It shall allow the attendees to: (1) become familiar with the different game theoretic models, algorithms and proof techniques to analyze the game models; (2) be able to apply the game theoretic results in formal analysis and proving correctness of reactive systems; and (3) be able to analyze and design new algorithms for new game models with new class of specifications with the knowledge about the basic game theoretic techniques.
1. Basic discrete mathematics (such as basic knowledge of set theory, monotonic functions, fixpoints etc);
2. Basic course in algorithms (such as how to prove correctness of basic graph algorithms such as minimum spanning tree, shortest path); and
3. Basic probability theory.
· Student evaluation (Grading)
1. Scribe notes for classes.
3. Class review and participation.
4. Student presentation of research papers.
· Lecture Notes
· Lectures and Course Content in details
A) Graphs with reachability and safety objectives: NLGOSPACE complete.
B) Liveness objective: algorithm, and NLGOPSPACE-completeness.
C) Other models: games and Markov decision processes.
Reachability and safety games
A) Attractors and how to use them to solve these games.
B) Polynomial time algorithm.
C) Memoryless determinacy.
Reachability and safety games (contd)
A) Linear time algorithm.
B) \Mu-calculus formula.
C) Symbolic algorithm.
Buechi and coBuechi Games
A) Quadratic algorithm.
B) Memoryless determinacy.
C) \Mu-calculus formula and symbolic algorithm.
A) Memoryless determinacy.
B) NP and coNP complexity.
C) Classical algorithm.
Parity Games Algorithms
A) Small-progress measure algorithm.
B) Sub-exponential time algorithm.
Strong fairness games (Rabin/Street games).
A) Memoryless strategies for Rabin games.
C) Algorithm for Rabin and Streett games.
Markov decision processes
A) Reachability as least fixpoint.
B) Memoryless strategies.
C) Linear programming solution.
MDPs with liveness
A) End components.
B) polynomial time solution for Buechi, coBuechi, parity.
Simple stochastic games
A) Anne condon's result on memoryless determinacy
B) connection with parity games.
C) NP cap coNP result and quadratic programming solution.
A) Reachability and safety conditions.
B) Qualitative solution.
Student presentations on papers.