  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 efficiency while maintaining soundness.
Concretely, compositional MDPs naturally arise from the combination of
individual components, and their structure can be expressed using, e.g., string
diagrams. Towards efficiency, we observe that compositional VI repeatedly
verifies individual components. We propose a technique called Pareto caching
that allows to reuse verification results, even for previously unseen queries.
Towards soundness, we present two stopping criteria: one generalizes the
optimistic value iteration paradigm and the other uses Pareto caches in
conjunction with recent baseline algorithms. Our experimental evaluations shows
the promise of the novel algorithm and its variations, and identifies
challenges for future work.
