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 proficient in 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.
• Logics for reactive systems:
  • Hennessy-Milner logic and its extensions.
  • Modal equivalence and bisimilarity.
  • Specification and verification of logic constraints.
• Tool support - Modelling and verification in mCRL2

Quantum Systems

• Fundamentals
  • Introduction to quantum information and computation.
  • Mathematical background: Hilbert spaces.
  • The Dirac notation.
• Quantum systems
  • 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 (2019-20)

T Lectures

• Feb 4 (T1): Introduction to Interaction and Concurrency and the course dynamics.

  Labelled transition systems. Morphisms between trarnsition systems. The relational and coalgebraic perspectives.

• Feb 11 (T2): Notions of equivalence between labelled transition systems. Notions of trace, simulation and bisimulation. Bisimilarity.

• Feb 18 (T3): Introducation to process algebra. Milner's calculus of communicating systems (CCS): motivation, syntax, operational semantics. Examples.

• Feb 25: CARNIVAL

• Mar 3 (T4): Weak bisimilarity. Observational equivalence and observational congruence. Laws of the weak process calculus.

• Mar 10: CANCELLED: Covid-19 preventive determination

• Mar 17 (T5): (Non presencial lecture) Introduction to mCRL2 as a process modeling tool.

  Lecture support: Modelling processes in mCRL2 (slides)
  Lecture support: Hands-on Lab session (pdf) and initial file (mCRL2)
  Live session 1: Join here!

• Mar 24 (T6): (Non presencial lecture) Modal logics for processes. The logic of Hennessy-Milner.

  Lecture support: Hennessy-Milner Logic (slides)
  Live session 3: Join here!

• Mar 31 (T7): (Non presencial lecture) Modal logics for processes: Examples and exercises.

  Lecture support: Hennessy-Milner Logic Exercises
  Live session 4 (on colibri.zoom.us) : Join here!

• Apr 14 (T8): (Non presencial lecture) Expressing temporal properties. Safety and liveness. Introduction to the modal Mu-calculus.

  Lecture support: The modal Mu-calculus (slides)
  Live session 6: Join here!

• Apr 21 (T9): (Non presencial lecture) The modal Mu-calculus: examples and exercises.

  Lecture support: Exercise sheet 6 (pdf)
  Live session 8: Join here! (zoom)

• Apr 28 (T10): (Non presencial lecture) Quantum data and actions. Introduction to the underlying mathematical framework. Hilbert spaces. Data representation and operators.

  Lecture support: The mathematical framework (pdf)
  Live session 10: Join here!

• Mai 5 (T11): (Non presencial lecture) Quantum systems. Postulates: state space, evolution and composition. Entanglement.

  Lecture support: The principles (pdf)
  Live session 12: Join here!

• May 12 (T12): (Non presencial lecture) The measurement postulate. Quantum gates and the circuit model. Application: the teleportation and dense coding protocols.

  Lecture support: Quantum gates and the circuit model (pdf)
  Live session 14: Join here!

• May 19 (T13): (Non presencial lecture) Introduction to quantum algorithms. The algorithms of Deutsch and Deutsch-Josza. Phase kick-back as an algorithmic technique.

  Lecture support: Quantum algorithms (pdf)
  Live session 16: Join here!

• May 26 (T14): (Non presencial lecture) Quantum search algorithms: Grover's algorithm. The technique of amplitude amplification. Closing remarks on quantum systems and the IC course.

  Lecture support: Quantum search algorithms (pdf)
  Live session 18: Join here!

• June 9 (T15): Written test

TP Lectures

• Feb 6 (TP1): Exercise sheet 1.

• Feb 13 (TP2): Exercise sheet 2.

• Feb 20 (TP3): Exercise sheet 3.

• Feb 27 (TP4): Expositive lecture (given the Carnival pause on the 25th): Process calculus: equational laws; the expansion theorem and its applications.

• Mar 5: CANCELLED: Lecturer in UM mission

• Mar 12: CANCELLED: Covid-19 preventive determination

• Mar 19 (TP5): (Non presencial lecture) Exercise sheet 4.

  Lecture support: Exercise sheet 4 (pdf)
  Lecture support: Exercise 6 (solution) (pdf)
  Live session 2: Join here!

• Mar 26: CANCELLED

• Apr 2 (TP6): (Non presencial lecture) Hennessy-Milner logic (conclusion). Exercise sheet 5.

  Lecture support: Exercise sheet 5 (pdf)
  Live session 5: Join here! (check the meeting id at your academic mailbox)

• Apr 16 (TP7): (Non presencial lecture) Modal Mu-calculus: case-studies.

  Lecture support: Slides from the previous T and Lecture Notes on Process Logic (pdf)
  Live session 7: Join here!

• Apr 23 (TP8): (Non presencial lecture) Quantum systems: motivation and introduction. Notion of qubit. Representation in the Bloch sphere.

  Lecture support: Introduction to quantum systems (slides)
  Live session 9: Join here! (zoom)

• Apr 30 (TP9): (Non presencial lecture) Exercises on the mathematical framework. Intuition for the quantum paradigm.

  Lecture support: Exercises and slides with solution
  Live session 11: Join here!

• Mai 7 (TP10): (Non presencial lecture) Introduction to Qiskit.

  Lecture support: About Qiskit, Demo, Exercises
  Live session 13: Join here!

• Mai 14 (TP11): (Non presencial lecture) Quantum Information Protocols (Quantum Teleportation and Dense Coding). Qiskit Aer - Simulation with noise.

  Lecture support: Exercises (Basics overview), Teleportation Protocol and Simulation with Noise, Exercises (Dense Coding)
  Live session 15: Join here!

• Mai 21 (TP12): (Non presencial lecture) Quantum Algorithms (Deutsch-Jotsza Algorithm). Qiskit Providers - Run in a quantum device.

  Lecture support: Tutorial, Exercises
  Live session 17: Join here!

• May 28 (TP13): (Non presencial lecture) Grover Algorithm. Qiskit Ignis - Noise mitigation

  Lecture support: Tutorial
  Live session 19: Join here!

• June 4: (TP14) (Non presencial lecture) Doubts clarification

  Live session 20: Join here!

• June 11: (TP15):

Support

Slides (2019-20)

• Labelled Transition Systems 1
• Labelled Transition Systems 2
• Process Algebra 1
• Process Algebra 2
• Modelling processes in mCRL2
• Hennessy-Milner Logic
• The modal Mu-calculus
• Lecture Notes on Process Logic
• Introduction to quantum systems
• The mathematical framework
• The principles of quantum computation
• Quantum gates and the circuit model
• Quantum algorithms (Deutsch-Josza)
• Quantum algorithms (Grover)

Practice (Exercises and Jupyter Notebooks)

• Exercises 1
• Exercises 2
• Exercises 3
• Exercises 4
• Exercises 5
• Exercises 6
• Exercises 7
• The mathematical framework TP
• Exercises 8 - Basics (Jupyter Notebook)
• About Qiskit (Jupyter Notebook)
• My First Quantum Program (Jupyter Notebook)
• Exercises 9 - Basics overview (Jupyter Notebook)
• Teleportation Protocol and Simulation with Noise (Jupyter Notebook)
• Exercises 10 - Dense Coding (Jupyter Notebook)
• Deutsch-Jotsza Algorithm and Qiskit Providers (Jupyter Notebook)
• Exercises 11 - Deutsch-Jotsza (Jupyter Notebook)
• Grover Algorithm and Qiskit Ignis (Jupyter Notebook)

Assignments

• TP 1 (deadline: 20 May)
• Note on TP1 in mCRL2
• TP 2 (deadline: 21 June)
• Grupos
• Horários para a defesa dos trabalhos
• Test with solutions NEW

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

Bibliography: 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

• mCRL2 website
• Qiskit website
• Arca website

News

May 24: Some references for the quantum systems module NEW

• Introductory text on quantum computation, covering essentially the topics discussed in the lectures, although sometimes with a different focus and notation.
• Quantum algorithms implementations for beginners a recent, systematic survey paper, a bit terse, but with implementation schemes in Qiskit.
• John Preskill 2017 paper on current NISQ technology --- very important reading to complement the stuff covered in the lectures.

Mar 16: Going virtual (from 16th March ...)

• Para cada aula será disponibilizado antecipadamente nesta página o material de suporte necessário que deverá ser estudado individualmente por cada um.
• No horário previsto para cada aula haverá uma sessão “live” que permitirá alguma sincronização à distância onde tentarei apresentar um sumário da matéria e responder às vossas questões. A duração da sessão será ajustada às necessidades de interacção, não excedendo o tempo regulamentar. Utilizaremos para isso a plataforma Blackboard Collaborate Ultra disponibilizada pela Universidade. O link para cada sessão estará anunciado nesta página.
• Para colmatar as dificuldades de comunicação síncrona (nomeadamente a ausência de um quadro onde escrever), estarei disponível para esclarecer qualquer dúvida de forma assíncrona.
• Ajuste dos instrumentos de avaliação
  • Trabalhos práticos individuais ou em grupo de 2 elementos passam a contar 40% (20% cada) da classificação final.
  • Substituição do teste presencial por uma avaliação individual composta por teste assíncrono se necessário complementado por uma oral (que incidirá igualmente sobre os trabalhos práticos).
  • Consultar nova calendarização abaixo.

Pragmatics

Lecturers

• Coordinator: Luís Soares Barbosa
• Teaching Assistant: Ana Neri

Assessment NEW

• Training assignment 1 (20%; published: 17 April): final report due: 24 May 2020.
• Training assignment 2 (20%; published: 22 May): final report due: 21 June 2020.
• Individual assignment (60%; 20 June, 9.30h).
• Oral discussion training assigments: week 25-26 June.

Contact

• Appointments: Tue, 08:00-09:00 and Thu, 18:00-20:00 (please send an email the day before)
• Email: lsb at di dot uminho dot pt
• Last update: 2020.07.08