Simply a Game: Model Checking and Games


  • Contact: Alina Bey

  The first session, 14th of April, is mandatory for every student who wants to give a talk!


Topics marked in red are already chosen by a student.

Provided links may only work inside the University or via VPN.

 Introduction to Game Theory

 Discrete Games

  1. Game solving and NuSMV with NuGAT
  2. Checking realizability of and synthesizing strategies for generalized reactivity specifications with gr1
  3. Synthesize reactive designs from multi-paradigm specifications written in an extension of Promela for open systems

 Full LTL Games

  1. LTL Realizability check & winning strategy synthesis with Acacia+
  2. Algorithmic games used in verification and synthesis using GAVS+
  3. The GASt platform (various topics)

Parity Game Solvers

  1. PGSolver Tools for generating, manipulating and solving parity games
  2. PDSolver Evaluating both mu-calculus formulas over pushdown systems and pushdown parity games

 Quantitative Games

  1. mpg-solver Mean-payoff game solver
  2. Solving probabilistic games with w-regular objectives qualitatively with GIST

 Hybrid Games

  1. Receding Horizon Temporal Logic Planning Toolbox (TuLiP)
  2. Designing, testing and implementing hybrid controllers generated automatically from task specifications written in Structured English or Temporal  Logic (LTLMoP and SLURP)
  3. Synthesis of correct-by-design embedded control software based on approximate bisimulations with PESSOA


  1. More topics if necessary


  • Master students
  • Bachelor students > 3. semester

Subject Area

Informatik der Systeme / Angewandte Informatik 


All materials are available through the Ilias-Website.

Registration is done using your university e-mail account.
The password will be presented in the first session on April 16th.

Credit Requirements

  • 30 Minutes Presentation + 15 Minutes Discussion 
  • Written report (8-10 pages)
  • Presence and active participation during the presentations of the other students.
  • The language for the presentation will be English.

4 ECTS-Points.