Course pages 2011–12

# Temporal Logic and Model Checking

**Principal lecturer:** Prof Mike Gordon**Taken by:** Part II**Past exam questions:** Temporal Logic and Model Checking, Specification and Verification II**Information for supervisors** (contact lecturer for access permission)

No. of lectures: 8

Prerequisite course: Logic and Proof

## Aims

The aim of the course is to introduce the use of temporal logic for specifying properties of hardware and software and model checking as a method for checking that properties hold or finding counter-examples.

## Lectures

**State transition systems.**Representation of state spaces. Reachable states.**Checking reachability properties**Fixed-point calculations. Symbolic methods using binary decision diagrams. Finding counter-examples.**Examples.**Various uses of reachability calculations.**Temporal properties.**Linear and branching time. Intervals. Path quantifiers.**Temporal logic.**Brief history (Prior to Pnueli). CTL and LTL. Standarised logics: PSL.**Model checking.**Simple algorithms for verifying that temporal properties hold. Reachability analysis as a special case.**Applications.**Software and hardware examples.**Advanced methods.**Brief introduction to recent development, e.g. Counter-example guided abstraction refinement (CEGAR).

## Objectives

At the end of the course students should

- be able to write properties in a variety of temporal logic;
- be familiar with the core ideas of model checking;
- understand what commercial model checking tools can be used for.

## Recommended reading

Huth, M. & Ryan M. (2004). *Logic in Computer Science: Modelling and Reasoning about Systems*. Cambridge University Press (2nd ed.).