Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Concurrency (48h, 6 ECTS)

Course directors: Roberto Amadio and Catuscia Palamidessi

Teachers for 2012-2013

  1. Roberto Amadio (12h)
  2. Daniele Varacca (12h)
  3. Kostas Chatzikokolakis (12h)
  4. Emmanuel Haucourt (12h)

Goals

This course introduces formal methods for reasoning about properties of concurrent and probabilistic systems.

Plan of the course

The course is organised in 20 lectures. The course is `breakable'. This means that you get 3 credits if you pass only the first part (up to the mid-term exam) or the second part (after the mid-term) and 6 credits if you pass both. Notice that the grade we consider to give 6 credits is the average of the grades of the first and second part. For instance, if your grade is 12/20 in one part and 8/20 in the other you get 6 credits.

  • Introduction (Amadio, 1h)
  • Basic models of concurrent systems (Amadio, 11h)
    • A shared variable parallel language. Compositional trace model and compositional reasoninig.
    • Labelled transition systems. Proof techniques. The trace-bisimulation spectrum and the related modal logics.
    • CCS a calculus of communicating systems. Characterisation of labelled bisimulation.
    • Notion of determinacy. Synchronous/timed models: the example of TCCS.
  • The pi-calculus (Varacca, 12h)
    • Syntax and reduction semantics.Observational equivalences. Labelled semantics and bisimulations.
    • Fragments of pi: asynchronous, local, internal, and others.
    • Functions as processes: compiling lambda into pi.
    • Types and subtyping. Typed functions as typed processes.
    • Other approaches to mobility
  • Probabilistic models and applications (Chatzikokolakis, 12h)
    • Probabilistic asyncronous pi calculus
    • Semantics based on simple probabilistic automata
    • Probabilistic bisimulation (maybe also testing equivalence)
    • Expressiveness: role of randomization in the encoding of the pi-calculus into the asynchronous fragment
    • Introduction to probabilistic model checking and PRISM
    • Verification of anonymity protocols: Dining Cryptographers, Crowds
  • Directed Algebraic Topology and Concurrency (Haucourt, 12h)
    • DijkstraPV language
    • Control-flow graph
    • Category of paths on a graph
    • Partially ordered spaces
    • Fundamental category in a partially ordered space
    • Seifert and van Kampen theorem for the fundamental category
    • Category of components
    • Factorisation of small, finite, connected, loopless categories
    • Some other topological models

French and English

Lectures are given in English if a non-French speaking student asks for it. The lecture notes and the text of the examinations are in English. The students may answer in French or English.

Material

The lecture notes will be available on line.

Related courses

2.1, 2.2, 2.4, 2.17.1, 2.18.2, 2.31.1

Prerequisites

It is useful, though not strictly necessary, to have attended the courses 1-15 (Semantics), 1-16 (Concurrency), and 1-20 (Categories).

Bibliography (following the order of the lectures)

  • Apt, R. and Olderog, E. Verification of sequential and concurrent programs. Springer-Verlag. 1997.
  • Brookes, S. Full Abstraction for a Shared-Variable Parallel Language. Inf. Comput. 127(2): 145-163, 1996.
  • Milner, R. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
  • Milner, R. The pi-calculus. Cambridge University Press, 2001.
  • Sangiorgi, D. and Walker, D. The pi-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.
  • Jonsson, B., Larsen, K. and W., Wang Yi. Probabilistic Extensions of Process Algebras. Handbook of Process Algebra. 2001.
  • Panangaden, P. Labelled Markov Processes. Imperial College Press. 2009.
  • Gunawardena, J. Homotopy and Concurrency. Bulletin EATCS, 54, 184-193. 1994.
  • Goubault, E. Geometry and concurrency: a user's guide. Mathematical Structures in Computer Science 10(4): 411-425 (2000).
  • Nachbin, L . Topology and Order. Van Nostrand Reinhold. 1965.
  • Higgins, P.J. Categories and Groupoids. Van Nostrand Reinhold. 1971 TAC reprints version

Possible teachers

R. AmadioUniv. Paris DiderotPPS
K. ChatzikokolakisINRIALIX
E. GoubaultCEA LIST Saclay
E. HaucourtCEA LIST Saclay
J.-J. LévyINRIARocquencourt
J. LeiferINRIARocquencourt
C. PalamidessiINRIALIX
F. ValenciaCNRSLIX
D. VaraccaUniv. Paris DiderotPPS

Calendar

Date Speaker Course documents
20 Sep Amadio Lecture notes
27 Sep Amadio
4 Oct Amadio
11 Oct Amadio
18 Oct Amadio
25 Oct Varacca Pi-calculus - Semantics and equivalences:Slides
8 Nov Varacca Fragments of the Pi-calculus: Slides
15 Nov Varacca Functions as Processes - Types: Slides
22 Nov Varacca More on types: Slides - A paper - Exercice Session
29 Nov Varacca Event structures, causality: Slides - Milner's original syntax
6 Dec Mid-term exam First-part with correction
13 Dec Chatzikokolakis Slides
20 Dec Chatzikokolakis Slides
10 Jan Chatzikokolakis Slides
17 Jan Chatzikokolakis Slides
24 Jan Chatzikokolakis Slides, Prism files, Last year's exam
31 Jan Haucourt Notes de cours (pdf) / Lecture notes (pdf)
7 Feb Haucourt
14 Feb Haucourt
21 Feb Haucourt
28 Feb Haucourt
14 Mar Final exam
* Previous years *
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA