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:
 HennessyMilner 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
 Timeevolutions 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 DeutschJozsa and Simon algorithms.
 Algorithms based on amplitude amplification.
 Tool support  Quantum modelling and programming in Qiskit.
Summaries (202021)
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 HennessyMilner 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 kickback technique. The DeutschJoza 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
DeutschJozsa 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, JoostPieter 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:0020:00 and Fri, 18:0020:00 (please send an email the day before)
 Appointments  Ana: Wed, 17:0019: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.09