* Benedikt Bollig

The lectures will take place on Wednesday, 12:45 - 14:15, in Bat. Sophie Germain, Room 1004. The first lecture is on September 15, 2021.

The exam will take place on March 2, 12:45 - 14:15, in Bat. Sophie Germain, Room 1004.

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.

Slides of 1st lecture

Lecture Notes

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.

The lecture is given in English.

• 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

• C. Aiswarya and P. Gastin. Reasoning about distributed systems: WYSIWYG. FSTTCS'14, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, December 2014. To appear.
• C. Aiswarya, P. Gastin et K. Narayan Kumar. Verifying Communicating Multi-pushdown Systems via Split-width. ATVA'14, Lecture Notes in Computer Science 8837. Springer, 2014. To appear.
• B. Bollig, D. Kuske, and I. Meinecke: Propositional Dynamic Logic for Message-Passing Systems. Logical Methods in Computer Science 6(3) (2010).
• B. Bollig and M. Leucker. Message-passing automata are expressively equivalent to EMSO logic. Theoretical Computer Science 358(2-3): 150-172 (2006).
• A. Cyriac. Verification of Communicating Recursive Programs via Split-width. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2014.
• A. Cyriac, P. Gastin, and K. Narayan Kumar. MSO Decidability of Multi-Pushdown Systems via Split-Width. CONCUR'12, Lecture Notes in Computer Science 7454, pages 547-561. Springer, 2012.
• A. Cyriac, P. Gastin and K. Narayan Kumar. Controllers for the Verification of Communicating Multi-Pushdown Systems. CONCUR'14, Lecture Notes in Computer Science 8704, pages 297-311. Springer, 2014.
• B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Information and Computation 204, pages 920-956. 2006
• J. G. Henriksen, M. Mukund, K. Narayan Kumar, M. A. Sohoni, P. S. Thiagarajan: A theory of regular MSC languages. Information and Computation 202(1): 1-38 (2005).
• M. Mukund, K. Narayan Kumar, and M. A. Sohoni. Bounded time-stamping in message-passing systems. Theoretical Computer Science, Volume 290, Issue 1, pages 221–239. 2003.
• B. Courcelle and J. Engelfriet. Graph structure and monadic second-order logic, a language theoretic approach. Cambridge University Press. 2012.