Categorical Liveness Checking by Corecursive Algebras
Categorical Liveness Checking by Corecursive Algebras
复制标题
通过核心递归代数进行分类活性检查
DOI：
10.1109/lics.2017.8005151
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Ichiro Hasuo
中科院分区：
文献类型：
--
作者：
Natsuki Urabe;Masaki Hara;Ichiro Hasuo
作为“范畴最大不动点”的终余代数在余代数理论中起着核心作用。在某种程度上类似地，其中研究的大多数证明方法都集中在最大不动点性质上，如安全性和生物相似性。在这里，我们向建立在余代数上的动力系统的最小不动点性质的范畴证明方法迈进了一步。具体地说，我们寻求了著名的活性证明方法的范畴公理化，即排序函数(在不确定设置下)和排序上鞅(在概率设置下)。我们在余代数模拟(作者以前研究过的)和余递归代数的适当组合中找到了答案，作为(非)良基的分类器。
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.