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

Feb 6:
Exercise sheet 1.

Feb 13:
Exercise sheet 2.

Feb 20:
Exercise sheet 3.

Feb 27:
(tba)

Mar 5:
(tba)

Mar 12:
(tba)

Mar 19:
(tba)

Mar 26:
(tba)

Apr 2:
Handson practice in mCRL2.

Apr 16:
(tba)

Apr 23:
(tba)

Apr 30:
(tba)

Mai 7:
(tba)

Mai 21:
(tba)

May 28:
TP discussion and presentation.
Support
Slides (201920)
Exercises
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
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
Pragmatics
Lecturers
Assessment
 Training assignment 1 (15%): final report expected by 2 May 2020.
 Training assignment 2 (15%): final report expected by 5 June 2020.
 Written test (70%): 26 May 2020, 09:0011:00.
Contact
 Appointments: Tue, 08:0009:00 and Thu, 18:0020:00 (please send an email the day before)
 Email: lsb at di dot uminho dot pt
 Last update: 2020.02.16