Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-56-51-M-6

Concurrency Theory (M, 8.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-56-51-M-6 Concurrency Theory 8.0 CP (240 h)

Basedata

CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in WiSe
Level [6] Master (General)
Language [EN] English
Module Manager
Lecturers
Area of study [INF-ALG] Algorithmics and Deduction
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
4V+2U INF-56-51-K-6
Concurrency Theory
P 84 h 156 h
U-Schein
ja PL1 8.0 WiSe
  • 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.


Contents

  • Multithreaded programs
    • 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
  • GPU Programs
    • Bulk synchrony
    • Small model property
    • Reduction to sequential program verification

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.

Literature

Will be announced during the lecture.

Requirements for attendance of the module (informal)

Modules:

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-56-51-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Computer Science Theory [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Formal Fundamentals [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective
[MAT-88.105-SG] M.Sc. Mathematics [Subsidiary Topic] Subsidiary Topic (Minor) [WP] Compulsory Elective