This lecture gives a basic account of temporal logic from the
viewpoint of computer science. Motivated by the specification of
reactive and concurrent systems, we introduce both linear and
branching-time temporal logics. We discuss the expressive power of
such logics, relating them to one another, to first and second order
logic, and to automata theory. We consider the two reasoning tasks
model checking and satisfiability checking, and perform a detailed
investigation of the computational complexity of these tasks.
Prerequesites: basics of complexity theory will be helpful
The lecture takes place every Tuesday in DS4
(13:00-14:30) in room GRU 350.
Since a script of the lecture is not available, it is recommended that
students attending the lecture copy what is written on the blackboard.
A correction of the beginning of Section 2.5 can be found here
Credits / Examinations
logic students can earn 3 credits by attending this lecture. The
lecture can be used for the modules SV and TCSL. In order to get
the credits, CL students have to pass an oral examination at the end
of the term.
The following literature is relevant for the lecture:
- E. Allen Emerson: Temporal and Modal Logic. In J. van Leeuwen,
editor, Handbook of Theoretical Computer Science, Elsevier, 1990.
- Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds: Temporal Logic
(Volume 1): Mathematical Foundations and Computational Aspects,
Oxford University Press, 1994.
- Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking.
MIT Press, 1999