基于自动机的第一阶逻辑无限树的特征化
计算机科学中的逻辑
2026-04-30 v1 形式语言与自动机理论
摘要
我们研究了第一阶逻辑（FO）在（无序）无限树上的表达力,旨在以分支时间规范形式识别稳健的特征化。虽然线性时间情景下的这种对应关系已广为人知,但分支时间案例面临著已知的结构挑战。为此,我们引入两种犹豫树自动机的类,并展示它们精确地捕获了两种分支时间模态逻辑的表达力,即 PolPCTL 和 CTLsf,这两种逻辑已被证明等价于无限树上的 FO。这些结果提供了统一的自动机论证,并为后者在新的 CTLs 片段中提供了自然的正规形。结果表明,FO 在此情境下的根本局限性:在每条分支上,它只能表达要么安全性要么反安全性的属性,从而揭示了第一阶可定义性在无限树上的尖锐表达边界。
引用
@article{arxiv.2604.26364,
title = {Automaton-based Characterisations of First Order Logic over Infinite Trees},
author = {Massimo Benerecetti and Dario Della Monica and Angelo Matteo and Fabio Mogavero and Gabriele Puppis},
journal= {arXiv preprint arXiv:2604.26364},
year = {2026}
}