Informatik an der TU Clausthal > Abteilungen > Computational Intelligence > Computational Intelligence > Teaching > International Lecturing > Model Checking Temporal and Strategic Logics (EASSS 2010)

Model Checking Temporal and Strategic Logics (EASSS 2010)


Nils Bulling
Jürgen Dix


  • Type: advanced, 6 hours
  • Time: Thursday 16:30-18:30, Friday 11:00-13:00 and 16:30-18:30


The course requires some basic knowledge on automata theory, complexity theory (Turing machines, reductions, P, NP, PSPACE, etc.) and some elementary understanding of propositional logic.

Overview of the course

In the first part of this lecture we introduce modal logic and show how it can be used to reason about knowledge of agents.We also discuss the correspondence of axioms with semantic properties of the models. In the second part we consider the temporal logics LTL, CTL and CTL*. Part III discusses the model checking problem and elaborates on the complexity needed to solve it for the considered temporal logics. We follow an automata theoretic approach. In part IV we introduce strategic logics which are used to model the abilities of agents. We discuss the effect of perfect and imperfect information and perfect and imperfect recall. Finally, in Part V, we consider the model checking problems of these logics.

Course Reader

As a course reader we provide the attached book chapter

Model Checking Logics of Strategic Ability: Complexity.
In Dastani, M., Hindriks, K. V., and Meyer, J.-J. C., editors, Specification and Verification of Multi-Agent Systems. Springer, 2010.

We are very thankful to Springer to grant us permission to use the chapter for this course: it is based on Sections 1, 2, and 3.



Slides (24.08.2010)


Kontakt  Suche  Sitemap  Datenschutz  Imprint
© TU Clausthal 2017