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.

翻译：我们提出了一种用于马尔可夫决策过程的组合模型检验算法，该算法在范畴论的图形化语言——字符串图框架下实现组合。该算法可计算最优期望奖赏。算法的理论发展以范畴论为基础，而我们所提出的期望奖赏分解等式则是关键推动因素。实验评估证明了其性能优势。