Categorical Liveness Checking by Corecursive Algebras

TL;DR

This paper develops a categorical framework for proving liveness properties in dynamical systems modeled as coalgebras, extending coalgebraic methods from safety to liveness verification.

Contribution

It introduces a novel categorical axiomatization of ranking functions and supermartingales using corecursive algebras and coalgebraic simulation.

Findings

Provides a categorical characterization of ranking functions.

Extends coalgebraic proof methods to liveness properties.

Bridges the gap between greatest and least fixed-point reasoning in coalgebras.

Abstract

Final coalgebras as "categorical greatest fixed points" play a central role in the theory of coalgebras. Somewhat analogously, most proof methods studied therein have focused on greatest fixed-point properties like safety and bisimilarity. Here we make a step towards categorical proof methods for least fixed-point properties over dynamical systems modeled as coalgebras. Concretely, we seek a categorical axiomatization of well-known proof methods for liveness, namely ranking functions (in nondeterministic settings) and ranking supermartingales (in probabilistic ones). We find an answer in a suitable combination of coalgebraic simulation (studied previously by the authors) and corecursive algebra as a classifier for (non-)well-foundedness.