Compositional Probabilistic Model Checking with String Diagrams of MDPs

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. The talk is based on the following paper:

• Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo. Compositional Probabilistic Model Checking with String Diagrams of MDPs. To appear in CAV’23. [preprint].

(This will probably not be a long talk, approximately 30-45 minutes.)

Zoom link: