Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-59-52-M-6

Game-Theoretic Techniques in Logic and Verification (M, 6.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-59-52-M-6 Game-Theoretic Techniques in Logic and Verification 6.0 CP (180 h)

Basedata

CP, Effort 6.0 CP = 180 h
Position of the semester 1 Sem. in WiSe
Level [6] Master (General)
Language [EN] English
Module Manager
Lecturers
Area of study [INF-ALG] Algorithmics and Deduction
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
3V+1U INF-59-52-K-6
Game-Theoretic Techniques in Logic and Verification
P 56 h 124 h
U-Schein
- PL1 6.0 WiSe
  • About [INF-59-52-K-6]: Title: "Game-Theoretic Techniques in Logic and Verification"; Presence-Time: 56 h; Self-Study: 124 h
  • About [INF-59-52-K-6]: The study achievement "[U-Schein] proof of successful participation in the exercise classes (ungraded)" must be obtained.

Examination achievement PL1

  • Form of examination: oral examination (20-60 Min.)
  • Examination Frequency: each semester
  • Examination number: 65952 ("Game-Theoretic Techniques in Logic and Verification")

Evaluation of grades

The grade of the module examination is also the module grade.


Contents

  • Ehrenfeucht–Fraïssé games (back and forth techniques), e.g., for first-order logic and modal logic.
  • Machine models with alternation
  • Multi-agent systems: Nash Equilibrium, CORE
  • Games with Probability: Markov Decision Processes, Stochastic games, randomized strategies.
  • Algorithms and complexity for various game problems: parity games, energy games, etc.
  • Applications to analysis of distributed protocols

Competencies / intended learning achievements

After successfully completing the module, students will be able to:
  • explain and apply suitable game-theoretic techniques and abstractions for problems in logic in computer science and formal verification,
  • describe game-theoretic algorithmic problems in logic and formal verification, including those in multi-agent settings, and the corresponding algorithms,
  • describe reductions between different types of game-theoretic algorithmic problems,
  • apply various verification tools (e.g. PRISM).

Literature

  • Erich Grädel, Wolfgang Thomas, and Thomas Wilke (Eds.). "Automata logics, and infinite games: a guide to current research" Springer-Verlag, 2002.
  • Christel Baier and Joost-Pieter Katoen. "Principles of Model Checking" MIT Press, 2008.
  • Jerzy Filar and Koos Vrieze. "Competitive Markov Decision Processes" Springer-Verlag, 1997.
  • Yoav Shoham and Kevin Leyton-Brown. "Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations" Cambridge University Press, 2008.
  • Wojciech Jamroga. "Logical Methods for Specification and Verification of Multi-Agent Systems" Monograph Series no 10, ICS PAS, 2015.
  • Leonid Libkin. "Elements of Finite model theory" Springer, 2004.
  • Dexter Kozen. "Theory of Computation" Springer 2006.

Requirements for attendance of the module (informal)

None

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-59-52-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective