Probabilistic Models of Concurrency

Seminar in Theoretical CS, Summer Semester 2020


  • 24.03.2020: until further notice, the seminar will be fully organised in electronic form, without in-class meetings. The first material will be provided on April 14 (or earlier).
  • 20.01.2020: We are online.

Introduction and Assignment of Topics

Dates & Deadlines

14.04.2020Introductory material online
17.04.2020Topic preferences due
04.05.2020Detailed outline due
02.06.2020Full report due
29.06.2020Presentation slides due
14.07.2020Seminar talks

Note that the full versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.


Today, concurrent programming has become mainstream, dictated by need for ever increasing performance which, having reached the end of Moore’s law, can only be achieved by parallelism. Indeed, application software from areas such as medicine or natural sciences heavily relies on parallel hardware infrastructure like (GP)GPU accelerators, FPGAs, and multi- and many-core machines. However, it is also today that we see concurrency faults coming up every day, which raises the need for rigorous design techniques for concurrent systems. Therefore, a number of theoretically challenging and practically relevant concurrency models such as process algebras or Petri nets has been developed.

The aim of this seminar is to get an understanding how quantifiable uncertainty (aka probability) extends these models and how to algorithmically deal with such extensions. For example, we will discuss popular process algebras such as CCS with probabilities. In addition we will look at various concurrent automata models which in different senses extend finite automata by probabilistic elements, and temporal logics for reasoning about their behaviour. Every such extension is motivated by a concrete practical application area.

The following topic areas will be considered:

  • Probabilistic automata models and their analysis
  • Probabilistic process algebras
  • Probabilistic extensions of temporal logics


Basic knowledge in the following areas is expected:

  • Automata theory
  • Mathematical logic
  • For advanced topics, previous knowledge in Concurrency Theory is very helpful.

Schedule of Talks

Morning sessionsJuly 14, 2020
09:00-10:30Vladimir Rzaev, Philipp Schröer, Domenic Quirl
10:45-11:45Clemens Frohnhofen, Fabian Meyer
Afternoon session
14:00-15:30Johannes Raufeisen, Darion Haase, Dario Veltri


(The annotations “B” and “M” respectively refer to topics on Bachelor and Master level.)

Automata Models

  1. Probabilistic Automata (B)
  2. Markov Automata (B)
  3. Probabilistic Timed Automata (B)
  4. Generalised Stochastic Petri Nets (B/M)
  5. Probabilistic Petri Nets (B/M)

Process Algebras

  1. Stochastic Process Algebras (B/M)
  2. Probabilistic CCS (B/M)
  3. Probabilistic CSP (B/M)
  4. Probabilistic pi-calculus (B/M)
  5. Markov Automata Process Algebra (B/M)


  1. Sampling of MDP Schedulers (M)
  2. Distributed Schedulers (M)

Abstraction Techniques

  1. Game-Based Abstraction (M)
  2. Probabilistic Partial-Order Reduction (M)
  3. Confluence Reduction (M)
  4. Probabilistic Bisimulation (M)
  5. Lumping of Markov Chains (M)

Probabilistic Temporal Logics

  1. Probabilistic Computation Tree Logic (B/M)

Additional Material


Registration to the seminar is possible via the central registration procedure of the CS Department.


Thomas Noll