Probabilistic Models of Concurrency

Audience

This Seminar addresses Master and Bachelor students in Computer Science and related study programs that mandate participation in at least one Seminar.

The first meeting

The first meeting takes place on Tuesday October 23, at 14:45 in room 528 of E1 3.

Structure

• Calibration - November 12: 5 minute presentations on Markov Decision Processes  (you will only present without any audience, you are not admitted to participate in the presentations of the others; we will ask the presenter of the presentation that we consider best to redo the presentation in public.) We recommend Chapter 3 of this book, but you are free to start off from other material.
  10% of the final grade
• Presentations - December to February: 40 minutes presentations, one or two presentations per week, you probably cannot present all the material in these 40 minutes - you need to construct a good story out of the material
  31% of the final grade
• Writeup - draft until March 1, final version until March 31: writeup of your presentation in a book chapter style.
  like in your presentation, you need to construct a good story and explain it properly therein (examples, exercises, etc.)
  29% of the final grade
• Reviews - until March 15: you will be assigned two write-ups of your colleagues, you need to read them and give a thorough written feedback
  10% of the final grade 
• Active participation: this involves feedback to the presentations of your colleagues and, most importantly, participation in the "scientific" discussions during and after the presentations
  20% of the final grade

Overview of the seminar

This Seminar has three goals:

1. to practice and to refine the skills of "scientific presentation", "scientific argumentation", and "scientific reflection";
2. to learn more about various theoretically challenging and practically relevant concurrency models.
3. to get an understanding how quantifiable uncertainty (aka probability) enters these model and how to algorithmically attack that.

The objective of the seminar is to provide a broad overview of the theoretical underpinnings of concurrency theory with a particular focus on probabilistic models and their analysis. 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. Every such extension is motivated by a concrete practical application area. This way, we can reason about timed behaviour of real-time systems; describe behaviour of reactive systems using languages composed not of finite but of infinite words; specify classes of models using a modal automata. We will see how these modelling feature are crucial for the respective application areas.

We selected a number of papers for each of these areas. Participation in the seminar includes writing a paper to give some motivation, examples, links to relevant literature and to provide the theoretical background of the selected topic. Furthermore, each participant gives a formal presentation (approx. 45 minutes) to explain the topic to the audience.

List of Potential Topics

1. Probabilistic CCS
   C. Baier: On algorithmic verification methods for probabilistic systems (Chapter 4).

2. Dynamic Programming & Monte Carlo Methods
   R.S. Sutton, G. Barto: Finite Markov Decision Processes (Chapter 4+5).

3. Temporal-Difference Learning & n-step Booststrapping
   R.S. Sutton, G. Barto: Finite Markov Decision Processes (Chapter 6+7).

4. Planning and Learning with Tabular Methods
   R.S. Sutton, G. Barto: Finite Markov Decision Processes (Chapter 8).

5. On-policy Prediction with Approximation
   R.S. Sutton, G. Barto: Finite Markov Decision Processes (Chapter 9).

6. Safety-Constrained Reinforcement Learning
   S. Junges et al.: Safety-Constrained Reinforcement Learning for MDPs.

7. Scheduler Sampling
   P.R. D'Argenio et al.: Smart sampling for lightweight verification of Markov decision processes.

8. Distributed Schedulers
   S. Giro, P.R. D'Argenio: Quantitative Model Checking Revisited: Neither Decidable Nor Approximable.

9. Game-based abstraction
   M. Kwiatkowska, G. Norman, D. Parker: Game-based abstraction of Markov decision processes.

10. Probabilistic Partial-Order Reduction

    C. Baier, P.R. D'Argenio, M. Größer: Partial Order Reduction for Probabilistic Branching Time.

11. Probabilistic Minimality
    C. Eisentraut et al.: The Quest for Minimal Quotients for Probabilistic an Markov Automata.

12. Axioms for Probabilistic Weak Bisimilarity
    N. Fischer, R.J. van Glabbeek: Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours.

13. Priced and Probabilistic Timed Automata
    G. Norman, D. Parker, J. Sproston: Model Checking for Probabilistic Timed Automata.
    P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey. Quantitative analysis of real-time systems using priced timed automata.