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

2023/02/10 by Demri, Stephane, Quaas, Karin
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2302.05327

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.

Related

• Model Checking Constraint LTL over Trees
• Alternating Automata on Data Trees and XPath Satisfiability
• The Emptiness Problem for Tree Automata with at Least One Disequality Constraint is NP-hard
• Alternating Nonzero Automata
• Automata for two-variable logic over trees with ordered data values