## Temporal Logic |
Technische Universität Dresden |

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.

A correction of the beginning of Section 2.5 can be found here

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