Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
Logic in Computer Science
2025-06-25 v7
Abstract
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.
Keywords
Cite
@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}
}