Model Checking Constraint LTL over Trees

TL;DR

This paper extends the model checking of constraint LTL to infinite trees, providing a PSPACE algorithm for automata emptiness and establishing complexity results for satisfiability and model checking.

Contribution

It introduces a PSPACE algorithm for T-constraint automata emptiness and proves PSPACE-completeness for related satisfiability and model checking problems.

Findings

PSPACE algorithm for T-constraint automata emptiness

PSPACE-completeness of satisfiability over infinite trees

PSPACE-completeness of model checking over infinite trees

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.