Generalised M\"obius Categories and Convolution Kleene Algebras

TL;DR

This paper introduces a generalized framework for convolution Kleene algebras based on M"obius categories, enabling new algebraic structures for computing and reasoning in concurrent, weighted, and higher-dimensional systems.

Contribution

It generalizes M"obius categories and star operations to construct convolution Kleene algebras applicable to a broad class of structures, including higher categories and semirings.

Findings

Constructed convolution Kleene algebras for various structures

Applied to verification of probabilistic and concurrent programs

Extended to Conway semirings for weighted automata

Abstract

Convolution algebras on maps from structures such as monoids, groups or categories into semirings, rings or fields abound in mathematics and the sciences. Of special interest in computing are convolution algebras based on variants of Kleene algebras, which are additively idempotent semirings equipped with a Kleene star. Yet an obstacle to the construction of convolution Kleene algebras on a wide class of structures has so far been the definition of a suitable star. We show that a generalisation of M\"obius categories combined with a generalisation of a classical definition of a star for formal power series allow such a construction. We discuss several instances of this construction on generalised M\"obius categories: convolution Kleene algebras with tests, modal convolution Kleene algebras, concurrent convolution Kleene algebras and higher convolution Kleene algebras (e.g. on strict higher categories and higher relational monoids). These are relevant to the verification of weighted and probabilistic sequential and concurrent programs, using quantitative Hoare logics or predicate transformer algebras, as well as for algebraic reasoning in higher-dimensional rewriting. We also adapt the convolution Kleene algebra construction to Conway semirings, which is widely studied in the context of weighted automata. Finally, we compare the convolution Kleene algebra construction with a previous construction of convolution quantales and present concrete example structures in preparation for future applications.