Computer Laboratory

Course pages 2013–14

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
Suggested hours of supervisions: 2
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. Simple software and hardware examples.

  • Advanced methods. Very 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.).