Concurrency Theory
Concurrency Theory
Course with SWS 2/2/0 (lecture/exercise/practical) in SS 2024
Lecturer
SWS
- 2/2/0
Modules
Examination method
- Oral exam
Matrix channel
Lecture series
Course Description
Modern computer systems are often multi-threaded or even fully distributed over several machines and geographical locations. Instead of the well-known sequential computational models (e.g., Turing machines, λ-calculus, etc.), the key notion for describing concurrent computations is that of a process. In this course, we study several phenomena occurring in concurrent computations using process calculi, for which we will define and analyze their formal semantics. As one of the key aspects, we ask when two processes are considered to be equivalent. Subsequently, we give an (incomplete) list of topics we strive for throughout the course.
- From sequential to parallel processes (LTS, CCS)
- Bisimulation and Coinduction
- From sequential to concurrent processes (Petri nets)
- Mobile processes (the π-calculus)
- Expressive power of process calculi
- Data-Aware Processes
Contact
If you have questions regarding the course, feel free to ask in the matrix chat or via email to the teacher of the course.
Schedule and Location
The course is taught in two sessions per week, one on Tuesdays DS2 (9.20-10.50) and Wednesdays DS3 (11.10-12.40). All the sessions take place in APB E005. We're currently planning the course sessions as on-site events. If necessary, we can retract to an Online mode, probably using Zoom. Exercises are intertwined with the lecture.
Acknowledgments
The first part of the lecture is based on the exposition Introduction to Bisimulation and Coinduction by Davide Sangiorgi. The slides Davide provides were an inspiration for the lecture material. The slides titled Part II have previously been used in lectures on coinduction.- Aceto, L., Ingólfsdóttir, A., Larsen, K. G., & Srba, J. (2007). Reactive Systems. Cambridge University Press.
- Sangiorgi, D., & Walker, D. (2003). The pi-calculus: a theory of mobile processes. Cambridge University Press.
- Sangiorgi, D. (2012). Introduction to bisimulation and coinduction. Cambridge University Press.
- Milner, R. (1980). A calculus of communicating systems. : Springer Berlin Heidelberg.
- Milner, R. (1999). Communicating and mobile systems. : Cambridge University Press.
- Davide Sangiorgi (2012). Advanced topics in bisimulation and coinduction. : Cambridge University Press.
- Reisig, W. (2013). Understanding Petri Nets. : Springer Berlin Heidelberg.
- Esparza, J. Petri Nets Lecture Notes from a course given at TU Munich Link to the Script
Subscribe to events of this course (icalendar)
Lecture | Introduction and Motivation: Labeled Transition Systems | DS2, April 9, 2024 in APB E005 | File |
Lecture | Towards Bisimilarity | DS3, April 10, 2024 in APB E005 | File |
Lecture | Semantics of Programming Languages | DS2, April 16, 2024 in APB E005 | File |
No session | --- | DS3, April 17, 2024 in APB E005 | |
Lecture | Direct Style Semantics | DS2, April 23, 2024 in APB E005 | File |
Exercise | Bisimulation and Bisimilarity | DS3, April 24, 2024 in APB E005 | File |
Exercise | Domains and Fixed Points | DS2, April 30, 2024 in APB E005 | File |
No session | Labor Day | DS3, May 1, 2024 in APB E005 | |
Lecture | Structural Operational Semantics | DS2, May 7, 2024 in APB E005 | |
Exercise | Denotational vs. Operational Semantics | DS3, May 8, 2024 in APB E005 | |
Lecture | Induction and Coinduction | DS2, May 14, 2024 in APB E005 | |
Exercise | Bisimilarity, Induction, Coinduction | DS3, May 15, 2024 in APB E005 | |
No session | Pentacost Week | DS2, May 21, 2024 in APB E005 | |
No session | Pentacost Week | DS3, May 22, 2024 in APB E005 | |
Lecture | Bisimilarity Explained | DS2, May 28, 2024 in APB E005 | |
Exercise | The Bisimilarity Problem | DS3, May 29, 2024 in APB E005 | |
Lecture | Algebraic Properties of Bisimilarity | DS2, June 4, 2024 in APB E005 | |
No session | Dies Academicus | DS3, June 5, 2024 in APB E005 | |
Lecture | A Testing Framework for CCS | DS2, June 11, 2024 in APB E005 | |
Exercise | Computational Properties of CCS | DS3, June 12, 2024 in APB E005 | |
Lecture | Petri Nets | DS2, June 18, 2024 in APB E005 | |
Exercise | Petri Net Modeling | DS3, June 19, 2024 in APB E005 | |
Lecture | Decidability for Petri Nets | DS2, June 25, 2024 in APB E005 | |
Exercise | True Concurrency Semantics | DS3, June 26, 2024 in APB E005 | |
Lecture | Immerman-Szelepcséni on Steroids | DS2, July 2, 2024 in APB E005 | |
Exercise | Petri Net Programs | DS3, July 3, 2024 in APB E005 | |
Lecture | Petri Net Languages | DS2, July 9, 2024 in APB E005 | |
Exercise | tba | DS3, July 10, 2024 in APB E005 | |
Lecture | Undecidability of Petri Nets | DS2, July 16, 2024 in APB E005 | |
Exercise | Summary and Outlook | DS3, July 17, 2024 in APB E005 |
Calendar