# Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata

Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, Damien Regnault

► To cite this version:

Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, Damien Regnault. Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata. Université Côte d'Azur, CNRS, I3S, France; IBISC, Univ. Evry, Université Paris-Saclay, France; Scalian Digital Systems, Valbonne, France. 2023. [hal-04155339v2](https://hal.science/hal-04155339v2)

HAL Id: hal-04155339

https://hal.science/hal-04155339v2

Submitted on 11 Jul 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 Attribution 4.0 International License
Complexity of Membership and Non-Emptiness Problems in
Unbounded Memory Automata

Clément Bertrand

Cinzia Di Giusto

Hanna Klaudel

Damien Regnault

Abstract

We study the complexity relationship between three models of unbounded memory automata: nu-automata (v-A), Layered Memory Automata (LaMA)and History-Register Automata (HRA). These are all extensions of finite state automata with unbounded memory over infinite alphabets. We prove that the membership problem is NP-complete for all of them, while they fall into different classes for what concerns non-emptiness. The problem of non-emptiness is known to be Ackermann-complete for HRA, we prove that it is PSPACE-complete for v-A.

# 1 Introduction

We study unbounded memory automata for words over an infinite alphabet, as introduced in [12, 16]. Such automata model essentially dynamic generative behaviours, i.e., programs that generate an unbounded number of distinct resources each with its own unique identifier (e.g. thread creation in Java, XML). For a detailed survey, we refer the reader to [4, 14]. We focus, in particular, on three formalisms, $v$-automata ($v$-A) [8, 5], Layered Memory Automata (LaMA) [4] and HRA for History-Register Automata [10]. All these models are extensions of finite state automata with memory-storing letters. The memory for HRA is composed of registers (that can store only one letter) and histories (that can store an unbounded number of letters). Whereas the memory for the other two models consists of a finite set of variables. Among the distinctive features of HRA, they can reset registers and histories, and select, remove and transfer individual letters. In $v$-A and LaMA, variables must satisfy an additional constraint, referred to as injectivity, meaning that they cannot store shared letters. Moreover, variables can be emptied (reset) but single letters cannot be removed. We know that LaMA are more expressive than $v$-A as the former are closed under intersection while it is not the case for the latter ones.

We tackle two problems: membership and non-emptiness. From a practical point of view, automata over infinite alphabets can be used to identify patterns in link-stream analysis [5]. In such a scenario, the alphabet is not known in advance (open systems) and runtime verification can help to recognize possible attacks on a network by looking for specific patterns. This problem corresponds to checking whether a pattern (word) belongs to a language (the membership problem). Concerning non-emptiness, this is the “standard” problem to address while considering automata in general.

Fig. 1 depicts the unbounded memory automata known in the literature (to the best of our knowledge). An implementation exists for $v$-A and LaMA which includes an implementation of the membership algorithm, but we have not found anything neither for Data Automata (DA) nor Class Memory Automata (CMA). Both DA and CMA are incomparable classes wrt to HRA, hence we chose not to consider them. Fresh-Register automata (FRA), $v$-A, LaMA and HRA
<figure><img src="image_2.png" /><figcaption>Figure 1: A classification of memory automata from [4]. Arrows represent strict language inclusion, while dotted lines denote language incomparability. The formalisms studied here are in yellow.</figcaption></figure>

are instead related from the expressiveness point of view. Given the similarities between those formalisms, the existence of implementations and the lack of complexity results we find it natural to consider these classes of automata.

Application-wise, $\nu$-A, called resource graphs in [8], model the use of unbounded resources in the $\pi$-calculus, aiming at minimizing them. Then, runtime verification on link-streams was the initial motivation for the introduction of (timed)$\nu$-A [5]. In subsequent works, LaMA have been introduced to be able to construct the synchronous product, hence being able to express the synchronization of resources. This entails the closure by intersection, which is interesting when one wants to define a language of expressions, an extension of (timed) regular expressions, which was proposed in the PhD thesis of Clément Bertrand [2].

For a precise discussion on the relations among these formalisms see [4], here we just recall the hierarchy: cfr. Fig. 1. Apart from expressiveness, a number of questions concerning complexity remains open. We know that checking whether the language recognized by an HRA is empty or not (referred to as the non-emptiness problem) is Ackermann-complete [10]. But the question has not been addressed for $\nu$-A and LaMA. For finite-memory automata (FMA), it is known that membership (testing whether a word belongs to the language) and non-emptiness are NP-complete [17]. Knowing whether a language is included in another is undecidable for FMA when considering their non-deterministic version, but it is PSPACE-complete for deterministic ones [15]. In [11] it is shown that the non-emptiness problem for Variable Finite Automata (VFA) is NL-complete, while membership is NP-complete. For FRA and Guessing-Register Automata (as they are called in [14]) we only know that both problems are decidable but we do not know the accurate complexity class. Finally, for data-languages where data-words are sequences of pairs of a letter from a finite alphabet and an element from an infinite set and the latter can only be compared for equality, the non-emptiness problem for FMA is PSPACE-complete [9], for DA and CMA, membership and non-emptiness are only shown to be decidable, but no complexity is given [7, 6].

**Contributions.** In this paper, we close some open problems on the complexity of membership and non-emptiness. We first prove that testing membership for HRA, $\nu$-A and LaMA is an equivalent problem. Then we address complexity and show that the problem is NP-complete with a reduction of 3-SAT to LaMA. Non-emptiness appears to be a much harder problem. We show that the non-emptiness problem is PSPACE-complete for $\nu$-A by reducing TQBF (True
Fully Quantified Boolean Formula) to $\nu$-A.

The paper is organized as follows. The three formalisms are introduced and the main differences are recalled quickly in Section 2. Section 3 presents the complexity of the membership problem and Section 4 the non-emptiness one. Finally, Section 5 concludes with some remarks. Proofs and additional material can be found in [3].

## 2 Formalisms

All three formalisms are generalizations of finite state automata with memory over an infinite alphabet $\mathcal{U}$. For all of them, configurations $(q, M)$ are pairs of a state of the automaton plus a memory context. A memory context assigns a set of letters to each identifier of the memory, variable or history depending on the formalism under consideration.

**Definition 2.1 (Memory context).** Given a finite set of memory identifiers or variables $V$ and an infinite alphabet $\mathcal{U}$, we define a memory context $M$ as an assignment: $M: V \to 2^{\mathcal{U}}$ where $M(v) \subset \mathcal{U}$ is the finite set of letters assigned to $v$.

The definition of accepted language common to the three formalisms is, as customary:

**Definition 2.2 (Accepted language).** For an automaton $A$ (LaMA, $\nu$-A or HRA), the language of $A$ is the set of words recognized by $A$: $\mathcal{L}(A) = \{w \in \mathcal{U}^* | (q_0, M_0) \underset{A}{\overset{w}{\Rightarrow}} (q_f, M) \text{ s.t. } q_f \in F\}$, where $\underset{A}{\overset{w}{\Rightarrow}}$ is the extension to sequences of transitions of $\underset{A}{\overset{u}{\Rightarrow}}$.

### 2.1 $n$-Layered Memory Automata

We start with $n$-Layered Memory Automata (n-LaMA). The idea is that finite state automata are enriched with $n$ layers each containing a finite number of variables. Variables on the same layer satisfy the *injectivity* constraint: variables on a given layer $l \in [1, n]$ (denoted $v^l$) do not share letters of the alphabet: $\forall v_1 \neq v_2 \in V, M(v_1^l) \cap M(v_2^l) = \emptyset$. Upon reading a letter, a transition can test if the letter is already stored in a set of variables and add a letter to a set of variables. The non-observable transition ($\varepsilon$-transition) empties a set of variables.

**Definition 2.3 (n-LaMA).** An $n$-LaMA $A$ is defined by the tuple $(Q, q_0, F, \Delta, V, n, M_0)$, where:

* $Q$ is a finite set of states,

* $q_0 \in Q$ and $F \subseteq Q$ are respectively an initial state and a set of final states,

* $\Delta$ is a finite set of transitions,

* $n$ is the number of layers, and $V$ is a finite set of variables, denoted $v^l$ with $l \in [1, n]$,

* $M_0: V \to 2^{\mathcal{U}}$ is an initial memory context.

A *fresh letter at layer* $l$, is a letter that is associated with no variable of this layer. The set of transitions $\Delta = \Delta_o \cup \Delta_\varepsilon$ encompasses two kinds of transitions with $\Delta_o$ the set of *observable transitions* that consume a letter of the input and $\Delta_\varepsilon$ the set of *non-observable transitions*, that do not consume any letter of the input but can reset a set of variables.

**Definition 2.4 (Observable transition).** An observable transition is a tuple of the form: $\delta = (q, \alpha, q') \in \Delta_o$ where:

* $q, q' \in Q$ are the source and destination states of the transition,
<figure><img src="image_3.png" /><figcaption>Figure 2: A 2-LaMA $A_p$ recognizing $\mathcal{P}(2) \cap \mathcal{P}(3)$ from Example 2.1</figcaption></figure>

• $\alpha : [1, n] \to (V \times \{\mathbf{r}, \mathbf{w}\}) \cup \{\#\}$, such that $\alpha(l) = (v^l, \mathbf{x})$ for $\mathbf{x} \in \{\mathbf{r}, \mathbf{w}\}$ and for some $v^l \in V$ indicates for each layer $l$ which variable is examined by the transition.

Notice that only one variable per layer can be examined, and it is not possible to have $\alpha(l) = (v^k, \mathbf{x})$ with $l \neq k$. The special symbol $\#$ indicates that no variable is to be read or written for a specific layer.

*Remark 2.1 (Any-letter transition).* If $\forall l \in [1, n], \alpha(l) = \#$ (i.e., no variable is examined) then the transition is executed consuming whatever letter is in input.

**Definition 2.5 (Non-observable transition).** A non-observable transition is a tuple of the form $\delta_{\varepsilon} = (q, \mathbf{reset}, q') \in \Delta_{\varepsilon}$ where:

• $q, q' \in Q$ are the source and destination states of $\delta_{\varepsilon}$,

• $\mathbf{reset} \subseteq 2^V$ is the set of variables reset (i.e., emptied) by the transition.

**Definition 2.6.** The semantics of an $n$-LaMA $A = (Q, q_0, F, \Delta, V, n, M_0)$ is defined as:

• An observable transition $(q, \alpha, q')$ can be executed on an input letter $u$ from memory context $M$ leading to $M': (q, M) \xrightarrow{u} \{q', M'\}$ if for each $\alpha(l) \neq \#$ such that $\alpha(l) = (v^l, \mathbf{x})$:

- if $\mathbf{x} = \mathbf{r}$, then $u \in M(v^l)$ and $M'(v^l) = M(v^l)$;

- if $\mathbf{x} = \mathbf{w}$, then $u$ is fresh for layer $l$ and $u$ is added to $v^l$ in the reached memory context: $M'(v^l) = M(v^l) \cup \{u\}$.

All variables $v^l$ not labeled through $\alpha$ remains associated to the same letters : if $\alpha(l) = \#$ or $\alpha(l) = (v_1^l, x)$ and $v_1^l \neq v^l$ then $M'(v^l) = M(v^l)$.

• A non-observable transition $(q, \mathbf{reset}, q')$ can be executed from memory context $M$ without reading any input letter leading to $M': (q, M) \xrightarrow{\varepsilon} \{q', M'\}$, where $\forall v^l \in \mathbf{reset}: M'(v^l) = \emptyset$ and otherwise $M'(v^l) = M(v^l)$.

**Example 2.1.** Let $\mathcal{P}(p) = \{u_1 \dots u_s \mid \forall j, k > 0, j \neq k, u_{j \cdot p} \neq u_{k \cdot p}\}$, be the language recognizing words where the letters at positions, which are multiples of $p$ are all different whereas the others are not constrained. Fig. 2 depicts a 2-LaMA for $\mathcal{P}(2) \cap \mathcal{P}(3)$.

## 2.2 $\nu$-automata

$\nu$-automata ($\nu$-A) can be seen as a restricted version of LaMA with only one layer. Hence, each variable is constrained under the injectivity property, and no letter can be stored in more than one variable.

**Definition 2.7 ($\nu$-A).** A $\nu$-A is defined as a tuple $(Q, q_0, F, \Delta, V, M_0)$, where
• $Q$ is a finite set of states containing an initial state $q_0 \in Q$ and a set of final ones $F \subseteq Q$,

• $V$ is a finite set of variables that may initially be storing a finite amount of letters from the infinite alphabet $\mathcal{U}$, as specified by the initial memory context $M_0$,

• and $\Delta$ is a finite set of transitions.

As before, $\Delta = \Delta_o \cup \Delta_\varepsilon$ where $\Delta_o$ is the set of observable transitions and $\Delta_\varepsilon$ is the set of non-observable ones. Differently from LaMA, observable transitions are decoupled in read and write transitions.

**Definition 2.8 (Observable transition).** An observable transition can be of two kinds: $(q, v, \mathbf{r}, q')$ and $(q, v, \mathbf{w}, q')$ ($\mathbf{r}$ for read and $\mathbf{w}$ for write) where $q, q' \in Q$ are the source and destination states and $v \in V$.

**Definition 2.9 (Non-observable transition).** A non-observable transition is a tuple of the form $\delta_\varepsilon = (q, \mathbf{reset}, q') \in \Delta_\varepsilon$ where: $q, q' \in Q$ are the source and destination states of $\delta_\varepsilon$, $\mathbf{reset} \subseteq 2^V$ is the set of variables reset by the transition.

**Definition 2.10.** The semantics of a $\nu$-A $A = (Q, q_0, F, \Delta, V, M_0)$ is defined as:

• An observable transition $(q, v, \mathbf{x}, q')$ reading input letter $u$ can be executed from memory context $M$ leading to $M'$: $(q, M) \xrightarrow{u} (q', M')$ if for each $v$:

- if $\mathbf{x} = \mathbf{r}$, then $u \in M(v)$ and $M'(v) = M(v)$;

- if $\mathbf{x} = \mathbf{w}$, then $u$ is fresh in $M$ and $u$ is added to $v$ in the reached memory context: $M'(v) = M(v) \cup \{u\}$.

All other variables $v_1 \neq v$, remains associated to the same letters $M'(v_1) = M(v_1)$.

• A non-observable transition $(q, \mathbf{reset}, q') \in \Delta_\varepsilon$ can be executed from memory context $M$ leading to $M'$: $(q, M) \xrightarrow{\varepsilon} (q', M')$ without reading any input letter, where $\forall v \in \mathbf{reset}: M'(v) = \emptyset$ and otherwise $M'(v) = M(v)$.

*Remark 2.2.* Analogously to LaMA, we consider any-letter transitions, denoted by $(q, \sharp, q')$ with $\sharp \notin \mathcal{U}$, which are enabled whenever a letter is read and the memory context of the target configuration is the same as the origin's one.

Notice that any-letter transitions do not alter the expressive power of $\nu$-A nor the complexity of its problems. Indeed, it is a sort of macro that can be encoded by a set of transitions searching for the presence of a letter or its freshness over the whole set $V$. To do so, one needs as many reading transitions as variables to allow the firing with any letter in memory. For fresh letters, one needs a transition writing in an extra variable, which is reset immediately after.

## 2.3 History-Register Automata

HRA are automata provided with a finite set $H$ of histories, i.e., variables storing a finite subset of letters of the infinite alphabet $\mathcal{U}$. To simplify the presentation, we consider HRA defined only with histories and no registers. The latter does not provide additional expressiveness [10]. An essential distinction between HRA and LaMA or $\nu$-A is that different histories are allowed to store the same letter (i.e., there is no injectivity constraint). Thus, an observable transition is annotated with the exact set of histories that should contain the letter read to enable it. This
entails that for each observable transition the whole memory has to be explored while LaMA allow ignoring some layers using symbol $\vdash$ (this can be crucial while implementing the formalisms<fnref n="1" />).

**Definition 2.11 (HRA).** A History-Register Automata is defined as a tuple of the form $A = (Q, q_0, F, \Delta, H, M_0)$ where $Q$ is the set of states, $q_0$ the initial one, $F$ the set of final ones, $\Delta$ the set of transitions, $H$ a finite set of histories and $M_0$ the initial memory context. The set of transitions $\Delta = \Delta_o \cup \Delta_\varepsilon$ are of the form:

* $(q, H_r, H_w, q') \in \Delta_o$ where $H_r, H_w \subseteq H$ (for read and write), which is an observable transition and

* $(q, H_\emptyset, q') \in \Delta_\varepsilon$ where $H_\emptyset \subseteq H$, which is a non-observable transition.

An observable transition $(q, H_r, H_w, q')$ is enabled if letter $u$ is present in exactly all the histories in $H_r$ and not present in $H \setminus H_r$. After the transition, $u$ is present only in the histories in $H_w$. Notice that this allows moving an input letter from one set of histories to another, or even forgetting it if $H_w = \emptyset$. This is not possible in $\nu$-A and LaMA. Finally, if $H_r = \emptyset$ then the input letter has to be fresh (absent from every history).

**Definition 2.12.** The semantics of an HRA $A = (Q, q_0, F, \Delta, H, M_0)$ is defined as:

* an observable transition $(q, H_r, H_w, q')$ is enabled for memory context $M$ when reading letter $u \in \mathcal{U}$: $(q, M) \xrightarrow{u} (q', M')$ if $u \in M(h_r) \Leftrightarrow h_r \in H_r$ and $\forall h_w \in H_w: M'(h_w) = M(h) \cup \{u\}$ and $\forall h \notin H_w: M'(h) = M(h) \setminus \{u\}$;

* a non-observable transition $(q, H_\emptyset, q')$ is enabled for any memory context $M$ and allows to move from configuration $(q, M)$ to $(q', M')$: $(q, M) \xrightarrow{\varepsilon} (q', M')$, where all the histories in $H_\emptyset$ have been reset in $M'$.

**Example 2.2.** Fig. 3 depicts an HRA that, with an initially empty memory context, recognizes the language

$$ \{u_1 u_2 \dots u_n \mid \begin{array}{l} \exists k < n, \forall i, j \in [1, k], u_i = u_j \Leftrightarrow i = j, \\ \forall m \in ]k, n], \exists p < m, u_p = u_m, p \bmod 2 \neq m \bmod 2, \exists q \in ]p, m[, u_m = u_q \end{array} \} $$

The two transitions looping between states $q_{ow}$ and $q_{ew}$ allow us to recognize words where the first $k$ letters are all different from each other. Letters are stored in histories $O$ (odd) and $E$ (even) to remember the parity of the position they are read at. The transitions between states $q_{er}$ and $q_{or}$ allow us to recognize words whose suffix is only composed of repetitions of the $k$ first letters, with the additional constraint that they can only occur at a position with opposed parity wrt the previous occurrence. Thus, if a letter was read for the last time at an even position, it is stored in history $E$ and can only be read in an odd position. Once it is read, it is transferred to the $O$ history to remember it can only be read at an even position the next time.

# 3 Complexity of the membership problem

We know that each $\nu$-A can be encoded into a LaMA and respectively each LaMA can be encoded into an HRA both recognizing the same language [4]. The encoding from LaMA to HRA is exponential in the number of layers, hence we know that the complexity of problems for

<footnote n="1">¹Implemented in tool available at https://github.com/clementber/MaTiNA/tree/master/LaMA</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 3: Example of an HRA $A_h$.</figcaption></figure>

HRA gives an upper bound to the complexity of the same problem for LaMA and $\nu$-A. In this section, we show that the complexity of the membership problem (i.e., given an automaton $A$ and a word $w$ decide whether $w \in \mathcal{L}(A)$) falls in the same class for these three automata models. To do so, we show that the membership problem for LaMA can be simulated using $\nu$-A, and the same can be done for HRA using LaMA.

**Simulating the membership for LaMA in $\nu$-automata** The idea is to represent an $n$-LaMA as a product of $n$ $\nu$-A, one for each layer. The main limitation is that having just one layer makes the injectivity constraint stronger. Indeed, it is not possible to trivially treat a same letter stored on different layers. To cope with this difficulty, we rename the word under consideration, replacing consistently each letter with a sequence of new ones - one per layer of the LaMA: i.e., for an $n$-LaMA the letter $u \in w$ is replaced by the letters $u^1, ..., u^n$ where all the $u^i$ are different in order to have the letters belonging to different layers all distinct from each other. This renaming is always possible as the alphabet $\mathcal{U}$ is infinite. For example, for the word aba, a consistent renaming, for a 2-LaMA, could produce $a^1 a^2 b^1 b^2 a^1 a^2$.

**Definition 3.1 (Renaming).** $\xi^n : \mathcal{U} \to \mathcal{U}^n$ is a renaming function that given a letter $u \in \mathcal{U}$ generates a new sequence of $n$ letters $u^1...u^n$ with for all $i \neq j \in [1, n]$ $u^i \neq u^j$ and such that if $u_1 \neq u_2$ then for all $i, j \in [1, n]$, $u_1^i \neq u_2^j$. $\xi^n(u_1...u_m) = u_1^1...u_1^n...u_m^1...u_m^n$ is its pointwise extension to words.

Let $A = (Q, q_0, F, \Delta, V, n, M_0)$ be an $n$-LaMA and $w = u_1...u_m \in \mathcal{U}^*$. We know that $w \in \mathcal{L}(A)$ if and only if there is a finite sequence of transitions such that for some $M_f, (q_0, M_0) \stackrel{w}{\underset{A}{\rightleftharpoons}} (q_f, M_f)$ with $q_f \in F$. It is then possible to construct a $\nu$-A that accepts $\xi^n(w)$, which simulates the recognition process of the $n$-LaMA over the word $w$. To do so, we encode every observable transition of $A$ into a sequence of transitions successively simulating the constraints applied to variables of each layer. Moreover, we apply the renaming function $\xi^n$ to the initial memory context. In order to simplify the notations, in the following, we denote by $x|_k$ the projection onto the $k$-th element of tuple $x$, e.g., $(a, b, c)|_2 = b$.

**Definition 3.2 (Encoding of a memory context).** Let $M$ be the memory context over the set of variables $V$ over $n$ layers, then $\forall v^l \in V$, its renaming through $\xi^n$, is defined as $\llbracket M \rrbracket_\xi(v^l) = \{\xi^n(u)|_l | u \in M(v^l)\}$.

**Definition 3.3 (Encoding of a LaMA).** Let $A = (Q, q_0, F, \Delta, V, n, M_0)$ be an $n$-LaMA, then the $\nu$-A $\llbracket A \rrbracket_\xi = (Q', q'_0, F', \Delta', V', M'_0)$ is the encoding of $A$ through the renaming $\xi^n$, where:

* $Q' = Q \cup Q_o$ and the set of states $Q_o = \{q_\delta^l | \delta = (q, \alpha, q') \in \Delta, l \in [2, n]\}$ is used by the sequence of transitions simulating each observable transition of $A$, $q_0' = q_0$ and $F' = F$;

* $V' = V$ is the set of variables of $A$ flattened on one layer;
• $M_0' = \llbracket M_0 \rrbracket_\xi$ is the initial memory context of A renamed in case it is not initially empty;

• $\Delta' = \Delta'_o \cup \Delta_\epsilon$ where $\Delta_\epsilon$ is the set of all non-observable transitions of A, and $\Delta'_o$ contains the encoding of every observable transition $\delta = (q, \alpha, q')$ of A, which is a sequence of transitions with $q_\delta^1 = q$ and $q_\delta^{n+1} = q'$ such that

$$ \Delta'_o = \{ (q_\delta^l, v^l, \mathbf{x}, q_\delta^{l+1}) \mid \delta = (q, \alpha, q') \in \Delta, l \in [1, n], \alpha(l) = (v^l, \mathbf{x}) \} \\ \cup \{ (q_\delta^l, \sharp, q_\delta^{l+1}) \mid \delta = (q, \alpha, q') \in \Delta, l \in [1, n], \alpha(l) = \sharp \}. $$

Notice that the language accepted by the encoded $\nu$-A $\llbracket A \rrbracket_\xi$ of a LaMA A is an approximation of the language accepted by A: $\xi(\mathcal{L}(A)) \subseteq \mathcal{L}(\llbracket A \rrbracket_\xi)$. They are equal only when the LaMA has one layer (i.e., $n = 1$). Nonetheless, this construction may be used to test the membership of a word $w$ to $\mathcal{L}(A)$. The proof is a simple induction on the length of the derivation of $w$ and $\xi^n(w)$ [3].

**Theorem 3.1.** Let A be an $n$-LaMA. $w \in \mathcal{L}(A)$ if and only if $\xi^n(w) \in \mathcal{L}(\llbracket A \rrbracket_\xi)$.

**Simulating the membership for HRA in LaMA** This section presents how to solve the membership problem for HRA using LaMA. The difference in expressiveness between HRA and LaMA comes from the ability of HRA of removing letters from histories when they are read. We resort to an encoding of words where each letter is duplicated and annotated with a number representing how many occurrences of that letter have been encountered so far. In detail, the first copy of the letter keeps the information on the number of occurrences of the letter seen so far and the second one the number of occurrences including the present one.

**Example 3.1.** Take $w = abaca$ then the encoded word is $w' = a^0a^1 b^0b^1 a^1a^2 c^0c^1 a^2a^3$

The idea behind the encoding of observable transitions is to use the first copy to check the presence and absence of the letter in every variable (simulating the role of $H_r$) while the second one (that is always fresh) can be used to simulate writing and removal (hence simulating $H_w$). More precisely, once we add an annotated letter to a variable, the encoded automaton will ensure that the variable always stores the last seen occurrence of that letter. Thus, removing a letter from a history consists in not storing the last seen occurrence of the letter in the corresponding encoded variable. Clearly, all the letters annotated with a number smaller than the current one will not be used in any of the transitions, representing a form of garbage.

We consider a renaming function $\zeta_i : \mathcal{U} \to \mathcal{U}^2$ which replaces $u$ by a pair of letters $u^{i-1}u^i$ for any $i \in \mathbb{N}^+$. Then, we define the encoding of words $\zeta : \mathcal{U}^* \to \mathcal{U}^*$ as follows $\zeta(u_1...u_m) = \zeta_{i_{u_1}}(u_1)...\zeta_{i_{u_m}}(u_m)$ where each $i_{u_j}$ is the number of occurrences of $u_j$ seen in the prefix $u_1...u_j$. Notice that when considering the word up to letter $u_j$, $\zeta_{i_{u_j}}(u_j)\llbracket_2$ is always a new letter (e.g., a fresh letter with respect to those in $\zeta(u_1...u_j)$).

**Definition 3.4 (Encoding of an HRA).** Let $A = (Q, q_0, F, \Delta_o \cup \Delta_\epsilon, \{h_1, ..., h_n\}, M_0)$ be an HRA, its encoding into an $n$-LaMA is $\llbracket A \rrbracket_\zeta = (Q', q'_0, F', \Delta', V', n, M'_0)$ where:

• $Q' = Q \cup Q_o$ and the set of states $Q_o = \{q_\delta | q \in Q, \delta = (q, H_r, H_w, q') \in \Delta\}$ is used by the sequence of transitions simulating each observable transition of A;

• $q'_0 = q_0$ and $F' = F$;

• $V' = \{h^l, \omega^l | l \in [1, n]\}$ and for each layer $l \in [1, n]$, $h^l$ plays the role of history $h_l$ and $\omega^l$ is used to check the absence of letters in $h^l$.
<figure><img src="image_5.png" /><figcaption>Figure 4: The 2-LaMA $[[A_h]]_\zeta$, encoding of the HRA $A_h$ from Example 2.2.</figcaption></figure>

• $M'_0(h^l) = \{\zeta_1(u)\vert_1 \mid u \in M_0(h_l)\}$ and $M'_0(\omega^l) = \emptyset$ for all $l \in [1, n]$ meaning that $M'_0$ is as $M_0$ with all letters renamed with $\zeta_1$ and empty for all extra variables;

• $\Delta' = \Delta'_\epsilon \cup \Delta'_o$ with

- $\Delta'_\epsilon = \{(q, \{h^l \mid h_l \in H_\emptyset\}, q') \mid (q, H_\emptyset, q') \in \Delta_\epsilon\}$, is the direct translation of the $\epsilon$-transitions in A.

- $\Delta'_o = \{(q, \alpha_{H_r}, q_\delta), (q_\delta, \alpha_{H_w}, q') \mid \delta = (q, H_r, H_w, q') \in \Delta_o\}$ with for all $l \in [1, n]$

$$ \alpha_{H_r}(l) = \begin{cases} (h^l, \mathbf{r}) & \text{if } h_l \in H_r \\ (\omega^l, \mathbf{w}) & \text{if } h_l \notin H_r \end{cases} \quad \text{and} \quad \alpha_{H_w}(l) = \begin{cases} (h^l, \mathbf{w}) & \text{if } h_l \in H_w \\ \# & \text{if } h_l \notin H_w \end{cases} $$

the first simulating the guard part of the observable transition and the second the writing/relocation.

**Example 3.2.** Fig. 4 depicts the encoding applied to the HRA of Example 2.2. Given the word $w = abcabb$ and its renaming $\zeta(w) = a^0a^1b^0b^1c^0c^1a^1a^2b^1b^2b^3$, we present how the encoding works. $A_h$ has two histories: $H = \{O, E\}$, thus the set of variables $V$ of $[[A_h]]_\zeta$ is $\{O^1, \omega^1\}$ on layer 1 and $\{E^2, \omega^2\}$ on layer 2. Let $(q_{ow}, M_\emptyset)$ be the initial state for both automata, with $M_\emptyset$ the memory context where all variables/histories are empty.

When reading the first letter $a$ in $A_h$, only transition $(q_{ow}, M_\emptyset) \xrightarrow{a} (q_{ew}, M_1)$ is enabled as $a$ is not stored in any of the histories in $M_\emptyset$, as a consequence, $a$ is added to $O$ in $M_1$. In $[[A_h]]_\zeta$, this transition is encoded with the sequence $(q_{ow}, M_\emptyset) \xrightarrow{a^0} (q'_{ow}, M') \xrightarrow{a^1} (q_{ew}, M'_1)$. The first transition when reading $a^0$, checks if $a^0$ is absent from both $O^1$ and $E^2$ using $\omega^1$ and $\omega^2$ with the injectivity constraint. When reading $a^1$ the transition $q'_{ow} \to q_{ew}$ writes the letter in $O^1$. Note that $a^0$ is still stored in $\omega^1$ and $\omega^2$, but it will never be read again (as the renaming $\zeta$ always increases the index of letters).

Similarly, when $A_h$ read the first occurrence of $b$, the only enabled transition is $(q_{ew}, M_1) \xrightarrow{b} (q_{ow}, M_2)$, where $b$ is stored in $E$ is $M_2$. And when reading $c$ the only transition enabled is $(q_{ow}, M_2) \xrightarrow{c} (q_{ew}, M_3)$ with $O$ storing both $a$ and $c$ while $E$ only stores $b$. In $[[A_h]]_\zeta$, this sequence of transitions is encoded by enabling the sequence of transitions $(q_{ew}, M'_1) \xrightarrow{b^0} (q'_{ew}, M''_1)$, $\xrightarrow{b^1} (q_{ow}, M'_2)$, $\xrightarrow{c^0} (q'_{ow}, M''_2)$, $\xrightarrow{c^1} (q_{ew}, M'_3)$. With $M'_2$ storing $b^1$ in $E^2$ and
$M'_3$ storing $c^1$ in $O^3$ in addition to $a^1$. This is the only sequence of transition that can be enabled as $b_0$ was not stored in $O^1$ in the state $(q_{ew}, M'_1)$ and $c^0$ was not stored in $E^2$ in $(q_{ow}, M'_2)$.

When reading the second occurrence of $a$ in $A_h$, the only enabled transition is $(q_{ew}, M_3) \xrightarrow{a} (q_{or}, M_4)$ where $a$ is transferred from $O$ to $E$ in $M_4$. In $[[A_h]]_\zeta$ this is encoded by the sequence of transitions $(q_{ew}, M'_3) \xrightarrow{a^1} (q''_{ew}, M''_3) \xrightarrow{a^2} (q_{or}, M'_4)$. The first transition is the only one enabled in configuration $(q_{ew}, M'_3)$ as $a^1$ is already stored in $O^1$, thus it would be impossible to write it in $\omega^1$ to enable the transition to $q'_{ew}$. In $M'_4$, the letter $a^2$ is stored in $E^2$ along with $b^1$, while $a^1$ is still stored in $O^1$ but will never be read again in $\zeta(w)$, so it can be ignored. This is how the transfer mechanism is encoded in this construction.

Reading $bb$, the last two letters of $w$, will enable in $A_h$ the sequence $(q_{or}, M_4) \xrightarrow{b} (q_{er}, M_5)$ transferring $b$ from $E$ to $O$ in $M_5$ and then enabling $(q_{er}, M_5) \xrightarrow{b} (q_{or}, M_6)$ transferring $b$ back from $O$ to $E$ in $M_6$. In $[[A_h]]_\zeta$, this is encoded by reading the letters $b^1b^2b^2b^3$ and enabling the loop of transition between states $q_{or}$, $q'_{or}$, $q_{er}$ and $q'_{er}$. Looking if the previous occurrence of $b$, here $b^2$ (resp. $b^3$), is stored in $E^2$ (resp. $O^1$) by reading in the variable. Also checking if it is absent from $O^1$ (resp. $E^2$) by writing in the $\omega$ of the same layer. Then writing the next occurrence of $b$, here $b^3$ (resp. $b^4$), in $O^1$ (resp. $E^2$) to encode its transfer.

Notice that, as before, the language recognized by $[[A]]_\zeta$ is actually larger than $\mathcal{L}(A)$.

**Remark 3.1.** In [10], HRA are presented with a set of registers able to store only one letter at a time. Their content is overwritten whenever a letter is written into it. The authors proved that HRA using only histories are as expressive as the ones using both histories and register. However, the construction presented to remove registers is exponential in their number. This is caused by the need of decoupling the overwriting into two phases, first, one uses the content to verify if an observable transition is enabled and then erases the content of histories. The exponential construction comes from the fact that to keep the languages equivalent, for each phase, one can use only one observable transition. Instead, to show membership we do not need to prove the equivalence of languages and the construction in Definition 3.4, already splits transitions into these two phases, using two observable transitions. Hence, it can be extended to registers avoiding the exponential cost.

**Theorem 3.2.** Let $A$ be an HRA. $w \in \mathcal{L}(A)$ if and only if $\zeta(w) \in \mathcal{L}([[A]]_\zeta)$.

**Complexity** The two previous encodings give polynomial reductions of the membership problem from HRA to LaMA and from LaMA to $\nu$-A. Therefore, there is a polynomial reduction of the problem for HRA to $\nu$-A. The expressiveness results from [4] give a linear construction from $\nu$-A to LaMA and an exponential construction, in the number of layers, from LaMA to HRA. As $\nu$-A are 1-LaMA, the same construction can be used to translate a $\nu$-A into an HRA of polynomial size. This implies an equivalence of complexity class of the membership problem for $\nu$-A and HRA, as well as for $\nu$-A and LaMA. By transitivity, we get the same equivalence between LaMA and HRA. Next, we show that the membership problem for LaMA is NP-complete. For the hardness part, this is shown by resorting to a reduction from the 3SAT problem, while the completeness part follows by observing what would be the cost of executing a word on an automaton. Fig. 5 depicts the intuition behind the encoding of a 3SAT instance. The idea is that the gadget in Fig. 5a chooses non-deterministically the truth assignment of $X_i$ or $\overline{X}_i$ and the one in Fig. 5b checks that this assignment indeed satisfies the given clauses.

**Theorem 3.3.** The membership problem for LaMA is NP-complete.
<figure><img src="image_6.png" /><figcaption>Figure 5: Gadgets used for showing NP-hardness of the membership problem.</figcaption></figure>

Hence we can conclude that:

**Corollary 3.3.1.** The membership problems for $\nu$-A, LaMA and HRA is NP-complete.

As a direct consequence and looking at the expressiveness hierarchy in Fig. 1 we can also give a complexity class for the membership problem in FRA. Indeed, since FMA can be encoded into FRA [18], we can deduce NP-hardness, and completeness follows from their encoding into LaMA [4].

**Corollary 3.3.2.** The membership problem for FRA is NP-complete.

# 4 Complexity of the non-emptiness problem

The non-emptiness problem consists in deciding whether the language accepted by an automaton is non-empty, or in other words checking if there is a path from the initial configuration to a final configuration. As mentioned before, in [10], it has been shown that deciding the non-emptiness for HRA is Ackermann-complete. Still, the complexity for non-emptiness is known neither for LaMA nor for $\nu$-A. We start with the non-emptiness Problem for $\nu$-A. We show that the problem is PSPACE-complete. To do so, we reduce the TQBF problem (true fully quantified Boolean formula) to $\nu$-A non-emptiness. TQBF is known to be PSPACE-complete (Meyer-Stockmeyer theorem [1]).

**Lemma 4.1.** The non-emptiness problem is PSPACE-hard for $\nu$-A.

*Proof.* Let $\nu$NEP be the short for non-emptiness Problem for $\nu$-A.

We show that TQBF can be reduced to $\nu$NEP. Let $Q_1 x_1 \dots Q_n x_n (C_1 \wedge \dots \wedge C_m)$, be a fully quantified Boolean formula, where each $Q_i \in \{\forall, \exists\}$ and each $C_j$ is a clause comprising at most $n$ literals ($x_i$ or $\overline{x_i}$). We assume that literals in clauses are ordered according to the order of variable declarations and at most one literal per variable is present. To encode TQBF in $\nu$-A we consider:

* for each existentially quantified $x_i$, variables $X_i$ and $\overline{X_i}$, and the gadget depicted in Fig. 5a, used in the proof of Theorem 3.3;

* for each universally quantified $x_i$, variables $X_i$, $\overline{X_i}$ and $\tilde{X}_i$, and the gadget depicted in Fig. 6a. Variable $\tilde{X}_i$ is used as a flag to indicate that all possible truth assignments of $x_i$ have been considered. The initial transition of the gadget initializes variable $\overline{X}_i$ to $1_i$. The dashed automaton connected between states $q_1$ and $q_2$, handling other variables and the clauses, is constructed recursively. The looping part starting in state $q_2$ writes letter $2_i$ into variable $\tilde{X}_i$, which is used after browsing once again the dashed part to reach the final state $q_f$. After this, variable $\overline{X}_i$ is reset and then variable $X_i$ is initialized to $1_i$ to consider
<figure><img src="image_7.png" /><figcaption>Figure 6: Gadgets used for showing NP-hardness of the emptiness problem for $\nu$-A.</figcaption></figure>

the other truth assignment of $x_i$. From state $q_5$ to $q_1$ all the variables for $x_j$, with $j$ from $i+1$ to $n$ are reset to reinitialize their truth assignments;

* for each clause $C_j$, a clause gadget depicted in Fig. 6b. It tests literals one after the other and takes the oblique transition for the first which makes the clause satisfied, which means that the remaining literals are just read up to the end of the clause, which is satisfied if $q_f$ is reached.

In order to construct the $\nu$-A $A$ encoding the instance of TQBF we connect first the clause gadgets by merging the final state of a clause gadget with the initial state of the next one. Let $C$ be the resulting automaton. Then, we connect to $C$ the gadgets for variable declarations starting from the $n$th, i.e., the last in the order of declarations. If the variable is under an existential quantifier, we connect the existential variable gadget in front of the automaton obtained so far by merging its final state with the initial state of $C$. If the variable is under a universal quantifier, we connect the corresponding gadget by merging the initial state of $C$ with state $q_1$ of the gadget, and the final state of $C$ with state $q_2$ of the gadget. We connect this way, i.e., following the inverse order of declarations, the gadgets for all the remaining variable declarations. The initial state of the first declared variable gadget is the initial state of $A$ and the unique state $q_f$ of the final construction is the unique final state of $A$. Finally, the input word $w$ is obtained recursively for each TQBF instance by the function *input*($\phi$) defined in Algorithm 1. The construction of the word follows the intuition given above (for the construction of the automaton), that is: it unfolds the loops generating the letters needed at each step.

Example: for the TQBF instance $\exists x_1 \forall x_2 \forall x_3 \exists x_4((x_1 \lor \overline{x_4}) \land (\overline{x_2} \lor \overline{x_3} \lor x_4))$, Fig. 7 represents a general construction schema of the corresponding $\nu$-A, and the input word is $1112131411141213142313141114121314232212131411141213142312131411141213142322$.

Note that every gadget of the automaton is deterministic, except for the existential variable gadget. The size of $A$ is polynomial in the size of the TQBF expression. The length of the word generated by Algorithm 1 is in $\Omega(2^n)$ but it is not a parameter of the construction of $A$. Clearly, only a word generated by Algorithm 1 (or a consistent renaming) can be accepted by $A$ starting
<caption>**Algorithm 1** Function to generate the word accepted by TQBF automaton</caption>

1: **function** INPUT($\phi$) 	$\triangleright \ \phi = Q_1x_1...Q_nx_n C_1...C_m$
2:   $\forall i \in [1, n] : init(x_i) = 1_i$
3:   $\forall i \in [1, n] : done(x_i) = 2_i$
4:   $\forall j \in [1, m] : w_j$
5:   $\triangleright$ contains exactly one $1_i$ for each $x_i$ or $\bar{x}_i$ present in clause $C_j$
6:   **else if** $\phi = \emptyset$ **then return** $\epsilon$
7:   **else if** $\phi = \exists x_i \phi'$ **then return** init($x_i$).input($\phi'$)
8:   **else if** $\phi = \forall x_i \phi'$ **then return** init($x_i$).input($\phi'$).done($x_i$).init($x_i$).input($\phi'$).done($x_i$)

**else if** $\phi = C_i \phi'$ **then return** $w_i$.input($\phi'$)

<figure><img src="image_8.png" /><figcaption>Figure 7: Schema of construction for TQBF instance $\exists x_1 \forall x_2 \forall x_3 \exists x_4 ((x_1 \lor \bar{x}_4) \land (\bar{x}_2 \lor \bar{x}_3 \lor x_4))$.</figcaption></figure>

with an empty memory context. Such a word can be accepted if and only if there is a solution to the TQBF instance. □

It remains to show that the non-emptiness problem for $\nu$-A is in PSPACE. This accounts for showing that if the language recognized by an $\nu$-A is non-empty then it contains a word whose size together with the length of the transition path needed to accept it, are exponentially bounded with respect to the size of the $\nu$-A. To this aim, we “build” a finite state machine (FSM) characterizing an abstraction of the state space of the $\nu$-A.

If one can choose the letters to read, the idea is that observable transitions that write a letter in a variable are never blocking. Since the alphabet is infinite there is always a fresh letter that can be added, which we call a token. Instead, observable transitions that read a letter from a variable are blocking, in the sense that concerned variables must contain at least a letter (that we call a key). The first step towards the construction of the FSM is to build a *canonical* $\nu$-A such that a word accepted by the canonical automaton will also be accepted by the initial $\nu$-A A and each word accepted by A will have a corresponding canonical version. Consider a $\nu$-A $A = (Q, q_0, F, \Delta, V, M_0)$, its *canonical* version $\text{cano}(A) = (Q, q_0, F, \Delta, V, M'_0)$ is an $\nu$-A over the alphabets $K$ and $T$, where:

* $K \subset \mathcal{U}$, such that $|K| = |V|$, is the set of *keys* $k_v$, each of them being associated with a variable $v \in V$. If $M_0(v) \neq \emptyset$, we select $k_v$ in $M_0(v)$. Also, if $M_0(v) = \emptyset$, we select $k_v$ such that $\forall v' \in V, k_v \notin M_0(v')$. The presence of a key in a variable $v$ denotes the fact that $v$ is non-empty.

* $T = \{t_1, t_2, \dots\} \subset \mathcal{U}$, $K \cap T = \emptyset$, is an infinite set containing letters called *tokens* intended to be used only once, which are never stored in memory. Hence, no letter in $T$ is present in the initial memory context of $A$, $\forall v \in V : M_0(v) \cap T = \emptyset$.

* For each $v \in V$, the initial memory context $M'_0(v)$ of $\text{cano}(A)$ is either empty if $M_0(v) = \emptyset$, or if $M_0(v) \neq \emptyset$, it only contains its key $k_v$.
Notice that a word $w$ is accepted by cano($A$) if the following conditions hold:

1. $w \in (K \cup T)^*$, and if $t_i \in T$ appears in $w$ then it occurs at most once,

2. let $(q_0, M'_0) \underset{cano(A)}{\overset{w}{\rightleftharpoons}} (q_f, M_f)$ with $q_f \in F$ be the accepting path for $w$ then for each intermediate configuration $(q, M)$ in the path and for each $k_v \in K$ either $k_v \in M(v)$ or for all $v' \in V$, $k_v \notin M(v')$.

Observe that cano($A$) is actually the same automaton as $A$ but over a subset of the alphabet $\mathcal{U}$ and where for each $v \in V$, $M'_0(v) \subseteq M_0(v)$, hence it is easy to conclude that the language of cano($A$) is included in the one of $A$.

**Lemma 4.2.** Let $A$ and cano($A$) be a $\nu$-A and its canonical version. If a word $w \in \mathcal{L}(cano(A))$ then $w \in \mathcal{L}(A)$.

We want to show that the language accepted by a $\nu$-A $A$ is empty if and only if the language accepted by cano($A$) is empty. The if part is the most involved and is the content of the following lemma.

**Lemma 4.3.** Let $A$ be a $\nu$-A and cano($A$) and its canonical version. If $w \in \mathcal{L}(A)$ then there exists $w' \in \mathcal{L}(cano(A))$.

*Proof.* Let $w = u_1 \dots u_n \in \mathcal{L}(A)$. Then there exists an accepting path $(q_0, M'_0) \underset{A}{\overset{w}{\rightleftharpoons}} (q_f, M_f)$ with $q_f \in F$ and intermediate configurations $(q_i, M_i)_{i \ge 0}$. Depending on those intermediate configurations we build a new word $w' = u'_1 \dots u'_n$ and the corresponding path in cano($A$) accepting $w'$. For each configuration $(q_i, M_i)$, the construction maintains an invariant: $\forall v \in V, M'_i(v) = \{k_v\}$ if and only if $M_i(v) \ne \emptyset$. The proof proceeds by induction:

**Base case:** By construction the initial configuration of cano($A$) satisfies the invariant.

**Inductive step:** We examine the transition $(q_i, M_i) \xrightarrow{\delta_i}{u_i} \rightarrow (q_{i+1}, M_{i+1})$. By inductive hypothesis, we know that there exists a sequence of transitions $(q_0, M'_0) \underset{cano(A)}{\overset{u'_1 \dots u'_{i-1}}{\rightleftharpoons}} (q_i, M'_i)$ such that $\forall v \in V, M'_i(v) = \{k_v\}$ if and only if $M_i(v) \ne \emptyset$. We prove there is a letter $u'_i$ leading to the configuration $(q_{i+1}, M'_{i+1})$ satisfying this property, through $\delta_i$ (by construction $A$ and cano($A$) are defined on the same set of transitions), we list all possible cases:

- $\delta_i = (q_i, \mathbf{reset}, q_{i+1})$: then $u_i = u'_i = \emptyset$ and $\delta_i$ will lead to a configuration with $M'_{i+1}(v) = \emptyset$ if $v \in \mathbf{reset}$ or $M'_{i+1}(v) = M'_i(v)$ otherwise. Hence satisfying the invariant.

- $\delta_i = (q_i, v, \mathbf{r}, q_{i+1})$: then $M_i(v) \ne \emptyset$ otherwise the transition could not be enabled, so $u'_i = k_v$ and by inductive hypothesis $M'_i(v) = \{k_v\}$. Since the memory context does not change for both automata, the invariant is satisfied;

- $\delta_i = (q_i, v, \mathbf{w}, q_{i+1})$: if $M_i(v) = \emptyset$, then $u'_i = k_v$, and $k_v$ will be written in variable $v$ in $M'_{i+1}$ satisfying the invariant. If $M_i(v) \ne \emptyset$, then $u'_i = t_i \in T$ is a token and $M'_i(v) = M'_{i+1}(v)$ since tokens are not stored in memory. By inductive hypothesis we know that $M'_i(v) = \{k_v\}$ and as $\delta_i$ is a writing transition, then $M_{i+1} \ne \emptyset$, satisfying the invariant.

From the previous construction, it follows immediately that $w' \in \mathcal{L}(cano(A))$. $\square$
Observe that, when reading a word $w \in \mathcal{L}(\mathit{cano}(A))$, we only need to store the letters be-
longing to $K$. Indeed, tokens in $T$ may occur only once in $w$. This entails that tokens can only
enable a write observable transition, while for read transitions keys are sufficient. Hence, in
practice, tokens do not need to be added to the memory context. Hence the number of different
configurations in $\mathit{cano}(A)$ is bounded by $|Q| \cdot 2^{|K|}$ as:

• we have $|Q|$ states that can be encoded on $\log|Q|$ bits, and

• there are $2^{|K|}$ possibilities to store the presence or not in the memory of letters in $K$ (2 possibilities per letter encoded on 1 bit since each $k_v$ can only be stored in $v$), so in total we need $|K|$ bits.

This shows that the number of configurations is finite. On top of this, as remarked above,
transitions over letters in T do not add constraints on the memory context and they can be
ignored. Hence the alphabet is now finite and we can reduce the non-emptiness of FSM to the
non-emptiness problem of $\nu$-A.

**Lemma 4.4.** The non-emptiness problem for $\nu$-A is in PSPACE

*Proof.* Given a $\nu$-A $A = (Q, q_0, F, \Delta, V, M_0)$, its canonical form has at most $|Q|2^{|K|}$ configura-
tions. The state space of $\mathit{cano}(A)$ could be constructed as an FSM by merging all transitions of
$A$ writing a token from $T$ going from state $q$ to $q'$ into a unique transition. This way, the FSM
would have $O(|\Delta|2^{|K|})$ transitions as each configuration $(q, M')$ of $\mathit{cano}(A)$ has at most as many
outgoing transitions as $q$ in $A$. A formal definition of the construction is in [3].

Moreover, if the underlying FSM is non-empty it implies that there is a sequence of at most $O(|\Delta|2^{|K|})$ transitions from an initial state of $A$ to one of its accepting state. Recall that finding a path between two vertexes/states in a graph $(V, E)$ is a problem called PATH which is NL-complete [1]. The algorithm for PATH, in logarithmic space, could be adapted to find whether there exists a sequence of transitions from an initial state of $A$ to an accepting state. Since this sequence of transitions is exponential in the size of $A$, we prove that the problem is in NPSPACE for $\nu$-A. Since PSPACE=NPSPACE [1] we show that the non-emptiness problem for $\nu$-A is in PSPACE.

The PATH algorithm adapted to our problem memorizes a state of $A$, the memory context of $\mathit{cano}(A)$ and a counter on $O(\log(|\Delta|) + |K|)$ bits. Each time that the counter is augmented by one, a transition starting in the memorized state will be chosen randomly and applied as follows: if this transition is a reset, then the state is updated and the memory is reset. If this transition is a write, then the state is updated and the corresponding key is added to the memory (if not already present). If the transition is a read then either the key is not in the memory and the algorithm halts and rejects or the state is updated. As soon as an accepting state is reached then the algorithm halts and accepts. If the counter reaches its maximum then the algorithm halts and rejects. Note that the FSM is not actually constructed in this algorithm, but only one of its paths is explored dynamically. $\square$

**Theorem 4.5.** The non-emptiness problem for $\nu$-A PSPACE-complete.

*Proof.* By Lemmata 4.1 and 4.4. $\square$

# 5 Conclusions

We have discussed the complexity of membership and non-emptiness for three formalisms $\nu$-
A, LaMA and HRA. We showed that concerning the membership problem, all three kinds of
automata fall in the NP-complete class. Non-emptiness is more delicate. We proved that the non-emptiness problem for $\nu$-A is PSPACE-complete.

For LaMA, we know the lower bound and the upper bound of the complexity class of the non-emptiness problem. As a consequence of Theorem 4.5 and from the expressiveness results in [4], the complexity is PSPACE-hard. However, it is a strict lower bound as we are able to construct a LaMA where the shortest accepted word is of size in $O(2^{2^n})$ with $n$ the number of variables. In our previous work [4], we showed an exponential encoding of LaMA into HRA for which the non-emptiness problem is shown to be Ackermann-complete in [10]. This also gives us the Ackermann class membership. As one of the reviewers suggested, we believe that we could adapt to LaMA the proof in [10] to show that the problem is actually Ackermann-complete.

As for future work, apart from formally showing the Ackermann-completeness of the non-emptiness problem for LaMA, we plan to address other expressiveness issues of LaMA. Indeed the number of layers seems to create a hierarchy of expressiveness and complexity.
References

[1] S. Arora and B. Barak. *Computational Complexity: A Modern Approach*. Cambridge University Press, 2006. URL: https://theory.cs.princeton.edu/complexity/book.pdf.

[2] Clement Bertrand. *Reconnaissance de motifs dynamiques par automates temporisés à mémoire*. Theses, Université Paris-Saclay, December 2020. URL: https://theses.hal.science/tel-03172600.

[3] Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, and Damien Regnault. Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata. Technical report, Université Côte d'Azur, CNRS, I3S, France ; IBISC, Univ. Evry, Université Paris-Saclay, France ; Scalian Digital Systems, Valbonne, France, 2023. URL: https://hal.science/hal-04155339.

[4] Clément Bertrand, Hanna Klaudel, and Frédéric Peschanski. Layered memory automata: Recognizers for quasi-regular languages with unbounded memory. In Luca Bernardinello and Laure Petrucci, editors, *Application and Theory of Petri Nets and Concurrency - 43rd International Conference, PETRI NETS 2022, Bergen, Norway, June 19-24, 2022, Proceedings*, volume 13288 of *Lecture Notes in Computer Science*, pages 43–63. Springer, 2022. doi:10.1007/978-3-031-06653-5\_3.

[5] Clément Bertrand, Frédéric Peschanski, Hanna Klaudel, and Matthieu Latapy. Pattern matching in link streams: Timed-automata with finite memory. *Sci. Ann. Comput. Sci.*, 28(2):161–198, 2018. URL: http://www.info.uaic.ro/bin/Annals/Article?v=XXVIII2&a=1.

[6] Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. *Theoretical Computer Science*, 411(4):702–715, 2010. Fundamentals of Computation Theory. URL: https://www.sciencedirect.com/science/article/pii/S0304397509007518, doi:10.1016/j.tcs.2009.10.009.

[7] Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. *ACM Trans. Comput. Log.*, 12(4):27:1–27:26, 2011. doi:10.1145/1970398.1970403.

[8] Aurelien Deharbe and Frédéric Peschanski. The omniscient garbage collector: A resource analysis framework. In *14th International Conference on Application of Concurrency to System Design, ACSD 2014, Tunis La Marsa, Tunisia, June 23-27, 2014*, pages 102–111. IEEE Computer Society, 2014. doi:10.1109/ACSD.2014.18.

[9] Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. *ACM Trans. Comput. Logic*, 10(3), April 2009. doi:10.1145/1507244.1507246.

[10] Radu Grigore and Nikos Tzevelekos. History-register automata. *Log. Methods Comput. Sci.*, 12(1), 2016. doi:10.2168/LMCS-12(1:7)2016.

[11] Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Variable automata over infinite alphabets. In *Adrian-Horia Dediu, Henning Fernau, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings*, volume 6031 of *Lecture Notes in Computer Science*, pages 561–572. Springer, 2010. doi:10.1007/978-3-642-13089-2\_47.
[12] Michael Kaminski and Nissim Francez. Finite-memory automata. *Theor. Comput. Sci.*, 134(2):329-363, 1994. doi:10.1016/0304-3975(94)90242-9.

[13] Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. *Int. J. Found. Comput. Sci.*, 21(5):741-760, 2010. doi:10.1142/S0129054110007532.

[14] Ahmet Kara. *Logics on data words: Expressivity, satisfiability, model checking*. PhD thesis, Technical University of Dortmund, Germany, 2016. URL: http://hdl.handle.net/2003/35216.

[15] Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Polynomial-time equivalence testing for deterministic fresh-register automata. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, *43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK*, volume 117 of LIPIcs, pages 72:1-72:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.MFCS.2018.72.

[16] Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. *ACM Trans. Comput. Logic*, 5(3):403-435, July 2004. doi:10.1145/1013560.1013562.

[17] Hiroshi Sakamoto and Daisuke Ikeda. Intractability of decision problems for finite-memory automata. *Theoretical Computer Science*, 231(2):297-308, 2000. URL: http://www.sciencedirect.com/science/article/pii/S030439759900105X doi:10.1016/S0304-3975(99)00105-X.

[18] Nikos Tzevelekos. Fresh-register automata. In Thomas Ball and Mooly Sagiv, editors, *Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011*, pages 295-306. ACM, 2011. doi:10.1145/1926385.1926420.
# A Simulating the membership for LaMA in $\nu$-automata – proofs

The proof of the main theorem relies on some lemmata, showing that the encoding is correct.

**Lemma A.1 (Non-observable transitions).** Let $A$ be an $n$-LaMA. $(q, M) \xrightarrow{\varepsilon} A$ if and only if $(q, [[M]]_{\xi}) \xrightarrow{\varepsilon} (q', [[M']']_{\xi})$.

*Proof.* For both sides the proof follows by the construction of the $\nu$-A, observing that non-observable transitions have the same semantics in both families of automata. $\square$

**Lemma A.2 (Observable transitions).** Let $A$ be an $n$-LaMA. $(q, M) \xrightarrow{u} A$ if and only if

$$ (q, [[M]]_{\xi}) \xrightarrow{\xi^n(u)} (q', [[M_1]]_{\xi}) $$

*Proof.* Let $(q, M) \xrightarrow{u} (q', M_1)$ then by definition we know that $\delta = (q, \alpha, q') \in \Delta_o$ and by construction of $[[A]]_{\xi}$, there is a path of length $n$ of observable transitions from $q$ to $q'$. Hence, let $\xi^n(u) = u^1 \dots u^n$, we need to prove that $(q, [[M]]_{\xi}) \xrightarrow{\xi^n(u)} (q', M_2)$ with $M_2 = [[M_1]]_{\xi}$. Each of these subsequent transitions considers the changes to a variable of the corresponding layer. By induction of the length of this path $n$. The base case $n = 1$ is trivial as a 1-LaMA is also a $\nu$-A. For $n > 1$, we know by inductive hypothesis that $(q, [[M]]_{\xi}) \xrightarrow{u^1 \dots u^{n-1}} [[A]]_{\xi}$ ($q_\delta^{n-1}, M_3$) where for all $l < n, M_3(\alpha(l)]_1) = [[M_1]]_{\xi}(\alpha(l)]_1$ and $M_3(\alpha(n)]_1) = [[M]]_{\xi}(\alpha(n)]_1)$. Now for the last step in the derivation, we have three possible cases, let $\alpha(n)]_1 = v^n$:

$\alpha(n)]_2 = \mathbf{r}$: by hypothesis we have $u \in M(v)$ and by construction $u^n \in [[M]]_{\xi}(v)$ hence the transition can be executed in $[[A]]_{\xi}$ leading to $(q', [[M_1]]_{\xi})$.

$\alpha(n)]_2 = \mathbf{w}$: by hypothesis $\forall v_1^n \in V, u \notin M(v_1^n)$, and $M'(v^n) = M(v^n) \cup \{u\}$. By construction, we know that $\forall v_1^n \in V', u^n \notin [[M]]_{\xi}(v_1^n)$. Moreover by definition of $\xi^n(u)$, $u^n \notin [[M]]_{\xi}(v_2)$ for all $v_2 \in V'$. Hence injectivity is satisfied and $u^n$ is added to $[[M]]_{\xi}(v)$ as expected leading to $(q', [[M_1]]_{\xi})$.

$\alpha(n) = \vdash$: the letter is consumed without examining any variable, leading to $(q', [[M_1]]_{\xi})$.

For the other direction, let $\xi^n(u) = u^1 \dots u^n$ we know that $(q, [[M]]_{\xi}) \xrightarrow{\xi^n(u)} (q', M_2)$, hence by construction $\delta = (q, \alpha, q') \in \Delta_o$. We need to show that $(q, M) \xrightarrow{u} (q', M_1)$ and $M_2 = [[M_1]]_{\xi}$.

Similarly as before the proof proceeds by induction on the length of the path from $q$ to $q'$ in $[[A]]_{\xi}$. For $n > 1$, we have that $(q, [[M]]_{\xi}) \xrightarrow{u^1 \dots u^{n-1}} [[A]]_{\xi}$ ($q_\delta^{n-1}, M_3$) and by inductive hypothesis for all $l < n, M_3(\alpha(l)]_1) = [[M_1]]_{\xi}(\alpha(l)]_1$ and $M_3(\alpha(n)]_1) = [[M]]_{\xi}(\alpha(n)]_1)$. Now for the last step in the derivation, we have three possible cases, let $\alpha(n)]_1 = v^n$:

$\alpha(n)]_2 = \mathbf{r}$: by hypothesis we have $u^n \in [[M]]_{\xi}(v^n) = M_3(v^n)$ thus by definition of the encoding of a memory context $[[\cdot]]_{\xi} u \in M(v^n)$ hence the transition can be executed in $A$ leading to $(q', M_1)$.
$\alpha(n)\lfloor_2 = w$: by hypothesis $u^n \notin \llbracket M\rrbracket_\xi(v_1)$ for all $v_1 \in V'$ this entails that $\forall v_1^n \in V, u \notin M(v_1^n)$ thus leading to $(q', M_1)$.

$\alpha(n) = \sharp$: the letter is consumed without examining any variable, leading again to $(q', M_1)$.

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

**Theorem 3.1.** Let $A$ be an $n$-LaMA. $w \in \mathcal{L}(A)$ if and only if $\xi^n(w) \in \mathcal{L}(\llbracket A\rrbracket_\xi)$.

*Proof.* The proof follows (for both sides) by induction on the length of the derivation of $w$ and $\xi^n(w)$ respectively using previous Lemmas A.1 and A.2. □

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

## B Simulating the membership for HRA in LaMA – proofs

Similarly as before, we first need to introduce some auxiliary definitions and lemmata.

**Definition B.1.** Let $M$ be a memory context, $H = h_1 \dots h_n$ a set of histories of an HRA $A$ and $w \in \mathcal{U}^*$. Then a memory context $M'$ for the set $V = h^1, \dots, h^n, \omega^1, \dots, \omega^n$ of variables of $\llbracket A\rrbracket_\zeta$ is well-formed with respect to $w$ and $M$ if it satisfies the following constraints: For all $l \in [1, n]$, if $u \in M(h_l)$ then

1. if $u$ appears in $w$ and $u_j$ is the last occurrence of $u$ in $w$ then $\zeta_{i_{u_j}}(u)\lfloor_2 \in M'(h^l)$

2. if $u$ does not appear in $w$ then $\zeta_1(u)\lfloor_1 \in M'(h^l)$ (i.e., $u_0 \in M'(h^l)$)

For all $l \in [1, n]$, if $u \notin M(h_l)$ then

1. if $u$ appears in $w$ and $u_j$ is the last occurrence of $u$ in $w$ then $\zeta_{i_{u_j}}(u)\lfloor_2 \notin M'(h^l)$

2. if $u$ does not appear in $w$ then $\zeta_1(u)\lfloor_1 \notin M'(h^l)$

**Lemma B.1.** Let $A$ be an HRA and $w = u_1 \dots u_m \in \mathcal{U}^*$. $(q_0, M_0) \xrightarrow{w} (q, M)$ if and only if $(q_0, M'_0) \xrightarrow{\zeta(w)} \llbracket A\rrbracket_\zeta$ with $M'$ well-formed with respect to $w$ and $M$.

*Proof.*

⇒ The proof proceeds by induction on the length of the derivation of $w$ with a case analysis on the last step of the derivation (with $w = w' \cdot x$):

$$(q_0, M_0) \xrightarrow{w'} (q_p, M_p) \xrightarrow{A} (q, M)$$

**Non-observable transitions:** Let $(q_p, M_p) \xrightarrow{\varepsilon} (q, M)$ then $x = \varepsilon$, $\delta = (q_p, H_\emptyset, q) \in \Delta_\varepsilon$.

By inductive hypothesis we know that $(q_0, M'_0) \xrightarrow{\zeta(w)} (q_p, M'_p)$ and $M'_p$ is well-formed with respect to $w$ and $M_p$. By construction $\delta' = (q_p, \text{reset}, q) \in \Delta'_\varepsilon$ with $\text{reset} = \{h^i | h_i \in H_\emptyset\}$ hence $(q_p, M'_p) \xrightarrow{\varepsilon} (q, M')$ where all variables in reset have been reset. It immediately follows that $M'$ is well-formed with respect to $w$ and $M$.
**Observable transitions:** Let $(q_p, M_p) \xrightarrow[A]{u_m} (q, M)$ then $x = u_m$, $\delta = (q_p, H_r, H_w, q) \in \Delta_o$. By inductive hypothesis we know that $(q_0, M'_0) \xrightarrow{\frac{\zeta(u_1...u_{m-1})}{[A]_\zeta}} (q_p, M'_p)$ and $M'_p$ is well-formed with respect to $u_1...u_{m-1}$ and $M_p$. Moreover by construction there are two transitions $(q_p, \alpha_{H_r}, q_\delta)$ and $(q_\delta, \alpha_{H_w}, q)$ in $\Delta'_o$. Hence $(q_p, M'_p) \xrightarrow{\frac{\zeta_{i_{u_m}}(u_m)_{\lfloor 1 \rfloor}}{[A]_\zeta}} (q, M')$

Transition $(q_p, M'_p) \xrightarrow{\frac{\zeta_{i_{u_m}}(u_m)_{\lfloor 1 \rfloor}}{[A]_\zeta}} (q_\delta, M'')$ can be executed as, since $M'_p$ is well formed with respect to $u_1...u_{m-1}$ and $M_p$, and $u_m \in M_p(h_i)$, $\forall h_j \in H_r$ then $\zeta_{i_{u_m}}(u_m)_{\lfloor 1 \rfloor} \in M'_p(h^j)$. Moreover since $u_m \notin M_p(h_j)$ for all $h_j \notin H_r$ then $\zeta_{i_{u_m}}(u_m)_{\lfloor 1 \rfloor} \notin M'_p(h^j)$ then $\zeta_{i_{u_m}}(u_m)_{\lfloor 1 \rfloor}$ can be added to $\omega^j$. Finally, transition $(q_\delta, M'') \xrightarrow{\frac{\zeta_{i_{u_m}}(u_m)_{\lfloor 2 \rfloor}}{[A]_\zeta}} (q, M')$ is always enabled as $\zeta_{i_{u_m}}(u_m)_{\lfloor 2 \rfloor}$ is a fresh letter.

As a last step, we need to show that $M'$ is well-formed with respect to $w$ and $M$. Now take $u \in M(h_i)$ there are three cases:

1. $u$ does not appear in $w$ then $u \in M_0(h_i)$ and hence by construction $\zeta_0(u) \in M'_0(h^i)$.

2. $u = u_j \neq u_m$, $j \in [1, m-1]$ then $u \in M_p(h_i)$ and since $M'_p$ is well-formed with respect to $u_1...u_{m-1}$ and $M_p$, then $\zeta_{i_{u_j}}(u)_{\lfloor 2 \rfloor} \in M'(h^i)$ with $u_j$ being the last occurrence of $u$ in $w$.

3. $u = u_m$ then this means that $h_i \in H_w$. Hence for what has been shown above $\zeta_{i_{u_m}}(u_m)_{\lfloor 2 \rfloor} \in M'(h^i)$.

Moreover for all $u \notin M(h_i)$ there are two cases

1. $u$ not occurs in $w$ then $u \notin M_0(h_i)$ and by construction $\zeta_1(u)_{\lfloor 1 \rfloor} \notin M'_0(h^i)$

2. $u$ occurs in $w$, let $u_j$ be the last occurrence of $u$ in $w$ then in the execution $(q_0, M_0) \xrightarrow[A]{w} (q, M)$ there is a transition $(q_1, M_1) \xrightarrow[A]{u_j} (q_2, M_2)$ with $\delta' = (q_1, H_r, H_w, q_2) \in \Delta_o$ and $h_i \notin H_w$ and hence by construction $\zeta_{i_{u_j}}(u)_{\lfloor 2 \rfloor} \notin M'_2(h^i)$ and hence $u_j \notin M'(h^i)$.

Suppose $(q_0, M'_0) \xrightarrow{\frac{\zeta(w)}{[A]_\zeta}} (q, M')$ with $M'$ well-formed with respect to $w$ and some $M$. We say that a step of the derivation is a sequence of transitions $(q_1, M_1) \xrightarrow[A]{x} (q_2, M_2)$ with $q_1, q_2 \in Q$, $x = \zeta_{i_{u_j}}(u_j)$ or $x = \varepsilon$ and all intermediate states $q' \notin Q$. The proof proceeds by induction on the length of the derivation of $\zeta(w)$ with a case analysis on the last step of the derivation:

**Non-observable transitions:** Let $(q_p, M'_p) \xrightarrow{\frac{\varepsilon}{[A]_\zeta}} (q, M')$ with $M'$ well-formed with respect to $w$ and $M$, then $\delta' = (q_p, \mathbf{reset}, q) \in \Delta'_o$. Now by construction there exists $\delta = (q_p, H_\emptyset, q) \in \Delta_\varepsilon$ such that $\mathbf{reset} = \{h^i \mid h_i \in H_\emptyset\}$. By inductive hypothesis we know that $(q_0, M_0) \xrightarrow[A]{w} (q_p, M_p)$ and $M'_p$ well-formed with respect to $w$ and $M_p$. Now the transition can be taken in $A$ and all variables in $H_\emptyset$ are emptied maintaining the well-formedness of $M'$.
**Observable transitions:** Let $(q_p, M'_p) \stackrel{\zeta_{i_{u_m}}(u_m)}{\rightleftharpoons} (q, M')$ then by construction there exists a transition $\delta = (q_p, H_r, H_w, q) \in \Delta_o$ such that there are two transitions $(q_p, \alpha_{H_r}, q_\delta)$ and $(q_\delta, \alpha_{H_w}, q)$ in $\Delta'_o$. By inductive hypothesis we know that $(q_0, M_0) \stackrel{u_1...u_{m-1}}{\rightleftharpoons} (q_p, M_p)$ and $M'_p$ is well-formed with respect to $u_1...u_{m-1}$ and $M_p$. Now $\delta$ can be executed because of well formedness of $M'_p$ if $\zeta_{i_{u_m}}(u_m) \rfloor_1 \in h^r$ with $h_r \in H_r$ then $u_m \in M_p(h_r)$, moreover we know that $\zeta_{i_{u_m}}(u_m) \rfloor_1 \notin M'_p(h^i)$ for all $h_i \notin H_r$ hence $u_m \notin M_p(h_i)$. Then, transition $(q_p, M_p) \stackrel{u_m}{\rightharpoons} (q, M)$ can be executed and $u_m$ is added to variables $h \in H_w$, keeping the well formedness of $M'$ with respect to $w$ and $M$.

□

And finally, we can conclude:

**Theorem 3.2.** Let $A$ be an HRA. $w \in \mathcal{L}(A)$ if and only if $\zeta(w) \in \mathcal{L}(\llbracket A \rrbracket_\zeta)$.

*Proof.* $w \in \mathcal{L}(A)$ if and only if $(q_0, M_0) \stackrel{w}{\rightleftharpoons} (q, M)$ with $q \in F$ if and only if by Lemma B.1 we have that $(q_0, M'_0) \stackrel{\zeta(w)}{\rightleftharpoons} (q, M')$ if and only if by construction $q \in F'$ if and only if $\zeta(w) \in \mathcal{L}(\llbracket A \rrbracket_\zeta)$. □

## C Complexity of membership – proofs

**Theorem 3.3.** The membership problem for LaMA is NP-complete.

*Proof.* Let LMP be the short for the membership problem for LaMA.

**NP-hardness:** we show that 3SAT can be reduced to LMP. Let $\exists X_1, \dots, \exists X_n C_1 \wedge \dots \wedge C_m$, where each $C_i$ is a clause of exactly 3 literals (i.e., positive or negative versions of variables $X_j$). To encode 3SAT in LaMA we consider for each $X_i$ two LaMA variables $X_i$ and $\bar{X}_i$ belonging to layer $i$, and an initialisation gadget composed of two states and two transitions depicted in Fig. 5a. For each clause $C_j$ we consider a clause gadget composed of two states and three transitions as depicted in Fig. 5b. In order to construct the $n$-LaMA $A$ encoding the instance of 3SAT we connect $n$ initialisation gadgets (one for each $X_i$) and then the $m$ clause gadgets. The initial state of the first variable is the initial state of $A$ and the exit state of the last clause gadget is the unique final state of $A$. The input word is $w = (1)^n(1)^m$, where the $n$ occurrences of letter 1 are used to non-deterministically initialise variable $X_i$ or $\bar{X}_i$. The next $m$ occurrences of letter 1 are used to accept at least one literal in each clause. It is easy to see that $w$ is accepted by $A$ starting with an empty memory context if and only if there is a solution to the 3SAT instance.

**NP-membership:** A certificate that a LaMA $A = (Q, q_0, F, \Delta, V, n, M_0)$ accepts $w$ is a sequence $\sigma = s_0 t_1 s_1 t_2 \dots s_m$ where all $s_i$ are configurations of the form $(q, M)$ with $q \in Q$ a state of $A$ and $M$ a memory context, $s_0 = (q_0, M_0)$, and each $t_i$ is a transition in $\Delta$. The certifier executes $\sigma$ and checks if (1) $s_m = (q', M')$ is a final configuration, i.e., if $q' \in F$ and (2) if $m \le (|w| + |w|(|Q| \cdot |V|))$. This upper bound comes from the observation that:

* each letter in $w$ needs exactly one transition;

* between two consecutive observable transitions in $\sigma$ there could be at most $O(|V| \cdot |Q|)$ reset transitions, as resetting the same variable twice has no effect and reaching the transition resetting a given variable can take at most $|Q| - 1$ steps.
This verification can be done in polynomial time since each observable transition takes $O(|V| \cdot |w|)$ steps and each reset transition $O(1)$.

□

## D Non-emptiness for $\nu$-automata is in PSPACE – proofs

**Lemma 4.2.** Let $A$ and cano($A$) be a $\nu$-A and its canonical version. If a word $w \in \mathcal{L}(cano(A))$ then $w \in \mathcal{L}(A)$.

*Proof.* Let $w \in \mathcal{L}(cano(A))$. Then there exists a path $(q_0, M'_0) \xrightarrow{w} (q_f, M'_f)$ with $q_f \in F$ and intermediate configurations $(q_i, M'_i)_{i \ge 0}$. We show by induction that $w \in \mathcal{L}(A)$ and the path accepting it is a sequence of configurations $(q_i, M_i)_{i \ge 0}$ with $M'_i$ being the projection of $M_i$ over the letters in $K$.

**Base case:** both automata start from the same initial state $q_0$. By definition, $\forall v \in V : k_v \in M_0(v)$ if and only if $M'_0(v) \neq \emptyset$. So, the property is true in the initial configuration.

**Inductive step:** We examine the transition $(q_i, M'_i) \xrightarrow{cano(A)} (q_{i+1}, M'_{i+1})$. By construction, the same transition must exist in $A$. Now, depending on the transition, consider the resulting memory context:

**reset:** the memory context of the variables in both automata are emptied, thus satisfying the property;

**read:** if it is a read of letter $u$ in $v$, the transition is fired in cano($A$) so $u = k_v$. By inductive hypothesis, in the memory context of $A$ we have $k_v \in M_i(v)$;

**write:** if it is a write of letter $u$ in $v$:

* if $k_v \notin M'_i(v)$, then $M_i(v) = \emptyset$ and it means $u = k_v$ as it is always the first letter written in an empty variable in cano($A$). Thus $M_{i+1}(v) = M'_{i+1}(v)$.

* if $k_v \in M'_i(v)$ then letter $u$ is a token, $u = t_i \in T$, and is written in $v$ for $A$, $t_i \in M_{i+1}(v)$ but not for cano($A$). The projection of $M_{i+1}(v)$ to $K$ will still contain $k_v$, thus the invariant is satisfied.

□

**Definition D.1 (FSM).** Let $A = (Q, q_0, F, \Delta, V, M_0)$ be a $\nu$-A and cano($A$) its canonical version, we define an FSM $fsm(A) = (K, S, s'_0, E, \delta)$, where

* $K = \{k_v \mid v \in V\}$ is the alphabet;

* $S = Q \times 2^K$ is the set of states, where $(q, m) \in S$ abstracts configuration $(q, M)$ of $A$ where $k_v \in m$ if and only if $k_v \in M(v)$;

* $s_0 = (q_0, m_0)$, with $m_0 = \{k_v \mid M_0(v) \neq \emptyset\}$ is the initial state;

* $E = F \times 2^K$ is the set of final states;

* $\delta \subseteq S \times (K \cup \{\epsilon\}) \times S$ is the set of transitions with

- $((q, m), k_v, (q', m)) \in \delta$ if and only if $((q, M), (v, r), (q', M)) \in \Delta$ and $k_v \in m$ (reads a key);
- $((q, m), k_v, (q', m')) \in \delta$ if and only if $((q, M), (v, w), (q', M')) \in \Delta$, $k_v \notin m$ and $m' = m \cup \{k_v\}$ (writes a key);

- $((q, m), \epsilon, (q', m)) \in \delta$ if and only if $((q, M), (v, w), (q', M')) \in \Delta$ and $k_v \in m$ (writes a token);

- $((q, m), \epsilon, (q', m')) \in \delta$ if and only if $((q, M), \mathbf{reset}, (q', M')) \in \Delta$ and $m' = m \setminus \mathbf{reset}$ (resets variables in $\mathbf{reset}$).

# E LaMA should not be in PSPACE

The LaMA presented in Fig. 8 accepts words of length in $O(2^{2^n})$, when its initial memory context is empty. We can decompose this automaton in three parts:

* The first part consists of the state $q_0$ with a self-loop allowing to write as many different letters as needed in $X^1$. This is the only transition actually adding new letters to $X^1$. The same $X^1$ is read to enable the final transition to $q_f$. State $q_0$ can be left through a $\epsilon$-transition to $q_1$.

* The second part includes the states from $q_1$ to $q_3$ will erase at least half of the letters stored in $X^1$. To do so, the two looping transitions between $q_1$ and $q_2$ will split in half the letters of $X^1$ between $Y^2$ and $Z^2$. Then the transition from $q_1$ to $q_3$ reset $X^1$, and the self-loop on $q_3$ allows to store back in $X^1$ the letters that were copied in $Y^2$. Finally, the outgoing transition of $q_3$ resets $Y^2$ and $Z^2$, definitely erasing the letters from $Z^2$. The whole process is non-deterministic, however, it is actually required to copy enough letters through this process so that the reset from $q_3 \to q_4$ will erase every letter in $X^1$, which is required for the final transition.

* The third part contains all states from $q_4$ to $q_m$. It is a repetition of the process described so far to ensure an exponential amount of iterations over the second part. In state $q_{m-2}$ (and respectively for all the previous states), there are two outgoing transitions: one that requires to read in $A^n$ and the other one that writes in (initialize) it. The reading transition is the one leading to the final state but it cannot be crossed as long as $A^n$ was not initialized through the other transition. The writing transition leads to the state $q_{m-1}$ and eventually back to $q_1$, while resetting every previous $A^i$ for $i < n$. As these variables are empty, all their initializations have to be done again.

The third part iterates back to the states of the second part $2^{n-2}$ times. Every time we pass through the second part, we lose at least half of the letters stored in $X^1$. Hence to be able to cross the last transitions, it is required that during the first part, at least $2^{n-2}$ letters are stored in $X^1$.
<figure><img src="image_11.png" /><figcaption>Figure 8: Example of a LaMA with words whose length is in $O(2^{2^n})$.</figcaption></figure>