基于余递归代数的范畴活性检验
Categorical Liveness Checking by Corecursive Algebras
摘要：
最终余代数作为“范畴最大不动点”在余代数理论中起着核心作用。有些类似的，大多数证明方法研究集中在最大的定点性质，如安全性和双相似性。在这里，我们做了一个步骤，以明确的证明方法至少不动点性质的动力系统建模为余代数。具体而言，我们寻求一个明确的公理化著名的证明方法的活性，即排名功能（在不确定性的设置）和排名上鞅（在概率）。我们找到了一个答案，在一个合适的组合coalgebraic模拟（研究以前的作者）和corecursive代数作为分类（非）良好的基础。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
