Course: Game Theory in Formal Verification

(A course on Distributed Systems will be taught by Ulrich Schmid on the same day: see link for more details. Also see the course flyers)

 

Shuttle Bus: Departure time Bus station Heiligenstadt: 09.45, Bus with IST Austria sign Departure time IST Campus: 16.15 (after course of Ulrich Schmid).

NO CLASS on JUNE 17, 2010.

THANKS FOR ATTENDING THE COURSE!!!

NEW: Student Presentation Schedule:

June 10: (1) Nathanael Fijalkow; (2) Arjun Radhakrishna; and (3) Friedrich Silvosky [Paper reading presentation: 35 minutes each]

June 24: (1) Matthias Függer and Thomas Nowak; (2) Damien Zufferey;  (3) Heinrich Mosser et.al.; and (4) Anmol Tomar [Research Project Presentation: 25 minutes each].

Feedback: Please send me an email with feedback about course material, presentation style, how to improve the course and any other relevant feedback.

 

Homeworks:

 Homework 3: Due date: May 20, 2010 (in class or by email by 10:00 AM) Link

  Homework 2: Due date: Apr 15, 2010 (in class or by email by 10:00 AM) Link

          Homework 1: Due date: Mar 11, 2010 (in class or by email by 10:00 AM) Link

Spring 2010

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

·        Lecture 2 Notes

·        Lecture 3 Notes

·        Lecture 4 Notes

·        Lecture 5 Notes

·        Lecture 6 Notes

·        Lecture 7 Notes

·        Lecture 8 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.