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: 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. 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Compositional Solution of Mean Payoff Games by String Diagrams

  • Kazuki Watanabe,
  • Clovis Eberhart,
  • Kazuyuki Asada,
  • Ichiro Hasuo

摘要

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: 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. 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.