Interacção e Concorrência 2018/19
Licenciatura em Ciências da Computação
Dep. Informática, Universidade do Minho
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.
Introduction to the course. Labelled transition systems. Morphisms between trarnsition systems. The relational and coalgebraic perspectives.
Examples of LTS. Exercise sheet 1.
Introduction to process algebra. Basic process operators. Syntax and semantics of CCS.
Modelling in CCS. Examples
Observational equivalences in process algebra. Weak bisimulation and process equality. Equational reasoning about processes.
Introduction to mCRL2 as a process modeling tool.
Modal logic: syntax and semantics. The logic of Hennessy-Milner.
The modal Mu-calculus. Case studies on specifying process properties.
Introduction to quantum processes. Basic definitions and concepts. Towards a quantum computational model.
Specification of quantum processes. The circuit model. Deutsch–Jozsa and Grover's algorithm.
Trace equivalence. Notions of simulation and bisimulation. Similarity and bisimilarity; properties.
Experiments with different notions of LTS equivalence. Exercise sheet 1.
Exercise sheet 2.
Exercise sheet 3.
Exercise sheet 4.
Exercise sheet 5.
Support to mCRL2 practice.
Use of mCRL2 for verification of process properties. Exercise sheet 6.
Hands-on session with Qiskit.
Lectures (from the 2014-15 edition, in Portuguese)
Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. CUP, 2007.
Jan Friso Groote, Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, 2008.
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!
- Appointments: Wed, 9-11 (please send an email the day before)
- Email: lsb at di dot uminho dot pt
- Last update: 2019.07.25