Course pages 2013–14
Subsections
Temporal Logic and Model Checking
Lecturer: Professor M.J.C. Gordon
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.).