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

TL;DR

This paper introduces tree constraint automata with data in Z and demonstrates their nonemptiness problem is ExpTime-complete, leading to decidability results for CTL(Z) and CTL*(Z) satisfiability problems, resolving longstanding open questions.

Contribution

The paper establishes the complexity and decidability of satisfiability for CTL(Z) and CTL*(Z) using automata-based methods, extending the understanding of logics with data constraints.

Findings

Nonemptiness of tree constraint automata in Z is ExpTime-complete.

Satisfiability for CTL(Z) is ExpTime-complete.

Satisfiability for CTL*(Z) is 2ExpTime-complete.

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.