Page Not Found
Page not found. Your pixels are in another canvas.
Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Sebastian Junges
About me
Page not in menu
This is a page not in th emain menu
Posts
projects
Furore: Fundamentals of Robust Runtime Monitoring (NWO ENW-M)
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.
Promise: Symbolic Probabilistic Model Checking with Massive Design Spaces (NWO Veni)
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.
StormAE: The Probabilistic Model Checker Storm for Almost Everyone (NWO OSF)
In this project, we aim to improve the usability of our open source model checker Storm.
publications
Robust Finite-State Controllers for Uncertain POMDPs
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
research
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
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.
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.
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.
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.
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.
talks
teaching
Teaching experience 1
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Teaching experience 2
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.