# Categorical Liveness Checking by Corecursive Algebras

arXiv: https://arxiv.org/abs/1704.04872 · HTML: https://mlsanity.com/paper/1704.04872/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Apr 2017.

## Built on by (most cited first, 2 of 2)

- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down](https://mlsanity.com/paper/2105.04817/) (2021)

## Abstract (arXiv)

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.