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

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 nonemptine…