59 citations · 174 across the 60 of their papers we have counts for
11 papers · 1 filter
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 Temporal Properties of Recursive Probabilistic Programs
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen
Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties ar…
The Probabilistic Termination Tool Amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen +1
We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber combin…
Reasoning about Reconfigurations of Distributed Systems
Emma Ahrens, Marius Bozga, Radu Iosif +1
This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs create and delete components and/or interaction…
Convex Optimization for Parameter Synthesis in MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges +2
Probabilistic model checking aims to prove whether a Markov decision process (MDP) satisfies a temporal logic specification. The underlying methods rely on an often unrealistic ass…