To become familiar with reactive and quantum systems, emphasising the ways they compose and interact.
To master techniques for (formal) specification, analysis and verification of reactive and quantum systems.
To become familiar with the use of computational tools supporting the specification and analysis of reactive and quantum systems.
- Basic models for reactive systems
- Interaction and concurrency.
- Labelled transition systems.
- Similarity and bisimilarity.
- Process algebra
- Action, process and behaviour.
- Modelling and analysis of reactive systems in CCS and mCRL2.
- Logics for reactive systems:
- Hennessy-Milner logic and its extensions.
- Modal equivalence and bisimilarity.
- Specification and verification of logic constraints.
- Introduction to quantum information and computation.
- Mathematical background: Hilbert spaces. The Dirac notation.
- Quantum states, processes and composition
- Time-evolutions and measurement.
- Mixed quantum states.
- Modelling quantum processes
- The circuit model.
- Quantum gates.
- Case study: Superdense coding and quantum teleportation.
- Introduction to quantum algorithms
- The Deutsch-Jozsa and Simon algorithms.
- Algorithms based on amplitude amplification.
- Tool support - Quantum modelling and programming in Qiskit.
Lectures (T - Monday, 11:00 - 13:00)
here every week
NOTE: Video record available from the course BlackBoard platform (in contents)
22 Feb 2021 [slides]
Introduction to "Interaction and Concurrency" and the course dynamics.
Labelled transition systems. Morphisms between trarnsition systems.
Notions of equivalence between labelled transition systems. Notions of trace, simulation and bisimulation. Bisimilarity.
1 Mar 2021 [slides]
Specification of reactive systems with process algebras. Introduction to CCS: motivation, syntax, semantics.
Exercise Sessions (TP - Tuesday, 16:00 - 18:00)
here every week
Classical reactive processes
- 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.
- 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
- N. Yanofsky, M. Mannucci. Quantum Computing for Computer Scientists. CUP, 2008.
- E. Rieffel and W. Polak. Quantum Computing: A Gentle Introduction. MIT Press, 2011.
- M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information (10th
Anniversary Edition). Cambridge University Press, 2010.
- S. Aaronson. Quantum Computing since Democritus. Cambridge
University Press, 2013.
- Training assignment (60%): with oral discussion on 24 and 25 May
(with intermediate ckeckpoints)
- Individual assynchronous test (40%): 4 exercises proposed along the T lectures
- Appointments - Luis: Wed, 18:00-20:00 and Fri, 18:00-20:00 (please send an email the day before)
- Appointments - Ana: Wed, 17:00-19:00 (please send an email the day before)
- Email: lsb at di dot uminho dot pt (Luis) and aicneri at gmail dot com (Ana)
- Last update: 2021.02.27