Organization

• The lectures are be given in English by Damien Zufferey and Anthony W. Lin. The tutorials are Felix Stutz.
• The dates and rooms of the lecture are:
  • Lecture: Monday, 11:45 - 13:15, room 48-453.
  • Lecture: Friday, 11:45 - 13:15, room 36-265.
  • The first tutorial will be on Tuesday, 29 Oct, in MPI-SWS room 111. The tutorial will cover the verification tool Spin which will be used for some exercises.
  • There will be no tutorial on 14th and 21st of January.
    We will have a substitute tutorial session on Thursday, 23rd of January, at 1:45pm in MPI-SWS room 111.
  • Tutorial: We have decided with the class' participants. The tutorial takes place on Tuesdays 8:15am in MPI-SWS room 111.
• Exercise sheets:
  • Published on this page on Mondays
  • Solutions due before the following Monday at 8am
  • Hand in solutions in groups of 3 to 4 people
  • Send your solutions by email to Felix Stutz in one readable pdf file (along with code if any).
• Mailing list
  We will announce everything on this website but may use the following mailing list as an additional channel. It is run by MPI-IST. In particular, you are very welcome to use it to find a group for submission.
• Exam:
  • There will be an oral exam.
  • To be admitted, you have to fulfil the following requirements:
    1. 60 percent of your exercises have to be marked by a plus (useful answer).
    2. You have to present some of your exercise solutions on the board.
  • Office hour: Damien and Felix will offer an office hour from 2:00pm to 3:00pm on Monday 2nd of March in MPI-SWS 207.
  • Dates: The exams will be on 5 and 6 March as well as 3 April. You should have received an e-mail with your slot. Please remember to confirm it until 16 February and to register with the university.
  • Format:
    • Questions: You will pick three questions at random from a pool and keep two
    • Preparation: You will have half an hour to think about the question and prepare. You will have access to the course material during that time.
    • Examination: The examination will last half an hour in which you will discuss the question and we will ask further questions/clarifications.
• Misc:
  • Misc:
    • The repository for this page is at https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2019
    • The *.md files are in the Markdown format with some extensions for math formula and graphs. The encoding is UTF-8 to get the math characters. Due to the extensions, it is recommended to view the files with the link below. If you want to view the notes offline you need to:
      1. Clone the repository.
      2. Run a local web server in the root folder of the repository (for instance: python -m SimpleHTTPServer 8080).
      3. View the notes through a browser (http://127.0.0.1:8080/concurrency_theory_2019/viewer.html?md=concurrency_theory_2019/notes/notes_1.md).

Tentative Schedule

Week 1 [draft notes]

• Overview of the course [notes]
• Reminder about basic automata theoretic concepts

Week 2 [draft notes]

• Properties and Verification
• Petri Nets
• Verification using linear programming

Week 3 [draft notes]

• Termination and Boundedness
• Karp and Miller Tree
• "Size" of Bounded Petri Nets

Week 4 [draft notes]

• Well-Structured Transition Systems
• Backward coverability algorithm

Week 5 [draft notes]

• Forward coverability algorithm (The notes have quite a lot of material. We will trim them down depending on what we have the time to cover in class.)

Week 6 [draft notes]

• Communicating state machines
• Turing completeness of communicating state machines with reliable FIFO channels

Week 7 [draft notes]

• Lossy Channel System
• Simple regular expression and WQO for LCS

Week 8 [draft notes]

• LTS, Simulations and bisimulations
• Calculus of Communicating Systems (CCS)
• Structural congruence
• Expressive power of CCS

Week 9 [draft notes]

• Weak (bi-) simulation
• The π‑calculus
• Variations and extensions of the π-calculus

Week 10

• Typing communicating processes (Damien) [draft notes]
• Testing of distributed systems (Burcu) [slides]

Week 11

• Testing of distributed systems (Burcu) [slides]
• Bulk synchronous model (Damien) [draft notes]

Week 12 [draft notes]

• Weak memory model
• TSO (Total Store Order)
• WSTS for TSO

Week 13

• Parameterized Systems (Daniel Stan) [slides]

Week 14

• Q&A for Theory and Exercises

Exercises

You can see that we are about to compile master solutions for the exercises. However, due to resource constraints, we will probably not be able to cover all of them until the first exams. This is why we encourage you to send an e-mail to Damien and Felix if you liked to have a particular solution. This way, we can prioritise accordingly. In case, we will not manage to write them up in time, we would like to hint at the office hour on Monday 2nd of March again.

• Exercise 0: Using the Spin model checker. We will use this in later exercises.
• Exercises 1 solutions: ex 1-3
• Exercises 2 solutions: ex 1-2
• Exercises 3 solutions: WIP solutions
• Exercises 4 solutions: WIP solutions
• Exercises 5 (29.11.2020) The 1st exercise has been clarified. solutions: WIP solutions
• Exercises 6 solutions: WIP solutions
• Exercises 7 solutions: WIP solutions
• Bonus exercises 1 (week 8) solutions: WIP solutions
• Exercises 8 (week 9) Due date updated to January 20. solutions: WIP solutions
• Exercises 9 (week 10) solutions: WIP solutions
• Exercises 10 (week 11) solutions: WIP solutions
• Bonus exercises 2 (week 12) solutions: WIP solutions

References

• Lecture Notes from previous years by Roland Meyer.
• Decidability and complexity of Petri net problems – an introduction by Javier Esparza.
• Free Choice Petri Nets by Jörg Desel and Javier Esparza, 1995.
• Well-Structured Transition Systems Everywhere! by Alain Finkel and Philippe Schnoebelen, 1998.
• Forward Analysis for WSTS, Part III: Karp-Miller Trees by Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq, 2017.
• On Communicating Finite-State Machines by Daniel Brand and Pitro Zafiropulo, 1983.
• A Calculus of Mobile Processes Pt.1 by R. Milner, J. Parrow and D. Walker, 1992.
• A Calculus of Mobile Processes Pt.2 by R. Milner, J. Parrow and D. Walker, 1992.
• The Polyadic pi-Calculus: A Tutorial by Robin Milner, 1993.
• On the Verification Problem for Weak Memory Models by Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, 2010.
• The Benefits of Duality in Verifying Concurrent Programs under TSO by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo, 2016.
• The Design and Implementation of a Verification Technique for GPU Kernels by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, and John Wickerson, 2015.
• ...

The files available in https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2017 are licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.