Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
CoRR(2024)
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined