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

Starting from June 12, the lecture will take place every Monday DS4 (13:00-14:00) in GRU 350 and every Thursday DS5 (14:50-16:20) in GRU 358

Lecture Material

A script of the lecture is available.

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