Description:
Concurrent systems are commonplace. They cover a vast variety of systems ranging from mobile and reactive systems, security protocols, biological systems and multimedia interaction scenarios. This course introduces formal methods for reasoning about concurrent systems. We start by studying the typical problems related to processes that interact in a concurrent system (synchronization, atomicity, deadlock, etc). We present the most fundamental equivalence relation from concurrency theory (bisimulation) and its associated proof technique. Then, we introduce two of the most representative process calculi: the Calculus of Communicating Systems -CCS- and the Pi-Calculus. We also compare the expressiveness power of different fragments of process calculi. Finally, we shall see how (modal) logics can be used for the specification and verification of concurrent system.
Schedule:
Each session of 2h, starting form 08-jan-2018
S1(08/01) : Introduction: (concurrent vs sequential systems, shared variables, atomicity, etc).
S2(10/10) : Labelled transition systems (traces, bisimulation, weak bisimulation, etc)
S3(12/10) : CCS (syntax and semantics)
S4(15/10) : CCS (equivalences and expressiveness results)
S5(17/10) : Logics for processes (specification, verification, Hennessy–Milner logic).
S6(19/10) : The Pi-Calculus (syntax, semantics and theory)
S7(22/10) : The Pi-Calculus (equivalences)
S8(24/10) : The Pi-Calculus (subcalculi and expressiveness)
S9(26/10) : Linear logic: Processes as terms and processes as formulas
S10(29/10) : Declarative models of concurrency (CCP)
- D. Walker and D. Sangiorgi. The pi-calculis: A theory of mobile processes. Cambridge University Press, 2003.
- R. Milner. Communicating and Mobile Systems. Cambridge University Press, 1999.
- R. Milner. Communication and Concurrency. Prentice Hall, 1989
