Stephane Demri ; Karin Quaas - Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures

lmcs:12982 - Logical Methods in Computer Science, May 30, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:16)2025
Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision ProceduresArticle

Authors: Stephane Demri ; Karin Quaas

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.


Volume: Volume 21, Issue 2
Secondary volumes: Selected Papers of the 34th International Conference on Concurrency Theory (CONCUR 2023)
Published on: May 30, 2025
Imported on: February 2, 2024
Keywords: Logic in Computer Science

Consultation statistics

This page has been seen 1138 times.
This article's PDF has been downloaded 247 times.