Seminar in Theoretical CS, Summer Semester 2020

## News

- 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.2020 | Introductory material online |

17.04.2020 | Topic preferences due |

04.05.2020 | Detailed outline due |

02.06.2020 | Full report due |

29.06.2020 | Presentation slides due |

14.07.2020 | Seminar 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*.

## Overview

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

## Prerequisites

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 sessions | July 14, 2020 |

09:00-10:30 | Vladimir Rzaev, Philipp Schröer, Domenic Quirl |

10:45-11:45 | Clemens Frohnhofen, Fabian Meyer |

Afternoon session | |

14:00-15:30 | Johannes Raufeisen, Darion Haase, Dario Veltri |

## Topics

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

### Automata Models

- Probabilistic Automata (B)
**Literature:**M. Stoelinga: An introduction to probabilistic automata. Bulletin of the European Association for Theoretical Computer Science, 2002**Supervisor:**Mojgan Kamali**Student:**Vladimir Rzaev

- Markov Automata (B)
**Literature:**C. Eisentraut, H. Hermanns, L. Zhang: Concurrency and Composition in a Stochastic World. CONCUR 2010**Supervisor:**–**Student:**–

- Probabilistic Timed Automata (B)
**Literature:**G. Norman, D. Parker, J. Sproston: Model Checking for Probabilistic Timed Automata. FMSD 2013**Supervisor:**–**Student:**–

- Generalised Stochastic Petri Nets (B/M)
**Literature:**Gianfranco Balbo: Introduction to Generalized Stochastic Petri Nets. SFM 2007**Supervisor:**–**Student:**–

- Probabilistic Petri Nets (B/M)
**Literature:**Roberto Bruni, Hernán C. Melgratti, Ugo Montanari: Concurrency and Probability: Removing Confusion, Compositionally. LMCS 2019**Supervisor:**–**Student:**–

### Process Algebras

- Stochastic Process Algebras (B/M)
**Literature:**Holger Hermanns, Ulrich Herzog, Joost-Pieter Katoen: Process algebra for performance evaluation. TCS 2002**Supervisor:**–**Student:**–

- Probabilistic CCS (B/M)
**Literature:**Alessandro Giacalone, Chi-chang Jou, Scott A. Smolka: Algebraic Reasoning for Probabilistic Concurrent Systems. IFIP TC2 Working Conference on Programming Concepts and Methods, 1990**Supervisor:**Thomas Noll**Student:**Clemens Frohnhofen

- Probabilistic CSP (B/M)
**Literature:**Gavin Lowe: Probabilistic and prioritized models of timed CSP. TCS 1995 (only second part)**Supervisor:**–**Student:**–

- Probabilistic pi-calculus (B/M)
**Literature:**Mihaela Herescu and Catuscia Palamidessi: Probabilistic asynchronous pi-calculus. FoSSaCS 2000**Supervisor:**Thomas Noll**Student:**Fabian Meyer

- Markov Automata Process Algebra (B/M)
**Literature:**Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Mariëlle I. A. Stoelinga: Efficient Modelling and Generation of Markov Automata. CONCUR 2012**Supervisor:**–**Student:**–

### Scheduling

- Sampling of MDP Schedulers (M)
**Literature:**P.R. D’Argenio et al.: Smart sampling for lightweight verification of Markov decision processes. STTT 2015**Supervisor:**Matthias Volk**Student:**Philipp Schröer

- Distributed Schedulers (M)
**Literature:**S. Giro, P.R. D’Argenio: Quantitative Model Checking Revisited: Neither Decidable Nor Approximable. FORMATS 2007**Supervisor:**–**Student:**–

### Abstraction Techniques

- Game-Based Abstraction (M)
**Literature:**Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker: A game-based abstraction-refinement framework for Markov decision processes. FMSD 2010**Supervisor:**–**Student:**–

- Probabilistic Partial-Order Reduction (M)
**Literature:**C. Baier, P.R. D’Argenio, M. Größer: Partial Order Reduction for Probabilistic Branching Time. ENTCS 2006**Supervisor:**Mojgan Kamali**Student:**Domenic Quirl

- Confluence Reduction (M)
**Literature:**Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga: Confluence reduction for Markov automata. TCS 2016**Supervisor:**–**Student:**–

- Probabilistic Bisimulation (M)
**Literature:**Jan Friso Groote, Jao Rivera Verduzco, Erik P. de Vink: An Efficient Algorithm to Determine Probabilistic Bisimulation. Algorithms 2018**Supervisor:**Shahid Khan**Student:**Johannes Raufeisen

- Lumping of Markov Chains (M)
**Literature:**Antti Valmari, Giuliana Franceschinis: Simple O(m log n) Time Markov Chain Lumping. TACAS 2010**Supervisor:**Shahid Khan**Student:**Darion Haase

### Probabilistic Temporal Logics

- Probabilistic Computation Tree Logic (B/M)
**Literature:**Pablo F. Castro, Cecilia Kilmurray, Nir Piterman: Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics. STACS 2015**Supervisor:**Joshua Moerman**Student:**Dario Veltri

## Additional Material

- Report template
- Presentation template
- How to write scientific papers
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to give presentations
- Introduction to LaTeX

## Registration

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