Compositional Solution of Mean Payoff Games by String Diagrams

TL;DR

This paper introduces a novel compositional framework for solving mean payoff games using string diagrams and category theory, enabling modular analysis and potential performance improvements over existing algorithms.

Contribution

It develops a categorical, compositional approach to solving MPGs, extending semantic domains and implementing an efficient Haskell-based solution.

Findings

Can outperform existing algorithms by an order of magnitude

Provides a modular, compositional framework for MPGs

Uses string diagrams and monoidal categories for solution structure

Abstract

Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs). The framework is derived from category theory, specifically that of monoidal categories: MPGs (extended with open ends) get composed in so-called string diagrams and thus organized in a monoidal category; their solution is then expressed as a functor, whose preservation properties embody compositionality. As usual, the key question to compositionality is how to enrich the semantic domain; the categorical framework gives an informed guidance in solving the question by singling out the algebraic structure required in the extended semantic domain. We implemented our compositional solution in Haskell; depending on benchmarks, it can outperform an existing algorithm by an order of magnitude.