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. Much of the work in probabilistic control program sketching, fault trees builds on top of model checking, and often, those applications required extension to the model checking algorithms.
I am broadly interested in the design and analysis of complex and robust (safety-)critical systems. In particular, I am interested in modeling 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.
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.
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. My thesis (missing reference) covers various aspects of parameter synthesis in Markov models. It also covers aspects of structural synthesis via sketching.
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.
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 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