Compositional Probabilistic Model Checking with String Diagrams of MDPs

TL;DR

This paper introduces a compositional model checking algorithm for Markov decision processes using string diagrams, supported by category theory, enabling efficient computation of optimal expected rewards with demonstrated performance benefits.

Contribution

It presents a novel categorical, diagrammatic approach to compositional model checking of MDPs, integrating theoretical foundations with practical algorithms.

Findings

Algorithm computes optimal expected rewards efficiently.

Experimental results show performance improvements.

Category theory underpins the compositional framework.

Abstract

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.