树代数与有限图上的互模拟不变 MSO
计算机科学中的逻辑
2025-02-05 v4
摘要
我们证明了，在有限迁移系统上，MSO 的互模拟不变片段在表达力上等价于模态 μ-演算，这是一个几十年来悬而未决的问题。证明过程将该问题转化为一个代数框架，并表明被其零类和一类型为有限的有限树代数识别的正则树语言是正则的，即可以在 μ-演算中表达。这对于树而言，对应于 Wilke 代数到无限词上的 ω-半群的关键翻译的一种弱形式，并且也是无限树正则语言代数理论中缺失了二十年的一个环节。
引用
@article{arxiv.2407.12677,
title = {Tree algebras and bisimulation-invariant MSO on finite graphs},
author = {Thomas Colcombet and Amina Doumane and Denis Kuperberg},
journal= {arXiv preprint arXiv:2407.12677},
year = {2025}
}