Temporal Logic

Temporal Logic

Technische Universität Dresden
Institut für Theoretische Informatik
Lehrstuhl für Automatentheorie

Carsten Lutz

Course Description

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

Organization

The lecture takes place every Tuesday in DS4 (13:00-14:30) in room GRU 350.

Lecture Material

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

Computational 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.

Literature

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

Carsten Lutz