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.
·
Pre-requisites
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.
2.
Home-works.
3.
Class
review and participation.
4.
Student
presentation of research papers.
·
Lecture Notes
·
Lectures and
Course Content in details
General
graph models
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.
D) PTIME-completeness
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.
Parity Games.
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.
B) NP-completeness.
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.
Concurrent games.
A) Reachability and safety conditions.
B) Qualitative solution.
Student presentations on papers.