4 papers
Compositional Verification of Almost-Sure Büchi Objectives in MDPs
Marck van der Vegt, Kazuki Watanabe, Ichiro Hasuo +1
This paper studies the verification of almost-sure Büchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is…
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…
A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs
Marnix Suilen, Marck van der Vegt, Sebastian Junges
Markov Decision Processes (MDPs) model systems with uncertain transition dynamics. Multiple-environment MDPs (MEMDPs) extend MDPs. They intuitively reflect finite sets of MDPs that…
Compositional Value Iteration with Pareto Caching
Kazuki Watanabe, Marck van der Vegt, Sebastian Junges +1
The de-facto standard approach in MDP verification is based on value iteration (VI). We propose compositional VI, a framework for model checking compositional MDPs, that addresses…