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%)

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.