Model Checking & Games (MCG)

Detailed Program, Material and Exam

 

Program

» Hours: 20

• Monday-Tuesday
  • Linear and Branching Temporal Logic: Introduction, syntax and semantics, decision problems and complexity
  • Infinite-state model checking: Petri nets
• Wednesday-Tuesday
  • Two players finite state games: Definition, Classes of Games, Reductions
  • Algorithms to solve parity games
  Friday
• Student's Seminars

Material

1. Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled,MIT Press,1999.
2. "Automata, Logics, and Infinite Games: A Guide to Current Research Erich Graedel, Wolfgang Thomas, Thomas Wilke. Lecture Notes in Computer Science 2500 Springer 2002

Handsout

1. Concepts, Algorithms, and Tools for Model Checking (pdf) Joost Peter Katoen
2. Note su Logica Modale, Temporale e Model Checking (pdf) Giorgio Delzanno

Exam

The exam will take the form of a 20 minutes oral presentation (in english).