- The lecture will be given in English by Damien Zufferey and the tutorials by Ivan Gavran.
- The dates and rooms of the lecture are:
- Lecture: Mondays, 11:45 - 13:15, room 48-453.
- Lecture: Wednesdays, 10:00 - 11:30, room 48-453.
- Tutorial: Thursdays, 17:15 - 18:45, room 48-453.

- Exercise sheets:
- Published on this page on Thursdays in the morning
- Solutions due the following Wednesday morning
- Hand in solutions in groups up to 3 people
- Send your solutions by email to Ivan Gavran in pdf, markdown, or text format (along with code if any).

- Exam:
- There will be an oral exam.
- 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.

- Dates: end of February / beginning of March (we will organize a poll over emails)
- 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.

- Guest lectures: during the semester we will have a guest lecturer to present current research development and application related to the class topics. This year Marko Horvat will give two lectures on security protocols.
- Misc:
- The repository for this page is at https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2017
- The
`*.md`files are Markdown formatted. The encoding is UTF-8 to get the math characters. If the math characters do not display properly try changing the font of your text editor. Not all fonts have math characters. Some text editors, e.g., atom can display an HTML preview which is easier to read. Looking at the file directly in the github repository also shows a formatted version

- Week 1 [lecture notes]
- Overview of the course
- Reminder about basic automata theoretic concepts

- Week 2 [lecture notes]
- Petri Nets
- Verification using linear programming

- Week 3 [lecture notes]
- Structural properties: siphons, traps
- Boundedness
- Karp and Miller Tree

- Week 4 [lecture notes]
- Well-Structured Transition Systems
- Backward coverability algorithm

- Week 5 [lecture notes]
- Ideal Completion for WSTS
- Forward coverability algorithm

- Week 6 by Marko Horvat [slides]
- Modeling and verification of security protocols

- Week 7 [lecture notes]
- Communicating state machines
- Turing completeness of communicating state machines with reliable FIFO channels

- Week 8 [lecture notes]
- Lossy Channel System
- Simple regular expression and WQO for LCS
- LTS, Simulations and bisimulations

- Week 9 [lecture notes]
- CCS
- Structural congruence
- Algebraic laws of bisimulation
- Decidability of bisimulation

- Week 10 [draft lecture notes]
- The π‑calculus
- Communication Topologies and Mobility
- Graphical interpretation of the π‑calculus

- Week 11 [draft lecture notes]
- Term embedding and the notion of depth
- The WQO of processes with depth at most k
- Coverability for depth-bounded processes

- Week 12 [draft lecture notes]
- Further analysis on depth-bounded processes
- Variations and extensions of the π-calculus
- Typing communicating processes

- Week 13 [draft lecture notes]
- Bulk synchronous model and cut-off bound
- Q&A

- Week 14
- Recap
- Q&A

- Exercises 1, solutions: [1-3, 4, 5]
- Exercises 2, solution: [5]
- Exercises 3
- Exercises 4 solutions: [1-4]
- Exercises 5 solutions: [normal, normal (another verison), optional]
- Exercises 6 solutions: [normal]
- Exercises 7 solutions: [1], [2]
- Exercises 8 solutions: [1] (rest to come)
- Exercises 9 solutions: [1-2]
- Exercises 10 solutions: [1] (rest to come)
- Exercises 11 solutions: [1-2]

- Lecture Notes from previous years by Roland Meyer.
- Decidability and complexity of Petri net problems – an introduction by Javier Esparza.
- Well-Structured Transition Systems Everywhere! by Alain Finkel and Philippe Schnoebelen, 1998.
- Forward Analysis for WSTS, Part I: Completions by Alain Finkel and Jean Goubault-Larrecq, 2009.
- Forward Analysis for WSTS, Part II: Complete WSTS by Alain Finkel and Jean Goubault-Larrecq, 2009.
- 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.
- 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.