Institute of Theoretical Computer Science

Lecture: Concurrency theory

Winter term 2018/19

News

December 2: There will be no lecture on Wednesday, December 5.
October 5: The first lecture will take place on Tuesday, ~~October 16~~ October 23, at 11:30 in room IZ 358.

Organisation

The lecture will be given by Prof. Dr. Roland Meyer and Elisabeth Neumann.
Entry in the list of lectures: Lecture, Exercises.
The dates for the lecture are:
- Tuesday, 11:30 - 13:00 in IZ 358,
- Wednesday, 11:30 - 13:00 in IZ 358,
The date for the exercise classes is:
- Thursday, 11:30 - 13:00 in IZ 358.

Lecture Notes

Lecture notes (last updated on March 25, 2018)

If you have questions or spot a bug in the notes, please contact Elisabeth.

Furthermore, there is material by Roland Meyer from past iterations of the lecture:

Exercises

The exercise sheets will be made available here. Please hand in your solution in groups of 2 to 3 people in the box next to room 343 in the Institute for Theoretical Computer Science, Muehlenpfordtstr. 23.

If you have questions or encounter problems with the exercises, please contact Elisabeth.

Module

Sucessfully finishing the module consists of two parts:

Prüfungsleistung: Oral exam after the lecture period.
Studienleistung: Get at least 60% of all points on your submitted solutions of the exercise sheets.

Description

The topic of the lecture is the verification of concurrent systems. We will study automata models for these systems (e.g Petri nets, WSTS, and distributed automata) and show how algorithmic problems for these models can be solved.

We plan to cover the following topics in detail:

Petri nets: Reachability and coverability
Well-structured transition systems
Distributed automata
Multi-pushdown automata
TSO - A weak memory model for x86

The following is the list of contents occording to the Modulhandbuch. The topics that we will cover in the lecture are a subset, see the description above.

Petri-nets
- Petri-nets as a model for concurrency
- Invariants, the marking equation
- Coverability, complexity results by Lipton and Rackoff, Karp & Miller coverability graph
- Reachability
- Unfoldings
- Restricted and extended variants of Petri nets
- Petri-net languages
Well-structured transition systems (WSTS)
- Well-quasi-orderings, upward- and downward-closures
- Abdulla's backwards search
- Geeraert's EEC algorithm
- Finkel's reachability tree
- Limits, forward coverability
- Lossy channel systems
- IC3 & IIC
Automata models for concurrent systems
- Automata with distributed alphabets
- Multi-pushdown systems
- Bounded context switching
Weak memory models
- Sequential consistency
- TSO, PSO, Power, C11
- Reachability under weak memory models
- Robustness
- Data races and DRF-free theorems
Reconfigurable networks and process algebra
- Calculus of communicating systems (CCS)
- Pi-calculus
- Boundedness in depth and breadth

Literature

The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.

L. Priese and H. Wimmel: Petri-Netze. Springer, 2003.
W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science - An EATCS Series, Springer, 1985.
P. H. Starke: Analyse von Petri-Netz-Modellen: Leitfäden und Monographien der Informatik, Teubner, 1990.
J. Esparza and S. Melzer: Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design, 2000. [PDF]
J. Esparza: Decidability and complexity of Petri net problems – an introduction: Lectures on Petri Nets I: Basic Models. Springer, 1998. [PDF]
J. Esparza and M. Nielsen: Decibility issues for Petri nets-a survey. Journal of Information Processing and Cybernetics EIK, 30(3):143-160, 1994. [PDF]
J. Esparza and K. Heljanko: Unfoldings. Monographs in Theoretical Computer Science - An EATCS Series, Springer, 2008. [PDF]
C. Rackoff: The covering and boundedness problems for vector addition systems. Theoretical Computer Science, Volume 6, issue 2, 1978. [Link]
C. Dufourd et al: Reset nets between decidability and undecidability. Automata, Languages and Programming, 1998. [PDF]
P. Jančar: Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, Volume 148, issue 2, 1995.
P. Jančar, J. Esparza, and F. Moller: Petri nets and regular processes. Journal of Computer and System Sciences, Volume 59, issue 3, 1999.
A. Finkel and Ph. Schnoebelen: Well-structured transition systems everywhere! Theoretical Computer Science, Volume 256, issue 1-2, 2001. [PDF]
C. ST. J. A. Nash-Williams. On well-quasi-ordering finite trees. Mathematical Proceedings of the Cambridge Philosophical Society, Cambridge Univsity Press, 1963. [PDF]
P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson: Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design, Volume 25, issue 1, 2004. [PDF]
A. Finkel and J. Goubault-Larrecq: Forward analysis for WSTS, part I: Completions. 26th International Symposium on Theoretical Aspects of Computer Science, 2009.
G. Geeraerts, J.-F. Raskin, L. Van Begin: Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2005.
P. Abdulla, A. Bouajjani, B. Jonsson: On-the-Fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc of the 10th International Conference on Computer Aided Verification, CAV, volume 1427 of LNCS, pages 305-318, Springer, 1998. [PDF]
A. Bouajjani, E. Derevenetc, R. Meyer: Checking and Enforcing Robustness against TSO. [PDF]
M. F. Atig, A. Bouajjani, S. Burckhardt, M. Musuvathi: On the Verification Problem for Weak Memory Models. [Link]
P. A. Abdulla, M. F. Atig, Y.-F. Chen, C. Leonardsson, A. Rezine: Counter-Example Guided Fence Insertion under Weak Memory Models. [PDF]
M. F. Atig, A. Bouajjani, G. Parlato: Getting Rid of Store-Buffers in TSO Analysis. [PDF]
R. Milner: Communicating and mobile systems: the pi-calculus. Cambridge University Press, 1999.
D. Sangiorgi, D. Walker: Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.
R. Meyer: On boundedness in depth in the π-calculus. Fifth IFIP International Conference On Theoretical Computer Science, 2008.
R. Meyer: Structural Stationarity in the pi-Calculus. PhD thesis, Department of Computing Science, University of Oldenburg, 2008. [PDF] [Slides]
T. Wies, D. Zufferey, and T. Henzinger: Forward analysis of depth-bounded processes. FoSSaCS, 2010.
E. D'Osualdo, C.H.-L. Ong: On Hierarchical Communication Topologies in the pi-calculus. Programming Languages and Systems: ESOP, 2016.
M. Mukund: Automata on Distributed Alphabets. Modern Applications of Automata Theory, 2012.
P. Saivasan: Analysis of Automata-theoretic models of Concurrent Recursive Programs. PhD thesis, Chennai Mathematical Institute, 2016.

Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig