# Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures

arXiv: https://arxiv.org/abs/2302.05327 · HTML: https://mlsanity.com/paper/2302.05327/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Feb 2023.

## Built on by (most cited first, 1 of 1)

- [Robustness of Constraint Automata for Description Logics with Concrete Domains](https://mlsanity.com/paper/2601.19644/) (2026)

## Abstract (arXiv)

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.