Course Catalogue

View Specification Document | Reading List

This course introduces the theory and practice of designing trustworthy computing systems through formal modelling, verification, and synthesis. Students learn the theoretical foundations of model checking algorithms, including automata theory, temporal logics (LTL and CTL), and graph algorithms. They gain practical experience modelling systems as Kripke structures, discrete-time Markov chains, Markov decision processes, and stochastic multiplayer games using the PRISM modelling language. Students express qualitative and quantitative behaviour specifications in temporal logic to capture properties such as correctness, reliability, and performance. Using PRISM and PRISM-games, students verify whether system models satisfy these specifications and synthesise optimal strategies for system control. The course equips students with foundational skills to reason about the safety and trustworthiness of complex systems, supporting the broader goal of responsible computing.

3 hours per week organised as: one 2-hour lecture per week and one 1-hour tutorial per week

Algorithmics I (H) (or equivalent)

None

None

Summative coursework include:

■ Multiple-choice quizzes on core concepts (20%)

■ Modelling and verification tasks using PRISM and PRISM-games analysis (40%)

■ Research-style poster or report on a selected research paper using PRISM, accompanied by a 1-page reflective commentary (40%)

Reassessments are normally available for all courses, except those which contribute to the Honours classification. Where, exceptionally, reassessment on Honours courses is required to satisfy professional/accreditation requirements, only the overall course grade achieved at the first attempt will contribute to the Honours classification. For non-Honours courses, students are offered reassessment in all or any of the components of assessment if the satisfactory (threshold) grade for the overall course is not achieved at the first attempt. This is normally grade D3 for undergraduate students and grade C3 for postgraduate students. Exceptionally it may not be possible to offer reassessment of some coursework items, in which case the mark achieved at the first attempt will be counted towards the final course grade. Any such exceptions for this course are described below. 

Resit examinations ARE NOT ALLOWED for Honours students.

Resit examinations ARE ALLOWED for Masters students.

The coursework cannot be redone because the nature of coursework is such that it takes a significant number of days to produce it and this effort is infeasible for supporting the re-doing of such coursework over the summer.

Course aims:

■ To provide the theoretical foundations of formal verification, including temporal logics, automata theory, and model checking algorithms

■ To introduce the modelling of concurrent and probabilistic systems using formal specification languages

■ The equip students with skills in property specification, automated verification, and controller synthesis using PRISM and PRISM-games

■ To foster critical and reflective engagement with formal methods in the context of trustworthy and responsible computing, understanding of the strengths, assumptions, and limitations of formal methods in practice

By the end of this course students will be able to:

1. Explain the core theoretical foundations of automata theory and temporal logics (LTL, CTL, Büchi automata), including their use in formal verification and synthesis.

2. Construct and analyse formal models of concurrent and probabilistic systems, including Kripke structures, discrete-time Markov chains, Markov decision processes, and stochastic multiplayer games.

3. Formulate and interpret system correctness, safety, liveness, and reward-based properties using temporal logic formalisms and their probabilistic extensions.

4. Apply model checking and strategy synthesis algorithms to nondeterministic and probabilistic models using PRISM and PRISM-games, including reasoning about multi-agent strategies and equilibrium behaviours.

5. Evaluate and justify modelling and verification decisions, identifying limitations, assumptions, and trade-offs in the use of formal methods for system analysis.

6. Demonstrate reflective practice by articulating how formal methods, property specifications and verification outcomes relate to design goals, correctness guarantees, and the responsible use of automation tools.

Students must submit at least 75% by weight of the components (including examinations) of the course's summative assessment.