Probabilistic Model Checking
A core part of my research considers the model-based analysis of (temporal,declaritive) specifications on Markov models such as Continous-Time Markov Chains, Markov Decision Processes, Markov Automata.
Research
I am broadly interested in the design and analysis of complex and robust (safety-)critical systems. In particular, I am interested in modelling formalisms to describe such systems and the use of automated reasoning to analyse these systems. Often, I develop such reasoning techniques myself. Many of these methods are rooted in (probabilistic) model checking and satisfiability solvers. Also see my list of publications. In the pages below, I gave a brief and often slightly outdated overview of my results.
Analysis for POMDPs
Partially observable MDPs are a rich modelling formalism to model real world systems. We have considered both verification and controller synthesis approaches to their analysis.
Parameter Synthesis in Markov Models
Markov models assume a fixed transition probability. However, often these transition probabilities are based on expert estimates or learned from data. It is therefore natural to consider symbolic probabilities in the form of parameters, and investigate for which parameter values a model satisfies a given specification.
Syntax-Guided Synthesis in Probabilistic Programs
As a variant to the parameter synthesis, we consider probabilistic programs with holes, where the right expression for the holes have to be synthesised. A technical difference to parameter synthesis is that we consider finite sets of programs with often different control flow diagrams.
Runtime Assurance and Enforcement
System safety must be ensured not only during design time, but also during runtime. Design-time verification may be too costly or make assumptions on the environment that later are not valid. This is where runtime verification comes into play.
Fault Trees and Reliability Engineering
Fault trees are a prominent model in reliability engineering. They help express the occurence of a top-level failure in terms of faults in the system. We have studied the quantitative analysis of Fault Trees, in particular of an extension of Fault Trees called Dynamic Fault Trees. Dynamic Fault Trees allow for complex and order-dependent combinations of faults to be expressed capturing e.g. different failure rates of unused spare components