# Compositional Probabilistic Model Checking with String Diagrams of MDPs

arXiv: https://arxiv.org/abs/2307.08765 · HTML: https://mlsanity.com/paper/2307.08765/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jul 2023.

## Built on by (most cited first, 4 of 4)

- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Reduce, Reuse, Recycle: Categories for Compositional Reinforcement Learning](https://mlsanity.com/paper/2408.13376/) (2024)
- [Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement](https://mlsanity.com/paper/2506.17792/) (2025)
- [Scenario-Based Compositional Statistical Model Checking for Safety Specifications](https://mlsanity.com/paper/2610.05571/) (2026)

## Abstract (arXiv)

We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.