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.
@article{arxiv.2307.08765,
title = {Compositional Probabilistic Model Checking with String Diagrams of MDPs},
author = {Kazuki Watanabe and Clovis Eberhart and Kazuyuki Asada and Ichiro Hasuo},
journal= {arXiv preprint arXiv:2307.08765},
year = {2023}
}