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

COURSE 2.8.1

Non-Sequential Theory of Distributed Systems

Lecturers

* Benedikt Bollig (responsible)

* Paul Gastin

Dates

The lectures will take place on Friday, 16:15 - 17:45, in Bat. Sophie Germain, room 1014. The first lecture is on September 18.

Description

The lecture shall cover basic automata-theoretic concepts and logical formalisms for the modeling and verification of concurrent and distributed systems. Many of these concepts naturally extend the classical automata and logics over words, which provide a framework for modeling sequential systems. A distributed system, on the other hand, combines several (finite or recursive) processes, and will therefore be modeled as a collection of (finite or pushdown, respectively) automata. A crucial parameter of a distributed system is the kind of interaction that is allowed between processes. In this lecture, we focus on two standard communication paradigms: message passing and shared memory. In general, communication in a distributed system creates complex dependencies between events, which are hidden when using a sequential, operational semantics.

The approach taken in this lecture is based on a faithful preservation of the dependencies of concurrent events. That is, an execution of a system is modeled as a partial order, or graph, rather than a sequence of events. This has to be reflected in high-level languages for formulating requirements to be met by a distributed system. Actually, specifications for distributed systems are, by nature, non-sequential. They should be interpreted directly on the partial order underlying a system execution, rather than on an (arbitrary) linearization of it. It is worth mentioning that using specifications working on linearizations are often the reason for undecidability, as they may assume synchronization that actually cannot happen. We present classical specification formalisms such as monadic second-order (MSO) logic and temporal logic, interpreted over partial-orders or graphs, as well as (high-level) rational expressions. We compare the expressive power of automata and logic and give translations of specifications into automata (synthesis and realizability). Moreover, we consider the satisfiability (Is a given specification consistent?) and the model-checking problem (Does a given distributed system satisfy its specification?). For both problems, we present elementary techniques (based on tree interpretations and tree automata) that yield decision procedures with optimal complexity.

Outline of the course

Lecture Date Contents
1st 18/09/2020 Introduction and motivating examples
2nd 25/09/2020 Automata models of concurrent processes with data structures; operational semantics
3rd 02/10/2020 graph semantics; MSO logic; expressive power of MSO logic
4th 09/10/2020 Expressive power of MSO logic; from CPDS to MSO logic
5th 16/10/2020 MSO logic is, in general, strictly more expressive than CPDS
6th 23/10/2020 Underapproximate verification; co-graphs and tree interpretation
7th 30/10/2020 Special tree-width, decomposition game, examples
8th 06/11/2020 Special tree-width, decomposition game, examples
9th 13/11/2020 Special tree-width and tree interpretation; decision procedures via MSO
10th 20/11/2020 Exercises
11th 11/12/2020 Propositional dynamic logic (PDL), syntax, semantics, examples
12th 18/12/2020 EQ-ICPDL, syntax, semantics, examples, from CPDS to EQ-PDL, undecidability
13th 08/01/2021 Underapproximate verification for ICPDL (1)
14th 15/01/2021 Underapproximate verification for ICPDL (2)
15th 22/01/2021 Synthesis of CPDS from PDL formulas (1)
29/01/2021 Synthesis of CPDS from PDL formulas (2)
05/02/2021 No lecture
12/02/2021 Asynchronous automata
Exercises

Lecture Notes

Slides of 1st lecture

Lecture Notes (version as of December 12, 2020)

Prerequisites

Basic knowledge in Automata, Logics, Complexity.

While not mandatory, it is useful to know the basics of verification. See for instance the level 1 course 1-22 Basics of verification which can also be taken during M2.

Language

Benedikt Bollig will lecture in English. Paul Gastin will lecture in French, unless some students request English.

Exam will be available in English (also in French upon request) and could be written in either French or English.

Related Courses

  • 2-3 Concurrency
  • 2-8-2 Foundations of real time and hybrid systems
  • 2-9-1 Mathematical foundations of the theory of infinite transition systems
  • 2-9-2 Algorithmic verification of programs
  • 2-16 Finite automata modelling
  • 2-20-1 Game theory techniques in computer science
  • 2-20-2 Mathematical foundations of automata theory

References

 
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