Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
arxiv(2023)
摘要
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.
更多查看译文
关键词
infinite data trees,automata,constraint
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要