无限数据树上的约束自动机：从 CTL(Z)/CTL*(Z) 到判定过程
计算机科学中的逻辑
2025-06-25 v7
摘要
我们引入具有 Z 中数据值的树约束自动机类（配备小于关系和到常量的相等谓词），并证明非空性问题为 ExpTime 完全。使用基于自动机的方法，我们确立带 Z 中约束的 CTL（CTL(Z)）的可满足性问题是 ExpTime 完全的，而 CTL*(Z) 的可满足性问题是 2ExpTime 完全的，从而解决了一个长期存在的开放问题（此前仅知可判定性）。我们还简要介绍了其他具体域和其他逻辑（如带具体域的描述逻辑）的附带结果。
引用
@article{arxiv.2302.05327,
title = {Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures},
author = {Stephane Demri and Karin Quaas},
journal= {arXiv preprint arXiv:2302.05327},
year = {2025}
}