Introduction to "Interaction and Concurrency" and the course dynamics. Labelled transition systems. Morphisms between transition systems.
Conclusion of the previous lecture: Notions of equivalence between labelled transition systems. Notions of trace, simulation and bisimulation. Bisimilarity.
Specification of reactive systems with process algebras. Introduction to CCS: motivation, examples.
CCS process combinators: syntax, semantics.
The calculus of (strict) bisimilarity. The expansion theorem. Introduction to observational equivalences.
Specification of process properties. Brief introduction to modal logic. The Hennessy-Milner logic for processes. [slides]
Semantics and proof system for the Hennessy-Milner logic. Bisimulation and modal equivalence. The Hennessy-Milner theorem. Going "temporal": modalities indexd by regular expressions.
Introduction to quantum processes. [slides] Notion of a qubit. Computing with qubits. Illustration: the Deutsch algorithm. [slides]
The principles of quantum computation: Quantum states and computation. [slides]
Quantum gates and the circuit model. The principles of quantum computation: Compositionality. [slides (from the previous lecture)]
Quantum algorithms. The phase kick-back technique. The Deutsch-Joza algorithm. [slides]
Search problemas and the Grover algorithm. The phase amplification technique. [slides]
Quantum communication protocols: teleportation and superdense conding. [slides]
F
Exercises on labelled transition systems and bisimilarity.
Exercises on process algebra - CCS combinators.
Exercises on process algebra - strict and observational equivalence calculi.
Exercises on process algebra - observational equivalence and process equality.
Exercises on process logic [Exercise Sheet 5].
Introduction to Quantum Computing using Qiskit [Jupyter Notebook].
Deutsch's algorithm [Jupyter Notebook].
Grover's algorithm [Jupyter Notebook].
Grover's algorithm [Jupyter Notebook].