Model Checking Constraint LTL over Trees
Logic in Computer Science
2015-04-24 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1504.06105,
title = {Model Checking Constraint LTL over Trees},
author = {Alexander Kartzow and Thomas Weidner},
journal= {arXiv preprint arXiv:1504.06105},
year = {2015}
}