%0 Journal Article
%T Model Checking Constraint LTL over Trees
%A Alexander Kartzow
%A Thomas Weidner
%J Computer Science
%D 2015
%I arXiv
%X Constraint automata are an adaptation of B\"uchi-automata that process data words where the data comes from some relational structure S. Every transition of such an automaton comes with constraints in terms of the relations of S. A transition can only be fired if the current and the next data values satisfy all constraints of this transition. These automata have been used in the setting where S is a linear order for deciding constraint LTL with constraints over S. In this paper, S is the infinitely branching infinite order tree T. We provide a PSPACE algorithm for emptiness of T-constraint automata. This result implies PSPACE-completeness of the satisfiability and the model checking problem for constraint LTL with constraints over T.
%U http://arxiv.org/abs/1504.06105v1