In this project, we investigate runtime monitoring under uncertainty. Technically, we consider a white-box setting where we are given a Markov model of the system and aim to extract all sequences of events that should be classified as dangerous.
In this project, we aim to combine symbolic probabilistic model checking methods with inductive synthesis to quickly analyze many different models. The novel methods in this project shall boost the PAYNT tool.
In this project, we aim to improve the usability of our open source model checker Storm.
Published in AAAI 2021, 2020
We show a first scalable approach to (small-memory) policy synthesis for uncertain POMDPs!
Recommended citation: Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, Ufuk Topcu: Robust Finite-State Controllers for Uncertain POMDPs. AAAI 2021. https://arxiv.org/abs/2009.11459
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
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.
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.
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.
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.
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.
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.