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.

翻译：在马可夫决策过程中计算优化可达概率的调度器是一项标准的验证任务。为解决可扩展性问题，我们聚焦于以高级描述形式化语言进行成分化描述的MDP。具体而言，本文考虑弦图——一种子MDP的代数化顺序组合规范。为实现其成分化验证，关键挑战在于无需考虑子MDP在弦图中的上下文即可对其上的调度器进行局部优化。本文提出在子MDP中考虑调度器，这些调度器在局部目标的组合上形成帕累托曲线。尽管穷举所有此类调度器难以处理，但由此可导出一种高效可靠的近似算法。基于模型检测器Storm的原型系统验证了该方法的可扩展性。