Interacção e Concorrência 2018/19
Licenciatura em Ciências da Computação
Dep. Informática, Universidade do Minho
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:
 HennessyMilner 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 (201819)
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 HennessyMilner.

Apr 23:
The modal Mucalculus. 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:
Handson session with Qiskit.
Support
Slides (201819)
Exercises
Lectures (from the 201415 edition, in Portuguese)
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, JoostPieter Katoen. Principles of Model Checking. MIT Press, 2008
Links
Pragmatics
Lecturer
Assessment
 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!
Contact
 Appointments: Wed, 911 (please send an email the day before)
 Email: lsb at di dot uminho dot pt
 Last update: 2019.07.25