Interacção e Concorrência 2018-2019

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.

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.

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.

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.

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]

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

Training assignment (20%): final report expected by 4 June 2019.
Written test (80%): 27 May 2019 - 16.30 (room Edf 1 - 2.07). Results available here!
FINAL MARKS available here!
FINAL MARKS (after Época Especial) available here!