Markovian models, like discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs), are widely used to describe systems with probabilistic or uncertain behavior. Application domains include reliability engineering, performance analysis, security, privacy, distributed systems, and optimization of highly reconfigurable systems like software product lines. Consequently, techniques for the quantitative analysis of Markovian models are paramount.

However, for many application domains, it neither suffices to consider a single finite-state Markovian model nor is the modeled system inherently infinite-state. For example, models of network protocols might depend on the number of clients or the number of retransmission attempts when sending messages over an unreliable channel. Furthermore, when analyzing an energy grid's expected power surplus, we might be uncertain about the grid's precise features, size, and topology. Rather than analyzing a single Markovian model, we thus need to reason about infinite families of finite-state models whose state spaces might depend on one or more parameters, e.g. the number of clients or the energy grid's size. The need to analyze families also shows up in many probabilistic model checking benchmarks: While probabilistic model checking tools work on individual finite-state Markovian models, their performance is often evaluated in terms of how far one can push parameters of those models until a tool is unable to verify the result within some time and memory bounds.

Project InFamoSS studies the following research question: How can we automatically prove or refute properties of infinite families of finite-state Markovian models whose underlying state spaces depend on one or more parameters?

Funding: German Research Council (DFG)

Randomization is a fundamental concept in computer science. It enables algorithms to run, on aver- age, faster and more resource-efficient than their deterministic counterparts, is essential in cryptography, and ensures fairness in distributed applications, such as electronic elections. In artificial intelligence, randomization expresses uncertainty, for example about the possible moves of a robot in difficult environments given limited sensor capabilities. Unfortunately, randomization is also the source of subtle bugs that are difficult to reproduce and counterintuitive to humans.

Project AuRoRa (Automated Reasoning about Randomized Algorithms) aims at improving the state of the art in automated verification of randomized systems by (1) developing novel intermediate verification languages for reasoning about quantitative properties of probabilistic programs and (2) exploring approaches for automating the building blocks of those languages.

Funding: Independent Research Fund Denmark (DFF project 1)