一句话：提出余代数上的一元二阶逻辑，并给出余代数模态 μ-演算恰为其行为不变片段的充分条件。
论文把 Kripke 模型上的标准一元二阶逻辑推广到任意集合函子余代数，研究 MSO 公式在行为等价下的不变性，追问余代数模态 μ-演算是否恰好刻画给定函子的双模拟不变 MSO 片段。作者采用自动机理论技术，证明只需为该类型函子构造“adequate uniform construction”，即可获得这种表达完备性定理。应用包括：给出模态 μ-演算 Janin-Walukiewicz 定理的部分新证明，避免语法范式；导出 bag 函子（分级模态逻辑）与所有指数多项式函子（含 game 函子）的双模拟不变性结果；并进一步证明单调邻域模型上单调模态 μ-演算的刻画定理。
Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the "game functor"). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.Comment: arXiv admin note: substantial text overlap with arXiv:1501.07215
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{EnqvistSV17,
title = {An expressive completeness theorem for coalgebraic modal mu-calculi},
author = {Sebastian Enqvist and Fatemeh Seifan and Yde Venema},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:14)2017}
}