一句话：用余递归代数与余代数模拟，统一范畴化活性验证中的 ranking function 与 ranking supermartingale。
在余代数理论中，终结余代数作为“范畴极大不动点”是核心工具，已有证明方法多面向安全性、互模拟等极大不动点性质；相比之下，活性等极小不动点性质的范畴化证明方法仍不充分。本文朝这一方向迈出一步：为非确定系统中的 ranking function 与概率系统中的 ranking supermartingale 这两类经典活性验证方法寻求范畴公理化。作者发现，合适的答案来自余代数模拟与余递归代数的组合，后者可作为（非）良基性的分类器。由此，论文为以余代数建模的动力系统上的活性性质提供了统一的范畴证明框架。
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.