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
    Published on: May 30, 2025
    Accepted on: March 11, 2025
    Submitted on: February 2, 2024
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 177 times.
    This article's PDF has been downloaded 54 times.