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.

翻译：我们引入了数据值域为Z（配备小于关系与常量的等词谓词）的树约束自动机类，并证明了其非空性问题为ExpTime-完全。基于自动机方法，我们确立了CTL(Z)（带Z域约束的CTL）的可满足性问题为ExpTime-完全，而CTL*(Z)的可满足性问题为2ExpTime-完全，从而解决了一个长期未决的开放问题（此前仅知其可判定性）。本文还简要给出了与其他具体域及其他逻辑（如带具体域的描述逻辑）的副产品结果。