59 citations · 458 across the 94 of their papers we have counts for
8 papers · 1 filter
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski +1
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be…
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…
Strategy Synthesis in POMDPs via Game-Based Abstractions
Leonore Winterer, Sebastian Junges, Ralf Wimmer +4
We study synthesis problems with constraints in partially observable Markov decision processes (POMDPs), where the objective is to compute a strategy for an agent that is guarantee…
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…
A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
Benjamin Lucien Kaminski, Joost-Pieter Katoen
We present a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of \emph{mixed-sign unbounded} random variables after execution of a pro…
A storm is Coming: A Modern Probabilistic Model Checker
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen +1
We launch the new probabilistic model checker storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the PRISM and JA…
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…
Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
Xiaoxiao Yang, Joost-Pieter Katoen, Hao Wu
The verification of linearizability -- a key correctness criterion for concurrent objects -- is based on trace refinement whose checking is PSPACE-complete. This paper suggests to…