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.

翻译：继我们近期开发马尔可夫决策过程的组合模型检测算法之后，本文提出一种求解均值收益博弈（MPGs）的组合框架。该框架源于范畴论，特别是幺半范畴：通过向MPGs（扩展开放末端）附加所谓的串图结构实现组合，并将其组织在幺半范畴中；博弈求解过程被表达为一个函子，其保持性质体现了组合性。组合性的核心问题在于如何丰富语义域；范畴框架通过甄别扩展语义域所需的代数结构，为该问题提供了明确的解决路径。我们在Haskell中实现了该组合求解方案；基准测试表明，该方案性能可比现有算法高出一个数量级。