paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Topological Mu-Calculus: completeness and decidability

拓扑 μ-演算:完全性与可判定性
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文研究拓扑 μ-演算与关系 μ-演算的完全性、可判定性和有限模型性质,属于纯逻辑与形式语义方向,与用户关注的 PL/AI 静态分析、Agentic 程序、浮点程序分析、贝叶斯程序分析及 LLM 交叉方向几乎没有直接关联。引用 10 inbox
Alexandru Baltag, Nick Bezhanishvili, David Fernandez-Duque
crossref: 2026-09-12

AI 速览

一句话:为拓扑 μ-演算建立完全性、可判定性与有限模型性质,并给出关系 μ-演算自然片段的通用完全性结果。

本文研究拓扑 μ-演算,它同时包含 Cantor 导数和闭包模态。作者在一般拓扑空间以及 T0、TD 空间上证明了该逻辑的完全性、可判定性和有限模型性质;随后研究关系 μ-演算,为关系框架的多种类上的所有自然片段给出通用完全性结果。与多数 μ-演算证明不同,该证明采用模型论方法,创新性地使用模态逻辑中已知的“最终”子模型(canonical model 的 final submodel),从而兼具高度一般性与本质简洁性。

问题
如何为基于 Cantor 导数和闭包模态的拓扑 μ-演算,以及关系 μ-演算的自然片段,建立完全性、可判定性与有限模型性质?
方法
采用模型论证明方法,创新性地利用模态逻辑中 canonical model 的“最终”子模型,统一处理一般拓扑空间、T0/TD 空间及多类关系框架。
评估
论文通过数学证明在一般拓扑空间、T0/TD 空间上建立完全性、可判定性与 FMP,并为关系框架多类上的自然 μ-演算片段给出通用完全性定理。
原文摘要(Abstract)

We study the topological μ-calculus, based on both Cantor derivative and closure modalities, proving completeness, decidability and FMP over general topological spaces, as well as over T0 and TD spaces. We also investigate relational μ-calculus, providing general completeness results for all natural fragments of μ-calculus over many different classes of relational frames. Unlike most other such proofs for μ-calculus, ours is modeltheoretic, making an innovative use of a known Modal Logic method (-the 'final' submodel of the canonical model), that has the twin advantages of great generality and essential simplicity.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot6236,
  title = {The Topological Mu-Calculus: completeness and decidability},
  author = {Alexandru Baltag and Nick Bezhanishvili and David Fernandez-Duque},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470560}
}