- Petri nets
- safety and liveness properties
- Petri nets invariants and linear programming
- Forward analysis: Karp & Miller tree
- Backward analysis: well structured transitions systems (WSTS)
Message passing programs
- Communicating state machines with FIFO or lossy channels
- Process algebra and the actor model
- Reduction to WSTS
- Bulk synchrony
- Small model property
- Reduction to sequential program verification
Concurrency Theory (M, 8.0 LP)
|Module Number||Module Name||CP (Effort)|
|INF-56-51-M-6||Concurrency Theory||8.0 CP (240 h)|
|CP, Effort||8.0 CP = 240 h|
|Position of the semester||1 Sem. in WiSe|
|Level|| Master (General)|
|Area of study||[INF-ALG] Algorithmics and Deduction|
|Reference course of study||[INF-88.79-SG] M.Sc. Computer Science|
|Type/SWS||Course Number||Title||Choice in |
|SL||SL is |
required for exa.
|P||84 h||156 h||
- About [INF-56-51-K-6]: Title: "Concurrency Theory"; Presence-Time: 84 h; Self-Study: 156 h
- About [INF-56-51-K-6]: The study achievement [U-Schein] proof of successful participation in the exercise classes (ungraded) must be obtained. It is a prerequisite for the examination for PL1.
Examination achievement PL1
- Form of examination: oral examination (20-60 Min.)
- Examination Frequency: Examination only within the course
- Examination number: 65651 ("Concurrency Theory")
Evaluation of grades
The grade of the module examination is also the module grade.
Competencies / intended learning achievements
- The students develop operational models for systems with multiple components interacting concurrently.
- The students understand correctness properties and algorithms to verify these properties.
- The students will apply existing techniques on examples and adapt them to related classes of systems.
Will be announced during the lecture.
Requirements for attendance (informal)
Requirements for attendance (formal)
References to Module / Module Number [INF-56-51-M-6]
|Course of Study||Section||Choice/Obligation|
|[INF-88.79-SG] M.Sc. Computer Science||Computer Science Theory||[WP] Compulsory Elective|
|[INF-88.79-SG] M.Sc. Computer Science||Formal Fundamentals||[WP] Compulsory Elective|
|[INF-88.79-SG] M.Sc. Computer Science||Specialization 1||[WP] Compulsory Elective|
|[MAT-88.105-SG] M.Sc. Mathematics||Subsidiary Topic (Minor)||[WP] Compulsory Elective|