关于无限树上一阶逻辑的自动机化表征
计算机科学中的逻辑
2025-09-18 v1 形式语言与自动机理论
摘要
本文研究了在无限树上解释的一阶逻辑（First Order Logic, FO）及其与分支时间逻辑的联系。具体而言，我们提供了 FO 在无限树上解释的自动机理论化表征。为此，引入两种不同的犹豫树自动机类，证明它们恰好捕获两种分支时间逻辑的表达能力，分别为受限制的计数 CTL 带过去（polcCTLp）和计数 CTL* 仅限于有限路径（cCTL*[f]），这两种逻辑此前已被证明等价于 FO 在无限树上。两种自动机表征自然导致两种时间逻辑的标准形式，并凸显了 FO 仅能表达的性质是安全或 co-安全性质的树分支。
引用
@article{arxiv.2509.14090,
title = {An Automaton-based Characterisation 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:2509.14090},
year = {2025}
}
备注
In Proceedings GandALF 2025, arXiv:2509.13258