# On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories

Stéphane Demri, Raul Fervari

► To cite this version:

Stéphane Demri, Raul Fervari. On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories. 22nd International Conference on Principles of Knowledge Representation and Reasoning, Nov 2025, Melbourne, Australia. pp.260-270. hal-05353430

HAL Id: hal-05353430

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

Submitted on 7 Nov 2025

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 Attribution 4.0 International License
# On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories

Stéphane Demri¹, Raul Fervari¹,²,³

¹Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-Sur-Yvette, France

²Universidad Nacional de Córdoba, FAMAF, Argentina

³Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Argentina

## Abstract

We introduce linear-time temporal logics with past operators featuring a simple assignment modality that performs local changes on the models. Such structures are infinite sequences of valuations interpreting variables by elements from a possibly infinite data domain. We study several fragments as well as the case with the Boolean domain, for which we establish that it is actually as expressive as first-order logic over infinite sequences of propositional valuations. For the logics over concrete domains $N, Z$ and $Q$ equipped with the respective linear ordering and equality tests, we show the satisfiability problem is decidable, and that the logics are as expressive as the version without the assignment operator. Interestingly, this entails such assignments provide a huge conciseness, which is then helpful for succinct specifications.

## 1 Introduction

**Temporal logics with concrete domains.** Enriching models with data values is a natural process that has led to the study of logics over the so-called concrete domains. In such logics, constraints about the data values are part of the formulae. Prominent examples include description logics with concrete domains, see e.g. (Lutz 2002a; Lutz 2002b; Labai, Ortiz, and Simkus 2020; Baader and Rydval 2022), temporal logics with concrete domains, see e.g. (Balbiani and Condotta 2002; Carapelle 2015), and more recently the so-called LTL modulo theories, see e.g. (Felli, Montali, and Winkler 2022; Cimatti et al. 2022; Geatti et al. 2023; Geatti, Gianola, and Gigante 2025; Beutner and Finkbeiner 2025). Considering data values is a natural perspective to reason about concrete information (like a person's age or the distance between two locations), see the seminal paper (Baader and Hanschke 1991), and about data structures in general (a string, a record, etc). This framework hosts many decision problems such as satisfiability, model-checking, realizability and runtime monitoring, to cite a few examples, see e.g. (Bhaskar and Praveen 2024; Faella and Parlato 2024; Rodríguez and Sánchez 2024; Gianola, Montali, and Winkler 2025).

**Changing models.** While the generalisation of propositional variables to constraints interpreted on domains better reflects the ubiquity of data structures, other investigations deal with the ability to *modify* the models, such as in public

announcement logics (Lutz 2006), in sabotage modal logics (Aucher, van Benthem, and Grossi 2018), in alternating-time temporal logics (Catta et al. 2024; Galimullin et al. 2025) or in modal logics with graph modifiers (Aucher et al. 2009; Areces, Fervari, and Hoffmann 2015). Other approaches focus on updating the value of a variable, as e.g. in formalisms with the freeze binding mechanism. Typically, a formula $\downarrow_{r=x} \varphi$ states that freezing the current value of $x$ in the register $r$, makes $\varphi$ true. This mechanism can be traced back to works about real-time logics, see e.g. (Alur and Henzinger 1994), modal hybrid logics, see e.g. (Areces and ten Cate 2007), logics for data trees, see e.g. (Figueira 2010), and modal logics with $\lambda$-abstraction (Fitting 2002).

**Our motivations.** In this paper, we aim at understanding logical formalisms that combine theory reasoning with the ability to update the model *atomically and locally* by replacing a value at the current position by a local value (available at bounded distance). Typically, we would like to handle properties of the form *"after replacing the current value of x by the previous value of y, the formula ϕ holds true."* From the perspective of formal verification of programs, it is natural to consider methods in which explicit assignments to variables are allowed. With a similar goal in mind, different approaches on this problem have been proposed, such as the Dynamic Logics with Propositional Assignments, a family of logics designed to reason about different mental/cognitive attitudes, including planning scenarios (Herzig, Maris, and Vianey 2019), and belief revision models (Herzig 2014). Another example is that of (Belardinelli et al. 2023; Belardinelli et al. 2025), extending Epistemic Logic with program assignments, tailored to modelling the global state of a (partially observed) set of variables, unlike here in which changes are local. Herein, we would like the assignment operators to perform local changes in the models made of $\omega$-sequences of valuations $\text{Var} \to \mathcal{D}$, where $\mathcal{D}$ is a domain equipped with relations. Unlike most assignments in the literature with global effects, see e.g. (van Ditmarsch, Herzig, and de Lima 2012; Galimullin et al. 2025), *only one* value is changed at once. In our case, computational difficulties arise because the domain $\mathcal{D}$ is possibly infinite and the position $i \in N$ where the replacement is performed is not stored. We would like to design linear-time temporal logics modulo theories in which the assignment operator leads to a decidable satisfiability problem. More generally,
we investigate decidability, complexity and expressivity issues for these logics. Consequently, while we aim at studying formalisms that cannot be captured by Boolean abstractions (for instance with the domain $\mathbb{N}$), we wish to express concisely non-trivial model changes that inherently concern data values and not the structure of the models as it is usually done, see e.g. (Aucher et al. 2009). By way of example, to express the property "The formula $\varphi$ does not hold but changing somewhere the value of x by 0 and the value of y by 1 leads to a model satisfying $\varphi$", the formula

$$ \neg\varphi \wedge F(\langle x:=0 \rangle (E\langle y:=1 \rangle P(\neg X^1 \top \wedge \varphi))) $$

could do the job assuming that $E\psi$ stands for $P\psi \lor F\psi$, the connective $F$ is the standard sometimes operator from LTL and $P$ is its past counterpart. Above, $\neg X^1 \top$ holds true only at the origin of the model. As far as we know, no logical formalism related to LTL modulo theories can express naturally this simple property. Still, this can be encoded within constraint PLTL (LTL with past) if the number of variables is doubled by considering the original model and the variant model after the two assignments. This works fine for this property but it may happen that the number of changes to be considered is unbounded, typically with a pattern of the form $G\langle x:=t \rangle$. Moreover, doubling the number of variables corresponds to an implicit existential second-order quantification and we would like to express the property directly in the native language (see a similar situation in (Wolper 1983, Sec. 4) with the even property).

**Our contributions.** Concrete domains $\mathbb{D}$ are defined as sets equipped with relations. We introduce the logic PLTL-A($\mathbb{D}$) (parameterised by $\mathbb{D}$) that extends past-time linear-time temporal logic PLTL($\mathbb{D}$) (where atomic formulae are made of $\mathbb{D}$-constraints between local values), by adding unary modalities as in $\langle x:=X^n y \rangle \varphi$. The latter is read as "after the value of the variable x is replaced by the local value for $X^n y$ (past or future values of y depending whether $n < 0$), the formula $\varphi$ holds". The variables are interpreted on the domain $\mathbb{D}$. We focus here on domains of the form $(\mathbb{D}, =, <, (=_d)_{d \in \mathbb{D}})$, where $=$, < are the corresponding equality and 'less than' relations, and $=_{d}$ is an equality test with respect to the constant $d$. So typically, $\mathbb{D} \in \{\{0, 1\}, \mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$. Modalities of the form $\langle x:=d \rangle$ for some $d \in \mathbb{D}$ are also allowed. To the best of our knowledge, data updates in logics with concrete domains have been seldom investigated, see an interesting example in (Bansal, Brochenin, and Lozes 2009) involving separation logic and dynamic data structures.

After providing reductions from the satisfiability problem for PLTL-A($\mathbb{D}$) to the problem for interesting strict fragments of PLTL-A($\mathbb{D}$) (typically by bounding the number of variables, or by restricting the shape of $t$ in $\langle x:=t \rangle$), we start our investigations on the simple extension PLTL-A($\{0, 1\}$) of PLTL (also written PLTL$^=\$). We show that PLTL$^=\$ is as expressive as PLTL by providing a translation into FO($\omega$) and then evoking Kamp's Theorem (Kamp 1968; Diekert and Gastin 2008; Rabinovich 2014). We show that PLTL$^=\$ is significantly more succinct than PLTL as we prove that for every $\mathbb{D} \in \{\{0, 1\}, \mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$, the satisfiability problem for PLTL-A($\mathbb{D}$) is Tower-hard (see (Schmitz 2016) for the definition of the complexity class Tower). Indeed,

the problem is PSpace-complete for PLTL($\mathbb{D}$). Moreover, we show that for every $\mathbb{D} \in \{\{0, 1\}, \mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$, the satisfiability problem for PLTL-A($\mathbb{D}$) is decidable. To do so, we introduce a new first-order logic on multi-attributed data words (that we actually believe interesting for its own sake, see landmark logical formalisms in (Bojańczyk et al. 2011; Jurdziński and Lazić 2011; Decker et al. 2014)) that can express 'local' domain constraints from $\mathbb{D}$ (see Sec. 4.1). We establish that the satisfiability problem for this logic is decidable. The semantics for PLTL-A($\mathbb{D}$) can be internalised in this new first-order logic, thus obtaining decidability. It is worth noting that handling the concrete domains $\mathbb{N}$ and $\mathbb{Z}$ is already notoriously difficult without assignment operators, see e.g. (Segoufin and Toruńczyk 2011; Labai, Ortiz, and Simkus 2020). Our results allow us to conclude that the new assignment operators add conciseness but not expressivity. Finally, our results easily apply to variants of PLTL-A($\mathbb{D}$), e.g. on finite traces, and for other concrete domains including RCC8 and Allen's interval algebra, just to name a few examples.

## 2 PLTL with constraints and assignments

We start by introducing linear-time temporal logics extending LTL (Pnueli 1977; Gabbay et al. 1980) where propositional variables are replaced by symbolic constraints. Herein, the models are $\omega$-sequences of valuations interpreting variables by elements in the domain $\mathbb{D}$, see e.g. (Balbiani and Condotta 2002). Furthermore, modalities $\langle x:=t \rangle$ are used to build formulae whose semantical counterpart is to perform a local change in the models.

### 2.1 The logics PLTL-A($\mathbb{D}$)

**Concrete domains.** In what follows, a concrete domain is a tuple $(\mathbb{D}, =, <, (=_d)_{d \in \mathbb{D}})$, where $\mathbb{D}$ is a non-empty set of elements, $=$ is the equality relation on $\mathbb{D}$, and $<$ is a total strict ordering on $\mathbb{D}$. Moreover, $=_{d}$ is interpreted as the singleton set $\{d\}$, which is helpful to perform equality tests with respect to the constant $d$. We often simply write $\mathbb{D}$ instead of $(\mathbb{D}, =, <, (=_d)_{d \in \mathbb{D}})$.

**Syntax.** Let $\text{Var} = \{x, y, z, \dots\}$ be a countably infinite set of variables. The set of formulae for the logic PLTL-A($\mathbb{D}$) is defined by the following grammar:

$$ \varphi, \psi ::= X^n x \sim X^m y \mid X^n x = d \mid \neg \varphi \mid \varphi \lor \psi \mid X \varphi \mid X^1 \varphi \\ \qquad \mid \varphi U \psi \mid \varphi S \psi \mid \langle x:=X^m y \rangle \varphi \mid \langle x:=d \rangle \varphi, $$

where $x, y \in \text{Var}$, $n, m \in \mathbb{Z}$, $\sim \in \{=, <\}$, and $d \in \mathbb{D}$ (elements of the concrete domains $\mathbb{N}, \mathbb{Z}, \mathbb{Q}$ and $\{0, 1\}$ are encoded in binary, and similarly for any other arbitrary domain $\mathbb{D}$ considered in this paper). The expression $X^n$ (resp. $X^n$) with $n \ge 0$ stands for the sequence of length $n$ made of the symbol $X$ (resp. $X^1$) only. This corresponds to a unary encoding. Expressions of the form $X^n x$ are sometimes called terms. Sometimes, we simply write $Xx$ if $n = 1$, or just $x$ if $n = 0$, both in terms and assignments. Other operators are defined as usual, in particular $X^n x \neq t \stackrel{\text{def}}{=} -(X^n x = t)$ (with $t \in \{X^m y, d\}$), $F\varphi \stackrel{\text{def}}{=} \top U \varphi$ and $G\varphi \stackrel{\text{def}}{=} \neg F \neg \varphi$. Finally, for all $n > 0$, we write $X^n \varphi$ (resp. $X^n \varphi$) to denote a sequence made of $n$ temporal operators $X$ (resp. $X^1$).
**Semantics.** A model for PLTL-A($\mathbb{D}$) is a map $\sigma : \mathbb{N} \to (\text{Var} \to \mathbb{D})$. We write $\sigma(i)(x)$ to denote the value assigned to the variable x at the position i. Let $\sigma$ be a model, and let $i \ge 0$, the **satisfaction relation** $\models$ between $\sigma$, i and formulae is inductively defined as follows (below $\in \{=, <\}$):

$$
\begin{align*}
\sigma, i \models X^n x \sim X^m y &\stackrel{\text{def}}{\iff} i + n \ge 0, i + m \ge 0 \text{ and} \\
&\phantom{\iff} \sigma(i + n)(x) \sim \sigma(i + m)(y) \\[1em]
\sigma, i \models X^n x = d &\stackrel{\text{def}}{\iff} i + n \ge 0 \text{ and } \sigma(i + n)(x) = d \\[1em]
\sigma, i \models \neg \varphi &\stackrel{\text{def}}{\iff} \sigma, i \not\models \varphi \\[1em]
\sigma, i \models \varphi \lor \psi &\stackrel{\text{def}}{\iff} \sigma, i \models \varphi \text{ or } \sigma, i \models \psi \\[1em]
\sigma, i \models X \varphi &\stackrel{\text{def}}{\iff} \sigma, i + 1 \models \varphi \\[1em]
\sigma, i \models X^1 \varphi &\stackrel{\text{def}}{\iff} i > 0 \text{ and } \sigma, i - 1 \models \varphi \\[1em]
\sigma, i \models \varphi U \psi &\stackrel{\text{def}}{\iff} \sigma, j \models \psi \text{ for some } j \ge i \text{ s.t.} \\
&\phantom{\iff} \sigma, k \models \varphi \text{ for all } i \le k < j \\[1em]
\sigma, i \models \varphi S \psi &\stackrel{\text{def}}{\iff} \sigma, j \models \psi \text{ for some } 0 \le j \le i \text{ s.t.} \\
&\phantom{\iff} \sigma, k \models \varphi \text{ for all } j < k \le i \\[1em]
\sigma, i \models \langle x := X^n y \rangle \varphi &\stackrel{\text{def}}{\iff} i + n \ge 0 \text{ and} \\
&\phantom{\iff} \sigma[x \mapsto i \sigma(i + n)(y)], i \models \varphi \\[1em]
\sigma, i \models \langle x := d \rangle \varphi &\stackrel{\text{def}}{\iff} \sigma[x \mapsto i d], i \models \varphi,
\end{align*}
$$

where $\sigma[x \mapsto i d](j)(y) = \sigma(j)(y)$ if $j \neq i$ or x is syntactically different from y, and $\sigma[x \mapsto i d](x)(i) = d$. Note that data values at distinct positions can therefore be compared. A formula $\varphi$ is **satisfiable** iff there is a model $\sigma$ such that $\sigma, 0 \models \varphi$. The interesting formulae $\langle x := X^n y \rangle \varphi$ are those containing past-time operators in $\varphi$ as the current position may be revisited after the change of the value x.

**Example 1.** We provide here some examples of formulae.

1. The formula $(x = 0 \Rightarrow \neg \varphi) \land \langle x := Xx \rangle \mathbb{F}\varphi$ states that the current value of $x$ equals 0 implies in the future $\varphi$ never holds, but after updating the value of $x$ by the value of $x$ at the next position, $\varphi$ holds eventually in the future.

2. The formula $XG(\langle x := X^1 x \rangle \varphi)$ states that always in the future, changing the value of $x$ to its previous value makes $\varphi$ true.

3. Atomic formulae of the form $X^n x \sim X^m y$ and $X^n x = d$ are handy to express certain properties but we could restrict the language while keeping the same expressive power. Indeed, $X^n x \sim X^m y$ (resp. $X^n x = d$) is logically equivalent to $X^n \top \land X^m \top \land X^n (x \sim X^{m-n} y)$ with $n < m$ (resp. $X^n(x = d)$).

The satisfiability problem of PLTL-A($\mathbb{D}$) without assignments, written PLTL($\mathbb{D}$), has been well-studied.

**Proposition 1.** (Sistla and Clarke 1985; Balbiani and Condotta 2002; Demri and Gascon 2008; Segoufin and Toruńczyk 2011) For all the domains $\mathbb{D} \in \{(0, 1), \mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$, the satisfiability problem for PLTL($\mathbb{D}$) is PSpace-complete.

## 2.2 Bounding syntactic resources

We present our decidability/complexity/expressivity results by considering different fragments. We restrict the syntactic resources in at least two ways, seldom simultaneously.

1. Bounding the number of variables is quite natural (see Lemma 1), similarly to restricting the number of propositional variables in modal and temporal logics, see e.g. (Halpern 1995) and (Spaan 1993, Thm. 5.4.6).

2. Bounding the term depth (i.e., the values $n, m$) in expressions of the form $X^n x \sim X^m y$ or $X^n x = d$, or in assignment operators $\langle x := X^n y \rangle$ allows us to compare or assign values that are very close to the current position. Typically, the renaming technique can be used to reduce term depth $n$ to a value in $\{-1, 0, +1\}$, at the cost of introducing new auxiliary variables. If $n \in \{-1, 0, +1\}$, then we say that $\langle x := X^n y \rangle$ is an **adjacent assignment**.

It is easy to eliminate assignments of the form $\langle x := d \rangle$ by adding a new variable $y_d$, to require the satisfaction of $G(y_d = d)$ and to replace $\langle x := d \rangle$ by $\langle x := y_d \rangle$. In the sequel, whenever the number of variables is not bounded, we do not need to make use of assignments of the form $\langle x := d \rangle$.

The following results state that we can restrict the number of variables, without affecting complexity bounds.

**Lemma 1.** There is a logspace reduction from the satisfiability problem for PLTL-A($\mathbb{D}$) to its restriction to formulae with one variable only.

The proof follows a standard pattern: we encode $n$ variables into a sequence of length $n$ with only one variable. Thus, each position in a model for an arbitrary formula is encoded as a sequence. The main challenge is to uniquely identify where each sequence starts. This is done by “marking” each of such sequences with a prefix $d^{n+2}d'$, where $d^{n+2}$ stands for $n + 2$ times the value $d$, and $d' \neq d$. The encoding of a valuation at a particular position has the following shape:

$$d^{n+2} d' \sigma(i)(x_1) \sigma(i)(x_2) \dots \sigma(i)(x_n).$$

Thus, the only way of finding a sequence of $n + 2$ consecutive values, followed by a value that is different from them, is at the beginning of each sequence. It is worth noticing that for this encoding, we only need the concrete domain $\mathbb{D}$ to have at least two values, slightly improving the encoding from (Demri, Lazić, and Nowak 2007, Prop. 4).

**Example 2.** Let us consider the following encoding, and show how the translation works. Suppose we have three variables $x_1, x_2, x_3$, i.e., $n = 3$. Thus, $\sigma$ is encoded as:

$$d^5 d' \begin{array}{c} d_1^0 \\ d_2^0 \\ d_3^0 \end{array} d^5 d' d_1^1 d_2^1 d_3^1 d^5 d' \begin{array}{c} d_1^2 \\ d_2^2 \\ d_3^2 \end{array} \dots$$

where the leftmost subsequence corresponds to position 0, $d_j^i$ stands for $\sigma(i)(x_j)$ and $d^5$ is a sequence made of five copies of $d$. At each position, the single variable $x$ stores the respective value $d_j^i$. Suppose we want to perform the update $\langle x_2 := X^2 x_1 \rangle$ at position 2. This position is marked in the encoding with an $\uparrow$ below. The encoding of the assignment results as $X^7 \langle x := X^{19} x \rangle$. It is easy to check that the involved values are those inside a box.

Below, we consider another syntactic restriction by admitting only adjacent assignments but at the cost of allowing two variables (instead of a single one earlier). The second variable is used to carry a value over adjacent assignments.

**Lemma 2.** There is a logspace reduction from the satisfiability problem for PLTL-A($\mathbb{D}$) to its restriction to formulae at most two variables and adjacent assignments only.
Observe that Lemmas 1 and 2 also hold for any concrete domain $\mathbb{D}$ equipped with the equality relation and not necessarily for domains of the form $(\mathbb{D}, =, <, (=_d)_{d \in \mathbb{D}})$. Indeed, the proofs can be slightly adapted.

To conclude this section, after having manipulated PLTL-A($\mathbb{D}$) formulae and the satisfaction relation for PLTL-A($\mathbb{D}$), it should be clear that the assignments of the form $\langle x := X^n y \rangle$ are only performed locally and the modified local value for x cannot be accessed directly all over the models, unlike the effect of the freeze operator, see e.g. (Figueira and Segoufin 2009).

### 3 Satisfiability problem for PLTL-A($\{0, 1\}$)

In this section, we investigate the decidability/complexity status of the satisfiability problem for the logic PLTL-A($\{0, 1\}$) whereas Sec. 4 is devoted to the more general case PLTL-A($\mathbb{D}$) with an arbitrary concrete domain $\mathbb{D}$. We provide elementary reductions between PLTL-A($\{0, 1\}$) and the first-order logic over $\omega$-words, known to admit a Tower-complete satisfiability problem and to be expressively equivalent to the linear-time temporal logic PLTL (Kamp 1968). The class Tower introduced in (Schmitz 2016) is closed under elementary reductions and Tower-hardness captures non-elementarity. In order to stick to the notations about PLTL, first we present the logic PLTL$^=\$ defined as a syntactic variant of the logic PLTL-A($\{0, 1\}$) in which we directly manipulate propositional variables and where the assignment operator updates their truth values. Hence, all the results presented below about PLTL$^=\$ can be easily rephrased for PLTL-A($\{0, 1\}$).

**Introducing PLTL$^=\$.** Let Prop be a countably infinite set of propositional symbols. The set of PLTL$^=\$ formulae is defined by the following grammar:

$$ \varphi, \psi ::= \mathbf{p} \mid \varphi \lor \psi \mid \neg \varphi \mid X\varphi \mid X^{-1}\varphi \mid \varphi U \psi \mid \varphi S \psi \\ \qquad \mid \langle \mathbf{p} := X^n \mathbf{q} \rangle \varphi \mid \langle \mathbf{p} := \top \rangle \varphi \mid \langle \mathbf{p} := \bot \rangle \varphi, $$

where $\mathbf{p}, \mathbf{q} \in \text{Prop}$ and $n \in \mathbb{Z}$. A model for PLTL$^=\$ is a map $\sigma : \mathbb{N} \to (\text{Prop} \to \{0, 1\})$. Let $\sigma$ be a model and $i \ge 0$. The satisfaction relation $\models$ between $\sigma$ and formulae is inductively defined as follows:

$$ \begin{align*} \sigma, i \models \mathbf{p} &\iff_{\text{def}} \sigma(i)(\mathbf{p}) = 1 \\ \sigma, i \models \langle \mathbf{p} := \top \rangle \varphi &\iff_{\text{def}} \sigma[\mathbf{p} \mapsto i \ 1], i \models \varphi \\ \sigma, i \models \langle \mathbf{p} := \bot \rangle \varphi &\iff_{\text{def}} \sigma[\mathbf{p} \mapsto i \ 0], i \models \varphi \\ \sigma, i \models \langle \mathbf{p} := X^n \mathbf{q} \rangle \varphi &\iff_{\text{def}} i + n \ge 0 \text{ and} \\ &\phantom{\iff} \sigma[\mathbf{p} \mapsto i \ \sigma(i+n)(\mathbf{q})], i \models \varphi. \end{align*} $$

#### 3.1 Hardness and first-order logic over $\omega$-words

In order to analyse the decidability/complexity status of PLTL$^=\$, we need to introduce first-order logic over $\omega$-words. Then, we will rely on results from (Stockmeyer 1974).

**First-order logic FO($\omega$).** We use a signature containing Prop (used as a countable set of unary predicate symbols), two binary symbols $<$ and $=$ (standing for ‘less than’ and ‘equal’, respectively) and a function $+1$ standing for successor function. Models in FO($\omega$) are models as for PLTL$^=\$.

The syntax of FO($\omega$) is given by the following grammar:

$$ \varphi, \psi ::= \mathbf{y} = \mathbf{y} \mid \mathbf{x} < \mathbf{y} \mid \mathbf{x} = \mathbf{y} + 1 \mid \neg \varphi \mid \varphi \lor \psi \mid \mathbf{p}(\mathbf{x}) \mid \exists \mathbf{x} \varphi. $$

Let $\sigma$ be a model, and let $g: \text{Var} \to \mathbb{N}$ be a function that assigns to each variable a position (called **environment**), the **satisfaction relation** $\models$ for FO($\omega$) is defined as follows (Boolean cases are omitted):

$$ \begin{align*} \sigma \models_g \mathbf{x} \star \mathbf{y} &\iff_{\text{def}} g(\mathbf{x}) \star g(\mathbf{y}) \quad (\text{for } \star \in \{=, <\}) \\ \sigma \models_g \mathbf{x} = \mathbf{y} + 1 &\iff_{\text{def}} g(\mathbf{x}) = g(\mathbf{y}) + 1 \\ \sigma \models_g \mathbf{p}(\mathbf{x}) &\iff_{\text{def}} \sigma(g(\mathbf{x}))(\mathbf{p}) = 1 \\ \sigma \models_g \exists \mathbf{x} \varphi &\iff_{\text{def}} \text{there is } k \ge 0 \text{ such that } \sigma \models_{g'} \varphi, \end{align*} $$

where $g'$ is exactly as $g$ except that $g'(\mathbf{x}) = k$. An FO($\omega$) formula $\varphi$ is **satisfiable** iff there are a model $\sigma$ and a function $g$ such that $\sigma \models_g \varphi$.

It is shown in (Stockmeyer 1974, Thm. 5.2) that the nonemptiness problem for star-free regular expressions can be reduced in polynomial time to the satisfiability problem for FO($\omega$). By (Schmitz 2016, Sec. 3.1), the equivalence problem SFEq for star-free expressions (that can be reduced to the nonemptiness problem) is Tower-complete. Consequently, satisfiability problem for FO($\omega$) is Tower-hard. Moreover, FO($\omega$) is a fragment of the monadic second-order logic MSO over $\omega$-words and MSO formulae can be turned into equi-expressive Büchi automata (Büchi 1962) with an effective automaton construction. This entails a Tower-membership for MSO satisfiability, and thus for FO($\omega$). Tower-hardness of FO($\omega$) is used to show Tower-hardness of the satisfiability problem of PLTL$^=\$.

**Lemma 3.** *There is a logspace reduction from the satisfiability problem for FO($\omega$) to the one for PLTL$^=\$.*

**Proof.** Let $\varphi$ be an FO($\omega$) sentence built over the unary predicates $p_1, \dots, p_\beta$ and the individual variables $x_1, \dots, x_\alpha$. Without any loss of generality, we can assume that distinct quantifier occurrences use distinct variables. We define a translation map $t$ into PLTL$^=\$ using the auxiliary propositional variables $q_1, \dots, q_\alpha$ such that $\varphi$ is FO($\omega$)-satisfiable iff $G(\bigwedge_{j=1}^\alpha \neg q_j) \land t(\varphi)$ is PLTL$^=\$-satisfiable.

The role of each propositional variable $q_j$ is to hold true at most at one position $k$, in order to encode the fact that the variable $x_j$ is interpreted by the position $k$. Initially, $q_j$ does not hold anywhere, which means that no value is assigned to the variable $x_j$. The translation $t$ is homomorphic for Boolean connectives and satisfies the clauses below.

* $t(\exists \mathbf{x}_j \psi) \stackrel{\text{def}}{=} E\langle \mathbf{q}_j := \top \rangle t(\psi)$ (E$\chi$ shortcut for $F\chi \lor P\chi$),

* $t(\mathbf{x}_i = \mathbf{x}_j) \stackrel{\text{def}}{=} E(\mathbf{q}_i \land \mathbf{q}_j)$; $t(\mathbf{x}_j = \mathbf{x}_i + 1) \stackrel{\text{def}}{=} E(\mathbf{q}_i \land \mathbf{Xq}_j)$.

* $t(\mathbf{x}_i < \mathbf{x}_j) \stackrel{\text{def}}{=} E(\mathbf{q}_i \land \mathbf{XFq}_j)$; $t(\mathbf{p}_i(\mathbf{x}_j)) \stackrel{\text{def}}{=} E(\mathbf{p}_i \land \mathbf{q}_j)$.

In order to prove the correctness of the reduction, we introduce a relation $\sigma, g \sim \sigma'$ between an FO($\omega$)-model $\sigma$ and an environment $g: \{x_1, \dots, x_\alpha\} \to \mathbb{N}$ (partial function) and an PLTL$^=\$ model $\sigma' : \mathbb{N} \to (\{p_1, \dots, p_\beta, q_1, \dots, q_\alpha\} \to \{0, 1\})$ satisfying the following clauses.

* For all $i \in \mathbb{N}$ and $j \in [1, \beta]$, $\sigma(i)(\mathbf{p}_j) = \sigma'(i)(\mathbf{p}_j)$.

* Let $j \in [1, \alpha]$. If the map $g$ is defined on $x_j$, then $\sigma'(g(x_j))(\mathbf{q}_j) = 1$ and for all $i \ne g(x_j)$, $\sigma'(i)(\mathbf{q}_j) = 0$. Otherwise, for all $i \in \mathbb{N}$, $\sigma'(i)(\mathbf{q}_j) = 0$.
The following properties can be easily established and are useful to complete the proof.

(P1) Given $\sigma$ and $g: \{x_1, \dots, x_\alpha\} \to \mathbb{N}$, there is a unique model $\sigma'$ such that $\sigma, g \sim \sigma'$.

(P2) Given $\sigma': \mathbb{N} \to (\{p_1, \dots, p_\beta, q_1, \dots, q_\alpha\} \to \{0, 1\})$ such that for all $j \in [1, \alpha]$, there is at most one position $i \in \mathbb{N}$ such that $\sigma'(i)(q_j) = 1$, there are a unique model $\sigma$ and environment $g$ such that $\sigma, g \sim \sigma'$.

By structural induction, one can show that if $\sigma, g \sim \sigma'$, then for all subformulae $\psi$ of $\varphi$ such that $g$ is defined for the free variables in $\psi$, we have $\sigma \Vdash_g \psi$ iff (for all $i \in \mathbb{N}$, we have $\sigma', i \Vdash t(\psi)$). $\square$

Notice that the reduction in the proof of Lemma 3 is logspace because the size of formulae is assumed to be the cardinality of its set of subformulae. Any other reasonable definitions for sizes would lead anyhow to elementary reductions, which is sufficient to get Tower-hardness. By using Lemmas 1 and 2, as well as Lemma 3 and the Tower-hard of FO($\omega$), we get the following results.

**Lemma 4.** *The satisfiability problem of PLTL<sup>=</sup> restricted to formulae with a single propositional variable (resp. with at most two propositional variables and adjacent assignments only) is Tower-hard.*

## 3.2 Introduction to symbolic assignments

In order to show that the satisfiability problem for PLTL<sup>=</sup> is in Tower, we define a faithful and polynomial-space reduction to FO($\omega$) (see Sec. 3.3).

First, let us identify a fragment of PLTL<sup>=</sup> to which the satisfiability problem for PLTL<sup>=</sup> can be reduced in logspace, and from which the forthcoming translation to FO($\omega$) becomes smoother. The flat fragment of PLTL<sup>=</sup> is defined as the fragment of PLTL<sup>=</sup> in which the only authorised modalities of the form $\langle p:=X^nq \rangle$ satisfy $n=0$, i.e., no strict past or future truth values are involved.

**Lemma 5.** *There is a logspace reduction from the satisfiability problem for PLTL<sup>=</sup> to the one for its flat fragment.*

*Proof.* (sketch) Let $\varphi$ be a PLTL<sup>=</sup> formula and $M \in \mathbb{N}$ be the minimal value such that for all modalities $\langle p:=X^nq \rangle$ occurring in $\varphi$, we have $|n| \le M$. Let $p_1, \dots, p_N$ be the propositional variables occurring in $\varphi$. To define the target formula in the flat fragment, we introduce the variables $p_j^i$ with $i \in [-M, +M]$ so that $p_j^i$ plays the role of the term $X_j^i p_j$. The formula $\varphi_{N,M}$ defined below specifies unambiguously what is expected from the new propositional variables.

$$G(\bigwedge_{i \in [0, M-1], j \in [1, N]} (p_j^{-i} \Leftrightarrow X_{p_j}^{-(i+1)} \wedge p_j^{i+1} \Leftrightarrow X_{p_j}^i) \wedge \bigwedge_{j \in [1, N]} p_j \Leftrightarrow p_j^0).$$

Furthermore, we define a translation map $t$ that is homomorphic for Boolean and temporal connectives, for modalities of the form $\langle p_j:=\top \rangle$ and $\langle p_j:=\bot \rangle$, and is equal to identity for propositional variables. The new variables that are part of the renaming techniques play their full role for the translation of formulae whose outermost connective is of the form $\langle p_j:=X^n p_k \rangle$. However, after performing local changes, we need to maintain the satisfaction of $\varphi_{N,M}$ (with the new

value), which causes some complications in the definition of the map $t$. Typically, changing the value of $p_j$ at position $i$, requires to update the variable $p_j^m$ at position $i+m$, for all $m \in [-M, M]$ such that $i+m \ge 0$. Below, $n \in [-M, M]$.

$$t(\langle p_j := X^n p_k \rangle \psi) \stackrel{\text{def}}{=} X^{n\top} \wedge \\ \langle p_j := p_k^n \rangle ((p_j \Rightarrow \psi_{\top}) \wedge (\neg p_j \Rightarrow \psi_{\bot})),$$

where the formulae $\psi_{\top}$ and $\psi_{\bot}$ are defined below. Given a truth value $b \in \{\bot, \top\}$ and $\gamma \in [1, M]$, we write $O^b(\gamma, \psi_1, \psi_2)$ to denote the formula $X^{1\top} \Rightarrow X^{1\bot} \langle p_j^\gamma := b \rangle \psi_2 \wedge \neg X^{1\top} \Rightarrow X^{\gamma-1} \psi_1$.

$$\psi_b \stackrel{\text{def}}{=} \langle p_j^0 := b \rangle (X \langle p_j^{-1} := b \rangle) \cdots (X \langle p_j^{-M} := b \rangle) X^{-M} \\ O^b(1, t(\psi), O^b(2, t(\psi), O^b(3, t(\psi), \dots, \\ O^b(M, t(\psi), X^M t(\psi), \dots))).$$

It is easy to check that $\varphi_{N,M} \wedge t(\varphi)$ belongs to the flat fragment of PLTL<sup>=</sup> and assuming that the size of a formula is its number of subformulae, it can be computed in logspace in the size of $\varphi$. One can show that $\varphi$ is satisfiable iff $\varphi_{N,M} \wedge t(\varphi)$ is satisfiable. $\square$

For the translation into FO($\omega$), we can assume that the source formula belongs to the flat fragment of PLTL<sup>=</sup>. Furthermore, before defining the translation, we introduce auxiliary notions such as symbolic assignments and symbolic contexts. Such syntactic objects are designed so that an argument of the translation map (to be defined) contains a symbolic context that corresponds to the sequence of symbolic assignments that have been performed so far.

A **symbolic assignment** is defined as an expression of the form $(p, e, y)$, where $p$ is a propositional variable, $e$ is an individual variable, and $e$ is either a truth constant or a propositional variable $q$. By way of example, $(p, q, y)$ encodes the process of updating the truth value of the propositional variable $p$ at the position $y$ with the truth value of the propositional variable $q$ at the position $y$. For such a statement to be formally correct, we still need an environment $g$ to interpret the variable $y$ so that we can really specify a position in $\mathbb{N}$. Given a sequence $S$ of symbolic assignments, written $(p_{i_1}, e_1, y_1), \dots, (p_{i_N}, e_N, y_N)$, we write $S[j, j']$ to denote its subsequence $(p_{i_j}, e_j, y_j), \dots, (p_{i_{j'}}$, $e_{j'}, y_{j'})$. Such a sequence $S$ is called a **symbolic context**.

Given a symbolic context $S$, to be able to apply the sequence of symbolic assignments from $S$ to a given model $\sigma$, we need an environment $g$ to interpret the individual variables occurring in $S$. That is why we define below the model update($\sigma, S, g$) that is intended to be the model $\sigma$ on which the local changes from the symbolic context $S$ are performed but under the environment $g$. Assuming that $S$ is of the form $(p_{i_1}, e_1, y_1), \dots, (p_{i_N}, e_N, y_N)$, the model update($\sigma, S, g$) is defined according to the clauses below.

* update($\sigma, \varepsilon, g$) $\stackrel{\text{def}}{=} \sigma$,

* if $N > 0$, then update($\sigma, S, g$) $\stackrel{\text{def}}{=} update(\sigma, S[1, N-1], g)[p_{i_N} \mapsto g(y_N) V_N]$,

where $V_N = \text{update}(\sigma, S[1, N-1], g)(g(y_N))(q)$ if $e_N = q, V_N = 1$ if $e_N = \top$, and $V_N = 0$ if $e_N = \bot$.
The last preliminary property that we need to establish is related to the value update($\sigma$, $S$, $g$)(i)(p) for some position i and some propositional variable p. Indeed, Lemma 6 below shall be essential to translate propositional variables.

**Lemma 6.** Let $\sigma$ be a model, $g$ be an environment, $S$ be a symbolic context $(p_i, e_1, y_1), \dots, (p_{i_N}, e_N, y_N)$, $i \in \mathbb{N}$ and $p \in \text{Prop}$. The value update($\sigma$, $S$, $g$)(i)(p) is obtained among the three disjoint cases below.

(I) If there is no $k$ such that $p = p_{i_k}$, then update($\sigma$, $S$, $g$)(i)(p) = $\sigma(i)(p)$.

(II) If (I) does not hold and for all $k$ such that $p = p_{i_k}$, we have $g(y_k) \neq i$, then update($\sigma$, $S$, $g$)(i)(p) = $\sigma(i)(p)$.

(III) If both (I) and (II) do not hold and $k = \max\{k' \mid g(y_{k'}) = i, p_{i_k'} = p\}$, then update($\sigma$, $S$, $g$)(i)(p) = update($\sigma$, $S$[1, $k-1$], $g$)(i)(q) with $e_k = q$. If $e_k$ takes the value $\perp$ or $\top$, then update($\sigma$, $S$, $g$)(i)(p) takes the value 0 or 1, respectively.

### 3.3 The translation map

We define a translation map $t$ from the flat fragment of PLTL$^=$ to FO($\omega$) that generalises the translation from PLTL into first-order logic (Kamp 1968). Instead of having only two arguments, namely the formula $\varphi$ to be translated and an individual variable $y$ interpreted as the position on which the formula $\varphi$ is evaluated, we add a third argument that encodes the succession of assignments, namely a symbolic context. The new cases are those for propositional variables and for assignments.

* $t(\psi \lor \psi', y, S) \stackrel{\text{def}}{=} t(\psi, y, S) \lor t(\psi', y, S)$. The translation for other Boolean cases is similar. Moreover, $t(\top, y, S) \stackrel{\text{def}}{=} \top$, $t(\bot, y, S) \stackrel{\text{def}}{=} \bot$ and $t(\psi S \psi', y, S) \stackrel{\text{def}}{=} \exists y' (y' \le y) \land t(\psi', y', S) \land (\forall y'' (y' < y'') \le y) \Rightarrow t(\psi, y'', S)$. The translation of formulae with another outermost temporal connective, is defined similarly based on the internalisation of PLTL semantics into FO($\omega$).

* The new cases are handled now. To start with, $t(\langle p:=q \rangle, \psi, y, S) \stackrel{\text{def}}{=} t(\psi, y, S \cdot (p, q, y))$ and for $B \in \{\bot, \top\}$, $t(\langle p:=B \rangle, \psi, y, S) \stackrel{\text{def}}{=} t(\psi, y, S \cdot (p, B, y))$.

* If there is no $j$ such that $p = p_{i_j}$ from $S$, then $t(p, y, S) \stackrel{\text{def}}{=} p(y)$ (which is the usual definition for PLTL, say with $S = \varepsilon$). This corresponds to case (I) in Lemma 6. Otherwise,

$$ t(p, y, S) \stackrel{\text{def}}{=} \left( \bigwedge_{j \text{ s.t. } p_{i_j} = p} (y_j \neq y) \land p(y) \right) \lor \\ \bigvee_{j \text{ s.t. } p_{i_j} = p} \left( \bigwedge_{j' \text{ s.t. } p_{i_{j'}} = p \text{ and } j' > j} (y_{j'} \neq y) \right) \land (y_j = y) \land \\ t(e_j, y_j, S[1, j-1]). $$

The first (resp. second) line corresponds to case (II) (resp. (III)), concluding the definition of $t$.

It is also possible to use shortcuts, for instance to translate E-formulae with the clause $t(E\psi, y, S) = \exists y' t(\psi, y', S)$. By way of example, the translation of $E\langle p:=q \rangle E\langle r:=p \rangle r$ is provided below (after a few propositional simplifications):

$$ \exists y_1 \exists y_2 ((y_2 = y_1) \land q(y_1)) \lor ((y_2 \neq y_1) \land p(y_2)). $$

**Lemma 7.** $\varphi$ is PLTL$^=$ satisfiable iff $\exists y (\neg \exists y' y' < y) \land t(\varphi, y, \varepsilon)$ is FO($\omega$) satisfiable.

In Lemma 7, we do not only use $t(\varphi, y, \varepsilon)$ as a target formula in FO($\omega$) because satisfiability of PLTL$^=$ formulae is defined from the origin position. Then, we get:

**Lemma 8.** There is a polynomial-space reduction from the satisfiability problem for PLTL$^=$ to the one for FO($\omega$).

We designed a reduction to FO($\omega$) leading to the decidability of the satisfiability problem for PLTL$^=$. We also get Tower-membership since the map $t$ induces a polynomial-space reduction to the satisfiability problem for FO($\omega$).

**Variants of symbolic contexts.** The idea of using a context made of the symbolic representation of a finite set of assignments to perform the translation into FO($\omega$) is reminiscent of the translation from sabotage modal logic and from other relation-changing logics into first-order logic, see e.g. (Aucher, van Benthem, and Grossi 2018, Sec. 2.3) and (Areces, Fervari, and Hoffmann 2015, Sec. 3.2). There, a context made of the symbolic representation of a finite set of edges is carried along the translation. Indeed, the two types of context encode different pieces of information but in both cases, there is some record of a finite amount of information about the modifications made on the original model. As far as assignments are concerned, the ordering is important; that is why sequences of the symbolic representation of assignments are involved. It is also worth noting that in (Belardinelli et al. 2023, Sec. 3), a program-epistemic logic admitting assignments is translated into FO but it is based on principles different from ours, though it obviously shares the idea of internalising the semantics of the source logic.

**Extension to arbitrary formula assignments.** In PLTL$^=$, it is possible to assign constant truth values or the values of propositional variables. However, we may wish to allow expressions of the form $\langle p:=\varphi \rangle \psi$, where $\varphi$ is an arbitrary formula of PLTL$^=$ (as done globally in e.g. (van Ditmarsch, Herzig, and de Lima 2012; Galimullin et al. 2025)). The formula $\langle p:=\varphi \rangle \psi$ can be internalised in PLTL$^=$ by:

$$ \varphi \Rightarrow \langle p:=\top \rangle \psi \land \neg \varphi \Rightarrow \langle p:=\bot \rangle \psi. $$

Thus, we directly obtain:

**Theorem 1.** The satisfiability problem for PLTL$^=$ extended with arbitrary assignments is Tower-complete.

As a consequence, the satisfiability problem for PLTL-A($\{0, 1\}$) is also Tower-complete. It is worth noting that we would get a similar complexity with the model-checking problem. Indeed, given a set of propositional variables $p_1, \dots, p_n$, the set of models for PLTL$^=$ can be generated by some one-state transition system with $2^n$ edges labelled by assignments on $p_1, \dots, p_n$. Consequently, the existential model-checking problem for FO($\omega$) is also Tower-hard (by an exponential-time reduction from the satisfiability problem). Using the encoding of Lemma 3, we conclude that the existential model-checking problem for PLTL-A is also Tower-hard. For concrete domains handled in Section 4, we can get a similar conclusion.
# 4 How to decide satisfiability for PLTL-A($\mathbb{D}$)

In this section, we consider the satisfiability problem for the linear-time temporal logic PLTL-A($\mathbb{D}$) with $\mathbb{D} \in \{\mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$. To do so, we rely on the proof methods from Sec. 3 dedicated to PLTL-A($\{0, 1\}$) though we generalise them in several directions. Recall that in the case of PLTL-A($\mathbb{D}$), in the formula $\langle x := Xx' \rangle \varphi$, the variable $x$ takes the next value of $x'$ that belongs to a potentially infinite set $\mathbb{D}$. The reduction from PLTL-A($\{0, 1\}$) to FO($\omega$) in Sec. 3 can be extended to PLTL-A($\mathbb{D}$). However, we need a target logic interpreted over $\omega$-sequences of tuples in $\mathbb{D}^\beta$ and therefore it is necessary to consider the appropriate decidable logic on multi-attributed data words if it exists. We know that first-order logic over multi-attributed data words with two data values per position is undecidable (even restricted to two variables), as well as over data words with one data value per position and three quantified variables (Bojańczyk et al. 2011) (see also other logics over multi-attributed data words in (Decker et al. 2014; Bollig, Sangnier, and Stietel 2024)).

Additionally, the satisfiability problem for FO2 with one datum per position and data equality only is shown equivalent to the reachability problem for Petri nets (Bojańczyk et al. 2011). This problem is shown Ack-complete (Leroux and Schmitz 2019; Czerwinski and Orlikowski 2021; Leroux 2021). To aim for decidability here, it is necessary to devise appropriate syntactic restrictions. This is precisely what we perform in Sec. 4.1 to design the logic FO$^{loc}$(β).

To start with, we establish Tower-hardness by using the Tower-hardness of PLTL-A($\{0, 1\}$), and requiring that every data value at every position is either 0 or 1.

**Theorem 2.** For all $\mathbb{D} \in \{\mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$, the satisfiability problem for PLTL-A($\mathbb{D}$) is Tower-hard.

In order to prove that PLTL-A($\mathbb{D}$) is decidable, we introduce a new first-order logic interpreted on multi-attributed data words whose satisfiability problem is shown decidable.

## 4.1 A new logic on multi-attributed data words

Given $\beta \ge 1$, we define the first-order logic FO$^{loc}$(β) interpreted on multi-attributed data words in $(\mathbb{D}^\beta)^\omega$. Observe that our multi-attributed data words do not use any additional finite alphabet because this can be simulated by increasing the dimension $\beta$ and using equality constraints. The dimension $\beta$ is intended to capture the number of variables in the PLTL-A($\mathbb{D}$) formula to be translated.

Quantifications in FO$^{loc}$(β) range over positions of the infinite multi-attributed data word as in FO($\omega$). The language for FO$^{loc}$(β) includes comparison predicates for positions = and <, as well as the successor relation +1. To access the $\beta$ data values at a given position, we introduce the unary symbols $f_1, \dots, f_\beta$ (as concrete features in description logics with concrete domains, see e.g. (Borgwardt, Bortoli, and Koopmann 2024)). Recall that to get decidability, syntactic restrictions are necessary. This is precisely what we perform below to define FO$^{loc}$(β) by requiring that data constraints of the form $f_i(x + k_1) \simeq f_j(x' + k_2)$ and $f_i(x + k_1) < f_j(x' + k_2)$ (with shifts $k_1, k_2 \in \mathbb{Z}$) are authorised only if $x$ is equal to $x'$ syntactically.

The syntax of FO$^{loc}$(β) is defined by the grammar:

$$ \varphi, \psi ::= \mathbf{x} = \mathbf{y} \mid \mathbf{x} < \mathbf{y} \mid \mathbf{x} = \mathbf{y} + 1 \mid \neg \varphi \mid \varphi \lor \psi \\ | f_i(\mathbf{x} + k_1) \simeq f_j(\mathbf{x} + k_2) \mid f_i(\mathbf{x} + k_1) \simeq d \\ | f_i(\mathbf{x} + k_1) < f_j(\mathbf{x} + k_2) \mid \exists \mathbf{x} \varphi, $$

with $\mathbf{x}, \mathbf{y} \in \text{Var}$, $k_1, k_2 \in \mathbb{Z}$, $i, j \in [1, \beta]$ and $d \in \mathbb{D}$. Models are of the form $(\mathbb{D}^\beta)^\omega$. Given $w \in (\mathbb{D}^\beta)^\omega$ and $g: \text{Var} \to \mathbb{N}$, the relation $\models$ is defined as follows (Boolean cases omitted).

$$ w \models_g \mathbf{x} \star \mathbf{y} \quad \overset{\text{def}}{\iff} \quad g(\mathbf{x}) \star g(\mathbf{y}) \quad (\star \in \{=, <\}) $$

$$ w \models_g \mathbf{x} = \mathbf{y} + 1 \quad \overset{\text{def}}{\iff} \quad g(\mathbf{x}) = g(\mathbf{y}) + 1 $$

$$ w \models_g f_i(\mathbf{x} + k_1) \simeq f_j(\mathbf{x} + k_2) \overset{\text{def}}{\iff} \begin{array}{l} g(\mathbf{x}) + \min(k_1, k_2) \ge 0 \text{ and} \\ w(g(\mathbf{x}) + k_1)(i) = w(g(\mathbf{x}) + k_2)(j) \end{array} $$

$$ w \models_g f_i(\mathbf{x} + k_1) < f_j(\mathbf{x} + k_2) \overset{\text{def}}{\iff} \begin{array}{l} g(\mathbf{x}) + \min(k_1, k_2) \ge 0 \text{ and} \\ w(g(\mathbf{x}) + k_1)(i) < w(g(\mathbf{x}) + k_2)(j) \end{array} $$

$$ w \models_g f_i(\mathbf{x} + k_1) \simeq d \quad \overset{\text{def}}{\iff} \quad g(\mathbf{x}) + k_1 \ge 0 \text{ and} \\ w(g(\mathbf{x}) + k_1)(i) = d $$

$$ w \models_g \exists \mathbf{x} \varphi \quad \overset{\text{def}}{\iff} \quad \text{there is } k \ge 0 \text{ s.t. } w \models_{g'} \varphi, $$

where $g'$ is exactly as $g$ except that $g'(x) = k$. It is worth noting that the logic FO$^{loc}$(β) contains two types of atomic formulae, those expressing constraints between positions (e.g. $\mathbf{x} = \mathbf{y} + 1$) and those expressing constraints between data values (e.g. $f_1(\mathbf{x}) \simeq f_3(\mathbf{x} + 2)$).

## 4.2 Symbolic assignments and translation

Below, we smoothly generalise what is done in Sec. 3.2 and in Sec. 3.3. Since $\mathbb{D}$ is infinite, we cannot take advantage of the existence of Lemma 5 and therefore the translation map and its correctness proof are a bit more complicated. Anyway, we rely on such previous sections whenever possible since the general idea of the translation that internalises the semantics of PLTL-A($\mathbb{D}$) is very similar.

A **symbolic assignment** is defined as an expression of the form $(\mathbf{x}, e, \mathbf{y})$, where $\mathbf{x}$ is a variable in PLTL-A($\mathbb{D}$), $\mathbf{y}$ is an individual variable in FO$^{loc}$(β), and $e$ is either a datum $d \in \mathbb{D}$ or a term of the form $\mathbf{X}^n \mathbf{x}'$. The **shift** of $e$, written $\text{shift}(e)$, is $n$ if $e$ is of the form $\mathbf{X}^n \mathbf{x}'$, otherwise it is 0. A **symbolic context** $\mathcal{S}$ is defined as a finite sequence of symbolic assignments (possibly empty). Given an environment $g$, we say that $\mathcal{S}$ is compatible with $g$ iff for every symbolic assignment $(\mathbf{x}, e, \mathbf{y})$ occurring in $\mathcal{S}$, we have $g(\mathbf{y}) + \text{shift}(e) \ge 0$.

Lemma 6 can be easily generalised. The only substantial difference rests on the requirement that $\mathcal{S}$ is compatible with $g$. Assuming that $\mathcal{S}$ is a symbolic context of the form $(\mathbf{x}_{\alpha_1}, e_1, \mathbf{y}_1), \dots, (\mathbf{x}_{\alpha_N}, e_N, \mathbf{y}_N)$ and $g$ is an environment such that $\mathcal{S}$ is compatible with $g$, the model $\text{update}(\sigma, \mathcal{S}, g)$ is defined according to the clauses below.

* $\text{update}(\sigma, \varepsilon, g) \stackrel{\text{def}}{=} \sigma$,

* if $N > 0$, then $\text{update}(\sigma, \mathcal{S}, g) \stackrel{\text{def}}{=} \text{update}(\sigma, \mathcal{S}[1, N-1], g)[x_{i_N} \mapsto g(\mathbf{y}_N) V_N]$,

where $V_N = \text{update}(\sigma, \mathcal{S}[1, N-1], g)(g(\mathbf{y}_N) + n)(x')$, if $e_N = \mathbf{X}^n \mathbf{x}'$, and $V_N = d$ if $e_N = d$. By compatibility, we have $g(\mathbf{y}_N) + n \ge 0$.
We define a translation map $t$ from PLTL-A($\mathbb{D}$) to FO$^{\text{loc}}(\beta)$ generalising that from PLTL into FO($\omega$) (Kamp 1968) and what is done in Sec. 3.3. The new cases are for atomic formulae and for assignments.

* Again, $t(\langle x:=X^n x' \rangle \psi, y, S) \stackrel{\text{def}}{=} t(\psi, y, S \cdot (x, X^n x', y))$. Similarly, $t(\langle x:=d \rangle \psi, y, S) \stackrel{\text{def}}{=} t(\psi, y, S \cdot (x, d, y))$.

* Let us focus on the translation of $X^n x_i = X^m x_j$. If there is no $k$ such that $\alpha_k = i$ or $\alpha_k = j$, then

$$t(X^n x_i = X^m x_j, y, S) \stackrel{\text{def}}{=} f_i(y+n) \simeq f_j(y+m).$$

Otherwise, the translation distinguishes three cases. Indeed, either the variables $x_i$ and $x_j$ may be present in the $x_{\alpha_k}$'s but not at the “positions” $y+n$ and $y+m$, respectively; or the last update is for $x_i$ at position $y+n$ (resp. $x_j$ at position $y+m$). Then, define $t(X^n x_i = X^m x_j, y, S) \stackrel{\text{def}}{=} (\bigwedge_{k \text{ s.t. } \alpha_k=i} (y_k \neq y+n) \wedge \bigwedge_{k \text{ s.t. } \alpha_k=j} (y_k \neq y+m) \wedge f_i(y+n) \simeq f_j(y+m)) \vee \bigvee_{k \text{ s.t. } \alpha_k=i} (\bigwedge_{k' \text{ s.t. } \alpha_{k'}=i \text{ and } k'>k} (y_{k'} \neq y+n) \wedge \bigwedge_{k' \text{ s.t. } \alpha_{k'}=j \text{ and } k'>k} (y_{k'} \neq y+m) \wedge (y_k = y+n) \wedge t_1(e_k, S[1, k-1]) \vee \bigvee_{k \text{ s.t. } \alpha_k=j} (\bigwedge_{k' \text{ s.t. } \alpha_{k'}=i \text{ and } k'>k} (y_{k'} \neq y+n) \wedge \bigwedge_{k' \text{ s.t. } \alpha_{k'}=j \text{ and } k'>k} (y_{k'} \neq y+m) \wedge (y_k = y+m) \wedge t_2(e_k, S[1, k-1]),$

$$\begin{align*}
& (\bigwedge_{k \text{ s.t. } \alpha_k=i} (y_k \neq y+n) \wedge \bigwedge_{k \text{ s.t. } \alpha_k=j} (y_k \neq y+m) \wedge f_i(y+n) \simeq f_j(y+m)) \vee \\
& \qquad \bigvee_{k \text{ s.t. } \alpha_k=i} (\bigwedge_{k' \text{ s.t. } \alpha_{k'}=i \text{ and } k'>k} (y_{k'} \neq y+n) \wedge \\
& \qquad \qquad \bigwedge_{k' \text{ s.t. } \alpha_{k'}=j \text{ and } k'>k} (y_{k'} \neq y+m) \wedge (y_k = y+n) \wedge t_1(e_k, S[1, k-1]) \\
& \qquad \bigvee_{k \text{ s.t. } \alpha_k=j} (\bigwedge_{k' \text{ s.t. } \alpha_{k'}=i \text{ and } k'>k} (y_{k'} \neq y+n) \wedge \\
& \qquad \qquad \bigwedge_{k' \text{ s.t. } \alpha_{k'}=j \text{ and } k'>k} (y_{k'} \neq y+m) \wedge (y_k = y+m) \wedge t_2(e_k, S[1, k-1]),
\end{align*}$$

where $t_1(e_k, S[1, k-1])$ and $t_2(e_k, S[1, k-1])$ are defined as follows. If $e_k = d$ then $t_1(e_k, S[1, k-1])$ is equal to $f_i(y+n) \simeq d$ and $t_2(e_k, S[1, k-1])$ is equal to $f_j(y+m) \simeq d$. Otherwise, if $e_k = X^{n'} x_\ell$, then

$$t_1(e_k, S[1, k-1]) \stackrel{\text{def}}{=} t(X^{n+n'} x_\ell = X^m x_j, y, S[1, k-1]), \\ t_2(e_k, S[1, k-1]) \stackrel{\text{def}}{=} t(X^n x_i = X^{m+n'} x_\ell, y, S[1, k-1]).$$

Above, first-order terms of the form $y+\ell$ with $\ell \in \mathbb{Z}$ are used. By adding the prefix $\exists x_0 \dots \exists x_\ell (x_0 = x) \wedge (x_1 = x_0 + 1) \wedge \dots \wedge (x_\ell = x_{\ell-1} + 1)$ into the formula right after every quantification of $x$, and replacing atomic formula using $x+\ell$ by $x_\ell$, we capture the intended effect in FO$^{\text{loc}}(\beta)$, assuming $\ell \ge 0$. Hence, we can assume FO$^{\text{loc}}(\beta)$ admits such terms without increasing its expressive power; negative shifts are handled in a similar way.

The translation is defined by cases just as in Lemma 6. Apart from the two cases in which no update affects $x_i$ nor $x_j$, the last part of the translation states that whenever $k$ is the last position of interest (e.g., it is the position of $S$ where the last update of $x_i$ appears w.r.t. the relative position $y+n$), a recursive call is performed. In such a call, the value of $X^n x_i$ is replaced as indicated by $e_k$ (if $e_k = X^{n'} x_\ell$, then a shift of $n+n'$ from $y$ is needed). The translation of $X^n x_i < X^m x_j$ is as above, except that occurrences of $\simeq$ must be replaced by $<$.

* The translation of $X^n x_i = d$ is a simplified version of the previous case. If there is no $k$ such that $\alpha_k = i$, then $t(X^n x_i = d, y, S) \stackrel{\text{def}}{=} f_i(y+n) \simeq d$. Otherwise,

$$\begin{align*}
t(X^n x_i = d, y, S) \stackrel{\text{def}}{=} & \left( \bigwedge_{k \text{ s.t. } \alpha_k=i} (y_k \neq y+n) \wedge f_i(y+n) \simeq d \right) \\
& \vee \bigvee_{k \text{ s.t. } \alpha_k=i} \left( \bigwedge_{k' \text{ s.t. } \alpha_{k'}=i \text{ and } k'>k} (y_{k'} \neq y+n) \wedge \right. \\
& \qquad \left. (y_k = y+n) \wedge t'(e_k, S[1, k-1]), \right. \\
& \text{with } t'(e_k, S[1, k-1]) \text{ defined as follows. In case that } e_k = d', \text{ if } d' = d, \text{ then } t'(e_k, S[1, k-1]) \text{ is equal to } \top, \\
& \text{otherwise it is equal to } \bot. \text{ If } e_k = X^{n'} x_\ell, \text{ then}
\end{align*}$$

$$t'(e_k, S[1, k-1]) \stackrel{\text{def}}{=} t(X^{n+n'} x_\ell = d, y, S[1, k-1]).$$

Again, it is also possible to use shortcuts, for instance to translate E-formulae with the clause $t(E\psi, y, S) = \exists y' t(\psi, y', S)$. By way of example, the translation of

$$E\langle x_1 := X x_2 \rangle E\langle x_3 := X x_1 \rangle X x_1 = XX x_3 \text{ is provided below (after simplifications):}$$

$$\exists y_1 \exists y_2 ((y_2 \neq y_2+2) \wedge (y_1 \neq y_2+1) \wedge f_1(y_2+1) \simeq f_3(y_2+2)) \vee ((y_2 \neq y_2+2) \wedge (y_1 = y_2+1) \wedge f_2(y_2+2) \simeq f_3(y_2+2)).$$

Thus, we can establish the following crucial result with a proof generalising the proof of Lemma 7.
**Lemma 9.** Assuming that $\varphi$ contains at most $\beta$ variables, we have $\varphi$ is PLTL-A($\mathbb{D}$) satisfiable iff $\exists y (\neg \exists y' y' < y) \wedge t(\varphi, y, \varepsilon)$ is FO$^{\text{loc}}(\beta)$ satisfiable.

Thus, the satisfiability problem for FO$^{\text{loc}}(\beta)$ with $\beta \ge 1$ is Tower-hard. Indeed, by combining Lemma 1, Thm. 2 and Lemma 9, we get Tower-hardness of FO$^{\text{loc}}(1)$.

## 4.3 How to decide FO$^{\text{loc}}(\beta)$ satisfiability

Below, we characterise the satisfiability status of some FO$^{\text{loc}}(\beta)$ formula by taking advantage of decision procedures to solve the satisfiability problem for PLTL($\mathbb{D}$).

Given an FO$^{\text{loc}}(\beta)$ formula $\varphi$, typically built over atomic formulae of the form $f_i(x+k_1) \simeq f_j(x+k_2)$, $f_i(y+k_1) < f_j(y+k_2)$ and $f_i(z+k_1) \simeq d$, we start by viewing it as an FO($\omega$) formula. Indeed, such atomic formulae can be understood as FO($\omega$) atomic formulae of the form $p(x), q(y)$ and $r(z)$. Here, the unary predicate $p$ (resp. $q$, $r$) is parameterised by $\simeq$, $i, k_1, j, k_2$ (resp. by $<$, $i, k_1, j, k_2$ and $d, i, k_1$). By way of example, below we write $p\simeq,i,k_1,j,k_2$, $p<,i,k_1,j,k_2$ and $p_{d,i,k_1}$ to denote such unary predicate symbols to relate atomic formulae in FO$^{\text{loc}}(\beta)$ and their reading in FO($\omega$).

Kamp's Theorem (Kamp 1968; Rabinovich 2014) states that, given an FO($\omega$) formula $\varphi(y)$ with free variable $y$, one can effectively construct an PLTL formula $\psi$ such that for all models $\sigma: \mathbb{N} \to (\text{Prop} \to \{0, 1\})$ and for all $i \in \mathbb{N}$, we have $\sigma, i \models \psi$ iff $\sigma \models_{[y \to i]} \varphi(y)$. Given an PLTL formula $\psi$ built over propositional variables of the form $p\simeq,i,k_1,j,k_2$, $p<,i,k_1,j,k_2$, and $p_{d,i,k_1}$, we write $t_{cc}$ to denote the translation map from PLTL to PLTL($\mathbb{D}$) such that $t_{cc}(\psi)$ is homogeneous for Boolean and temporal connectives, and

$$\begin{align*}
t_{cc}(p\simeq,i,k_1,j,k_2) &\stackrel{\text{def}}{=} X^{k_1} x_i = X^{k_2} x_j, \\
t_{cc}(p<,i,k_1,j,k_2) &\stackrel{\text{def}}{=} X^{k_1} x_i < X^{k_2} x_j, \\
t_{cc}(p_{d,i,k_1}) &\stackrel{\text{def}}{=} X^{k_1} x_i = d.
\end{align*}$$
We say that $t_{cc}(\psi)$ is the **concretisation** of $\psi$.

**Lemma 10.** Let $\varphi(y)$ be an $FO^{oc}(\beta)$ formula with one free variable $y$ and $\psi$ be some PLTL formula equivalent to $\varphi(y)$ read in $FO(\omega)$. Then, $\varphi(y)$ is $FO^{oc}(\beta)$ satisfiable iff $E t_{cc}(\psi)$ is PLTL($D$) satisfiable.

*Proof.* We write $Prop'$ to denote the finite set of propositional variables of one of the forms $p_{\simeq,i,k_1,j,k_2}$, $p_{<,i,k_1,j,k_2}$ and $p_{d,i,k_1}$ obtained from the atomic formulae occurring in $\varphi(y)$. The following statements can be shown equivalent.

1. There are an $FO^{loc}(\beta)$ model $w \in (D^{\beta})^{\omega}$ and an environment $g$ such that $w \Vdash_g \varphi(y)$ in $FO^{loc}(\beta)$.

2. There are an $FO(\omega)$ model $\sigma$ over the set $Prop'$ of propositional variables, an environment $g$ such that $\sigma \Vdash_g \varphi(y)$ in $FO(\omega)$ and an $FO^{loc}(\beta)$ model $w \in (D^{\beta})^{\omega}$ such that

(a) if $p_{\simeq,i,k_1,j,k_2} \in \text{Prop}'$, then $\sigma(\alpha)(p_{\simeq,i,k_1,j,k_2}) = 1$ iff $w(\alpha + k_1)(i) \simeq w(\alpha + k_2)(j)$, for all $\alpha \in \mathbb{N}$,

(b) if $p_{<,i,k_1,j,k_2} \in \text{Prop}'$, then $\sigma(\alpha)(p_{<,i,k_1,j,k_2}) = 1$ iff $w(\alpha + k_1)(i) < w(\alpha + k_2)(j)$, for all $\alpha \in \mathbb{N}$,

(c) if $p_{d,i,k_1} \in \text{Prop}'$, then $\sigma(\alpha)(p_{\simeq,i,k_1,j,k_2}) = 1$ iff $w(\alpha + k_1)(i) = d$, for all $\alpha \in \mathbb{N}$.

3. There are an PLTL model $\sigma$ over $Prop'$ and a position $\gamma$ such that $\sigma, \gamma \Vdash \psi$ and an $FO^{loc}(\beta)$ model $w \in (D^{\beta})^{\omega}$ such that (a), (b) and (c) above. (by Kamp's Theorem)

4. There is an PLTL($D$) model $\sigma$ such that $\sigma, 0 \Vdash E t_{cc}(\psi)$. (by the semantics of PLTL($D$)) $\square$

By Prop. 1, Lemma 10 and the effective construction of $\psi$ from $\varphi(y)$ (see e.g. (Rabinovich 2014)), we can conclude.

**Theorem 3.** *Satisfiability problem for FO<sup>oc</sup>(β) is decidable.*

If it is possible to build $\psi$ in time $\exp(Q(|\varphi(y)|, |\varphi(y)|)$, for some elementary function $Q$ and $|\varphi(y)|$ denoting the size of $\varphi(y)$, then $FO^{loc}(\beta)$ is in Tower (Schmitz 2016). Here $\exp$ is the function defined by induction on the first argument with $\exp(0, n) = n$ and $\exp(m + 1, n) = 2^{\exp(m, n)}$. Currently, Tower-membership is open.

Interestingly, $FO^{loc}(\beta)$ can be viewed as a first-order logic over the concrete domain $D$, following the terminology from (Baader and De Bortoli 2024). By way of example, the formula $f(x + k) \simeq f'(x + k')$ in $FO^{loc}(\beta)$, corresponds to the atomic formula = $(succ^k \cdot f, succ^k \cdot f')(x, x)$ in $FO(D)$ from (Baader and De Bortoli 2024, Sec. 2), with the interpretation domain $\mathbb{N}$ (not understood as a concrete domain), succ interpreted as the successor relation and the feature symbols $f$'s having total interpretation. If the concrete domain $D$ is either $\mathbb{N}$ or $\mathbb{Z}$, then $D$ is not homomorphism $\omega$-compact and therefore we cannot take advantage of (Baader and De Bortoli 2024, Thm. 3.1). Unfortunately, we cannot also take advantage of the decidability result in (Baader and De Bortoli 2024, Cor. 4.3) because $D$ has a binary predicate.

## 4.4 PLTL-A(D) satisfiability is decidable

Now, we state the main corollaries of our previous results.

**Corollary 1.** *The satisfiability problem for PLTL-A($D$) is decidable.*

From Lemmas 1 and 9 and Thm. 3 with $\beta = 1$, we get decidability of PLTL-A($D$). Thus, adding modalities of the form $\langle x:=X^n y \rangle$ to PLTL($D$) preserves the decidability (see Prop. 1) but at the cost of moving from PSpace to Tower-hardness. The same argument applies if we consider finite traces instead of infinites ones. All the decidability/complexity results still hold true. We can also conclude by a characterisation of the expressive power of PLTL-A($D$).

**Corollary 2.** *For every PLTL-A(D) formula $\varphi$, there is a PLTL(D) formula $\varphi'$ logically equivalent to $\varphi$.*

Since PLTL($D$) is a syntactic fragment of PLTL-A($D$), we conclude that PLTL-A($D$) and PLTL($D$) have the same expressive power. The reasoning chain is summarised below.

$$ 
\begin{array}{ccc}
\text{PLTL-A}(\mathbb{D}) & \xrightarrow{\text{Lemma 9}} & \text{FO}^{\text{loc}}(\beta) \xrightarrow{\text{Abstraction}} \text{FO}(\omega) \\
\text{FO}(\omega) & \xrightarrow{\text{Kamp's Theorem}} & \text{PLTL} \xrightarrow{\text{Concretisation}} \text{PLTL}(\mathbb{D}).
\end{array}
 $$

Cor. 2 can be extended to other concrete domains, as long as it is possible to define $FO^{loc}(\beta)$ over symbolic models. This does not imply necessarily the decidability of PLTL-A($D$), since the satisfiability problem for PLTL($D$) may not be decidable. However, the same techniques apply for instance for PLTL-A($D$), where $D$ is the concrete domain RCC8 with space regions in $\mathbb{R}^2$ equipped with topological relations between spatial regions, see e.g. (Wolter and Zakharyaschev 2000; Balbiani and Condotta 2002).

# 5 Concluding remarks

We introduced a version of LTL modulo theories with the new modality $\langle x:=t \rangle$ performing local assignments, which amounts to change locally the value of the variable $x$. The concrete domains are of the form $(D, =, <, (=_d)_{d \in D})$, including $D$ in $\{\mathbb{N}, \mathbb{Z}, \mathbb{Q}\}$ as well as any finite domain $\{0, \dots, k-1\}$, for some $k \ge 2$. We established the decidability of the satisfiability problem by reduction into a new first-order logic on multi-attributed data words. Decidability of this instrumental logic is obtained by translation into PLTL($D$) and evoking Kamp's Theorem. The addition of such local assignments allows us to express concisely many properties and the satisfiability problem is still decidable. We have also shown how to restrict ourselves to syntactic fragments, typically the one with a single variable. Using Kamp's Theorem (again), we show that PLTL($D$) is as expressive as PLTL-A($D$). Our method can be used with finite traces or with other concrete domains such as RCC8.

This work can be continued in many ways. First, the complexity of PLTL-A($D$) restricted to one variable and to adjacent assignments is open. More interestingly, it would be possible to have a change operator stating that there is a way to change $k \ge 1$ values in the model such that a given formula $\varphi$ holds afterwards. As far as we can judge, the techniques developed herein cannot handle this and the decidability status of such a variant is unclear. Last but not least, it would be interesting to resolve the satisfiability problem for PLTL-A($\mathbb{N}$) or fragments using SMT techniques, see e.g. (Barrett and Tinelli 2018). This is already challenging with PLTL($\mathbb{N}$) (without assignments) as the set of symbolic models of formulae in PLTL($\mathbb{N}$) is not always $\omega$-regular.
Acknowledgments

We would like to thank the anonymous reviewers for their comments and suggestions that helped us to improve the quality of the document. R. Fervari is supported by Agen-cia I+D+i grant PICT 2021-00400, the EU H2020 research and innovation programme under the Marie Skłodowska-Curie grant agreements 101008233 (MISSION), the IRP SIN-FIN, SeCyT-UNC grant 33620230100178CB, and as part of France 2030 program ANR-11-IDEX-0003.

References

Alur, R., and Henzinger, T. 1994. A really temporal logic. *Journal of the ACM* 41(1):181–204.

Areces, C., and ten Cate, B. 2007. Hybrid logics. In *Handbook of Modal Logic*, volume 3 of *Studies in logic and practical reasoning*. North-Holland. 821–868.

Areces, C.; Fervari, R.; and Hoffmann, G. 2015. Relation-changing modal operators. *Logic Journal of the IGPL* 23(4):601–627.

Aucher, G.; Balbiani, P.; Fariñas del Cerro, L.; and Herzig, A. 2009. Global and local graph modifiers. *Electronic Notes in Theoretical Computer Science* 231:293–307.

Aucher, G.; van Benthem, J.; and Grossi, D. 2018. Modal logics of sabotage revisited. *Journal of Logic and Computation* 28(2):269–303.

Baader, F., and De Bortoli, F. 2024. The abstract expressive power of first-order and description logics with concrete domains. In *SAC'24*, 754–761. ACM.

Baader, F., and Hanschke, P. 1991. A scheme for integrating concrete domains into concept languages. In *IJCAI'91*, 452–457.

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

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

Bansal, K.; Brochenin, R.; and Lozes, E. 2009. Beyond shapes: Lists with ordered data. In *FoSSaCS'09*, volume 5504 of *LNCS*, 425–439. Springer.

Barrett, C., and Tinelli, C. 2018. Satisfiability Modulo Theories. In *Handbook of Model Checking*. Springer. 305–343.

Belardinelli, F.; Boureanu, I.; Malvone, V.; and Rajaona, F. 2023. Automatically verifying expressive epistemic properties of programs. In *AAAI'23*, 6245–6252. AAAI Press.

Belardinelli, F.; Boureanu, I.; Malvone, V.; and Rajaona, F. 2025. An SMT-based approach to the verification of knowledge-based programs. *Formal Aspects of Computing* 37(1):3:1–3:24.

Beutner, R., and Finkbeiner, B. 2025. AutoHyper: leveraging language inclusion checking for hyperproperty model-checking. *International Journal on Software Tools for Technology Transfer*. To appear in special issue for TACAS'23.

Bhaskar, A., and Praveen, M. 2024. Realizability problem for constraint LTL. *I&C* 296:105126.

Bojańczyk, M.; David, C.; Muscholl, A.; Schwentick, T.; and Segoufin, L. 2011. Two-variable logic on data words. *ACM ToCL* 12(4):27.

Bollig, B.; Sangnier, A.; and Stietel, O. 2024. On the satisfiability of local first-order logics with data. *Logical Methods in Computer Science* 20(3).

Borgwardt, S.; Bortoli, F. D.; and Koopmann, P. 2024. The precise complexity of reasoning in *ALC* with $\omega$-admissible concrete domains. In *DL'24*, volume 3739 of *CEUR Workshop Proceedings*. CEUR-WS.org.

Büchi, J. 1962. On a decision method in restricted second-order arithmetic. In *International Congress on Logic, Method and Philosophical Science'60*, 1–11.

Carapelle, C. 2015. *On the satisfiability of temporal logics with concrete domains*. Ph.D. Dissertation, Leipzig University.

Catta, D.; Leneutre, J.; Malvone, V.; and Murano, A. 2024. Obstruction alternating-time temporal logic: A strategic logic to reason about dynamic models. In *AAMAS'24*, 271–280. International Foundation for Autonomous Agents and Multiagent Systems / ACM.

Cimatti, A.; Griggio, A.; Mover, S.; Roveri, M.; and Tonetta, S. 2022. Verification modulo theories. *Formal Methods in System Design* 60(3):452–481.

Czerwinski, W., and Orlikowski, L. 2021. Reachability in vector addition systems is Ackermann-complete. In *STOC'21*, 1229–1240. IEEE.

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

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

Demri, S.; Lazić, R.; and Nowak, D. 2007. On the freeze quantifier in constraint LTL: decidability and complexity. *I&C* 205(1):2–24.

Diekert, V., and Gastin, P. 2008. First-order definable languages. In Flum, J.; Grädel, E.; and Wilke, T., eds., *Logic and Automata: History and Perspectives*, volume 2 of *Texts in Logic and Games*. Amsterdam University Press. 261–306.

Faella, M., and Parlato, G. 2024. A unified automata-theoretic approach to LTL<sub>f</sub> modulo theories. In *ECAI'24*, 1254–1261.

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

Figueira, D., and Segoufin, L. 2009. Future-looking logics on data words and trees. In *MFCS'09*, volume 5734 of *LNCS*, 331–343. Springer.

Figueira, D. 2010. *Reasoning on words and trees with data*. Ph.D. Dissertation, ENS Cachan.

Fitting, M. 2002. Modal logic between propositional and first-order. *Journal of Logic and Computation* 12(6):1017–1026.
Gabbay, D.; Pnueli, A.; Shelah, S.; and Stavi, J. 1980. On the temporal analysis of fairness. In *POPL'80*, 163–173. ACM Press.

Galimullin, R.; Galdyshev, M.; Mittelmann, M.; and Montamed, N. 2025. Changing the rules of the game: reasoning about dynamic phenomena in multi-agent systems. In *AAMAS'25*, 829–838.

Geatti, L.; Gianola, A.; Gigante, N.; and Winkler, S. 2023. Decidable fragments of LTL<sub>f</sub> modulo theories. In *ECAI'23*, volume 372, 811–818. IOS Press.

Geatti, L.; Gianola, A.; and Gigante, N. 2025. First-order automata. In *AAAI'25*, 14940–14948.

Gianola, A.; Montali, M.; and Winkler, S. 2025. SMT Techniques for Data-Aware Process Mining. *Künstliche Intelligenz*. To appear.

Halpern, J. 1995. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. *AI* 75(2):361–372.

Herzig, A.; Maris, F.; and Vianey, J. 2019. Dynamic logic of parallel propositional assignments and its applications to planning. In *IJCAI'19*, 5576–5582. ijcai.org.

Herzig, A. 2014. Belief change operations: A short history of nearly everything, told in dynamic logic of propositional assignments. In *KR'14*. AAAI Press.

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

Kamp, J. 1968. *Tense Logic and the theory of linear order*. Ph.D. Dissertation, UCLA, USA.

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

Leroux, J., and Schmitz, S. 2019. Reachability in vector addition systems is primitive-recursive in fixed dimension. In *LiCS'19*, 1–13. IEEE.

Leroux, J. 2021. The reachability problem for Petri nets is not primitive recursive. In *STOC'21*, 1241–1252. IEEE.

Lutz, C. 2002a. Adding numbers to the SHIQ description logic: First results. In *KR'02*, 191–202. Morgan Kaufmann.

Lutz, C. 2002b. *The Complexity of Description Logics with Concrete Domains*. Ph.D. Dissertation, RWTH, Aachen.

Lutz, C. 2006. Complexity and succinctness of public announcement logic. In *AAMAS'06*, 137–143. ACM.

Pnueli, A. 1977. The temporal logic of programs. In *FOCS'77*, 46–57. IEEE Computer Society Press.

Rabinovich, A. 2014. A Proof of Kamp's theorem. *Logical Methods in Computer Science* 10(1):1–16.

Rodríguez, A., and Sánchez, C. 2024. Realizability modulo theories. *Journal of Logical and Algebraic Methods in Programming* 140:100971.

Schmitz, S. 2016. Complexity hierarchies beyond elementary. *TOCT* 8(1):3:1–3:36.

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

Sistla, A., and Clarke, E. 1985. The complexity of propositional linear temporal logic. *Journal of the ACM* 32(3):733–749.

Spaan, E. 1993. *Complexity of Modal Logics*. Ph.D. Dissertation, ILLC, Amsterdam University.

Stockmeyer, L. J. 1974. *The complexity of decision problems in automata theory and logic*. Ph.D. Dissertation, Massachusetts Institute of Technology, USA.

van Ditmarsch, H.; Herzig, A.; and de Lima, T. 2012. Public announcements, public assignments and the complexity of their logic. *Journal of Applied Non-Classical Logics* 22(3):249–273.

Wolper, P. 1983. Temporal logic can be more expressive. *I&C* 56:72–99.

Wolter, F., and Zakharyaschev, M. 2000. Spatio-temporal representation and reasoning based on RCC-8. In *KR'00*, 3–14.