Theoretical Computer Science

Concurrency Theory 2016/2017

News

• 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
  • wqo (material added, Higman and subword)
  • Coverability for WSTS there was a missing page!
  • Lossy Channel Systems there was a missing page!
• 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

Organisation

• 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.
• Exercise sheets:
  • 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.

Log

• Week 1: lec. notes §1.1, §2.1
  • Overview of the course
  • Basic Petri Nets definitions
• Week 2: lec. notes §2 this paper
  • Petri Nets Invariants and Traps
  • Sound, Incomplete Verification using Linear Programming
• Week 3:
  • Decidability of Boundedness for Petri Nets lec. notes §1.2
  • Karp & Miller Coverability Graphs lec. notes §4
• Week 4:
  • Lipton's lower bound on Petri Net coverability this paper §7
  • Rackoff's upper bound on Petri Net coverability notes the original paper
• Week 5: lec. notes §6.1, §6.3 notes
  • Well-quasi-order characterisations
  • Constructing wqos
• Week 6:
  • Invariants and Reachability in Petri nets notes other notes
  • Variants of Petri Nets this paper
  • Lossy Channel Systems lec. notes §5 notes
  • WSTS and the Finite Reachability Tree notes
• Week 7: notes
  • Backwards Search for Coverability in WSTS see also this paper
  • Ideal Completions and Forwards Coverability
• Week 8:
  • Ideal Completions for Well Quasi Orders notes
  • Simple Regular Languages, Forwards Coverability for LCS notes
• Week 9: notes most material is from this book
  • LTS, Simulations and Bisimulations also these notes
  • Calculus of Communicating Systems notes
• Week 10: notes p.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 notes p.22
  • Decidability of Bisimulation notes
• Week 12: notes
  • The π‑calculus, Reaction semantics
  • Communication Topologies and Mobility
• Week 13: notes p.44
  • Bisimulation and Full Bisimulation in the π‑calculus
  • Term embedding and the notion of Depth
• Week 14: notes p.49
  • The wqo of processes with depth at most k
  • Coverability for depth-bounded processes

Exercises

• Exercise Sheet 1
• Exercise Sheet 2
• Exercise Sheet 3
• Exercise Sheet 4
• Exercise Sheet 5
• Exercise Sheet 6
• Exercise Sheet 7
• Exercise Sheet 8
• Exercise Sheet 9
  
• Exercise Sheet 10
• Exercise Sheet 11
• Exercise Sheet 12
• Exercise Sheet 13

Topics

• Petri Nets
  • Petri Nets as models of concurrency
  • Invariants
  • The marking equation
  • (Forwards) Coverability
  • Complexity bounds on coverability
  • Reachability and variants of Petri Nets
• Well-Structured Transition Systems
  • Well-quasi-orders
  • Termination
  • Abdulla's backwards search
  • Adequate domains of limits and forward coverability
  • Applications to Petri Nets and Lossy Channels Systems
• Process Algebra
  • Calculus of Communicating Systems (CCS)
  • Bisimulations
  • The π‑calculus
  • Boundedness in breadth and depth
  • Coverability and Termination for Depth-bounded terms

Notes and Additional Material

• Lecture notes from the past years, by Roland Mayer PDF
• Handwritten notes for this year:
  1. Rackoff's proof by R. Meyer (17 Nov 2016) PDF
  2. Reachability for Petri Nets (02 Dec 2016) PDF
  3. Well-Quasi-Orderings (20 Feb 2017) PDF
  4. Well Structured Transition Systems (12 Jan 2017) PDF
  5. Coverability for WSTS (20 Feb 2017) PDF
  6. Lossy Channel Systems (22 Feb 2017) PDF
  7. Bisimulations and decidability issues (03 Feb 2017) PDF
  8. Process Algebra: CCS (06 Feb 2017) PDF
  9. Process Algebra: π‑calculus (21 Feb 2017) PDF

1. L. Priese and H. Wimmel. Petri-Netze. Springer-Verlag, 2003.
2. W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 1985.
3. R. Milner. Communicating and mobile systems: the π‑calculus. Cambridge University Press, 1999.
4. D. Sangiorgi, D. Walker Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.

1. J. Esparza and S. Melzer. 2000 PDF
   Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design.
2. J. Esparza. 1998 PDF
   Decidability and complexity of Petri net problems – an introduction. Lectures on Petri Nets I: Basic Models. Springer.
3. C. Rackoff. 1978 LINK
   The covering and boundedness problems for vector addition systems. Theoretical Computer Science. Volume 6, issue 2.
4. C. Dufourd et al. 1998. PDF
   Reset nets between decidability and undecidability. Automata, Languages and Programming.
5. C. ST. J. A. Nash-Williams. 1963. PDF
   On well-quasi-ordering finite trees. In Mathematical Proceedings of the Cambridge Philosophical Society. Cambridge Univ Press.
6. A. Finkel and P. Schnoebelen. 2001 PDF
   Well-structured transition systems everywhere! Theoretical Computer Science. Volume 256, issue 1-2.
7. P. A. Abdulla Collomb-A. Annichini A. Bouajjani and B. Jonsson. 2004 PDF
   Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design. Volume 25, issue 1.
8. A. Finkel and Goubault-J. Larrecq. 2009 PDF
   Forward analysis for WSTS, part I: Completions. 26th International Symposium on Theoretical Aspects of Computer Science.
9. P. Jančar, 1995.
   Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science. Volume 148, issue 2.
10. Petr Jančar, Javier Esparza, and Faron Moller, 1999.
    Petri nets and regular processes. Journal of Computer and System Sciences. Volume 59, issue 3.
11. R. Meyer. 2008.
    On boundedness in depth in the π‑calculus. Fifth IFIP International Conference On Theoretical Computer Science.
12. T. Wies, D. Zufferey, and T. Henzinger. 2010.
    Forward analysis of depth-bounded processes. FoSSaCS 2010.
13. E. D'Osualdo, C.H.-L. Ong. 2016.
    On Hierarchical Communication Topologies in the pi-calculus. Programming Languages and Systems: ESOP 2016.