Completeness of Flat Coalgebraic Fixpoint Logics
Completeness of Flat Coalgebraic Fixpoint Logics
复制标题
DOI：
10.1145/3157055
复制
发表时间：
2018-01
期刊：
影响因子：
--
通讯作者：
Lutz Schröder;Y. Venema
中科院分区：
文献类型：
--
作者：
Lutz Schröder;Y. Venema
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性方面。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的不动点逻辑倾向于用表达性换取简单性和可读性，事实上，它们经常存在于μ演算的单变量片段中。这种平坦定点逻辑的家族包括，例如，线性时态逻辑（LTL）、计算树逻辑（CTL）和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算的平坦片段（如交替时间时序逻辑），以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The μ-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics tend to trade expressivity for simplicity and readability and in fact often live within the single variable fragment of the μ-calculus. The family of such flat fixpoint logics includes, e.g., Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and the logic of common knowledge. Extending this notion to the generic semantic framework of coalgebraic logic enables covering a wide range of logics beyond the standard μ-calculus including, e.g., flat fragments of the graded μ-calculus and the alternating-time μ-calculus (such as alternating-time temporal logic), as well as probabilistic and monotone fixpoint logics. We give a generic proof of completeness of the Kozen-Park axiomatization for such flat coalgebraic fixpoint logics.