Concurrency Theory (SS2025): Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Stephan Mennicke (Diskussion | Beiträge) (add lecture 02) |
Stephan Mennicke (Diskussion | Beiträge) (updated schedule) |
||
| Zeile 65: | Zeile 65: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=Bisimilarity and All That | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/04/14 | |Date=2025/04/14 | ||
| Zeile 72: | Zeile 72: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Übung | |Lehrveranstaltungstype=Übung | ||
|Title=The Linear Time - Branching Time Spectrum | |Title=The Linear Time - Branching Time Spectrum (1) | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/04/15 | |Date=2025/04/15 | ||
| Zeile 93: | Zeile 93: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=Algebraic Properties of Bisimilarity | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/04/28 | |Date=2025/04/28 | ||
| Zeile 100: | Zeile 100: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Übung | |Lehrveranstaltungstype=Übung | ||
|Title= | |Title=The Linear Time - Branching Time Spectrum (2) | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/04/29 | |Date=2025/04/29 | ||
| Zeile 107: | Zeile 107: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=Bisimilarity and Testing | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/05/05 | |Date=2025/05/05 | ||
| Zeile 121: | Zeile 121: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title=Checking Bisimilarity is | |Title=Checking Bisimilarity is Complete for P | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/05/12 | |Date=2025/05/12 | ||
| Zeile 135: | Zeile 135: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=Checking Bisimilarity is Undecidable | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/05/19 | |Date=2025/05/19 | ||
| Zeile 149: | Zeile 149: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=Everything you always wanted to know about Petri Nets | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/05/26 | |Date=2025/05/26 | ||
| Zeile 163: | Zeile 163: | ||
{{Vorlesung Zeiten | {{Vorlesung Zeiten | ||
|Lehrveranstaltungstype=Vorlesung | |Lehrveranstaltungstype=Vorlesung | ||
|Title= | |Title=What is Decidable about Petri Nets? | ||
|Room=APB E005 | |Room=APB E005 | ||
|Date=2025/06/02 | |Date=2025/06/02 | ||
Version vom 8. April 2025, 13:01 Uhr
Concurrency Theory
Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2025
Dozent
Umfang (SWS)
- 2/2/0
Module
Leistungskontrolle
- Mündliche Prüfung
Vorlesungsreihe
Course Description
Modern computer systems are often multi-threaded or even fully distributed over several machines and geographic locations. Instead of computation (e.g., in Turing machines, λ-calculus, etc.), the key notion for describing concurrent computations is interaction leading to the concept of processes. 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 about the course, feel free to ask in the matrix chat or email the teacher(s).
Schedule and Location
The course is taught in two sessions per week,
* weekly lecture sessions will happen on Mondays DS4 (13.00-14.30) * weekly exercise sessions happen on Tuesdays 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.
- 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.
* especially chapter 3 on "Algorithmics of Bisimilarity" by Luca Aceto et al.
- 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
Veranstaltungskalender abonnieren (icalendar)
| Vorlesung | Introduction and Motivation | DS4, 7. April 2025 in APB E005 | Datei |
| Vorlesung | Linear Time vs. Branching Time | DS3, 8. April 2025 in APB E005 | Datei |
| Vorlesung | Bisimilarity and All That | DS4, 14. April 2025 in APB E005 | Datei |
| Übung | The Linear Time - Branching Time Spectrum (1) | DS3, 15. April 2025 in APB E005 | Datei |
| Entfällt | Easter Monday | DS4, 21. April 2025 in APB E005 | |
| Entfällt | Easter Tuesday | DS3, 22. April 2025 in APB E005 | |
| Vorlesung | The Calculus of Communicating Systems | DS4, 28. April 2025 in APB E005 | Datei |
| Übung | The Linear Time - Branching Time Spectrum (2) | DS3, 29. April 2025 in APB E005 | Datei |
| Vorlesung | Algebraic Properties of Bisimilarity | DS4, 5. Mai 2025 in APB E005 | Datei |
| Übung | CCS and Bisimilarity | DS3, 6. Mai 2025 in APB E005 | Datei |
| Vorlesung | Checking Bisimilarity is Complete for P | DS4, 12. Mai 2025 in APB E005 | |
| Übung | Algebraic Properties of Bisimilarity | DS3, 13. Mai 2025 in APB E005 | Datei |
| Vorlesung | Checking Bisimilarity is (Un-)Decidable | DS4, 19. Mai 2025 in APB E005 | |
| Übung | Hennessy-Milner Logic and Bisimilarity | DS3, 20. Mai 2025 in APB E005 | |
| Vorlesung | Everything you always wanted to know about Petri Nets | DS4, 26. Mai 2025 in APB E005 | |
| Übung | Efficient Algorithms for Checking Bisimilarity (2) | DS3, 27. Mai 2025 in APB E005 | |
| Vorlesung | What is Decidable about Petri Nets? | DS4, 2. Juni 2025 in APB E005 | |
| Übung | Properties of Petri Nets | DS3, 3. Juni 2025 in APB E005 | |
| Entfällt | Pentecost Week | DS4, 9. Juni 2025 in APB E005 | |
| Entfällt | Pentecost Week | DS3, 10. Juni 2025 in APB E005 | |
| Vorlesung | The Complexity of Petri Nets (1) | DS4, 16. Juni 2025 in APB E005 | |
| Übung | The Coverability Problem | DS3, 17. Juni 2025 in APB E005 | |
| Vorlesung | The Complexity of Petri Nets (2) | DS4, 23. Juni 2025 in APB E005 | |
| Übung | Region Theory | DS3, 24. Juni 2025 in APB E005 | |
| Vorlesung | The Complexity of Petri Nets (3) | DS4, 30. Juni 2025 in APB E005 | |
| Übung | Petri Net Languages | DS3, 1. Juli 2025 in APB E005 | |
| Vorlesung | Towards Mobile Processes (1) | DS4, 7. Juli 2025 in APB E005 | |
| Übung | Petri Net Processes | DS3, 8. Juli 2025 in APB E005 | |
| Vorlesung | Summary and Outlook | DS4, 14. Juli 2025 in APB E005 | |
| Entfällt | Probably no Exercise Session | DS3, 15. Juli 2025 in APB E005 |
Kalender
