README.md 5.85 KB
Newer Older
Daniel Stan's avatar
Daniel Stan committed
1
2
# Game theory WS21

Muhammad Najib's avatar
Muhammad Najib committed
3
4
This is the directory for the [Game-Theoretic Techniques in Logic and Verification module](https://modhb.uni-kl.de/mhb/courses/INF-59-52-K-6/) for WS'21. The module is 3V+1Ü. 

Muhammad Najib's avatar
Muhammad Najib committed
5
6
Game theoretic techniques provide mathematical foundations for the formal analysis of computerised systems, such as the correctness of reactive systems, controller synthesis, design and verification of multi-agent systems, etc. Game theoretic techniques also provide important tools that have been widely used in the field of formal logic. In this course, we will study the fundamental game models commonly used in formal verification, as well as their connection with formal logic. This course shall enable students to (1) have a knowledge of basic game models, and algorithms and analytical tools to study them; (2) apply the game theoretic techniques to model and analyse reactive systems; (3) use games for the study of formal systems.

Muhammad Najib's avatar
Muhammad Najib committed
7
8
9
10
11
## Registration
It is of utmost importance that you register to this course as soon as possible.
Please follow the following 
[OLAT link](https://olat.vcrp.de/auth/RepositoryEntry/3392342057/CourseNode/104427981506026).

Muhammad Najib's avatar
Muhammad Najib committed
12
13
14
15
## Examination
- Format: oral exam
- Schedule: First 2 weeks after teaching period

Muhammad Najib's avatar
Muhammad Najib committed
16
17
## Time+Venues for Lectures
The lectures will be a combination of live lectures and recorded lectures. Keep yourself updated by joining the OLAT page: [OLAT](https://olat.vcrp.de/auth/RepositoryEntry/3392342057/CourseNode/104427981506026)
Muhammad Najib's avatar
Muhammad Najib committed
18

Muhammad Najib's avatar
Muhammad Najib committed
19
- Time: Friday 10:00 - 11:30
Muhammad Najib's avatar
Muhammad Najib committed
20
21
- Venues: 
    - Weekly: OLAT (prerecorded)
Muhammad Najib's avatar
Muhammad Najib committed
22
23
24
    - Every 2 weeks: 
        - 13-370 (in-person): Week 2, 4
        - OLAT (online): Week 6, 8, 10, 12
Muhammad Najib's avatar
Muhammad Najib committed
25
26
27

## Time+Venues for Tutorials 

Muhammad Najib's avatar
Muhammad Najib committed
28
- Time: Wednesday 14:00 - 15:30, every 2 weeks: Week 2, 4, 6, 8, 10, 12
Muhammad Najib's avatar
Muhammad Najib committed
29
- Venues: OLAT
Muhammad Najib's avatar
Muhammad Najib committed
30
31
32
33
34
35
36
37

## Prerequisites
There is no *hard* prerequisite, but we strongly encourage that you have done 
something equivalent to our Logik und Semantik von Programmiersprachen 
[INF-02-05-V-2](https://arg-git.informatik.uni-kl.de/pub/logic19w).
In particular, this course should not be your first course on Propositional Logic and First-Order Logic. The course assumes no prior knowledge of game theory.

## Requirements for a Zulassung
Muhammad Najib's avatar
Muhammad Najib committed
38
39
40
- ≥50% (programming project + average for exercise sheets)/2
- ≥50% average for multiple choice questions. (To access the quizzes, please enroll to the course via [OLAT](https://olat.vcrp.de/auth/RepositoryEntry/3392342057/CourseNode/104427981506026)).
- Come up with ≥ 5 questions during Q&A sessions
Muhammad Najib's avatar
Muhammad Najib committed
41

Muhammad Najib's avatar
Muhammad Najib committed
42
## Instructors
Muhammad Najib's avatar
Muhammad Najib committed
43
44
45
- Prof. Anthony W. Lin [lin _at sign_ cs.uni-kl.de]
- Dr. Muhammad Najib [najib _at sign_ cs.uni-kl.de]
- Dr. Daniel Stan [stan _at sign_ cs.uni-kl.de]
Muhammad Najib's avatar
Muhammad Najib committed
46

Muhammad Najib's avatar
Muhammad Najib committed
47
48
49
50
## Übungs organization and Tutors
- Dr. Di-De Yen
- Pascal Bergsträßer [bergstraesser _at sign_ cs.uni-kl.de]
- Oliver Markgraf [markgraf _at sign_ cs.uni-kl.de]
Muhammad Najib's avatar
Muhammad Najib committed
51

Muhammad Najib's avatar
Muhammad Najib committed
52
## Exercises
Muhammad Najib's avatar
Muhammad Najib committed
53
54
55
- There is one exercise sheet for each corresponding weekly lecture, released after the lecture (on Friday)
- The deadline is at 12:00 on the day the tutorials take place (see tutorials schedule above). Deadlines are written on the sheets.
- Submission via OLAT
Muhammad Najib's avatar
Muhammad Najib committed
56
- Exercise sheets can be found [here](exercises)
Muhammad Najib's avatar
Muhammad Najib committed
57

Muhammad Najib's avatar
Muhammad Najib committed
58
59
60
61
## OLAT quizzes
- OLAT quizzes are released every week on Friday
- Deadlines are the following Wednesdays, at 12:00

Muhammad Najib's avatar
Muhammad Najib committed
62
## Some reference books
Muhammad Najib's avatar
Muhammad Najib committed
63
64
65
66
- **Automata, logics, and infinite games: a guide to current research** by Erich Grädel, Wolfgang Thomas, and Thomas Wilke, 2002.
- **Principles of Model Checking** by Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
- **Competitive Markov Decision Processes** by Jerzy Filar and Koos Vrieze, 1997.
- **Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations** by Yoav Shoham and Kevin Leyton-Brown. Cambridge UP, 2009. (Available free (legally!) [here](http://www.masfoundations.org/download.html))
67
- **Logical Methods for Specification and Verification of Multi-Agent Systems** by Wojciech Jamroga, 2015. (Available free (legally!) [here](https://home.ipipan.waw.pl/w.jamroga/papers/jamroga15specifmas-20200411.pdf))
Muhammad Najib's avatar
Muhammad Najib committed
68
69
70

## Tentative Schedule

Muhammad Najib's avatar
Muhammad Najib committed
71
### Week 1 (29.10.2021) {[draft notes](week1/overview.md)}{[slides](week1/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
72
73
74
75
76
- Intro
- Finite duration games
- Automata on Finite Words
- Determinacy of Finite Duration Games

Muhammad Najib's avatar
Muhammad Najib committed
77
### Week 2 (05.11.2021) {[draft notes](week2/overview.md)}{[slides](week2/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
78
79
80
81
- Inifinite Duration Games
- Automata on Infinite Words
- Winning Conditions of Infinite Duration Games

Muhammad Najib's avatar
Muhammad Najib committed
82
### Week 3 (12.11.2021) {[draft notes](week3/overview.md)}{[slides](week3/ltlaut.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
83
84
85
86
- A Brief Intro to Linear Temporal Logic (LTL)
- Alternating Finite Automata
- On Model Checking LTL Formulae

Muhammad Najib's avatar
Muhammad Najib committed
87
### Week 4 (19.11.2021) {[draft notes](week4/overview.md)}{[slides](week4/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
88
- Beyond 2-player Zero-Sum Games
Muhammad Najib's avatar
Muhammad Najib committed
89
90
91
- Normal-form and Extensive-form Games
- Boolean Games

Muhammad Najib's avatar
Muhammad Najib committed
92
### Week 5 (26.11.2021) {[draft notes](week5/overview.md)}{[slides](week5/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
93
- Iterated Boolean Games
Muhammad Najib's avatar
Muhammad Najib committed
94
95
- Cooperative Games

Daniel Stan's avatar
Daniel Stan committed
96
### Week 6 (02.12.2021)  {[draft notes](week6/overview.md)}{[slides](week6/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
97
98
- Probability Theory and Stochastic Processes for Markov Chains

Daniel Stan's avatar
Daniel Stan committed
99
### Week 7 (09.12.2021) {[draft notes](week7/overview.md)}{[slides](week7/slides.pdf)}
Muhammad Najib's avatar
Muhammad Najib committed
100
- Reachability in Markov Chains
Daniel Stan's avatar
Daniel Stan committed
101
102
- Steady State analysis of Markov Chains
- Reachability in Markov Decision Process
Muhammad Najib's avatar
Muhammad Najib committed
103
104
105
106

### Week 8
- Programming Week

Daniel Stan's avatar
Daniel Stan committed
107
108
109
110
### Week 9 (06.12.2021) {[draft notes](week9/overview.md)}{[slides](week9/slides.pdf)}
- Discounted Rewards
- Parity/Priority Payoff
- 2-player Parity Games
Muhammad Najib's avatar
Muhammad Najib committed
111

Anthony Widjaja Lin's avatar
Typo    
Anthony Widjaja Lin committed
112
### Week 10 {[draft notes](week10/overview.md)}
Anthony Widjaja Lin's avatar
Anthony Widjaja Lin committed
113
114
- Ehrenfeucht–Fraïssé Game 
- Limitation of FO (first-order logic)
Muhammad Najib's avatar
Muhammad Najib committed
115

Anthony Widjaja Lin's avatar
Anthony Widjaja Lin committed
116
### Week 11 {[draft notes](week11/overview.md)}
Anthony Widjaja Lin's avatar
Anthony Widjaja Lin committed
117
118
119
120
121
122
123
124
- Kamp's Theorem (LTL = FO)

### Week 12
- Games on infinite systems
- Applications to control synthesis

### Week 13
- Games on infinite systems
Muhammad Najib's avatar
Muhammad Najib committed
125
126
127
128

### Week 14
- Reviews

Daniel Stan's avatar
Daniel Stan committed
129
130
131
Cross references:

 * https://modhb.uni-kl.de/mhb/courses/INF-59-52-K-6/
Muhammad Najib's avatar
Muhammad Najib committed
132
 * https://olat.vcrp.de/url/RepositoryEntry/3392342057