Concurrency Theory 2016/2017
- 23 Feb: minor update to page 3, notes on LCS
- 22 Feb: minor update to page 4, notes on LCS (? instead of ! in definition of ⊕)
- 21 Feb: minor update to page 34, notes on π‑calculus
- 20 Feb: updated notes on
- 10 Feb: uploaded full notes on π‑calculus
- 6 Feb: uploaded notes on Process Algebra and CCS (10 Feb darker scan)
- Dates of the exams announced
- 3 Feb: updated and expanded notes on Bisimulation
- 3 Feb: minor update to notes on Coverability for WSTS
The lecture will be given (in English) by Emanuele D'Osualdo.
The dates and rooms of the lecture are:
- Mondays, 11:45 - 13:15, room 48-453.
- Wednesdays, 10:00 - 11:30, room 48-453.
The tutorials will be held in room 48-453 on Thursdays at 17:15.
The tutors are Matthias Lederer and Thomas Schneider.
- Published on this page on Thursdays in the morning
- Solutions due the following Wednesday morning
- Please hand in solutions in groups of 2 to 3 people
- The mailbox is in the staircase between buildings 34 and 36, 4th floor, close to the SofTech AG
There will be an oral exam, given by Emanuele D'Osualdo.
To be admitted, you have to fulfil the following requirements:
- 60 percent of your exercises have to be marked by a plus (useful answer).
- You have to present some of your exercise solutions on the board.
The available dates for the exam are
23rd, 24th and 27th February 2017.
Please contact Matthias Lederer
for booking a slot for your exam.
- Week 1:
lec. notes §1.1, §2.1
- Overview of the course
- Basic Petri Nets definitions
- Week 2:
lec. notes §2
- Petri Nets Invariants and Traps
- Sound, Incomplete Verification using Linear Programming
- Week 3:
- Week 4:
- Week 5:
lec. notes §6.1, §6.3
- Well-quasi-order characterisations
- Constructing wqos
- Week 6:
- Week 7:
- Backwards Search for Coverability in WSTS
see also this paper
- Ideal Completions and Forwards Coverability
- Week 8:
- Ideal Completions for Well Quasi Orders
- Simple Regular Languages, Forwards Coverability for LCS
- Week 9:
most material is from this book
- Week 10:
most material is from this book
- CCS, Structural Congruence, Reaction semantics
- Labelled Transition semantics, Strong and Weak Bisimulation
- Week 11:
- Algebraic Laws of Bisimulation
- Decidability of Bisimulation
- Week 12:
- The π‑calculus, Reaction semantics
- Communication Topologies and Mobility
- Week 13:
- Bisimulation and Full Bisimulation in the π‑calculus
- Term embedding and the notion of Depth
- Week 14:
- The wqo of processes with depth at most k
- Coverability for depth-bounded processes
The overall theme is automatic verification of models of concurrent computation.
A list of topics:
- Petri Nets as models of concurrency
- The marking equation
- (Forwards) Coverability
- Complexity bounds on coverability
- Reachability and variants of Petri Nets
Well-Structured Transition Systems
- Abdulla's backwards search
- Adequate domains of limits and forward coverability
- Applications to Petri Nets and Lossy Channels Systems
- Calculus of Communicating Systems (CCS)
- The π‑calculus
- Boundedness in breadth and depth
- Coverability and Termination for Depth-bounded terms
Notes and Additional Material
Here you can find an up-to-date list of notes for the course.
There might be typos, the date of the last update is indicated for each document.
Lecture notes from the past years, by Roland Mayer
Handwritten notes for this year:
Rackoff's proof by R. Meyer (17 Nov 2016)
Reachability for Petri Nets (02 Dec 2016)
Well-Quasi-Orderings (20 Feb 2017)
Well Structured Transition Systems (12 Jan 2017)
Coverability for WSTS (20 Feb 2017)
Lossy Channel Systems (22 Feb 2017)
Bisimulations and decidability issues (03 Feb 2017)
Process Algebra: CCS (06 Feb 2017)
Process Algebra: π‑calculus (21 Feb 2017)
Additional material can be found in published research papers:
- L. Priese and H. Wimmel.
Petri-Netze. Springer-Verlag, 2003.
- W. Reisig.
Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 1985.
- R. Milner.
Communicating and mobile systems: the π‑calculus.
Cambridge University Press, 1999.
- D. Sangiorgi, D. Walker
Pi-Calculus: A Theory of Mobile Processes.
Cambridge University Press, 2001.
- J. Esparza and S. Melzer. 2000
Verification of Safety Properties Using Integer Programming: Beyond the State Equation.
Formal Methods in System Design.
- J. Esparza. 1998
Decidability and complexity of Petri net problems – an introduction.
Lectures on Petri Nets I: Basic Models. Springer.
- C. Rackoff. 1978
The covering and boundedness problems for vector addition systems.
Theoretical Computer Science. Volume 6, issue 2.
- C. Dufourd et al. 1998.
Reset nets between decidability and undecidability.
Automata, Languages and Programming.
- C. ST. J. A. Nash-Williams. 1963.
On well-quasi-ordering finite trees.
In Mathematical Proceedings of the Cambridge Philosophical Society. Cambridge Univ Press.
- A. Finkel and P. Schnoebelen. 2001
Well-structured transition systems everywhere!
Theoretical Computer Science. Volume 256, issue 1-2.
- P. A. Abdulla Collomb-A. Annichini A. Bouajjani and B. Jonsson. 2004
Using forward reachability analysis for verification of lossy channel systems.
Formal Methods in System Design. Volume 25, issue 1.
- A. Finkel and Goubault-J. Larrecq. 2009
Forward analysis for WSTS, part I: Completions.
26th International Symposium on Theoretical Aspects of Computer Science.
- P. Jančar, 1995.
Undecidability of bisimilarity for Petri nets and some related problems.
Theoretical Computer Science. Volume 148, issue 2.
- Petr Jančar, Javier Esparza, and Faron Moller, 1999.
Petri nets and regular processes.
Journal of Computer and System Sciences. Volume 59, issue 3.
- R. Meyer. 2008.
On boundedness in depth in the π‑calculus.
Fifth IFIP International Conference On Theoretical Computer Science.
- T. Wies, D. Zufferey, and T. Henzinger. 2010.
Forward analysis of depth-bounded processes.
- E. D'Osualdo, C.H.-L. Ong. 2016.
On Hierarchical Communication Topologies in the pi-calculus.
Programming Languages and Systems: ESOP 2016.