Satisfiability of ECTL* with tree constraints

TL;DR

This paper demonstrates the decidability of satisfiability for ECTL* with constraints over certain tree-like structures using a new model-theoretic approach, while also identifying structures where this approach does not apply.

Contribution

It applies a novel technique to establish decidability of ECTL* satisfiability over semi-linear orders, ordinal trees, and finite-height infinite trees, and shows limitations with infinite trees.

Findings

Decidability of ECTL* satisfiability over semi-linear orders.

Decidability over ordinal trees.

Decidability over finite-height infinite trees.

Abstract

Recently, we have shown that satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathbb{Z}$ is decidable using a new technique. This approach reduces the satisfiability problem of $\mathsf{ECTL}^*$ with constraints over some structure A (or class of structures) to the problem whether A has a certain model theoretic property that we called EHD (for "existence of homomorphisms is decidable"). Here we apply this approach to concrete domains that are tree-like and obtain several results. We show that satisfiability of $\mathsf{ECTL}^*$ with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb{N}$. We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraisse-games for $\mathsf{WMSO}+\mathsf{B}$ (weak $\mathsf{MSO}$ with the bounding quantifier) and use them to show that the infinite (order) tree does not have property EHD. As a consequence, a different approach has to be taken in order to settle the question whether satisfiability of $\mathsf{ECTL}^*$ (or even $\mathsf{LTL}$) with constraints over the infinite (order) tree is decidable.