Learning outcomes
-
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.
Syllabus
Reactive 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.
Quantum Systems
- Fundamentals
- 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.
Summaries (2020-21)
Lectures (T - Monday, 11:00 - 13:00)
Virtual classroom: Join
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.
-
8 Mar 2021
Introduction to CCS combinators. Examples.
-
15 Mar 2021 [slides]
The process calculus.
-
22 Mar 2021
Observational equivalence and its calculus. Introduction to mCRL2 - a tool for process modelling. [slides]
-
6 Abr 2021
Specification of process properties. Brief introduction to modal logic. The Hennessy-Milner logic por processes. [slides]
-
12 Abr 2021
Modal equivalence and bisimilarity. Temporal reasoning.
-
19 Abr 2021
Introduction to quantum processes. [slides]
Notion of a qubit. Computing with qubits. Illustration: the Deutsch algorithm. [slides]
-
26 Abr 2021
Computing with qubits illustrated through the Deutsch algorithm. Brief introduction to Hilbert spaces.
The principles of quantum computation: The state space postulate [slides (see sections 1 and 2)].
-
3 May 2021
Representation of qubits in the Bloch sphere.
The principles of quantum computation: The state evolution,composition and measurement postulates. [slides (see section 3, 4 and 5)]
-
10 May 2021
Quantum gates. The circuit model. Two quantum communication protocols: Teleportations and dense coding. [slides]
-
17 May 2021
Quantum algorithms. The phase kick-back technique. The Deutsch-Joza algorithm. [slides]
Search problemas and the Grover algorithms. The phase amplification technique. [slides]
Exercise Sessions (TP - Tuesday, 16:00 - 18:00)
From 19 April onwards: room CP1 A5 (0.08)
-
23 Feb 2021 [Exercise Sheet 1]
Exercises on labelled transition systems.
-
2 Mar 2021
Exercises on bisimilarity (Exercise Sheet 1).
-
9 Mar 2021 [Exercise Sheet 2]
Exercises on process algebra - CCS combinators.
-
16 Mar 2021
Exercises on process algebra (conclusion)
-
23 Mar 2021 [Exercise Sheet 3]
Exercises on observation equivalence in CCS.
-
29 Mar 2021 (extra)
Demo class in mCRL2 [example] [template].
-
13 Abr 2021 (extra)
Exercises on process logic [Exercise Sheet 4].
-
20 Apr 2021
Exercises on the mathematical framework. Intuition for the quantum paradigm. [Slides] [Exercises]
-
27 Apr 2021
Create an account at IBM Q
and install Qiskit.
Introduction to Qiskit. [Notebook Jupyter]
-
04 May 2021
Quantum Information Protocols (Quantum Teleportation and Dense Coding).
Qiskit Aer - Simulation with noise.
[Notebook Jupyter]
-
11 May 2021
Deutsch-Jozsa Algorithm
IBM Q Provider
[Notebook Jupyter]
-
18 May 2021
Grover's Algorithm
Run in a quantum computer
IGNIS
[Notebook Jupyter]
-
24 May 2021
Discussing and clarifying the experimental assignment
Live session: Join
here!
-
01 Jun 2021
Discussing and clarifying the experimental assignment
Live session: Join
here!
Bibliography
Classical reactive processes
Basic
- 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]
Complementary
- 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
Quantum processes
Basic
- N. Yanofsky, M. Mannucci. Quantum Computing for Computer Scientists. CUP, 2008.
[book]
- E. Rieffel and W. Polak. Quantum Computing: A Gentle Introduction. MIT Press, 2011.
[book]
Complementary
- 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.
Links
News
Assignments
Pragmatics
Lecturers
Assessment
- Training assignment (60%): with oral discussion on 9 June
(with intermediate ckeckpoints)
- Individual assynchronous test (40%): 2 Problem Sets proposed along the T lectures
Contact
- 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 ana dot neri at quantalab dot uminho dot pt (Ana)
- Last update: 2021.06.29