3 papers
cs.LO2024
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…
cs.LO2024
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…
cs.LO2024
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo +2
Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally de…