## Learning outcomes

• To become familiar with reactive systems, emphasising their concurrent composition and continuous interaction with their environment.
• To master techniques for (formal) specification, analysis and verification of reactive systems.
• To become proficient in the use of computational tools supporting the specificationa and analysis of reactive systems.

## Syllabus

• Basic models for reactive systems (state, behaviour, interaction, concurrency).
• Labelled transition systems.
• Similarity and bisimilarity.
• Process algebra
• Action, process and behaviour.
• Modelling and analysis of reactive systems in CCS.
• Modelling and analysis of reactive systems in mCRL2.
• Logics for reactive systems:
• Hennessy-Milner logic and its extensions.
• Modal equivalence and bisimilarity.
• Specification and verification of logic constraints.
• Quantum processes:
• Introduction to the quantum computation model.
• Quantum processes and algorithms.

## Summaries (2018-19)

##### T Lectures
• Feb 4: Introduction to the course. Labelled transition systems. Morphisms between trarnsition systems. The relational and coalgebraic perspectives.
• Feb 11: Examples of LTS. Exercise sheet 1.
• Feb 18: Introduction to process algebra. Basic process operators. Syntax and semantics of CCS.
• Mar 4: Modelling in CCS. Examples
• Mar 11: Observational equivalences in process algebra. Weak bisimulation and process equality. Equational reasoning about processes.
• Mar 18: Introduction to mCRL2 as a process modeling tool.
• Mar 25: Modal logic: syntax and semantics. The logic of Hennessy-Milner.
• Apr 23: The modal Mu-calculus. Case studies on specifying process properties.
• Apr 29: Introduction to quantum processes. Basic definitions and concepts. Towards a quantum computational model.
• May 6: Specification of quantum processes. The circuit model. Deutsch–Jozsa and Grover's algorithm.
##### P Lectures
• Feb 5: Trace equivalence. Notions of simulation and bisimulation. Similarity and bisimilarity; properties.
• Feb 12: Experiments with different notions of LTS equivalence. Exercise sheet 1.
• Feb 19: Exercise sheet 2.
• Mar 5: Exercise sheet 3.
• Mar 19: Exercise sheet 4.
• Mar 26: Exercise sheet 5.
• Apr 9: Support to mCRL2 practice.
• Apr 30: Use of mCRL2 for verification of process properties. Exercise sheet 6.
• May 7: Hands-on session with Qiskit.

## Support

##### Basic Bibliography
• Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007. [book]
• Jan Friso Groote, Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2008. [book]
• Noson Yanofsky, Mirco Mannucci. Quantum Computing for Computer Scientists. CUP, 2008.[book]
##### Complementary Bibliography
• J. C. M. Baeten, T. Basten, M. A. Reniers. Process Algebra: Equational Theories of Communicating Processes. CUP, 2010.
• Robin Milner. Communicating and Mobile Systems: The Pi Calculus. CUP, 1999.
• Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008