Institute of Theoretical Computer Science

Lecture: Concurrency theory

Winter term 2017/18

News

January 24: We will give some overview over the material that is relevant for the oral exam during the final exercise class on Wednesday, January 31.
January 24: The final exercise sheet and the updated lecture notes are now available.
January 19: We have updated Exercise sheet 11, clarifying the meaning of the program in Exercise 2. (The program itself remains unchanged.)
January 16: Information on the oral exams can be found below.
January 10: The new exercise sheet is available! We will add the material on TSO to the lecture notes later.
December 21: The new exercise sheet is available! We wish all of you a Merry Christmas and a happy New Year!
December 13: The lecture and exercise classes for today are canceled!
November 09: Exercise-4, question 1c should read do you need labels on the edges. Also note that there is a modification to the question 2a.
October 20: There was a minor bug in the definition of the Ackermann function in Exercise 3 that we just have fixed.
October 18: The first exercise sheet and the lecture notes are now available.
October 9: The first lecture will take place on Tuesday, October 17, at 11:30 in room IZ 358.

Oral exams

We offer appointments for oral exams on February 20 and March 14. (If those are booked out, we will then use February 21 respectively March 13.)
To book an appointment, please write an email to Sebastian by February 7. It should contain the name of the lecture, the date, your full name, your student id ("Matrikelnummer"), and whether you want to do the exam in German or English. If you have any restrictions (e.g. only in the morning or in the afternoon) please also tell us. We will then send you a confirmation.
If you have three or more oral exam with us, we can also offer an appointment at the end of April (after April 23). This is usually not allowed, but it should be possible if we apply for it. Please contact us in advance.

Organisation

The lecture will be given by Dr. Prakash Saivasan and Sebastian Muskalla, supervised by Prof. Dr. Roland Meyer.
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:
- Wednesday, 16:45 - 18:15 in RR 58.4.

Lecture Notes

We offer lecture notes that will be updated during the term.

Lecture notes (last updated on February 2)

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

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 Sebastian or Prakash.

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.

Traditionally, the contents of this lecture change every year. True to this spirit, the syllabus of this year's lecture will overlap, but not be same, as the one of the past four iterations of the lecture.

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

You can find more details on these topics in the introduction of the lecture notes (to be uploaded soon).

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