59 citations · 191 across the 36 of their papers we have counts for
23 papers · 1 filter
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Roman Andriushchenko, Alexander Bork, Milan Češka +3
This paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making un…
A Practitioner's Guide to MDP Model Checking Algorithms
Arnd Hartmanns, Sebastian Junges, Tim Quatmann +1
Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popul…
Robust Almost-Sure Reachability in Multi-Environment MDPs
Marck van der Vegt, Nils Jansen, Sebastian Junges
Multiple-environment MDPs (MEMDPs) capture finite sets of MDPs that share the states but differ in the transition dynamics. These models form a proper subclass of partially observa…
Parameter Synthesis in Markov Models: A Gentle Survey
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations…
Sampling-Based Verification of CTMCs with Uncertain Rates
Thom S. Badings, Nils Jansen, Sebastian Junges +2
We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while th…
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Kevin Batz, Mingshuai Chen, Sebastian Junges +3
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet eff…
Inductive Synthesis of Finite-State Controllers for POMDPs
Roman Andriushchenko, Milan Ceska, Sebastian Junges +1
We present a novel learning framework to obtain finite-state controllers (FSCs) for partially observable Markov decision processes and illustrate its applicability for indefinite-h…
Scenario-Based Verification of Uncertain Parametric MDPs
Thom Badings, Murat Cubuktepe, Nils Jansen +3
We consider parametric Markov decision processes (pMDPs) that are augmented with unknown probability distributions over parameter values. The problem is to compute the probability…
Gradient-Descent for Randomized Controllers under Partial Observability
Linus Heck, Jip Spel, Sebastian Junges +2
Randomization is a powerful technique to create robust controllers, in particular in partially observable settings. The degrees of randomization have a significant impact on the sy…
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte +3
We revisit the symbolic verification of Markov chains with respect to finite horizon reachability properties. The prevalent approach iteratively computes step-bounded state reachab…
Runtime Monitoring for Markov Decision Processes
Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk,…
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
Roman Andriushchenko, Milan Ceska, Sebastian Junges +1
This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov…
The Complexity of Reachability in Parametric Markov Decision Processes
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez +1
This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where tran…
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski +3
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our…
Scenario-Based Verification of Uncertain MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges +2
We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. The pr…
Are Parametric Markov Chains Monotonic?
Jip Spel, Sebastian Junges, Joost-Pieter Katoen
This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct -…
On the Complexity of Reachability in Parametric Markov Decision Processes
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez +1
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over…
Shepherding Hordes of Markov Chains
Milan Ceska, Nils Jansen, Sebastian Junges +1
This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, pl…
Parameter Synthesis for Markov Models: Covering the Parameter Space
Sebastian Junges, Erika Ábrahám, Christian Hensel +4
Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such a…
Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
Sebastian Junges, Nils Jansen, Ralf Wimmer +4
We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight…
Markov Automata with Multiple Objectives
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen
Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is u…
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges +4
Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of th…
Parameter Synthesis for Markov Models: Faster Than Ever
Tim Quatmann, Christian Dehnert, Nils Jansen +2
We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic cho…