Lecturer
Nils Bulling
Jürgen Dix
Misc
- Type: advanced, 6 hours
- Time: Thursday 16:30-18:30, Friday 11:00-13:00 and 16:30-18:30
Prerequisites
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.