## 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

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

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