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