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 (informal)

Modules:

Requirements for attendance (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 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