一句话：引入整数数据树约束自动机，证明非空性 ExpTime 完全，并判定 CTL(Z)/CTL*(Z) 可满足性。
该文研究带有整数数据值（含小于关系与对常量的相等谓词）的无限数据树上的约束自动机，并给出其非空性问题的 ExpTime 完全性。作者采用基于自动机的方法，将带具体域约束的时序逻辑可满足性归约到这类自动机的非空性判定：证明 CTL(Z) 的可满足性是 ExpTime 完全的，CTL*(Z) 的可满足性是 2ExpTime 完全的，从而解决了长期悬而未决的问题——此前仅知可判定性。论文还简要给出对其他具体域和逻辑（如带具体域的描述逻辑）的副产品结果。
We introduce the class of tree constraint automata with data values in Z (equipped with the less than relation and equality predicates to constants) and we show that the nonemptiness problem is ExpTime-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(Z) (CTL with constraints in Z) is ExpTime-complete and the satisfiability problem for CTL*(Z) is 2ExpTime-complete solving a longstanding open problem (only decidability was known so far). By-product results with other concrete domains and other logics, such as description logics with concrete domains, are also briefly presented.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DemriQ25,
title = {Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures},
author = {Stephane Demri and Karin Quaas},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:16)2025}
}