Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

TL;DR

This work addresses scalable verification of MDPs described compositionally as string diagrams, by harnessing Pareto curves to capture trade-offs among multiple exits. It introduces open MDPs and shortcut MDPs to enable compositional analysis, and presents a sound approximation algorithm that computes under- and over-approximations of Pareto curves during recursive composition. The approach is implemented as a prototype on Storm and demonstrates significant gains over monolithic construction for large state spaces, while acknowledging challenges with many exits and potential error propagation. Overall, the paper contributes a principled, scalable framework for multi-objective, compositionally verified reachability in MDPs expressed via string diagrams, with practical implications for modular verification of complex probabilistic systems.

Abstract

Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.

Figures (9)

• Figure 1: Open Markov decision processes $\mathcal{A}$ and $\mathcal{B}$.
• Figure 2: Sequential composition $\mathcal{A}\fatsemi\mathcal{B}$ and sum $\mathcal{A}\oplus\mathcal{B}$
• Figure 3: From a multi-room MDP to a string diagram $\mathcal{A}\fatsemi (\mathcal{B} \oplus \mathrm{id})\fatsemi \mathcal{C}$.
• Figure 4: Our approach
• Figure 5: oMDP $\mathcal{A}$, $\mathrm{tp}(\mathcal{A}) = (1, 0) \rightarrow (2, 0)$

Theorems & Definitions (6)

• definition thmcounterdefinition: MDP
• definition thmcounterdefinition: oMDP
• definition thmcounterdefinition: $\fatsemi$ operator
• definition thmcounterdefinition: $\oplus$ operator
• definition thmcounterdefinition
• remark thmcounterremark