# Constraint Automata on Infinite Data Trees: from CTL() / CTL*() to Decision Procedures

Stéphane Demri, Karin Quaas

► To cite this version:

Stéphane Demri, Karin Quaas. Constraint Automata on Infinite Data Trees: from CTL() / CTL*() to Decision Procedures. 34th International Conference on Concurrency Theory (CONCUR 2023), Sep 2023, Antwerp, Belgium. 10.4230/LIPIcs.CONCUR.2023.29 . hal-04201369

HAL Id: hal-04201369

https://hal.science/hal-04201369v1

Submitted on 28 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Constraint Automata on Infinite Data Trees: From CTL($\mathbb{Z}$)/CTL*(Z) To Decision Procedures

Stéphane Demri

Université Paris-Saclay, LMF, CNRS, ENS Paris-Saclay, France

Karin Quaas<fnref n="1" />

Universität Leipzig, Fakultät für Mathematik und Informatik, Germany

## Abstract

We introduce the class of tree constraint automata with data values in $\mathbb{Z}$ (equipped with the less than relation and equality predicates to constants), and we show that the nonemptiness problem is EXPTIME-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL($\mathbb{Z}$) (CTL with constraints in $\mathbb{Z}$) is EXPTIME-complete, and the satisfiability problem for CTL*(Z) is 2EXPTIME-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed.

2012 ACM Subject Classification Theory of computation → Logic and verification

Keywords and phrases Constraints, Constraint Automata, Temporal Logics, Infinite Data Trees

Digital Object Identifier 10.4230/LIPIcs.CONCUR.2023.29

## 1 Introduction

In this paper, we study the satisfiability problem for the branching-time temporal logics CTL($\mathbb{Z}$) and CTL*(Z), extending the classical temporal logics CTL and CTL* in that atomic formulae express constraints about the relational structure ($\mathbb{Z}$, <, =, (=$_0$)$_{\partial \in \mathbb{Z}$}). Formulae in these logics are interpreted over Kripke structures that are annotated with values in $\mathbb{Z}$. A typical CTL*(Z) formula is the formula AGF($x < Xx$) stating that on all paths infinitely often the value of the variable x at the current position is strictly smaller than the value of x at the next position. Formalisms defined over relational structures, also known as concrete domains, are considered in many works, including works on temporal logics [40, 13, 54, 48, 19, 35], description logics [50, 51, 52, 53, 16, 45, 3], and automata [38, 61, 43, 71, 65, 57]. Combining reasoning in your favourite logic with reasoning in a relevant concrete domain reveals to be essential for numerous applications, for instance for reasoning about ontologies, see e.g. [52, 46], or data-aware systems, see e.g. [28, 34]. A brief survey can be found in [26].

Decidability results for concrete domains handled in [53, 38, 3] exclude the ubiquitous concrete domain ($\mathbb{Z}$, <, =, (=$_0$)$_{\partial \in \mathbb{Z}$}). By contrast, decidability results for logics with concrete domain $\mathbb{Z}$ require dedicated proof techniques, see e.g. [11, 23, 61, 46]. In particular, fragments of CTL*(Z) are shown decidable in [11] using integral relational automata from [17], and the satisfiability problem for existential and universal CTL* with gap-order constraints (more general than the ones in this paper) can be solved in PSPACE [12, Theorem 14]. Another important breakthrough came with the decidability of CTL*(Z) [15, Theorem 32] (see also [14]) by designing a reduction to a decidable second-order logic, whose formulae are made of Boolean combinations of formulae from MSO and from WMSO+U [10], where U is the unbounding second-order quantifier, see e.g. [8, 9]. This is all the more remarkable as the decidability result is part of a powerful general approach [15], but no sharp complexity upper bound can be inferred. More recently, the condition $C_Z$ [23] to approximate the set

<figure><img src="image_2.png" /></figure>

<footnote n="1">¹ Supported by the Deutsche Forschungsgemeinschaft (DFG), project 504343613.</footnote>
## 29:2 Constraint Automata on Infinite Data Trees

of satisfiable symbolic models of a given LTL($\mathbb{Z}$) formula is extended to the branching case in [46] leading to the EXPTIME-easiness of a major reasoning task for the description logic $ALCF^P(\mathbb{Z}_c)$. However, no elementary complexity upper bounds for the satisfiability problem for CTL($\mathbb{Z}$) nor CTL\*(Z) were known since their decidability was established in [13, 15].

In this paper, we prove that the satisfiability problem for CTL($\mathbb{Z}$) is EXPTIME-complete, and the satisfiability problem for CTL\*(Z) is 2EXPTIME-complete. We pursue the automata-based approach for solving decision problems for temporal logics, following seminal works for temporal logics, see e.g. [68, 69, 44]. This popular approach consists of reducing logical problems (satisfiability, model-checking) to automata-based decision problems while taking advantage of existing results and decision procedures from automata theory, see e.g. [67].

It is well-known that decision procedures for CTL\* are difficult to design, and the combination with the concrete domain $\mathbb{Z}$ is definitely challenging. Moreover, we aim at proposing a general framework: we do not wish for every new logic with concrete domain to study again and again what is the proper way to define products of automata leading to optimal complexity. That is why our main goal in this work is to investigate a new class of tree constraint automata, understood as a target formalism in the pure tradition of the automata-based approach, and easy to reuse. The structures accepted by such tree constraint automata are infinite trees in which nodes are labelled by a letter from a finite alphabet and a tuple in $\mathbb{Z}^\beta$ for some $\beta \ge 1$ (this excludes the automata designed in [36, 37] dedicated to finite trees where no predicate $<$ is involved). Decision problems for alternating automata over infinite alphabets are often undecidable, see e.g. [56, 47, 25, 41], and therefore we advocate the introduction of nondeterministic constraint automata without alternation. Our definition of tree constraint automata naturally extends the definition of constraint automata for words (see e.g. [17, 59, 61, 43, 57]) and as far as we know, the extension to infinite trees in the way done herein has not been considered earlier in the literature.

As a key result, we show that the nonemptiness problem for tree constraint automata over $(\mathbb{Z}, <, =, (\text{=}\delta)_{\delta\in\mathbb{Z}})$ is EXPTIME-complete. In order to obtain the EXPTIME upper bound, we adapt results from [46, 45] (originally expressed in the context of interpretations for description logics) and we take advantage of several automata-based constructions for Rabin/Streett tree automata. As a corollary, we establish that the satisfiability problem for CTL($\mathbb{Z}$) is EXPTIME-complete (Theorem 14), which is one of the main results of the paper. As a by-product, it also allows us to conclude that the concept satisfiability problem w.r.t. general TBoxes for $ALCF^P(\mathbb{Z}_c)$ is in EXPTIME, a result known since [46].

Our main contribution is the characterisation of the complexity for CTL\*(Z) satisfiability, which is an open problem evoked in [15, Section 9] and [46, Section 5] (decidability was established ten years ago in [14]). In Section 6, we show that the satisfiability problem for CTL\*(Z) is in 2EXPTIME by using Rabin tree constraint automata (introduced herein). We have to check that the essential steps for CTL\* can be lifted to CTL\*(Z) to get the optimal upper bound. In general, our contributions stem from the cross-fertilisation of automata-based techniques for temporal logics and reasoning about (infinite) structures made of Z-constraints.

A complete version with all the proofs can be found in [27].

# 2 Temporal Logics with Numerical Domains

## 2.1 Concrete Domain $(\mathbb{Z}, <, =, (\text{=}\delta)_{\delta\in\mathbb{Z}})$ and Kripke Structures

In the sequel, we consider the concrete domain $(\mathbb{Z}, <, =, (\text{=}\delta)_{\delta\in\mathbb{Z}})$ (also written $\mathbb{Z}$), where $\text{=}\delta$ is a unary predicate stating the equality with the constant $\delta$ and, $<$ and $=$ are the usual
relations on $\mathbb{Z}$. Let VAR = {$x, y, ...$} be a countably infinite set of variables. A term $t$ over VAR is an expression of the form $X^i x$, where $x \in$ VAR and $X^i$ is a (possibly empty) sequence of $i$ symbols 'X'. A term $X^i x$ should be understood as a variable (that needs to be interpreted) but, later on, we will see that the prefix $X^i$ will have a temporal interpretation. We write $T_{VAR}$ to denote the set of all terms over VAR. For all $i \in \mathbb{N}$, we write $T_{VAR}^{\leq i}$ to denote the subset of terms of the form $X^j x$, where $j \leq i$. For instance, $T_{VAR}^{\leq 0} =$ VAR. An atomic constraint $\theta$ over $T_{VAR}$ is an expression of one of the forms below:

$$t < t' \quad t = t' \quad =_\mathfrak{o}(t) \quad (\text{also written } t = \mathfrak{o}),$$

where $\mathfrak{o} \in \mathbb{Z}$ and $t, t' \in T_{VAR}$. A constraint $\Theta$ is defined as a Boolean combination of atomic constraints. Constraints are interpreted on valuations $v : T_{VAR} \to \mathbb{Z}$ that assign elements from $\mathbb{Z}$ to the terms in $T_{VAR}$, so that $v$ satisfies $\theta$, written $v \models \theta$, if and only if, the interpretation of the terms in $\theta$ makes $\theta$ true in $\mathbb{Z}$ in the usual way. The Boolean connectives are interpreted as usual. A constraint $\Theta$ is satisfiable $\iff$ there is a valuation $v : T_{VAR} \to \mathbb{Z}$ such that $v \models \Theta$. Similarly, a constraint $\Theta_1$ entails a constraint $\Theta_2$ (written $\Theta_1 \models \Theta_2$) $\iff$ for all valuations $v$, we have $v \models \Theta_1$ implies $v \models \Theta_2$. The satisfiability problem restricted to finite conjunctions of atomic constraints can be solved in PTIME (see e.g. [17, Lemma 5.5]) and entailment is in coNP. In the sequel, quite often, the valuations $v$ are of the form $\{x_1, ..., x_\beta\} \to \mathbb{Z}$ when we are only interested in the values for the variables in $\{x_1, ..., x_\beta\}$.

**Kripke structures.** In order to define logics with the concrete domain $\mathbb{Z}$, the semantical structures of such logics are enriched with valuations that interpret the variables by elements in $\mathbb{Z}$. A $\mathbb{Z}$-decorated Kripke structure (or Kripke structure for short) $\mathcal{K}$ is a triple $(\mathcal{W}, \mathcal{R}, v)$, where $\mathcal{W}$ is a non-empty set of worlds, $\mathcal{R} \subseteq \mathcal{W} \times \mathcal{W}$ is the accessibility relation and $v : \mathcal{W} \times \mathcal{VAR} \to \mathbb{Z}$ is a valuation function. A Kripke structure $\mathcal{K}$ is total whenever for all $w \in \mathcal{W}$, there is $w' \in \mathcal{W}$ such that $(w, w') \in \mathcal{R}$. Given a Kripke structure $\mathcal{K} = (\mathcal{W}, \mathcal{R}, v)$ and a world $w \in \mathcal{W}$, an infinite path $\pi$ from $w$ is an $\omega$-sequence $w_0, w_1 ... w_n, ...$ such that $w_0 = w$ and for all $i \in \mathbb{N}$, we have $(w_i, w_{i+1}) \in \mathcal{R}$. Finite paths are defined accordingly.

**Labelled trees.** Given $D \geq 1$, a labelled tree of degree $D$ is a map $\mathfrak{t} : dom(\mathfrak{t}) \to \Sigma$ where $\Sigma$ is some (potentially infinite) alphabet and $dom(\mathfrak{t})$ is an infinite subset of $[0, D-1]*$ such that $n \in dom(\mathfrak{t})$ and $n \cdot i \in dom(\mathfrak{t})$ for all $0 \leq i < j$ whenever $n \cdot j \in dom(\mathfrak{t})$ for some $n \in [0, D-1]*$ and $j \in [0, D-1]$. The elements of $dom(\mathfrak{t})$ are called nodes. The empty word $\varepsilon$ is the root node of $\mathfrak{t}$. For every $n \in dom(\mathfrak{t})$, the elements $n \cdot i$ ($i \in [0, D-1]$) are called the children nodes of $n$, and $n$ is called the parent node of $n \cdot i$. We say that the tree $\mathfrak{t}$ is a full $D$-ary tree if every node $n$ has exactly $D$ children $n \cdot 0, ..., n \cdot (D-1)$. Given a tree $\mathfrak{t}$ and a node $n$ in $dom(\mathfrak{t})$, an infinite path in $\mathfrak{t}$ starting from $n$ is an infinite sequence $n \cdot j_1 \cdot j_2 \cdot j_3 ...$, where $j_i \in [0, D-1]$ and $n \cdot j_1 ... j_i \in dom(\mathfrak{t})$ for all $i \geq 1$.

A tree Kripke structure $\mathcal{K}$ is a Kripke structure $(\mathcal{W}, \mathcal{R}, v)$ such that $(\mathcal{W}, \mathcal{R})$ is a tree (not necessarily a full $D$-ary tree). Tree Kripke structures $(\mathcal{W}, \mathcal{R}, v)$ such that $(\mathcal{W}, \mathcal{R})$ is isomorphic to the tree induced by $[0, D-1]*$ are represented by maps of the form $\mathfrak{t} : [0, D-1]* \to \mathbb{Z}^\beta$. This assumes that we only care about the value of the variables $x_1, ..., x_\beta$ and $\mathfrak{t}(n) = (\mathfrak{o}_1, ..., \mathfrak{o}_\beta)$ encodes that for all $i \in [1, \beta]$, we have $v(n, x_i) = \mathfrak{o}_i$.

## 2.2 The Logic CTL\*(Z)

We introduce the logic CTL\*(Z) extending the temporal logic CTL\* from [29] but with constraints over $\mathbb{Z}$. State formulae $\phi$ and path formulae $\Phi$ of CTL\*(Z) are defined below

$$\phi := \neg \phi \mid \phi \wedge \phi \mid E \Phi \quad \Phi := \phi \mid t = \mathfrak{o} \mid t_1 = t_2 \mid t_1 < t_2 \mid \neg \Phi \mid \Phi \wedge \Phi \mid X \Phi \mid \Phi U \Phi,$$

where $t, t_1, t_2 \in T_{VAR}$. The size of a formula is understood as its number of symbols with integers encoded with a binary representation. We use also the universal path quantifier $\mathcal{A}$
## 29:4 Constraint Automata on Infinite Data Trees

and the standard temporal connectives $R$ and $G$ ($A\Phi \stackrel{\text{def}}{=} \neg E \neg \Phi$, $\Phi_1 R \Phi_2 \stackrel{\text{def}}{=} \neg(\neg \Phi_1 U \neg \Phi_2)$, and $G\Phi \stackrel{\text{def}}{=} \bot R \Phi$ with $\bot$ equal to $E(x < x)$). No propositional variables occur in $CTL^*(\mathbb{Z})$ formulae, but it is easy to simulate them with atomic formulae of the form $E(x = 0)$. We say that a formula in $CTL^*(\mathbb{Z})$ is in simple form if it is in negation normal form (using $A, R$ and $\vee$ as primitive) and all terms occurring in the formula are from $T_{\text{VAR}}^{\le 1}$. State formulae are interpreted on worlds from a Kripke structure, whereas path formulae are interpreted on infinite paths. The two satisfaction relations are defined as follows (we omit the clauses for Boolean connectives), where $\mathcal{K} = (\mathcal{W}, \mathcal{R}, \mathfrak{v})$ is a total Kripke structure, and $w \in \mathcal{W}$.

■ $\mathcal{K}, w \models E\Phi \stackrel{\text{def}}{\Leftrightarrow}$ there is an infinite path $\pi$ from $w$ such that $\mathcal{K}, \pi \models \Phi$.

Let $\pi = w_0, w_1, \dots$ be an infinite path of $\mathcal{K}$. Let us define $\mathfrak{v}(\pi, X^j x) \stackrel{\text{def}}{=} \mathfrak{v}(w_j, x)$, for all terms of the form $X^j x$. For every $n, \pi[n, +\infty)$ is the suffix of $\pi$ truncated by the $n$ first worlds.

■ $\mathcal{K}, \pi \models t = \mathfrak{o} \stackrel{\text{def}}{\Leftrightarrow} \mathfrak{v}(\pi, t) = \mathfrak{o}$; $\mathcal{K}, \pi \models t_1 \sim t_2 \stackrel{\text{def}}{\Leftrightarrow} \mathfrak{v}(\pi, t_1) \sim \mathfrak{v}(\pi, t_2)$ for all $\sim \in \{<, =\}$,

■ $\mathcal{K}, \pi \models \Phi U \Psi \stackrel{\text{def}}{\Leftrightarrow}$ there is $j \ge 0$ such that $\mathcal{K}, \pi[j, +\infty) \models \Psi$ and for all $j' \in [0, j-1]$, we have $\mathcal{K}, \pi[j', +\infty) \models \Phi$;

■ $\mathcal{K}, \pi \models X\Phi \stackrel{\text{def}}{\Leftrightarrow} \mathcal{K}, \pi[1, +\infty) \models \Phi$.

Let us define two fragments of $CTL^*(\mathbb{Z})$. Formulae in the logic $CTL(\mathbb{Z})$ are of the form

$$ \phi := E \Theta \mid A \Theta \mid \neg \phi \mid \phi \wedge \phi \mid \phi \vee \phi \mid EX\phi \mid E\phi U\phi \mid E\phi R\phi \mid AX\phi \mid A\phi U\phi \mid A\phi R\phi, $$

where $\Theta$ is a constraint. LTL($\mathbb{Z}$) formulae are defined from path formulae for $CTL^*(\mathbb{Z})$ according to $\Phi := \Theta \mid \Phi \wedge \Phi \mid \Phi \vee \Phi \mid X\Phi \mid \Phi U\Phi \mid \Phi R\Phi$, where $\Theta$ is a constraint. Negation occurs only in constraints since the LTL logical connectives have their dual in LTL($\mathbb{Z}$). In contrast to $CTL^*(\mathbb{Z})$ and $CTL(\mathbb{Z})$, LTL($\mathbb{Z}$) formulae are evaluated over infinite paths of valuations $\mathfrak{v}: \text{VAR} \to \mathbb{Z}$ (no branching involved).

The satisfiability problem for $CTL^*(\mathbb{Z})$, written $SAT(CTL^*(\mathbb{Z}))$, is defined as follows.
**Input:** A $CTL^*(\mathbb{Z})$ state formula $\phi$.

**Question:** Is there a total Kripke structure $\mathcal{K}$ and a world $w$ such that $\mathcal{K}, w \models \phi$?

The satisfiability problem $SAT(CTL(\mathbb{Z}))$ for $CTL(\mathbb{Z})$ is defined analogously; for $LTL(\mathbb{Z})$, $SAT(LTL(\mathbb{Z}))$ is the problem to decide whether there exists an infinite sequence of valuations $\mathfrak{v}: \text{VAR} \to \mathbb{Z}$ for a given $LTL(\mathbb{Z})$ formula $\Phi$.

Decidability, and, more precisely, PSPACE-completeness of $SAT(LTL(\mathbb{Z}))$ is shown in [24]. For some strict fragments of $CTL^*(\mathbb{Z})$, decidability is shown in [11, 12]. It is only recently in [14, 13, 15], that decidability is established for the full logic using a translation into a decidable second-order logic:

**Proposition 1** ([14, 15]). $SAT(CTL^*(\mathbb{Z}))$ is decidable.

The proof in [14, 15] does not provide a complexity upper bound as the target decidable 2nd-order logic admits an automata-based decision procedure with open complexity [10, 8, 9].

Let us shortly explain why the satisfiability problem is challenging. First of all, observe that $CTL^*(\mathbb{Z})$ has atomic formulae in which integer values at the current and successor states are compared. This prevents us from using a simple translation from $CTL^*(\mathbb{Z})$ to $CTL^*$ with new propositions. Models of $CTL^*(\mathbb{Z})$ formulae can be viewed as an infinite network of constraints on $\mathbb{Z}$; even if a formula contains only a finite set of constants, a model may contain an infinite set of values, as it is the case for, e.g., the formula $EG(x < Xx)$. Hence a direct Boolean abstraction does not work. On the other hand, $CTL^*(\mathbb{Z})$ has no freeze quantifier and no data variable quantification, and hence no way to directly compare values at unbounded distance (but this can only be done by propagating local constraints), unlike e.g. the formalisms in [21, 63, 5, 1]. Hence, the lower bounds from [42] cannot apply either.

A problem related to satisfiability is the *model-checking problem*. Fragments of the *model-checking problem* involving a temporal logic similar to $CTL^*(\mathbb{Z})$ are investigated
in [17, 11, 12, 34] (see also [39, 20, 70, 2]). However, model-checking problems with CTL\*(Z)-like languages are easily undecidable, see e.g. [17, Theorem 1] and [54, Theorem 4.1] (more general constraints are used in [54] but undecidability proof uses only the constraints involved herein). The difference between model-checking and satisfiability is subtle and underlines that decidability/complexity of CTL(Z)/CTL\*(Z) satisfiability is not immediate.

In this paper, we prove the precise computational complexity of SAT(CTL\*(Z)) and SAT(CTL(Z)). We follow the automata-based approach, that is, we translate formulae in our logics into equivalent automata – tree constraint automata for CTL(Z), and Rabin tree constraint automata for CTL\*(Z) – so that we can reduce the satisfiability problem for the logics to the nonemptiness problem for the corresponding automata.

## 3 Tree Constraint Automata

In this section, we introduce the class of tree constraint automata that accept sets of infinite trees of the form $\mathfrak{t} : [0, D-1]^* \to (\Sigma \times \mathbb{Z}^\beta)$ for some finite alphabet $\Sigma$ and some $\beta \ge 1$. The transition relation of such automata states constraints between the $\beta$ integer values at a node and the integer values at its children nodes. The acceptance condition is a Büchi condition (applied to the infinite branches of the input tree), but this can be easily extended to more general conditions (which we already consider by the end of this section). Moreover, our definition is specific to the concrete domain $\mathbb{Z}$ but it can be easily adapted to other concrete domains. Formally, a tree constraint automaton (TCA, for short) is a tuple $\mathcal{A} = (Q, \Sigma, D, \beta, Q_{\text{in}}, \delta, F)$, where

- $Q$ is a finite set of locations; $\Sigma$ is a finite alphabet,

- $D \ge 1$ is the (branching) degree of (the trees accepted by) $\mathcal{A}$,

- $\beta \ge 1$ is the number of variables (a.k.a. registers),

- $Q_{\text{in}} \subseteq Q$ is the set of initial locations; $F \subseteq Q$ encodes the Büchi acceptance condition,

- $\delta$ is a finite subset of $Q \times \Sigma \times (\text{TreeCons}(\beta) \times Q)^D$, the transition relation. Here, $\text{TreeCons}(\beta)$ denotes the constraints (Boolean combinations of atomic constraints) built over the terms $\mathbf{x}_1, \dots, \mathbf{x}_\beta, \mathbf{x}'_1, \dots, \mathbf{x}'_\beta$, where $\mathbf{x}'_i$ denotes the term $\mathbf{X}\mathbf{x}_i$. $\delta$ consists of tuples $(q, \mathbf{a}, (\Theta_0, q_0), \dots, (\Theta_{D-1}, q_{D-1}))$, where $q \in Q$ is called the source location, $q_0, \dots, q_{D-1} \in Q$, $\mathbf{a} \in \Sigma$, and $\Theta_0, \dots, \Theta_{D-1}$ are constraints.

**Runs.** Let $\mathfrak{t} : [0, D-1]^* \to (\Sigma \times \mathbb{Z}^\beta)$ be an infinite full $D$-ary tree over $\Sigma \times \mathbb{Z}^\beta$. A run of $\mathcal{A}$ on $\mathfrak{t}$ is a mapping $\rho : [0, D-1]^* \to \delta$ satisfying the following conditions:

- $\rho(\varepsilon) = (q_{\text{in}}, \dots)$ such that $q_{\text{in}} \in Q_{\text{in}}$;

- for every $\mathbf{n} \in [0, D-1]^*$ with $\rho(\mathbf{n}) = (q, \mathbf{a}, (\Theta_0, q_0), \dots, (\Theta_{D-1}, q_{D-1}))$, $\mathfrak{t}(\mathbf{n} \cdot i) = (a_i, z_i)$, and $\rho(\mathbf{n} \cdot i)$ starts by the location $q_i$ for all $0 \le i < D$, we have $\mathfrak{t}(\mathbf{n})$ of the form $(\mathbf{a}, \mathbf{z})$ and $\mathbb{Z} \models \Theta_i(\mathbf{z}, z_i)$ for all $0 \le i < D$. Here, $\mathbb{Z} \models \Theta_i(\mathbf{z}, z_i)$ is a shortcut for $[\mathbf{x} \leftarrow \mathbf{z}, \mathbf{x}' \leftarrow z_i] \models \Theta_i$ where $[\mathbf{x} \leftarrow \mathbf{z}, \mathbf{x}' \leftarrow z_i]$ is a valuation $\mathfrak{v}$ on the variables $\{\mathbf{x}_j, \mathbf{x}'_j \mid j \in [1, \beta]\}$ with $\mathfrak{v}(\mathbf{x}_j) = z_j$ and $\mathfrak{v}(\mathbf{x}'_j) = z_i$ for all $j \in [1, \beta]$.

We show an example of a run $\rho$ on $\mathfrak{t}$ in Figure 1. Suppose $\rho$ is a run of $\mathcal{A}$. Given a path $\pi = j_1 \cdot j_2 \cdot j_3 \dots$ in $\rho$ starting from $\varepsilon$, we define $\text{inf}(\rho, \pi)$ to be the set of locations that appear infinitely often as the source locations of the transitions in $\rho(\varepsilon)\rho(j_1)\rho(j_1 \cdot j_2)\rho(j_1 \cdot j_2 \cdot j_3)\dots$. A run $\rho$ is *accepting* if for all paths $\pi$ in $\rho$ starting from $\varepsilon$, we have $\text{inf}(\rho, \pi) \cap F \ne \emptyset$. We write $L(\mathcal{A})$ to denote the set of trees $\mathfrak{t}$ that admit an accepting run.

**Nonemptiness problem.** As usual, the nonemptiness problem for TCA asks whether a TCA $\mathcal{A}$ satisfies $L(\mathcal{A}) \ne \emptyset$. To define the size of $\mathcal{A}$ in a reasonably succinct encoding, we need to consider the size of constraints from $\text{TreeCons}(\beta)$. Indeed, unlike (plain) Büchi tree automata [68], the number of transitions in a tree constraint automaton is a priori unbounded
## 29:6 Constraint Automata on Infinite Data Trees

(TreeCons($\beta$) is infinite) and the maximal size of a constraint occurring in transitions is unbounded too. In particular, this means that $\text{card}(\delta)$ is a priori unbounded, even if $Q$ and $\Sigma$ are fixed. We write $\mathsf{MCS}(\mathsf{A})$ to denote the maximal size of a constraint occurring in $\mathsf{A}$ (with binary encoding of the integers). The complexity of the nonemptiness problem should take into account these parameters. Note also that our automaton model differs from the Presburger Büchi tree automata from [62, 6] for which, in the runs, arithmetical expressions are related to constraints between numbers of children labelled by different locations. Herein, the arithmetical expressions state constraints between integer values.

Next, we introduce a variant of TCA by considering the Rabin acceptance condition (as opposed to the Büchi acceptance condition). A Rabin tree constraint automaton (Rabin TCA, for short) is a tuple $\mathsf{A} = (Q, \Sigma, D, \beta, Q_{\text{in}}, \delta, \mathcal{F})$ defined as for TCA except that $\mathcal{F}$ is a set of pairs of the form $(L, U)$, where $L, U \subseteq Q$. All the definitions about TCA apply except that a run $\rho: [0, D-1]^* \to \delta$ is accepting iff for all paths $\pi$ in $\rho$ starting from $\varepsilon$, there is some $(L, U) \in \mathcal{F}$ such that $\inf(\rho, \pi) \cap L \neq \emptyset$ and $\inf(\rho, \pi) \cap U = \emptyset$.

**Finite alphabet.** The set $\Sigma$ in data trees $\mathfrak{t}: [0, D-1]^* \to (\Sigma \times \mathbb{Z}^\beta)$ plays no specific role herein, especially that it could be encoded with simple constraints of the form $x^* = \mathfrak{d}$, where $x^*$ is a distinguished variables. Its inclusion is more handy when the logical atomic formulae include constraints on variables and propositional variables, as done in [27, Section 5.2] dedicated to description logics (developments on description logics are very little in this paper, due to lack of space).

## 4 Complexity of the Nonemptiness Problem for TCA

This section is dedicated to prove the $\text{ExpTIME}$-completeness of the nonemptiness problem for TCA (Theorem 11) and Rabin TCA (Theorem 13) (we make a distinction between TCA and Rabin TCA because the complexity bounds differ slightly, see Lemma 10 and Lemma 12). Before we prove the $\text{ExpTIME}$ upper bound, let us drop a few words on the lower bound. We show $\text{ExpTIME}$-hardness of the nonemptiness problem for TCA by reduction from the acceptance problem for alternating Turing machines running in polynomial space, see e.g. [18, Corollary 3.6]. Indeed, the polynomial-space tape using a finite alphabet $\Sigma$ can be encoded by a polynomial amount of variables taking values in $[1, \text{card}(\Sigma)]$, details can be found in [27, Section 4.1]. $\text{ExpTIME}$-hardness for Rabin TCA follows, as every TCA with set $F$ of accepting locations can be encoded as a Rabin TCA with a single Rabin pair $(F, \emptyset)$.

The proof of the $\text{ExpTIME}$ upper bound is divided into two parts. In order to determine whether $L(\mathsf{A})$ is nonempty for a given TCA $\mathsf{A}$, we first reduce the existence of some tree $\mathfrak{t} \in L(\mathsf{A})$ to the existence of some *regular symbolic tree* that is *satisfiable*, that is, it admits a concrete model (Sections 4.1 and 4.2). Second, we characterise the complexity of determining the existence of such satisfiable regular symbolic trees (Section 4.3). The result for Rabin TCA is presented in Section 4.4.

From now on, we assume a fixed TCA $\mathsf{A} = (Q, \Sigma, D, \beta, Q_{\text{in}}, \delta, F)$ with the constants $\mathfrak{d}_1, \dots, \mathfrak{d}_\alpha$ occurring in $\mathsf{A}$ such that $\mathfrak{d}_1 < \dots < \mathfrak{d}_\alpha$ (we assume there is at least one constant).

### 4.1 Symbolic Trees

A type over the variables $z_1, \dots, z_n$ is an expression of the form

$$ (\bigwedge_i \Theta_i^{\text{CST}}) \wedge (\bigwedge_{i<j} z_i \sim_{i,j} z_j), \text{ where} $$

for all $i \in [1, n]$, $\Theta_i^{\text{CST}}$ is equal to either $z_i < \mathfrak{d}_1$, or $z_i > \mathfrak{d}_\alpha$ or $z_i = \mathfrak{d}$ for some $\mathfrak{d} \in [\mathfrak{d}_1, \mathfrak{d}_\alpha]$. This definition goes a bit beyond the constraint language in $\mathbb{Z}$ (because of expressions of
<figure><img src="image_3.png" /><figcaption>■ **Figure 1** A tree $\mathfrak{t}$ (middle), a run $\rho$ of some TCA on $\mathfrak{t}$ (left), where, $T_a = (q, \mathbf{a}, (\Theta_0, q), (\Theta_1, q))$ and $T_b = (q, \mathbf{b}, (\Theta_0, q), (\Theta_1, q))$, and the symbolic tree $t_{\mathfrak{t}}$ (abstraction of $\mathfrak{t}$) (right).</figcaption></figure>

the form $z_i < \mathfrak{d}_1$ and $z_i > \mathfrak{d}_\alpha$), but this is harmless in the sequel. What really matters in a type is the way the variables are compared to each other and to the constants.

273 $\sim_{i,j} \{>,=,<\}$ for all $i < j$.

274 Checking the satisfiability of a type can be done in polynomial-time, based on a standard cycle detection, see e.g. [17, Lemma 5.5]. The set of satisfiable types built over the variables $\mathbf{x}_1, \dots, \mathbf{x}_\beta, \mathbf{x}'_1, \dots, \mathbf{x}'_\beta$ is written $\text{SatTypes}(\beta)$ ($n$ above is equal here to $2\beta$). Observe that $\text{card}(\text{SatTypes}(\beta)) \le ((\mathfrak{d}_\alpha - \mathfrak{d}_1) + 3)^{2\beta} \times 3^{\beta^2}$. The restriction of the type $\Theta$ to some set of variables $X \subseteq \{\mathbf{x}_i, \mathbf{x}'_i \mid i \in [1, \beta]\}$ is made of all the conjuncts in which only variables in $X$ occur. The type $\Theta$ restricted to $\{\mathbf{x}'_i \mid i \in [1, \beta]\}$ agrees with the type $\Theta'$ restricted to $\{\mathbf{x}_i \mid i \in [1, \beta]\}$ iff $\Theta$ and $\Theta'$ are logically equivalent modulo the renaming for which $\mathbf{x}_i$ and $\mathbf{x}'_i$ are substituted, for all $i \in [1, \beta]$. For instance, in Figure 1, $\Theta$ restricted to $\{\mathbf{x}'_1, \mathbf{x}'_2\}$ agrees with $\Theta_0$ restricted to $\{\mathbf{x}_1, \mathbf{x}_2\}$. The main properties we use about satisfiable types are stated below.

284 (I) Let $z, z' \in \mathbb{Z}^\beta$. There is a unique $\Theta \in \text{SatTypes}(\beta)$ such that $\mathbb{Z} \models \Theta(z, z')$.

285 (II) For every constraint $\Theta$ built over the variables $\mathbf{x}_1, \dots, \mathbf{x}_\beta, \mathbf{x}'_1, \dots, \mathbf{x}'_\beta$ and the constants $\mathfrak{d}_1, \dots, \mathfrak{d}_\alpha$ there is a disjunction $\Theta_1 \lor \dots \lor \Theta_\gamma$ logically equivalent to $\Theta$ and each $\Theta_i$ belongs to $\text{SatTypes}(\beta)$ (empty disjunction stands for $\perp$).

288 (III) For all $\Theta \neq \Theta' \in \text{SatTypes}(\beta)$, the constraint $\Theta \wedge \Theta'$ is not satisfiable.

The proof is by an easy verification and this justifies the term ‘type’ used in this context.

289 **Abstraction with types.** A symbolic tree $t$ is a map $t: [0, D-1]^* \to \Sigma \times \text{SatTypes}(\beta)$. Symbolic trees are intended to be abstractions of trees labelled with concrete values in $\mathbb{Z}$. Given a tree $\mathfrak{t}: [0, D-1]^* \to \Sigma \times \mathbb{Z}^\beta$, its abstraction is the symbolic tree $t_{\mathfrak{t}}: [0, D-1]^* \to \Sigma \times \text{SatTypes}(\beta)$ such that for all $\mathbf{n} \cdot i \in [0, D-1]^*$ with $\mathfrak{t}(\mathbf{n}) = (\mathbf{a}, \mathbf{z})$ and $\mathfrak{t}(\mathbf{n} \cdot i) = (\mathbf{a}_i, \mathbf{z}_i)$, $t_{\mathfrak{t}}(\mathbf{n} \cdot i) \stackrel{\text{def}}{=} (\mathbf{a}_i, \Theta_i)$ for the unique $\Theta_i \in \text{SatTypes}(\beta)$ such that $\mathbb{Z} \models \Theta_i(\mathbf{z}, \mathbf{z}_i)$. Note that the primed variables in $\Theta_i$ refer to the $\beta$ values at the node $\mathbf{n} \cdot i$, whereas the unprimed ones refer to the $\beta$ values at the parent node $\mathbf{n}$. At the root $\varepsilon$ with $\mathfrak{t}(\varepsilon) = (\mathbf{a}, \mathbf{z})$, we have $t_{\mathfrak{t}}(\varepsilon) \stackrel{\text{def}}{=} (\mathbf{a}, \Theta)$ for the unique $\Theta \in \text{SatTypes}(\beta)$ such that $\mathbb{Z} \models \Theta(\mathbf{0}, \mathbf{z})$, where $\mathbf{0} \in \mathbb{Z}^\beta$ is arbitrary as there are actually no parent values at the root. A symbolic tree $t$ is satisfiable $\stackrel{\text{def}}{\iff}$ there is $\mathfrak{t}: [0, D-1]^* \to \Sigma \times \mathbb{Z}^\beta$ such that $t_{\mathfrak{t}} = t$. We say that $\mathfrak{t}$ witnesses the satisfaction of $t$, also written $\mathfrak{t} \models t$. A symbolic tree $t$ is regular if its set of subtrees is finite.

301 **A-consistency.** In our quest to decide whether $L(\mathcal{A}) \neq \emptyset$, we are interested in symbolic trees that satisfy certain properties that we subsume under the name **A-consistent**. A symbolic tree $t: [0, D-1]^* \to \Sigma \times \text{SatTypes}(\beta)$ is A-consistent if the following conditions are satisfied:

304 ■ $t$ is locally consistent: for every node $\mathbf{n}$, the type $\Theta$ labelling $\mathbf{n}$ restricted to $\mathbf{x}'_1, \dots, \mathbf{x}'_\beta$ agrees with all types $\Theta_i$ labelling its children nodes $\mathbf{n} \cdot i$ restricted to $\mathbf{x}_1, \dots, \mathbf{x}_\beta$, and

306 ■ there is an accepting run $\rho$ of $\mathcal{A}$ (but ignoring the conditions on data values) such that for all $\mathbf{n} \in [0, D-1]^*$ with $t(\mathbf{n}) = (\mathbf{a}, \Theta)$, $t(\mathbf{n} \cdot i) = (\mathbf{a}_i, \Theta_i)$ for all $i \in [0, D-1]$, and $\rho(\mathbf{n}) = (q, \mathbf{a}, (\Theta'_0, q_0) \dots (\Theta'_{D-1}, q_{D-1}))$, we have $\Theta_i \models \Theta'_i$ for all $i \in [0, D-1]$.
## 29:8 Constraint Automata on Infinite Data Trees

► **Example 2.** In Figure 1, we show a tree $\mathfrak{t}$ with concrete values in $\mathbb{Z}^\beta$ for $\beta = 2$ (middle) and its abstraction $t_\mathfrak{t}$ (right). We assume that $\mathfrak{d}_1 = 0$ is the only constant; consequently, $t_\mathfrak{t}$ uses constraints in SatTypes($\beta$) that are built with variables $\mathbf{x}_1, \mathbf{x}_2$, their primed variants $\mathbf{x}'_1, \mathbf{x}'_2$, and the constant $\mathfrak{d}_1$. We underline constraints to illustrate the property of local consistency. It is not hard to prove that the set of all A-consistent symbolic trees is $\omega$-regular, that is, it can be accepted by a classical tree automaton without constraints. In the following, we use the standard letter $A$ to distinguish automata without constraints from TCA.

► **Lemma 3.** There exists a Büchi tree automaton (without constraints) $A_{\text{cons}(\mathfrak{d})}$ such that $L(A_{\text{cons}(\mathfrak{d})})$ is equal to the set of A-consistent symbolic trees.

The locations in $A_{\text{cons}(\mathfrak{d})}$ are from SatTypes($\beta$) $\times Q$ and the transition relation for $A_{\text{cons}(\mathfrak{d})}$ can be decided in polynomial-time in $\text{card}(\delta) + \beta + \text{card}(\Sigma) + D + \text{MCS}(A)$.

However, not every A-consistent symbolic tree admits a concrete model. Thus the more important property is to check whether $L(A_{\text{cons}(\mathfrak{d})})$ contains some satisfiable symbolic tree (and we explain how to do this in the next two subsections). The result below is a variant of many similar results relating symbolic models and concrete models in logics for concrete domains, see e.g. [23, Corollary 4.1], [38, Lemma 3.4], [16, Theorem 25], [46, Theorem 11].

► **Lemma 4.** $L(\mathfrak{A}) \neq \emptyset$ iff there is a satisfiable symbolic tree in $L(A_{\text{cons}(\mathfrak{d})})$.

## 4.2 Satisfiability for Regular Locally Consistent Symbolic Trees

Below, we focus on deciding when $L(A_{\text{cons}(\mathfrak{d})})$ contains a satisfiable symbolic tree, while evaluating the complexity to check its existence. Given a locally consistent symbolic tree $t: [0, D-1]^* \to \Sigma \times \text{SatTypes}(\beta)$, we introduce an infinite labelled graph that contains exactly the same types as $t$ but expressed in a tree-like graph from which it is convenient to characterize satisfiability in terms of paths, under the premise that $t$ is regular. Similar symbolic structures are introduced in [49, 23, 14, 46]. The graph is equal to the structure

$$G_t^C = (V_t, \overset{\equiv}{\to}, \overset{\leq}{\to}, U_{<\mathfrak{d}_1}, (U_i)_{i \in [\mathfrak{d}_1, \mathfrak{d}_\alpha]}, U_{>\mathfrak{d}_\alpha}),$$

where $V_t = [0, D-1]^* \times (\{\mathbf{x}_1, \dots, \mathbf{x}_\beta\} \cup \{\mathfrak{d}_1, \mathfrak{d}_\alpha\})$, $\overset{\equiv}{\to}$ and $\overset{\leq}{\to}$ are two binary relations over $V_t$, and $\{U_{<\mathfrak{d}_1}, U_{\mathfrak{d}_1}, U_{\mathfrak{d}_1+1}, \dots, U_{\mathfrak{d}_\alpha}, U_{>\mathfrak{d}_\alpha}\}$ is a partition of $V_t$. Elements in $\{\mathbf{x}_1, \dots, \mathbf{x}_\beta\} \cup \{\mathfrak{d}_1, \mathfrak{d}_\alpha\}$ are denoted by $\mathbf{xd}, \mathbf{xd}_1, \mathbf{xd}_2, \dots$ (variables or constants). Moreover, $V_t^\beta \stackrel{\text{def}}{=} [0, D-1]^* \times \{\mathbf{x}_1, \dots, \mathbf{x}_\beta\}$. The rationale behind the construction of $G_t^C$ is to reflect the constraints between parent and children nodes as well as the constraints regarding constants, in such a way that, if $\mathfrak{t}$ witnesses the satisfaction of $t$, then, e.g., $\mathfrak{t}(\mathbf{n})(\mathbf{xd}) < \mathfrak{t}(\mathbf{n}')(\mathbf{xd}')$ if $(\mathbf{n}, \mathbf{xd}) \overset{\mathfrak{t}}{\rightleftharpoons} (\mathbf{n}', \mathbf{xd}')$, and $\mathfrak{t}(\mathbf{n})(\mathbf{xd}) = \mathfrak{d}_1$ if $(\mathbf{n}, \mathbf{xd}) \in U_{\mathfrak{d}_1}$. Here are all conditions for building $G_t^C$.

(VAR) For all $(\mathbf{n}, \mathbf{x}_i), (\mathbf{n}', \mathbf{x}'_i) \in V_t^\beta$, for all $\sim \in \{<, =\}$, $(\mathbf{n}, \mathbf{x}_i) \overset{\sim}{\to} (\mathbf{n}', \mathbf{x}'_i)$ iff either $\mathbf{n}' = \mathbf{n} \cdot \mathbf{j}$ and $\mathbf{x}_i \sim \mathbf{x}'_i$ in $\Theta$ with $t(\mathbf{n}') = (\mathbf{a}, \Theta)$, or $\mathbf{n} = \mathbf{n}'$ and $\mathbf{x}'_i \sim \mathbf{x}'_i$ in $\Theta$ with $t(\mathbf{n}') = (\mathbf{a}, \Theta)$, or $\mathbf{n} = \mathbf{n}' \cdot \mathbf{j}$ and $\mathbf{x}'_i \sim \mathbf{x}'_i$ in $\Theta$ with $t(\mathbf{n}) = (\mathbf{a}, \Theta)$.

(P1) For all $\mathfrak{d} \in [\mathfrak{d}_1, \mathfrak{d}_\alpha]$ and $(\mathbf{n}, \mathbf{x}_j) \in V_t^\beta$, $(\mathbf{n}, \mathbf{x}_j) \in U_{\mathfrak{d}}$ iff $\mathbf{x}'_j = \mathfrak{d}$ in $\Theta$ with $t(\mathbf{n}) = (\mathbf{a}, \Theta)$.

(P2) For all $(\mathbf{n}, \mathbf{x}_j) \in V_t^\beta$, $(\mathbf{n}, \mathbf{x}_j) \in U_{<\mathfrak{d}_1}$ iff $\mathbf{x}'_j < \mathfrak{d}_1$ in $\Theta$ with $t(\mathbf{n}) = (\mathbf{a}, \Theta)$.

(P3) For all $(\mathbf{n}, \mathbf{x}_j) \in V_t^\beta$, $(\mathbf{n}, \mathbf{x}_j) \in U_{>\mathfrak{d}_\alpha}$ iff $\mathbf{x}'_j > \mathfrak{d}_\alpha$ in $\Theta$ with $t(\mathbf{n}) = (\mathbf{a}, \Theta)$.

(P4) For all $\mathbf{n} \in [0, D-1]^*$, $(\mathbf{n}, \mathfrak{d}_1) \in U_{\mathfrak{d}_1}$ and $(\mathbf{n}, \mathfrak{d}_\alpha) \in U_{\mathfrak{d}_\alpha}$.

(CONS) This is about elements of $V_t$ labelled by constants and how the edge labels reflect the relationships between the constants. Formally, for all $((\mathbf{n}, \mathbf{xd}), (\mathbf{n}', \mathbf{xd}')) \in (V_t \times V_t) \setminus (V_t^\beta \times V_t^\beta)$, for all $\mathfrak{d}^\dagger, \mathfrak{d}^{\dagger\dagger}$ in $<\mathfrak{d}_1', \mathfrak{d}_1, \dots, \mathfrak{d}_\alpha, >\mathfrak{d}_\alpha$ s.t. $(\mathbf{n}, \mathbf{xd}) \in U_{\mathfrak{d}^\dagger}$ and $(\mathbf{n}', \mathbf{xd}') \in U_{\mathfrak{d}^{\dagger\dagger}}$, for all $\sim \in \{<, =\}$, $(\mathbf{n}, \mathbf{xd}) \overset{\sim}{\to} (\mathbf{n}', \mathbf{xd}')$ iff either $\mathfrak{d}^\dagger, \mathfrak{d}^{\dagger\dagger} \in [\mathfrak{d}_1, \mathfrak{d}_\alpha]$ and $\mathfrak{d}^\dagger \sim \mathfrak{d}^{\dagger\dagger}$, or $\mathfrak{d}^\dagger = <\mathfrak{d}_1'$, $\mathfrak{d}^{\dagger\dagger} \neq <\mathfrak{d}_1'$ and $\sim$ is equal to $< \mathfrak{d}^\dagger \neq > \mathfrak{d}_\alpha$, $\mathfrak{d}^{\dagger\dagger} = > \mathfrak{d}_\alpha$ and $\sim$ is equal to $<$.
Below, we illustrate the definition of the graph $G_t^C$ for the symbolic tree $t_t$ in Figure 1. The edges labelled with $=$ or $<$ reflect the constraints (we omit edges if they can be inferred from the other edges).

For instance, $(1, \mathbf{x}_1) \stackrel{<}{\rightarrow} (\varepsilon, \mathbf{x}_1)$ corresponds to the constraint $\mathbf{x}'_1 < \mathbf{x}_1$. Grey nodes are in $U_{\mathbf{d}_1}$, all other nodes are in $U_{>\mathbf{d}_1}$ (no nodes in $U_{<\mathbf{d}_1}$).

<figure><img src="image_4.png" /></figure>

A map $p : \mathbb{N} \to V_t$ is a *path map* in $G_t^C \stackrel{\text{def}}{\Leftrightarrow}$ for all $i \in \mathbb{N}$, either $p(i) \stackrel{=}{} \to p(i+1)$ or $p(i) \stackrel{<}{\to} p(i+1)$ in $G_t^C$. Similarly, $r : \mathbb{N} \to V_t$ is a *reverse path map* in $G_t^C \stackrel{\text{def}}{\Leftrightarrow}$ for all $i \in \mathbb{N}$, either $r(i) \stackrel{=}{} \to r(i+1)$ or $r(i+1) \stackrel{<}{\to} r(i)$. A path map $p$ (resp. reverse path map $r$) is *strict* $\stackrel{\text{def}}{\Leftrightarrow}$ $\{i \in \mathbb{N} \mid p(i) \stackrel{=}{} \to p(i+1)\}$ (resp. $\{i \in \mathbb{N} \mid r(i+1) \stackrel{=}{} \to r(i)\}$) is infinite. An infinite branch $\mathcal{B}$ is an element of $[0, D-1]^\omega$. We write $\mathcal{B}[i, j]$ with $i \le j$ to denote the subsequence $\mathcal{B}(i) \cdot \mathcal{B}(i+1) \cdots \mathcal{B}(j)$. Given $(\mathbf{n}, \mathbf{x}\mathbf{d}) \in V_t$, a path map $p$ from $(\mathbf{n}, \mathbf{x}\mathbf{d})$ along $\mathcal{B}$ is such that $p(0) = (\mathbf{n}, \mathbf{x}\mathbf{d})$ and for all $i \ge 0$, $p(i)$ is of the form $(\mathbf{n} \cdot \mathcal{B}[0, i], \cdot)$. A reverse path map $r$ from $(\mathbf{n}, \mathbf{x}\mathbf{d})$ along $\mathcal{B}$ admits a similar definition. We present the condition $(\star^C)$ that is the central property for characterising regular symbolic trees in $L(A_{\text{cons}(\mathcal{A})})$ that are satisfiable, following the remarkable result established in [46, Lemma 22] that non-satisfiability of a symbolic tree can be witnessed along a *single branch*.

($\star^C$) There are *no* elements $(\mathbf{n}, \mathbf{x}\mathbf{d})$, $(\mathbf{n}, \mathbf{x}\mathbf{d}')$ in $G_t^C$ (same node $\mathbf{n}$ from $[0, D-1]^*$) and no infinite branch $\mathcal{B}$ such that

1. there exists a path map $p$ from $(\mathbf{n}, \mathbf{x}\mathbf{d})$ along $\mathcal{B}$,

2. there exists a reverse path map $r$ from $(\mathbf{n}, \mathbf{x}\mathbf{d}')$ along $\mathcal{B}$,

3. $p$ or $r$ is strict, and

4. for all $i \in \mathbb{N}$, $p(i) \stackrel{<}{\to} r(i)$.

The following proposition states a key property: non-satisfaction of a regular locally consistent symbolic tree can be witnessed along a *single* branch by violation of $(\star^C)$.

**Proposition 5.** For every regular locally consistent symbolic tree $t$, $G_t^C$ satisfies $(\star^C)$ iff $t$ is satisfiable.

A proof can be found in [27, Section 7].

**Example 6.** Assume that every node along the rightmost branch in the symbolic tree $t_t$ in Figure 1 is labelled with $(\mathbf{a}, \Theta_1)$. Then $t_t$ is not satisfiable: in order to satisfy $\Theta_1$'s conjunct $\mathbf{x}'_1 < \mathbf{x}_1$, the value of $\mathbf{x}_1$ must inevitably become finally smaller than $\mathbf{d}_1$, violating the conjunct $\mathbf{d}_1 < \mathbf{x}_1$. Consequently, the rightmost branch of $G_t^C$ presented above does not satisfy $(\star^C)$: there exists a path map $p$ from $(\varepsilon, \mathbf{d}_1)$ along $1^\omega$, there exists a strict reverse path map $r$ from $(\varepsilon, \mathbf{x}_1)$ along $1^\omega$, and for all $i \in \mathbb{N}$ we have $p(i) \stackrel{<}{\to} r(i)$.

**New constant nodes.** Proposition 5 above is a variant of [46, Lemma 22]. Before going any further, let us in short explain the improvement of our developments compared to what is done in [46, 45]. The *framified constraint graphs* defined in [46, Definition 14] correspond to the above defined graph $G_t^C$ without $[0, D-1]^* \times \{\mathbf{d}_1, \mathbf{d}_\alpha\}$ and corresponding edges. However, Example 6 illustrates the importance of taking into account these elements when deciding satisfiability (without $\mathbf{d}_1$, the graph would satisfy $(\star^C)$). Actually, Example 6 invalidates $(\star)$ as used in [46, 45] because the constants are missing to apply properly [15]. The problematic part in [46, 45] is due to the proof of [45, Lemma 5.18] whose main argument takes advantage
29:10 Constraint Automata on Infinite Data Trees

of [15] but without the elements related to constant values (see also [24, Lemma 8]). With Proposition 5, we also propose a proof to characterise satisfiability of symbolic trees that is independent of [15]. Note also that the condition (⋆) in [46, Section 3.3] generalises the condition C<sub>Z</sub> from [23, Section 6] (see also the condition C in [24, Definition 2] and a similar condition in [32, Section 2]). A condition similar to (⋆) is also introduced recently in [7, Lemma 18] to decide a realizability problem based on LTL(Z, <, =).

We recall that there are *nonregular* locally consistent symbolic trees *t* such that $G_t^C$ satisfies $(\star^C)$ (see e.g. [23, 46]) but *t* is not satisfiable; indeed, satisfiability of symbolic trees is not an *ω*-regular property. The next result states that $(\star^C)$ is *ω*-regular; hence, satisfiability of symbolic trees can be overapproximated advantageously.

**► Lemma 7.** There is a Rabin tree automaton $A_{\star C}$ such that $L(A_{\star C}) = \{t \mid G_t^C \text{ satisfies } (\star^C)\}$, the number of Rabin pairs is bounded above by $8(\beta + 2)^2 + 3$, the number of locations is exponential in $\beta$, the transition relation can be decided in polynomial-time in

$$ \max([\log(|\mathfrak{d}_1|)], [\log(|\mathfrak{d}_\alpha|)]) + \beta + \mathrm{card}(\Sigma) + D. $$

**Proof sketch.** The proof of Lemma 7 is structured as follows (see [27, Section 4.3]).
(1) We construct a Büchi word automaton $A_B$ accepting the complement of $(\star^C)$ for $D = 1$.
(2) $A_B$ is nondeterministic, but we can determinize it and get a deterministic Rabin word automaton $A_{B \to R}$ such that $L(A_B) = L(A_{B \to R})$ (using the determinisation construction from [60, Theorem 1.1]).
(3) By an easy construction, we obtain a deterministic Street word automaton $A_S$ accepting the complement of $L(A_{B \to R})$; it accepts words that satisfy $(\star^C)$ for $D = 1$.
(4) By [60, Lemma 1.2], we construct a deterministic Rabin word automaton $A_R$ s.t. $L(A_S) = L(A_R)$.
(5) Finally, we construct a Rabin tree automaton $A_{\star C}$, the intuitive idea is to "let run the automaton $A_R$" along every branch of a run of $A_{\star C}$, doable thanks to the determinism of $A_R$. Since $(\star^C)$ states a property on every branch, we are done.

**Differences with [46].** Lemma 7 is similar to [46, Proposition 26] but there is an essential difference: the number of Rabin pairs in Lemma 7 is not a constant but a value depending on $\beta$, an outcome of our investigations. It is important to know the number of Rabin pairs in $A_{\star C}$ for our complexity analysis as checking nonemptiness of Rabin tree automata is exponential in the number of Rabin pairs [30, Theorem 4.1]. Our proof of Lemma 7 also proposes a slight novelty compared to the construction in [46]: we design $A_{\star C}$ without firstly constructing a tree automaton for the complement language (as done in [46]) and then using results from [55] (elimination of alternation in tree automata). Our new approach shall be rewarding: not only we can better understand how to express the condition $(\star^C)$, but also we control the size parameters of $A_{\star C}$ involved in our forthcoming complexity analysis. Furthermore, it may be useful to implement the decision procedure for solving the satisfiability problem for CTL(Z) (resp. for CTL*(Z)). Note also that the above analysis about the number of Rabin pairs is independent from the question discussed above about having the elements in $[0, D - 1]^* \times \{\mathfrak{d}_1, \mathfrak{d}_\alpha\}$ within $G_t^C$.

Summarizing the developments so far, we can conclude this subsection as follows:

**► Lemma 8.** $L(\mathcal{A}) \neq \emptyset$ iff $L(A_{\mathrm{cons}(\mathcal{A})}) \cap L(A_{\star C}) \neq \emptyset$.

For its proof, by way of example, if $L(A_{\mathrm{cons}(\mathcal{A})}) \cap L(A_{\star C})$ is non-empty, then as $L(A_{\mathrm{cons}(\mathcal{A})}) \cap L(A_{\star C})$ is regular, it contains a regular $\mathcal{A}$-consistent symbolic tree $t$ (see e.g. [58] and [64, Section 6.3] for the existence of regular trees) and by Proposition 5, $t$ is satisfiable. By Lemma 4, we get $L(\mathcal{A}) \neq \emptyset$. For the other direction, we use Lemma 3 as well as the property that for every satisfiable symbolic tree $t$, $G_t^C$ satisfies the condition $(\star^C)$.
## 4.3 ExpTime Upper Bound for TCAs

437

438

439

440

441

Lemma 8 justifies why deciding the nonemptiness of $L(A_{\text{cons}(\mathcal{A})}) \cap L(A_{\star C})$ is crucial. In the proof of Lemma 9 below (see [27, Section 4.4]), we propose a construction for the intersection of Rabin tree automata that only performs an exponential blow-up for the number of locations, which is fine for our purposes.

442

443

444

445

**▶ Lemma 9.** There is a Rabin tree automaton $A$ such that $L(A) = L(A_{\text{cons}(\mathcal{A})}) \cap L(A_{\star C})$ and the number of Rabin pairs is polynomial in $\beta$, the number of locations is in $O(\text{card}(\text{SatTypes}(\beta))) \times \text{card}(Q) \times 2^{P(\beta)}$ for some polynomial $P(\cdot)$ and the transition relation can be decided in polynomial-time in $\text{card}(\delta) + \beta + \text{card}(\Sigma) + D + \text{MCS}(A)$.

446

447

448

449

450

451

452

453

454

455

Nonemptiness of Rabin tree automata is polynomial in the cardinality of the transition relation and exponential in the number of Rabin pairs, see e.g. [30, Theorem 4.1]. More precisely, it is in time $(m \times n)^{O(n)}$, where $m$ is the number of locations and $n$ is the number of Rabin pairs, see the statement [30, Theorem 4.1]. However, this is not exactly what we need herein, as the complexity expression above concerns binary trees, and it assumes that the transition relation $\delta$ can be decided in constant time. If, as in our case, $D \ge 1$ and deciding whether a tuple belongs to $\delta$ requires $\gamma$ time units, checking nonemptiness is actually in time $(\text{card}(\delta) \times \gamma \times n)^{O(n)}$ (by scrutiny of the proof of [30, Theorem 4.1], page 144). Here, $\gamma$ may depend on parameters related to $A$ and in Lemma 10 below, $\gamma$ takes the value $\text{card}(\delta) + \beta + \text{card}(\Sigma) + D + \text{MCS}(A)$ (by Lemma 9). Hence the following result:

456

457

**▶ Lemma 10.** The nonemptiness problem for TCA can be solved in time in $O(R_1(\text{card}(Q) \times \text{card}(\delta) \times \text{MCS}(A) \times \text{card}(\Sigma) \times R_2(\beta))^{R_2(\beta) \times R_3(D)})$ for some polynomials $R_1, R_2$ and $R_3$.

458

459

460

461

462

Assuming that the size of the TCA $A = (Q, \Sigma, D, \beta, Q_{\text{in}}, \delta, F)$, written $\text{size}(A)$, is polynomial in $\text{card}(Q) + \text{card}(\delta) + D + \beta + \text{MCS}(A)$ (which makes sense for a reasonably succinct encoding), from the computation of the bound in Lemma 10, the nonemptiness of $L(A)$ can be checked in time $O(R(\text{size}(A))^{R'(\beta+D)})$ for some polynomials $R$ and $R'$. The $\text{EXPTIME}$ upper bound of the nonemptiness problem for TCA is now a consequence of the above complexity expression.

463

**▶ Theorem 11.** Nonemptiness problem for tree constraint automata is $\text{EXPTIME}$-complete.

## 4.4 Rabin Tree Constraint Automata

464

465

466

467

468

469

470

471

We can prove the $\text{EXPTIME}$ upper bound of the nonemptiness problem for Rabin TCA (Theorem 13) and follow the same lines of arguments as for TCA. Given a Rabin TCA $A = (Q, \Sigma, D, \beta, Q_{\text{in}}, \delta, \mathcal{F})$, we define a Rabin tree automaton $A'_{\text{cons}(A)}$ such that $L(A) \ne \emptyset$ iff there is $t \in L(A'_{\text{cons}(A)})$ that is satisfiable (cf. Lemma 4 for TCA). Moreover, we take advantage of $A_{\star C}$ so that $L(A) \ne \emptyset$ iff $L(A'_{\text{cons}(A)}) \cap L(A_{\star C})$ is non-empty (cf. Lemma 8). It remains to determine the cost for testing nonemptiness of $L(A'_{\text{cons}(A)}) \cap L(A_{\star C})$. Here is the counterpart of Lemma 9 (same kind of arguments).

472

473

474

475

**▶ Lemma 12.** There is a Rabin tree automaton $A$ s.t. $L(A) = L(A'_{\text{cons}(A)}) \cap L(A_{\star C})$, the number of Rabin pairs is polynomial in $\beta + \text{card}(\mathcal{F})$, the number of locations is in $O(\text{card}(\text{SatTypes}(\beta)) \times \text{card}(Q) \times 2^{P(\beta+\text{card}(\mathcal{F}))})$ for some polynomial $P(\cdot)$, and the transition relation can be decided in polynomial-time in $\text{card}(\delta) + \beta + \text{card}(\Sigma) + D + \text{MCS}(A)$.

476

477

478

479

As for Lemma 10, we conclude that the nonemptiness problem for Rabin TCA can be solved in time $O(R_1(\text{card}(Q) \times \text{card}(\delta) \times \text{MCS}(A) \times \text{card}(\Sigma) \times R_2(\beta+\text{card}(\mathcal{F})))^{R_2(\beta+\text{card}(\mathcal{F})) \times R_3(D)})$ for polynomials $R_1, R_2$ and $R_3$. The nonemptiness problem for Rabin TCA is also in $\text{EXPTIME}$.
► **Theorem 13.** The nonemptiness problem for Rabin TCA is EXPTIME-complete.

This result is mainly useful to characterize the complexity of SAT(CTL*(Z)) in Section 6.

## 5 Tree Constraint Automata for CTL(Z)

Below, we harvest the first results from what is achieved in the previous section: SAT(CTL(Z)) is in EXPTIME. So, enriching the CTL models with numerical values interpreted in Z does not cause a complexity blow-up. We follow the automata-based approach and (after proving a refined version of the tree model property for CTL(Z)) the key step is to translate CTL(Z) formulae into equivalent TCA. Theorem 14 below is one of our main results.

► **Theorem 14.** The satisfiability problem for CTL(Z) is EXPTIME-complete.

**Sketch.** EXPTIME-hardness is inherited from CTL. For EXPTIME-easiness, let $\phi$ be a CTL(Z) formula. A first step is to preprocess the formula into a formula in simple form (see definition in Section 2.2). Then, we can construct from a formula $\phi$ in simple form a TCA $A_{\phi}$ s.t. $\phi$ is satisfiable iff $L(A_{\phi}) \neq \emptyset$ and $A_{\phi}$ satisfies the following properties.

- The degree $D$ and the number of variables $\beta$ are bounded by $\text{size}(\phi)$.

- The number of locations is bounded by $(D \times 2^{\text{size}(\phi)}) \times (\text{size}(\phi) + 1)$.

- The number of transitions is in $O(2^{P(\text{size}(\phi))})$ for some polynomial $P(\cdot)$.

- The finite alphabet $\Sigma$ in $A_{\phi}$ is unary; $\text{MCS}(A_{\phi})$ is quadratic in $\text{size}(\phi)$.

By Lemma 10, the nonemptiness problem for TCA can be solved in time

$$O(R_1(\text{card}(Q) \times \text{card}(\delta) \times \text{MCS}(A) \times \text{card}(\Sigma) \times R_2(\beta))^{R_2(\beta) \times R_3(D)}).$$

Since the transition relations of the automata $A_{\text{cons}(A)}$ and $A_{\star C}$ can be built in polynomial-time, we get that nonemptiness of $L(A_{\phi})$ can be solved in exponential-time. ◀

Let $\mathbb{N}$ be the concrete domain $(\mathbb{N}, <, =, (\cdot_{\emptyset}), \emptyset)$ for which we can also show that nonemptiness of TCA with constraints interpreted on $\mathbb{N}$ has the same complexity as for TCA with constraints interpreted on $\mathbb{Z}$. Let CTL($\mathbb{N}$) be the variant of CTL(Z) with constraints interpreted on $\mathbb{N}$. As a corollary, SAT(CTL($\mathbb{N}$)) is EXPTIME-complete. With the concrete domain $(Q, <, =, (\cdot_{\emptyset}), \emptyset)$, all the trees in $L(A_{\text{cons}(A)})$ are satisfiable (no need to intersect $A_{\text{cons}(A)}$ with a hypothetical $A_{\star C}$, see e.g. [49, 4, 23, 38]), and therefore SAT(CTL(Q)) is in EXPTIME too. TCA can be also used to show that the concept satisfiability w.r.t. general TBoxes for the description logic $\mathcal{ALCF}^{\mathcal{P}}(\mathbb{Z}_c)$ is in EXPTIME [46, 45], see more details in [27, Section 5.2].

## 6 Complexity of the Satisfiability Problem for the Logic CTL*(Z)

We show that SAT(CTL*(Z)) can be solved in 2EXPTIME. We follow the automata-based approach for CTL*, see e.g. [31, 30], but adapted to Rabin TCA. The main challenge here is to carefully check that essential steps for CTL* can be lifted to CTL*(Z), but also that computationally we are in a position to provide an optimal complexity upper bound.

Let us explain in short all steps necessary to obtain the result. We start by establishing a special form for CTL*(Z) formulae from which Rabin TCA will be defined, following ideas from [31] for CTL*. A CTL*(Z) state formula $\phi$ is in special form if it has the form below

$$E(x = 0) \wedge (\bigwedge_{i \in [1, D-1]} \text{AGE} \ \Phi_i) \wedge (\bigwedge_{j \in [1, D]} A \ \Phi'_j),$$

where the $\Phi_i$'s and the $\Phi'_j$'s are LTL(Z) formulae in simple form (see Section 2), for some $D \ge 1$, $D' \ge 0$. We can restrict ourselves to CTL*(Z) state formulae in special form (see the proof of [27, Proposition 6]).
**Proposition 15.** For every CTL\*(Z) formula φ, one can construct in polynomial time in the size of φ a CTL\*(Z) formula φ' in special form s.t. φ is satisfiable iff φ' is satisfiable.

521

522

523

524

525

So φ' is also of polynomial size in the size of φ. Let us state a tree model property of special formulae, with a strict discipline on the witness paths. Proposition 16 below is a counterpart of [31, Theorem 3.2] but for CTL\*(Z) instead of CTL\*, see also the variant [38, Lemma 3.3].

526

527

528

**Proposition 16.** Let φ be a CTL\*(Z) formula in special form built over x₁, ..., xβ. φ is satisfiable iff there is a tree t : [0, D - 1] → Zβ such that t, ε |= φ and for each i ∈ [1, D - 1], t satisfies AGE Φi via i, that is, if t, n |= E Φi, then Φi is satisfied on the path n · i · 0ω.

529

530

531

532

533

534

Proposition 16 justifies our restriction to infinite trees and to TCA in the rest of this section. Proposition 15 allows us to restrict our attention to constructing automata for formulae of (only) the form AGE Φ and A Φ, where Φ is a simple formula in LTL(Z). The first step is to translate simple formulae in LTL(Z) into equivalent word constraint automata (TCA with degree D = 1). Adapting the standard automata-based approach for LTL [69], we can show the following proposition (see the proof of [27, Proposition 8]).

535

536

**Proposition 17.** Let Φ be an LTL(Z) formula in simple form. There is a constraint word automaton AΦ such that {w : N → Zβ | w |= Φ} = L(AΦ), and the following conditions hold.

537

(I) The number of locations in AΦ is bounded by size(Φ) × 22×size(Φ).

538

(II) The cardinality of δ in AΦ is in O(2P(size(Φ))) for some polynomial P(·).

539

(III) The maximal size of a constraint in AΦ is quadratic in size(Φ).

We can now construct, for every $i \in [0, D-1]$, a TCA $A_i$ such that $L(A_i) = \{t : [0, D-1]^* \to \mathbb{Z}^\beta | t \models \text{AGE } \Phi_i \text{ and } t \models \text{AGE } \Phi_i \text{ via } i\}$. The idea is to construct $A_i$ so that it starts off the word constraint automaton $A_{\Phi_i}$ at each node $n$ of the tree and runs it down the designated path $n \cdot i \cdot 0^\omega$ to check whether $\Phi_i$ actually holds along this path. This can be easily done for AGE $\Phi_i$; however, for formulas of the form $A \Phi'_j$, for this construction to be correct, the underlying constraint word automaton $A'_j$ must be deterministic, that is, for all locations $s$, letters $a$ and pairs of valuations $(z, z') \in \mathbb{Z}^{2\beta}$, there exists in $A'_j$ at most a single transition $(s, a, \Theta, s')$ such that $\mathbb{Z} \models \Theta(z, z')$. A well-known construction to transform nondeterministic Büchi automata to equivalent deterministic Rabin automata is due to Safra [60, Theorem 1.1]. An important step towards the optimal complexity for CTL\*(Z) is to show that it is possible to lift this construction to word constraint automata, which is a result of its own interest. A special attention is given to the cardinality of the transition relation and to the size of the constraints in transitions, as these two parameters are, a priori, unbounded in constraint automata but essential to perform a forthcoming complexity analysis.

540

541

542

543

544

545

546

547

548

549

550

551

552

553

554

**Theorem 18.** Let $\mathcal{A} = (Q, \Sigma, \beta, Q_{in}, \delta, F)$ be a Büchi word constraint automaton involving the constants $\mathfrak{d}_1, \dots, \mathfrak{d}_\alpha$. There is a deterministic Rabin word constraint automaton $\mathcal{A}' = (Q', \Sigma, \beta, Q'_{in}, \delta', \mathcal{F})$ such that $L(\mathcal{A}) = L(\mathcal{A}')$ verifying the following quantitative properties.

555

556

557

(I) $card(Q')$ is exponential in $card(Q)$ and the number of Rabin pairs in $\mathcal{A}'$ is bounded by $2 \cdot card(Q)$ (same bounds as in [60, Theorem 1.1]).

558

559

(II) The constraints in the transitions are from SatTypes(β), are of size cubic in β + max([log(|d₁|)], [log(|dα|)]) and card(δ') ≤ card(Q')² × card(Σ) × ((dα - d₁) + 3)²β × 3β².

560

561

562

This and Proposition 17 lead us to the result below on LTL(Z) formulae in simple form.

**Corollary 19.** Let $\Phi$ be an LTL(Z) formula in simple form built over the variables $x_1, \dots, x_\beta$ and the constants $\mathfrak{d}_1, \dots, \mathfrak{d}_\alpha$. There exists a deterministic Rabin word constraint automaton $A_\Phi$ such that $\{w : N \to \mathbb{Z}^\beta | w \models \Phi\} = L(A_\Phi)$, and the following conditions hold.

563

564

565
29:14 Constraint Automata on Infinite Data Trees

(I) The number of locations in $A_\Phi$ is bounded by $2^{2^{P^\dagger(size(\Phi))}}$ for some polynomial $P^\dagger(\cdot)$.

(II) The number of Rabin pairs is bounded by $2 \times \text{size}(\Phi) \times 2^{2 \times \text{size}(\Phi)}$.

(III) The cardinality of $\delta$ in $A_\Phi$ is bounded by $\text{card}(\text{SatTypes}(\beta)) \times 2^{2^{P^\dagger(size(\Phi))+1}}$.

(IV) MCS($A_\Phi$) is cubic in $\beta + \max([\log(|\mathfrak{D}_1|)], [\log(|\mathfrak{D}_\alpha|)])$, i.e. polynomial in size($\Phi$).

This enables us to use the idea illustrated above for formulas of the form AGE $\Phi_i$ also for formulas of the form $A \Phi'_j$, and define Rabin TCA $A'_j$ such that $L(A'_j) = \{\mathfrak{t} : [0, D-1]^* \to \mathbb{Z}^\beta \mid \mathfrak{t}$ satisfies $A \Phi'_j\}$. We are now ready to perform the final step towards the main result of this section. Let us recapitulate what we have so far.

One can define a TCA $A_0$ with two locations such that $L(A_0)$ is the set of trees $\mathfrak{t} : [0, D-1]^* \to \mathbb{Z}^\beta$ such that $\mathfrak{t}(\varepsilon)(\mathbf{x}_1) = 0$, to handle $E(\mathbf{x}_1 = 0)$ in formulae in special form.

For all $1 \le i < D$, there are (Büchi) TCA $A_i$ such that $L(A_i)$ is the set of trees $\mathfrak{t} : [0, D-1]^* \to \mathbb{Z}^\beta$ such that $\mathfrak{t}, \varepsilon \models AGE \Phi_i$ and $\mathfrak{t}$ satisfies AGE $\Phi_i$ via $i$. Recall that TCA can be seen as Rabin TCA with a single Rabin pair.

For all $1 \le j \le D'$, there are Rabin TCA $A'_j$ such that $L(A'_j)$ is the set of trees $\mathfrak{t}$ such that $\mathfrak{t}$ satisfies $A \Phi_j$, with an exponential number of Rabin pairs in size($\Phi$).

To define a Rabin TCA $A$ such that $L(A) = L(A_0) \cap \bigcap_{i \in [1, D-1]} L(A_i) \cap \bigcap_{j \in [1, D']} L(A'_j)$, and then use the complexity bounds previously established, we need the result below (see the full proof in [27, Section 6.5]).

**Lemma 20.** Let $(A_k)_{1 \le k \le n}$ be a family of Rabin TCA such that $A_k = (Q_k, \Sigma, D, \beta, Q_{k,in}, \delta_k, \mathcal{F}_k)$, $card(\mathcal{F}_k) = N_k$ and $N = \prod_k N_k$. There is a Rabin TCA $A$ such that $L(A) = \bigcap_k L(A_k)$ and

the number of Rabin pairs is equal to $N$; MCS($A$) $\le n + MCS(A_1) + \dots + MCS(A_n)$,

the number of locations (resp. transitions) is less than $(\prod_k card(Q_k))(2n)^N$ (resp. $\prod_k card(\delta_k)$).

Putting all results together, the nonemptiness of $L(A)$ can be checked in double-exponential time in size($\phi$), leading to Theorem 21 below, which is the main result of the paper. It answers open questions from [11, 15, 16, 46].

**Theorem 21.** SAT(CTL\*($\mathbb{Z}$)) is 2EXPTIME-complete.

2EXPTIME-hardness is from SAT(CTL\*) [66, Theorem 5.2]. As a corollary, SAT(CTL\*($\mathbb{N}$)) is also 2EXPTIME-complete. Furthermore, assuming that $<_{\text{pre}}$ is the prefix relation on $\{0, 1\}^*$, we can use the reduction from [22, Section 4.2] to conclude SAT(CTL\*($\{0, 1\}^*$, $<_{\text{pre}}$)) is 2EXPTIME-complete too. Furthermore, as observed earlier, when the concrete domain is $(Q, <, =, (\approx_\delta)_{\delta \in Q})$, all the trees in $L(A_{\text{cons}(A)})$ are satisfiable, and therefore SAT(CTL\*($\mathbb{Q}$)) is also in 2EXPTIME, which is already known from [38, Theorem 4.3].

7 Concluding Remarks

We developed an automata-based approach to solve SAT(CTL($\mathbb{Z}$)) and SAT(CTL\*($\mathbb{Z}$)), by introducing tree constraint automata that accept infinite data trees with data domain $\mathbb{Z}$. The nonemptiness problem for tree constraint automata with Büchi acceptance conditions (resp. with Rabin pairs) is EXPTIME-complete, see Theorem 11 (resp. Theorem 13). The difficult part consists in proving the EXPTIME-easiness for which we show how to substantially adapt the material in [45, Section 5.2] that guided us to design the correctness proof of $(\star^C)$. The work [46] was indeed a great inspiration but we adjusted a few statements from there (see also [27]). We recall that $(\star)$ in [46] is not fully correct (see Section 4.2) as we need to add constants (leading to the variant condition $(\star^C)$). Moreover, our construction of the automaton in Lemma 7 does depend on the number of variables unlike [46, Proposition 26].
This is crucial for complexity, as it is related to the number of Rabin pairs. We also use [30] more precisely than [46, p.621] as we handle non-binary trees. In short, we introduced TCA for which we characterise complexity of the non-emptiness problem (providing a few improvements to [46]). We left aside the question of the expressiveness of TCA, which is interesting but out of the scope of this paper.

This lead us to show that SAT(CTL(Z)) is EXPTIME-complete (Theorem 14), and SAT(CTL*(Z)) is 2EXPTIME-complete (Theorem 21). The only decidability proof for SAT(CTL*(Z)) done so far, see [15, Theorem 32], is by reduction to a decidable second-order logic. Our complexity characterisation for SAT(CTL*(Z)) provides an answer to several open problems related to CTL*(Z) fragments, see e.g. [11, 38, 15, 16, 46]. We believe that our results on TCA can help to establish complexity results for other logics (see also Section 6 about a domain for strings and [33, Section 4] to handle more concrete domains).

References

1 S. Abriola, D. Figueira, and S. Figueira. Logics of repeating values on data trees and branching counter systems. In *FoSSaCS'17*, volume 10203 of LNCS, pages 196-212, 2017.

2 E.G. Amparore, S. Donatelli, and F. Gallà. A CTL* model checker for Petri nets. In *Petri Nets'20*, volume 12152 of LNCS, pages 403-413. Springer, 2020.

3 F. Baader and J. Rydval. Using model theory to find decidable and tractable description logics with concrete domains. *JAR*, 66(3):357-407, 2022.

4 Ph. Balbiani and J.F. Condotta. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In *FroCoS'02*, volume 2309 of LNAI, pages 162-173. Springer, 2002.

5 K. Bartek and M. Lelyk. Modal mu-calculus with atoms. In *CSL'17*, pages 30:1-30:21. Leibniz-Zentrum für Informatik, LIPICS, 2017.

6 B. Bednarczyk and O. Fiuk. Presburger Büchi tree automata with applications to logics with expressive counting. In *WoLLIC'22*, volume 13468 of LNCS, pages 295-308. Springer, 2022.

7 A. Bhaskar and M. Praveen. Realizability problem for constraint LTL. In *TIME'22*, volume 247 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

8 M. Bojańczyk. A bounding quantifier. In *CSL'04*, volume 3210 of LNCS, pages 41-55. Springer, 2004.

9 M. Bojańczyk and Th. Colcombet. Bounds in $\omega$-Regularity. In *LiCS'06*, pages 285-296. IEEE Computer Society, 2006.

10 M. Bojańczyk and S. Toruńczyk. Weak MSO+U over infinite trees. In *STACS'12*, LIPIcs, pages 648-660, 2012.

11 L. Bozzelli and R. Gascon. Branching-time temporal logic extended with Presburger constraints. In *LPAR'06*, volume 4246 of LNCS, pages 197-211. Springer, 2006.

12 L. Bozzelli and S. Pinchinat. Verification of gap-order constraint abstractions of counter systems. *TCS*, 523:1-36, 2014.

13 C. Carapelle. *On the satisfiability of temporal logics with concrete domains*. PhD thesis, Leipzig University, 2015.

14 C. Carapelle, A. Kartzow, and M. Lohrey. Satisfiability of CTL* with constraints. In *CONCUR'13*, LNCS, pages 455-463. Springer, 2013.

15 C. Carapelle, A. Kartzow, and M. Lohrey. Satisfiability of ECTL* with constraints. *Journal of Computer and System Sciences*, 82(5):826-855, 2016.

16 C. Carapelle and A.-Y. Turhan. Description Logics Reasoning w.r.t. General TBoxes is Decidable for Concrete Domains with the EHD-property. In *ECAI'16*, volume 285, pages 1440-1448. IOS Press, 2016.

17 K. Čerāns. Deciding properties of integral relational automata. In *ICALP'94*, volume 820 of LNCS, pages 35-46. Springer, 1994.

18 A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. *JACM*, 28(1):114-133, 1981.
29:16 Constraint Automata on Infinite Data Trees

659

19 R. Condurache, C. Dima, Y. Oualhdaj, and N. Troquard. Rational Synthesis in the Commons with Careless and Careful Agents. In *AAMAS'21*, pages 368–376, 2021.

660

661

20 B. Cook, H. Khlaaf, and N. Piterman. On automation of CTL* verification for infinite-state systems. In *CAV'15*, volume 9206 of LNCS, pages 13–29. Springer, 2015.

662

663

21 N. Decker, P. Habermehl, M. Leucker, and D. Thoma. Ordered navigation on multi-attributed data words. In *CONCUR'14*, volume 8704 of LNCS, pages 497–511, 2014.

664

665

22 S. Demri and M. Deters. Temporal logics on strings with prefix relation. *Journal of Logic and Computation*, 26:989–1017, 2016.

666

667

23 S. Demri and D. D'Souza. An automata-theoretic approach to constraint LTL. *I & C*, 205(3):380–415, 2007.

668

669

24 S. Demri and R. Gascon. Verification of qualitative Z constraints. *TCS*, 409(1):24–40, 2008.

670

25 S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. *ACM ToCL*, 10(3), 2009.

671

672

26 S. Demri and K. Quaas. Concrete domains in logics: a survey. *ACM SIGLOG News*, 8(3):6–29, 2021.

673

674

27 S. Demri and K. Quaas. Constraint automata on infinite data trees: From CTL(Z)/CTL*(Z) to decision procedures. CoRR, abs/2302.05327, 2023.

675

676

28 A. Deutsch, R. Hull, and V. Vianu. Automatic verification of database-centric system. *SIGMOD Record*, 43(3):5–17, 2014.

677

678

29 E.A. Emerson and J. Halpern. ‘sometimes’ and ‘not never’ revisited: on branching versus linear time temporal logic. *JACM*, 33:151–178, 1986.

679

680

30 E.A. Emerson and C.S. Jutla. The complexity of tree automata and logics of programs. *SIAM Journal of Computing*, 29(1):132–158, 2000.

681

682

31 E.A. Emerson and P. Sistla. Deciding full branching time logic. *Information and Control*, 61:175–201, 1984.

683

684

32 L. Exibard, E. Filiot, and A. Khalimov. Church synthesis on register automata over linearly ordered data domains. In *STACS'21*, volume 187 of LIPIcs, pages 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.

685

686

687

33 L. Exibard, E. Filiot, and A. Khalimov. A generic solution to register-bounded synthesis with an application to discrete orders. In *ICALP'22*, volume 229 of LIPIcs, pages 122:1–122:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

688

689

690

34 P. Felli, M. Montali, and S. Winkler. CTL* model checking for data-aware dynamic systems with arithmetic. In *IJCAR'22*, volume 13385 of LNCS, pages 36–56. Springer, 2022.

691

692

35 P. Felli, M. Montali, and S. Winkler. Linear-time verification of data-aware dynamic systems with arithmetic. In *AAAI'22*, pages 5642–5650. AAAI Press, 2022.

693

694

36 D. Figueira. *Reasoning on words and trees with data*. PhD thesis, ENS Cachan, 2010.

695

37 D. Figueira. Decidability of Downward XPath. *ACM ToCL*, 13(4):1–40, 2012.

696

38 R. Gascon. An automata-based approach for CTL* with constraints. *Electronic Notes in Theoretical Computer Science*, 239:193–211, 2009.

697

698

39 S. Göller, Ch. Haase, J. Ouaknine, and J. Worrell. Branching-time model checking of parametric one-counter automata. In *FoSSaCS'12*, volume 7213 of LNCS, pages 406–420. Springer, 2012.

699

700

40 J.F. Groote and R. Mastescu. Verification of temporal properties of processes in a setting with data. In *AMAST'98*, volume 1548 of LNCS, pages 74–90, 1998.

701

702

41 R. Iosif and X. Xu. Alternating automata modulo first order theories. In *CAV'19*, volume 11562 of LNCS, pages 46–63, 2019.

703

704

42 M. Jurdziński and R. Lazić. Alternating automata on data trees and XPath satisfiability. *ACM ToCL*, 12(3):19:1–19:21, 2011.

705

706

43 A. Kartzow and Th. Weidner. Model checking constraint LTL over trees. *CoRR*, abs/1504.06105, 2015.

707

708

44 O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. *JACM*, 47(2):312–360, 2000.

709
710

45 N. Labai. *Automata-based reasoning for decidable logics with data values*. PhD thesis, TU Wien, May 2021.

711

712

46 N. Labai, M. Ortiz, and M. Simkus. An Exptime Upper Bound for *ALC* with integers. In *KR'20*, pages 425–436. Morgan Kaufman, 2020.

713

714

47 S. Lasota and I. Walukiewicz. Alternating timed automata. *ACM ToCL*, 9(2):10:1–10:27, 2008.

715

716

48 A. Lechner, R. Mayr, J. Ouaknine, A. Pouly, and J. Worrell. Model checking flat freeze LTL on one-counter automata. *Logical Methods in Computer Science*, 14(4), 2018.

717

718

49 C. Lutz. Interval-based temporal reasoning with general TBoxes. In *IJCAI'01*, pages 89–94. Morgan-Kaufmann, 2001.

719

720

50 C. Lutz. *The Complexity of Description Logics with Concrete Domains*. PhD thesis, RWTH, Aachen, 2002.

721

722

51 C. Lutz. Description logics with concrete domains—a survey. In *Advances in Modal Logics Volume 4*, pages 265–296. King's College Publications, 2003.

723

724

52 C. Lutz. NEXPTIME-complete description logics with concrete domains. *ACM ToCL*, 5(4):669–705, 2004.

725

726

53 C. Lutz and M. Milicić. A Tableau Algorithm for Description Logics with Concrete Domains and General Tboxes. *JAR*, 38(1-3):227–259, 2007.

727

728

54 R. Mayr and P. Totzke. Branching-time model checking gap-order constraint systems. *Fundamenta Informaticae*, 143(3-4):339–353, 2016.

729

730

55 D. Muller and E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. *TCS*, 141(1-2):69–107, 1995.

731

732

733

56 F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. *ACM ToCL*, 5(3):403–435, 2004.

734

735

57 D. Peteler and K. Quaas. Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order. In *MFCS'22*, volume 241 of *LIPIcs*, pages 76:1–76:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

736

737

738

58 M.O. Rabin. Decidability of second-order theories and automata on infinite trees. *Transactions of the AMS*, 141:1–35, 1969.

739

740

59 P. Revesz. *Introduction to Constraint Databases*. Springer, New York, 2002.

741

60 S. Safra. *Complexity of Automata on Infinite Objects*. PhD thesis, The Weizmann Institute of Science, Rehovot, 1989.

742

743

61 L. Segoufin and S. Toruńczyk. Automata based verification over linearly ordered data domains. In *STACS'11*, pages 81–92, 2011.

744

745

62 H. Seidl, Th. Schwentick, and A. Muscholl. Counting in trees. In *Logic and Automata: History and Perspectives*, volume 2 of *Texts in Logic and Games*, pages 575–612. Amsterdam University Press, 2008.

746

747

748

63 F. Song and Z. Wu. On temporal logics with data variable quantifications: decidability and complexity. *I & C*, 251:104–139, 2016.

749

750

64 W. Thomas. Automata on infinite objects. In *Handbook of Theoretical Computer Science, Volume B, Formal models and semantics*, pages 133–191. Elsevier, 1990.

751

752

65 Sz. Torunczyk and Th. Zeume. Register automata with extrema constraints, and an application to two-variable logic. *Logical Methods in Computer Science*, 18(1), 2022.

753

754

66 M. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In *STOC'85*, pages 240–251. ACM, 1985.

755

756

67 M. Vardi and Th. Wilke. Automata: from logics to algorithms. In *Logic and Automata: History and Perspectives*, number 2 in *Texts in Logic and Games*, pages 629–736. Amsterdam University Press, 2008.

757

758

759

68 M. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. *Journal of Computer and System Sciences*, 32:183–221, 1986.

760

761

69 M. Vardi and P. Wolper. Reasoning about infinite computations. *I & C*, 115:1–37, 1994.
762

70 S. Vester. On the complexity of model-checking branching and alternating-time temporal logics in one-counter systems. In *ATVA'15*, volume 9364 of LNCS, pages 361-377. Springer, 2015.

763

764

71 Th. Weidner. *Probabilistic Logic, Probabilistic Regular Expressions, and Constraint Temporal Logic*. PhD thesis, University of Leipzig, 2016.

765

766