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

HAL
open science

# Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Nicolas Waldburger

► To cite this version:

Nicolas Waldburger. Checking Presence Reachability Properties on Parameterized Shared-Memory Systems. MFCS 2023 - Mathematical Foundations of Computer Science, Aug 2023, Bordeaux, France. pp.88:1-88:15, 10.4230/LIPIcs.MFCS.2023.88 . hal-04394124

HAL Id: hal-04394124

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

Submitted on 15 Jan 2024

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Nicolas Waldburger ☐

Univ Rennes, Inria, CNRS, IRISA, France

## Abstract

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.

**2012 ACM Subject Classification** Theory of computation → Verification by model checking; Theory of computation → Distributed algorithms

**Keywords and phrases** Verification, Parameterized models, Distributed algorithms

**Digital Object Identifier** 10.4230/LIPIcs...

## 1 Introduction

**Parameterized verification.** Distributed systems consist of multiple processes running in parallel. Verification of such systems is a major topic of modern verification, because of how common these systems are and how difficult their verification has proven to be. Indeed, when multiple processes run asynchronously, the number of relevant interleavings to consider quickly becomes large. An intuitive approach for their verification is to fix the number of processes involved and try to apply classical verification techniques. Another approach is that of parameterized verification, where one aims to prove the more general statement that the property of interest holds for any number of participants. The interest of this approach is threefold. First, it allows to prove that the system is correct regardless of the number of processes. Second, the efficiency of parameterized techniques does not depend on the number of participants, which makes them more suitable for large systems for which classical techniques scale poorly. Third, parameterized verification often yields decidability or better computational complexity for problems that are hard to solve with classical techniques; see for example [14] for a problem that becomes decidable in the parameterized case. In their seminal work [13], German and Sistla consider systems consisting of a leader and arbitrarily many contributors, all of which are finite-state machines communicating via *rendez-vous*. In this setting, the safety verification problem is EXPSPACE-complete and the complexity drops down to polynomial time when the leader is removed. Since then, many similar models have been studied, with variations on the expressiveness of the processes and the means of communication in order to capture the large variety of existing distributed algorithms [10, 7].

**Contributions.** We study parameterized verification of systems where all processes are identical and anonymous finite-state machines that communicate via reading from and writing to a shared memory. The read and write actions are performed non-atomically, meaning that no process may perform a read-write combination while preventing all other processes from

<figure><img src="image_3.png" /></figure>
acting. Our registers are *initialized* with a special symbol; this assumption is common in parameterized verification of shared-memory systems [8, 1], since some algorithms require initialized registers, e.g. [2]. First, we study a model with finitely many registers. This model is inspired by [11] where registers were uninitialized and the verification is restricted to safety properties. In contrast, we study the more general *presence reachability problems*, in which one asks whether one may reach a configuration that satisfies a property. This property takes the form of a Boolean combination of constraints expressing whether there is at least one process in a given state of the finite-state machine. We prove that this problem is NP-complete and we provide several natural restrictions on the process description and on the property that make the problem solvable in polynomial time. We then work on the more general setting of *round-based shared-memory systems* [6], which are designed to model round-based shared-memory algorithms present in the literature, see e.g. [2, 16]. In this model, the processes proceed in asynchronous rounds, each round having its own fresh set of registers. The source of infinity is twofold, as the number of processes and the number of registers are both unbounded, making round-based systems particularly challenging to verify. The safety problem was proved to be PSPACE-complete in round-based shared-memory systems [6]. In this article, we go beyond safety by considering a round-based, richer version of the presence reachability problem where the property may quantify existentially and universally over the rounds. Nonetheless, we establish that the round-based presence reachability problem is PSPACE-complete.

**Related work.** Similar models and problems have been studied in the literature. In the shared-memory model (without rounds and without register initialization), the safety problem has been studied extensively with variations on the expressiveness given to the leader and the contributors [11]; in particular, when processes are finite-state machines, the safety problem is shown to be coNP-complete and to decrease to PTIME when the leader is removed. However, this result does not hold when registers are initialized or when the property is more general than safety. A model that has perhaps been more studied is that of *reconfigurable broadcast networks* (RBN), where processes communicate via broadcasting messages that can be received by any of the other processes. This model has similarities with shared-memory systems, although broadcast tends to be simpler (messages disappear after being sent, while written values remain in the registers). A source of inspiration for the first part of our article is the study of reachability problems in RBN [9], where it is shown that the cardinality reachability problem, where one wants to reach a configuration that satisfies cardinality constraints, is PSPACE-complete. When the constraints cannot count processes, this problem is analogous to our presence reachability problem; for RBN, it is shown to be NP-complete, a complexity that we also obtain in our setting. Finally, this complexity drops down to PTIME in RBN when considering the special case of safety. This tractability result no longer holds in the shared-memory world unless we make further assumptions about the number of registers or their initialization. The cube reachability problem is a generalization of the cardinality constraint problem where the initial configuration is also subject to cardinality constraints; this problem is PSPACE-complete both in RBN and in (roundless) asynchronous shared-memory systems [9, 5, 4], although it is unknown whether this remains true when allowing the Pre* and Post* operators in the description of the cubes [4, 3]. While it is interesting to compare results on RBN with our results on shared-memory systems without rounds, such a comparison is not possible with the more expressive model of round-based shared-memory systems, in particular because the unboundedness in the number of registers has no equivalent in broadcast networks.

Due to space constraints, most of the proofs can be found in the appendix.
## 2 Roundless Register Protocols

In this section, we introduce register protocols, a model inspired by [11]. We call these systems roundless to distinguish them from round-based systems introduced later in this article.

### 2.1 Definitions

**► Definition 1 (Roundless register protocols).** A roundless register protocol is a tuple $\mathcal{P} = (Q, Q_0, \dim, D, d_0, \Delta)$ where

- $Q$ is a finite set of states with a distinguished subset of initial states $Q_0 \subseteq Q$;

- $\dim \in \mathbb{N}$ is the number of shared registers;

- $D$ is a finite data alphabet containing the initial symbol $d_0$;

- $\Delta \subseteq Q \times \mathcal{A} \times Q$ is the set of transitions, where $\mathcal{A} := \{\text{read}_\alpha(d) \mid \alpha \in [1, \dim], d \in D\} \cup \{\text{write}_\alpha(d) \mid \alpha \in [1, \dim], d \in D \setminus \{d_0\}\}$ is the set of actions.

Roundless register protocols are executed on multiple processes that behave asynchronously and can only communicate via reading from and writing to the shared registers. The behavior of a process is described by a finite-state machine. The possible actions of the transitions are reading a symbol from and writing a symbol to one of the dim shared registers; $d \in D$ denotes the symbol and $\alpha$ indicates the register on which the action is performed. Each register stores one symbol from the finite set $D$ at a time. Read-write combinations are performed non-atomically, i.e., no process can perform a read-write combination while excluding all other processes. The size of the protocol $\mathcal{P}$ is defined as $|\mathcal{P}| := |Q| + |D| + |\Delta| + \dim$. For all $\alpha \in [1, \dim]$, we write $\text{rg}[\alpha]$ for the register of index $\alpha$. We also write $\text{Reg}$ for the set $\{\text{rg}[\alpha] \mid \alpha \in [1, \dim]\}$ of all registers.

Processes are assumed to have no identifiers so they are identical anonymous agents. Therefore, a configuration is a pair $\gamma = (\mu, \bar{d}) \in \mathbb{N}^Q \times \mathbb{D}^{\text{Reg}}$ such that $0 < \sum_{q \in Q} \mu(q) < \infty$. Let $\text{st}(\gamma) := \mu$ which indicates the number of processes in each state, and $\text{data}(\gamma) := \bar{d}$ mapping to each register its symbol: for all $r \in \text{Reg}$, $\text{data}(\gamma)(r)$ is the symbol contained in register $r$ in $\gamma$. Let $\Gamma := \mathbb{N}^Q \times \mathbb{D}^{\text{Reg}}$ denote the set of all configurations. Let $\text{supp}(\gamma) := \{q \in Q \mid \text{st}(\gamma)(q) > 0\}$ denote the support of the multiset $\text{st}(\gamma)$. We write $\oplus$ and $\ominus$ the operations on multisets that add and remove elements, respectively. A configuration is initial if all processes are in states from $Q_0$ while all registers have value $d_0$. We denote by $\text{Init}_c$ the set of initial configurations (the letter c stands for “concrete” as opposed to “abstract” configurations defined later). Formally, $\text{Init}_c := \{\gamma \mid \text{st}(\gamma) \subseteq Q_0, \text{data}(\gamma) = d_0^{\text{Reg}}\}$.

Given $\gamma, \gamma' \in \Gamma$, $\gamma'$ is a successor of $\gamma$ when there exists $\delta = (q, a, q') \in \Delta$ such that $\text{st}(\gamma)(q) > 0$, $\text{st}(\gamma') = (\text{st}(\gamma) \ominus \{q\}) \oplus \{q'\}$ and:

- if $a = \text{read}_\alpha(d)$ then $\text{data}(\gamma)(\text{rg}[\alpha]) = d$ and $\text{data}(\gamma') = \text{data}(\gamma)$,

- if $a = \text{write}_\alpha(d)$ then $\text{data}(\gamma')(\text{rg}[\alpha]) = d$ and $\forall \alpha' \neq \alpha$, $\text{data}(\gamma')(\text{rg}[\alpha']) = \text{data}(\gamma)(\text{rg}[\alpha'])$.

In that case, we write $\gamma \xrightarrow{\delta} \gamma'$ or simply $\gamma \to \gamma'$, which is called a step. A concrete execution is a sequence $\pi = \gamma_0, \delta_1, \gamma_1, \dots, \gamma_{l-1}, \delta_l, \gamma_l$ such that for all $i$, $\gamma_i \xrightarrow{\delta_{i+1}} \gamma_{i+1}$. We write $\gamma_0 \xrightarrow{*} \gamma_l$ for the existence of such an execution. $\gamma'$ is reachable from $\gamma$ when $\gamma \xrightarrow{*} \gamma'$. Given a set $C$ of configurations, we write $\text{Reach}_c(C) := \{\gamma' \mid \exists \gamma \in C, \gamma \xrightarrow{*} \gamma'\}$. A configuration is reachable when it is in $\text{Reach}_c(\text{Init}_c)$.

**► Example 2.** Figure 1 provides an example of a roundless register protocol $\mathcal{P}$ with $D = \{d_0, a, b, c\}$, $Q_0 = \{q_0\}$ and $\dim = 1$, hence read and write actions are implicitly on register $\alpha = 1$. The red and blue labels are to be ignored for now.
XX:4 Checking PRPs on Parameterized Shared-Memory Systems

<figure><img src="image_4.png" /><figcaption>Figure 1 An example of a protocol</figcaption></figure>

The set of initial configurations is Init$_c := \{\langle q_0^n, d_0 \rangle | n \ge 1\}$. The following execution with two processes witnesses that $\langle q_f \oplus C, a \rangle \in \text{Reach}_c(\text{Init}_c)$:

$$ \begin{align*} \langle q_0^2, d_0 \rangle \xrightarrow{\langle q_0, \text{read}(d_0), B \rangle} \langle q_0 \oplus B, d_0 \rangle \xrightarrow{\langle B, \text{read}(d_0), C \rangle} \langle q_0 \oplus C, d_0 \rangle \xrightarrow{\langle q_0, \text{write}(c), A \rangle} \\ \langle A \oplus C, c \rangle \xrightarrow{\langle C, \text{write}(a), C \rangle} \langle A \oplus C, a \rangle \xrightarrow{\langle A, \text{read}(a), q_f \rangle} \langle q_f \oplus C, a \rangle. \end{align*} $$

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

## 2.2 Reachability Problems

Our first problem of interest is the *coverability problem* (COVER):

COVER FOR ROUNDLESS REGISTER PROTOCOLS

**Input:** A roundless register protocol $\mathcal{P}$, $q_f \in Q$

**Question:** Does there exist $\gamma \in \text{Reach}_c(\text{Init}_c)$ such that $\text{st}(\gamma)(q_f) > 0$?

Note that, because the model is parameterized, a witness execution of COVER may have an arbitrarily large number of processes. The dual is the *safety problem*, the answer to which is yes when an error state cannot be covered regardless of the number of processes. A similar problem is the *target problem* (TARGET) where processes must synchronize at $q_f$:

TARGET FOR ROUNDLESS REGISTER PROTOCOLS

**Input:** A roundless register protocol $\mathcal{P}$, $q_f \in Q$

**Question:** Does there exist $\gamma \in \text{Reach}_c(\text{Init}_c)$ s.t. for all $q \neq q_f$, $\text{st}(\gamma)(q) = 0$?

**Remark 3.** TARGET is harder than COVER: consider the reduction in which one adds a loop on $q_f$ writing a joker symbol which, from any state, may be read to reach $q_f$.

*Presence constraints* are Boolean combinations (with $\wedge$, $\vee$ and $\neg$) of atomic propositions of the form “q populated” with $q \in Q$, or of the form “r contains d” with $r \in \text{Reg}$ and $d \in D$. A presence constraint is interpreted over a configuration $\gamma$ by interpreting “q populated” as true if and only if $\text{st}(\gamma)(q) > 0$ and “r contains d” as true if and only if $\text{data}(\gamma)(r) = d$. Note that presence constraints cannot refer to how many processes are on a given state. We write $\gamma \models \phi$ when configuration $\gamma$ satisfies presence constraint $\phi$.

**Example 4.** If $Q = \{q_1, q_2, q_3\}$, $\text{dim} = 2$, $D = \{d_0, a, b\}$ and $\phi := (q_1 \text{ populated}) \vee ((q_2 \text{ populated}) \wedge (\text{rg}[1] \text{ contains } a))$ then $\langle q_1 \oplus q_3, d_0^2 \rangle \models \phi$, $\langle q_2^2, (a, b) \rangle \models \phi$ but $\langle q_2^2, b^2 \rangle \not\models \phi$. ◀

The *Presence Reachability Problem* (PRP) generalizes both COVER and TARGET. It corresponds to the cardinality reachability problem for cardinality constraints restricted to $CC[\ge 1, = 0]$ studied for broadcast protocols [9].

PRP FOR ROUNDLESS REGISTER PROTOCOLS

**Input:** A roundless register protocol $\mathcal{P}$, a presence constraint $\phi$

**Question:** Does there exist $\gamma \in \text{Reach}_c(\text{Init}_c)$ such that $\gamma \models \phi$?
The formula $\phi$ automatically makes PRP NP-hard, since one can encode the SAT problem. Therefore, we also consider the *DNF Presence Reachability Problem* (DNF-PRP), in which $\phi$ is in *disjunctive normal form*. COVER and TARGET are special cases of DNF-PRP, with $\phi = (q_f \text{ populated})$ for COVER and $\phi = \bigwedge_{q \neq q_f} \neg(q \text{ populated})$ for TARGET.

**Example 5.** Consider again the protocol $\mathcal{P}$ defined in Figure 1. ($\mathcal{P}, q_f$) is a positive instance of COVER, as proved in Example 2. Let $\mathcal{P}_{\text{blue}}$ be the protocol obtained from $\mathcal{P}$ by changing to read(c) the label of the transition from $q_0$ to B (in blue in Figure 1). ($\mathcal{P}_{\text{blue}}, q_f$) is a negative instance of COVER. In fact, a process can only get to B if c has been written to the register, and then $d_0$ can no longer be read so no process may go to state C, a cannot be written and no process may go from A to $q_f$.

($\mathcal{P}, q_f$) is a negative instance of TARGET: to leave $A$, one needs to read $a$, hence must have a process on state $C$, and to leave $C$, one must read $b$ which would force us to send a process to $A$. Let $\mathcal{P}_{\text{red}}$ be the protocol obtained from $\mathcal{P}$ by changing to write(a) the label of the transition from $C$ to $A$ (in red in Figure 1). ($\mathcal{P}_{\text{red}}, q_f$) is a positive instance of TARGET:
$$ \langle q_0^2, d_0 \rangle \xrightarrow{(q_0, \text{read}(d_0), B)} \langle q_0 \oplus B, d_0 \rangle \xrightarrow{(B, \text{read}(d_0), C)} \langle q_0 \oplus C, d_0 \rangle \xrightarrow{(q_0, \text{write}(c), A)} \langle A \oplus C, c \rangle \xrightarrow{(C, \text{write}(a), A)} \langle A^2, a \rangle \xrightarrow{(A, \text{read}(a), q_f)} \langle A \oplus q_f, a \rangle \xrightarrow{(A, \text{read}(a), q_f)} \langle q_f^2, a \rangle. $$

Let $\phi := \neg(C \text{ populated}) \wedge ((\text{rg contains } a) \vee [(\text{rg contains } b) \wedge \neg(A \text{ populated})])$. $\phi$ is a presence constraint and ($\mathcal{P}, \phi$) is a negative instance of PRP. Indeed, if $a$ is in the register, then $C$ must be populated and if $b$ is in the register, then $A$ must be populated. ◀

## 2.3 Abstract Semantics

In this subsection, we define an abstraction of the semantics that is sound and complete with respect to PRP. The intuition of this abstraction is that the exact number of processes in a given state is not relevant. Indeed, register protocols, thanks to non-atomicity, enjoy a classical monotonicity property named copycat property.

**Lemma 6 (Copycat).** *Consider $\gamma_1, \gamma_2, q_2$ such that $\gamma_1 \xrightarrow{*} \gamma_2, q_2 \in \text{supp}(\gamma_2)$. There exists $q_1 \in \text{supp}(\gamma_1)$ s.t. $\langle \text{st}(\gamma_1) \oplus q_1, \text{data}(\gamma_1) \rangle \xrightarrow{*} \langle \text{st}(\gamma_2) \oplus q_2, \text{data}(\gamma_2) \rangle$.*

An *abstract configuration* is a pair $\sigma = (\text{st}(\sigma), \text{data}(\sigma)) \in 2^Q \times \mathbf{D}^{\text{Reg}}$ such that $\text{st}(\sigma) \neq \emptyset$. The set of *initial configurations* is $\text{Init}_a := \{\langle S, d_0^{\text{dim}} \rangle \mid S \subseteq Q_0\}$. Given a concrete configuration $\gamma$, the projection $\text{abst}(\gamma)$ is the abstract configuration $\langle \text{supp}(\gamma), \text{data}(\gamma) \rangle$. Let $\Sigma := 2^Q \times \mathbf{D}^{\text{Reg}}$ denote the set of abstract configurations. For $\sigma, \sigma' \in \Sigma$, $\sigma'$ is the *successor* of $\sigma$ when there exists $\delta = (q, a, q') \in \Delta$ such that $q \in \text{st}(\gamma)$, either $\text{st}(\gamma') = \text{st}(\gamma) \cup \{q'\}$ or $\text{st}(\gamma') = (\text{st}(\gamma) \setminus \{q\}) \cup \{q'\}$, and: if $a = \text{read}_\alpha(d)$ then $\text{data}(\gamma)(\text{rg}[\alpha]) = d$ and $\text{data}(\sigma) = \text{data}(\sigma')$, and if $a = \text{write}_\alpha(d)$ then $\text{data}(\sigma')(\text{rg}[\alpha]) = d$ and for all $\alpha' \neq \alpha$, $\text{data}(\sigma')(\text{rg}[\alpha']) = \text{data}(\sigma)(\text{rg}[\alpha'])$. Again, we denote such a step by $\sigma \xrightarrow{\delta} \sigma'$ or $\sigma \to \sigma'$. Note that one could equivalently define $\sigma \xrightarrow{\delta} \sigma'$ by: $\sigma \xrightarrow{\delta} \sigma' \iff \exists \gamma, \gamma' \in \Gamma, \gamma \xrightarrow{\delta} \gamma'$ and $\text{abst}(\gamma) = \sigma, \text{abst}(\gamma') = \sigma'$. This notion of abstraction is classical in parameterized verification of systems with identical anonymous agents that enjoy monotonicity properties. Note, however, that this semantics is non-deterministic: one could have $\sigma'' \neq \sigma'$ such that $\sigma \xrightarrow{\delta} \sigma'$ and $\sigma \xrightarrow{\delta} \sigma''$. This alternative corresponds to whether all processes in $q$ take the transition $(\text{st}(\gamma') = (\text{st}(\gamma) \setminus \{q\}) \cup \{q'\})$ or only some $(\text{st}(\gamma') = \text{st}(\gamma) \cup \{q'\})$. We define *abstract executions* similarly to concrete ones, and denote them using $\rho$. We also define the *reachability set* $\text{Reach}_a(A)$ and the notion of *coverability* as in the concrete case. This abstraction is sound and complete for PRP:

**Proposition 7 (Soundness and completeness of the abstraction).** For all $S \subseteq Q, \vec{d} \in \mathbf{D}^{\text{Reg}}$:
$(\exists \gamma \in \text{Reach}_c(\text{Init}_c) : \text{supp}(\gamma)=S, \text{data}(\gamma)=\vec{d}) \iff (\exists \sigma \in \text{Reach}_a(\text{Init}_a) : \text{st}(\sigma)=S, \text{data}(\sigma)=\vec{d})$.
XX:6 Checking PRPs on Parameterized Shared-Memory Systems

The intuition of the proof is the following: any concrete configuration can easily be lifted
into an abstract one. Conversely, any abstract execution may be simulated in the concrete
semantics for a sufficiently large number of processes by using the copycat property.

Given a presence constraint $\phi$ and $\sigma \in \Sigma$, we define whether $\sigma$ satisfies $\phi$, written $\sigma \models \phi$, in a natural way. Given a concrete configuration $\gamma$, one has $\gamma \models \phi$ if and only if $\text{abst}(\gamma) \models \phi$. Indeed, $\gamma \in \text{Reach}_c(\text{Init}_c)$ such that $\gamma \models \phi$ if and only if there exists $\sigma \in \text{Reach}_a(\text{Init}_a)$ such that $\sigma \models \phi$: one can consider PRP directly in the abstract semantics.

3 Complexity Results for Roundless Register Protocols

In this section, we provide complexity results for the presence reachability problems defined above in the general case and in some restricted cases. Throughout the rest of the section, all configurations and executions are implicitly abstract.

**3.1 NP-Completeness of the General Case**

First, all problems defined in the previous section are NP-complete.

► **Proposition 8.** *COVER, TARGET, DNF-PRP and PRP for roundless register protocols are all NP-complete.*

**Proof.** First, we prove that all four problems are in NP. It suffices to prove it for PRP, as the three other problems reduce to it.

Let $\rho : \sigma_0 \xrightarrow{\ast} \sigma$ an abstract execution, we simply prove the existence of $\rho' : \sigma_0 \xrightarrow{\ast} \sigma$ of length at most $4|Q|$. To obtain $\rho'$ from $\rho$, we iteratively:

- remove any read step that is non-deserting and does not cover a new location,

- remove any write step that is non-deserting, does not populate a new state and whose written symbol is never read,

- make non-deserting any deserting step whose source state is populated again later in $\rho$.

In $\rho'$, at most $|Q|$ steps populate a new state and at most $|Q|$ steps are deserting. This implies that there are at most $2|Q|$ read steps, therefore, at most $2|Q|$ write steps whose written value is actually read. In total, this bounds the number of steps by $4|Q|$. In particular, for PRP, we can look for an execution of length less than $4|Q|$ which can be guessed in polynomial time.

We now prove NP-hardness of COVER, as it reduces to the three other problems.

The proof is by a reduction from 3-SAT. Consider a 3-CNF formula $\phi = \bigwedge_{i=1}^m l_{i,1} \vee l_{i,2} \vee l_{i,3}$ over $n$ variables $x_1, \dots, x_n$ where, for all $i \in [1, m]$, for all $k \in [1, 3]$, $l_{i,k} \in \{x_j, \neg x_j \mid j \in [1, n]\}$. We define a roundless register protocol $\mathcal{P}_{\text{SAT}}(\phi)$ with a distinguished state $q_f$ which is coverable if and only if $\phi$ is satisfiable. In $\mathcal{P}_{\text{SAT}}(\phi)$, one has $\text{D} = \{\mathbf{d}_0, \mathbf{T}\}$ and $\text{dim} = 2n$, there are two registers for each variable $x_i$, $\text{rg}(x_i)$ and $\text{rg}(\neg x_i)$. The protocol is represented on Figure 2.

While any register may be set to $\mathbf{T}$ thanks to the loops on $q_0$, a register set to $\mathbf{T}$ can never be set back to $\mathbf{d}_0$. $l$ is considered true if $\text{rg}(l)$ is set to $\mathbf{T}$ while $\text{rg}(\neg l)$ still has value $\mathbf{d}_0$.

Suppose that the instance of 3-SAT is positive, i.e., $\phi$ is satisfiable by some assignment $\nu$. Consider an execution that writes $\mathbf{T}$ exactly to all $\text{rg}(l)$ with $l$ true in $\nu$. For each clause, one of the three literals is true in $\nu$. Therefore the execution may cover $C_i$? for all $i$ so it may cover $q_f$ and the instance of COVER is positive. Conversely, if the instance COVER is positive, there exists an execution $\rho : \sigma_0 \xrightarrow{\ast} \sigma$ with $\sigma_0 \in \text{Init}_a$ and $q_f \in \text{st}(\sigma)$. Consider $\nu$ that assigns to each variable $x$ value true if $\text{rg}(x)$ is written before $\text{rg}(\neg x)$ in $\rho$ and false
<figure><img src="image_6.png" /><figcaption>Figure 2 The protocol $\mathcal{P}_{\text{SAT}}(\phi)$ for NP-hardness of COVER.</figcaption></figure>

otherwise. Given a litteral $l$, $\rho$ may only go through $\text{Test}(l)$ if $\nu(l)$ is true; because $\rho$ covers $q_f$, this proves that $\nu \models \phi$.

► **Remark 9.** In [11], the authors prove NP-completeness of COVER in a similar model, but with a leader: in the NP-hardness reduction, the leader make non-deterministic decisions about the values of the variable. This argument does not hold in the leaderless case.

## 3.2 Interesting Restrictions

Although all the problems defined above are NP-complete, they are sometimes tractable under appropriate restrictions on the protocols. We will consider two restrictions on the protocols. The first one is having $\dim = 1$, i.e., a single register. The second restriction is the *uninitialized case* where processes are not allowed to read the initial value $d_0$ from the registers. Formally, a protocol $\mathcal{P}$ is *uninitialized* if its set of transitions $\Delta$ does not contain an action reading symbol $d_0$: in uninitialized protocols, it is structurally impossible to read from an unwritten register. One might object that forbidding transitions that read $d_0$ contradicts the intuition that, when a process reads from a register, it does not know whether the value is initial or not; one could settle the issue by considering that reading $d_0$ sends processes to a sink state. The uninitialized setting tends to yield better complexity than the general, initialized case, see for example [1, Section 7].

Of course, for PRP, the formula itself always makes the problem NP-hard.

► **Proposition 10.** *PRP for roundless register protocols is NP-hard even with $\dim = 1$ and the register uninitialized.*

## 3.3 Tractability of COVER and DNF-PRP under Restrictions

In this subsection, we prove that COVER is solvable in PTIME when the protocol is uninitialized or when $\dim$ is fixed and that DNF-PRP is solvable in PTIME when $\dim = 1$.

In [11, Theorem 9.2], uninitialized COVER is proved to be PTIME-complete; their approach, based on languages, is quite different from the one presented here. Our approach, similar to the one presented in [9, Algorithm 1] in the setting of reconfigurable broadcast networks, is to compute the set of coverable states using a simple *saturation* technique, a fixed-point computation over the set of states.

When registers are initialized, the saturation technique breaks down as it may be that some states are coverable but not in the same execution, as they require registers to lose their
XX:8 Checking PRPs on Parameterized Shared-Memory Systems

initial value in different orders (see the notion of first-write order developed in [6] for more
development on this in a round-based setting). However, in the initialized case with a fixed
number of registers, one can iterate over every such order and COVER is tractable as well.

► **Proposition 11.** *COVER for roundless register protocols is PTIME-complete either when the registers are uninitialized or when dim is fixed.*

For DNF-PRP, we provide a PTIME algorithm in the more restrictive case of dim = 1.

► **Proposition 12.** *DNF-PRP for roundless register protocols with dim = 1 is in PTIME.*

**Proof sketch.** We give here the proof for TARGET. See Appendix A.4 for the proof and pseudocode for DNF-PRP. Our algorithm shares similarities with [12, page 41] for broadcast protocols, although it is more complex because of the persistence of symbols in the register.

First, we have a polynomial reduction from initialized TARGET with dim = 1 to uninitialized TARGET with dim = 1. It proceeds as follows. Consider the graph G = (Q, E) when (q₁, q₂) ∈ E when there exists (q₁, read(d₀), q₂) ∈ Δ. Let I ⊆ Q the set of states that are reachable in G from Q₀. The reduction simply replaces Q₀ by I as set of initial states.

Any (abstract) execution $\rho : \sigma_0 \xrightarrow{*} \langle q_f, d_f \rangle$, called synchronizing execution, can be rearranged into $\rho_+ : \sigma_0 \xrightarrow{*} \langle S, d \rangle$ and $\rho_- : \langle S, d \rangle \xrightarrow{*} \langle q_f, d_f \rangle$ where S contains all states that appear in $\rho$. Additionally, we can make $\rho_-$ start with a write action (there is a transition in $\rho$ that writes d). To obtain the decomposition, $\rho_+$ mimics $\rho$ but does not empty any state, and $\rho_-$ mimics $\rho$ but from a configuration with more states. We compute the maximum such set S by iteratively deleting states that cannot appear in any synchronizing execution. Let

$$
\mathcal{C}(\mathcal{P}) := \max\{S \subseteq Q \mid \exists d \in D, \exists \sigma_0 \in \mathrm{Init}_a, \sigma_0 \xrightarrow{*} \langle S, d \rangle\}
$$

$$
\mathcal{B}\mathcal{C}(\mathcal{P}) := \max\{S \subseteq Q \mid \forall d \in D, \exists d_f \in D, \langle S, d \rangle \xrightarrow{*} \langle q_f, d_f \rangle\}
$$

Both maxima exist as the sets are non-empty ($Q_0$ is included in the first set and $q_f$ is in the second set) and they are stable by union (concatenate the corresponding executions). Intuitively, $\mathcal{C}(\mathcal{P})$ corresponds to the set of coverable sets, and $\mathcal{BC}(\mathcal{P})$ to the set of backward coverable states. In the decomposition $\rho_+$: $\sigma_0 \xrightarrow{*} \langle S, d \rangle$, $\rho_-: \langle S, d \rangle \xrightarrow{*} \langle q_f, d_f \rangle$, $\rho_+$ is a witness that $S \subseteq \mathcal{C}(\mathcal{P})$ and $\rho_-$ that $S \subseteq \mathcal{BC}(\mathcal{P})$ (because $\rho_-$ starts with a write action, for every $d' \in D$ one has $\langle S, d' \rangle \xrightarrow{*} \langle q_f, d_f \rangle$).

$\mathcal{C}(\mathcal{P})$ and $\mathcal{BC}(\mathcal{P})$ can be computed in polynomial time. For $\mathcal{C}(\mathcal{P})$, we use a saturation technique. For $\mathcal{BC}(\mathcal{P})$, we work backwards: a symbol is read before it is written. We start with $S := \{q_f\}$. Until a fixpoint for $S$ is reached, we do the following. We iterate on $D$, trying to pick the symbol that was in the register before $S$ could be reached. For each $d \in D$, we saturate $S$ with backward transitions reading $d$, then check if $d$ can be written by a transition ending in $S$. If not, we backtrack by removing states that were just added.

The algorithm iteratively removes from $\mathcal{P}$ states that are not in $\mathcal{C}(\mathcal{P}) \cap \mathcal{BC}(\mathcal{P})$. Indeed, states that are not in $\mathcal{C}(\mathcal{P}) \cap \mathcal{BC}(\mathcal{P})$ cannot appear in any synchronizing execution. If it ends up with $Q(\mathcal{P}) = \emptyset$, then there is no synchronizing execution and the algorithm rejects. If it ends up with $\mathcal{C}(\mathcal{P}) = \mathcal{BC}(\mathcal{P}) = Q(\mathcal{P}) \neq \emptyset$, then applying the definitions of $\mathcal{C}(\mathcal{P})$ and $\mathcal{BC}(\mathcal{P})$ gives a synchronizing execution, and the algorithm accepts. ◀

It is unknown whether the previous result still holds when dim is fixed to a value greater
than 1. The case dim = 1 is particularly easy because writing to the register completely
erases its content.

Unlike COVER, TARGET and therefore DNF-PRP are not tractable under the uninitialized hypothesis. For TARGET, one cannot add fresh processes at no cost, since the
fresh processes would eventually have to get to $q_f$. For example, if a register $r$ can only be written from a given state $q$, the last process to leave $q$ will fix the value in register $r$.

**► Proposition 13.** *TARGET for uninitialized roundless register protocols is NP-hard.*

<table><caption>Figure 3 Summary of complexity results for roundless register protocols</caption><thead><tr><th></th><th>COVER</th><th>TARGET</th><th>DNF-PRP</th><th>PRP</th></tr></thead><tbody><tr><th>General case</th><td>NP-complete<br>(Prop. 8)</td><td>NP-complete<br>(Prop. 8)</td><td>NP-complete<br>(Prop. 8)</td><td>NP-complete<br>(Prop. 8)</td></tr><tr><th>Uninitialized</th><td>PTIME-complete<br>(Prop. 11)</td><td>NP-complete<br>(Prop. 8 & 13)</td><td>NP-complete<br>(Prop. 8 & 13)</td><td>NP-complete<br>(Prop. 8 & 10)</td></tr><tr><th>dim = 1 (one register)</th><td>PTIME-complete<br>(Prop. 11)</td><td>PTIME-complete<br>(Prop. 12 & 11)</td><td>PTIME-complete<br>(Prop. 12 & 11)</td><td>NP-complete<br>(Prop. 8 & 10)</td></tr></tbody></table>

# 4 Round-based Register Protocols

We now extend the previous model to a round-based setting. The model and semantics are the same as in [6], however we consider a more general problem than COVER. Thus, the abstract semantics developed here differs from [6].

## 4.1 Definitions

In round-based settings, there is a fresh set of dim registers at each round, and each process has its own private round value that starts at 0 and never decreases. Processes may only read from and write to registers of nearby rounds.

**► Definition 14 (Round-based register protocols).** A round-based register protocol is a tuple $\mathcal{P} = (Q, Q_0, \dim, D, d_0, v, \Delta)$ where

- $Q$ is a finite set of states with a distinguished subset of initial states $Q_0 \subseteq Q$;

- $\dim \in \mathbb{N}$ is the number of shared registers per round;

- $D$ is a finite data alphabet with an initial symbol $d_0$;

- $v$ is the visibility range;

- $\Delta \subseteq Q \times \mathcal{A} \times Q$ is the set of transitions, where $\mathcal{A} = \{\text{read}_\alpha^{-i}(d) \mid i \in [0, v], \alpha \in [1, \dim], d \in D\} \cup \{\text{write}_\alpha(d) \mid \alpha \in [1, \dim], d \in D \setminus \{d_0\}\} \cup \{\text{Inc}\}$ is the set of actions.

Read actions specify the round of the register: $\text{read}_\alpha^{-i}(d)$ means, for a process at round $k$, “read $d$ from register $\alpha$ of round $k-i$”. A process at round $k$ may only write to the registers of round $k$. The Inc action increments the round of a process.

Let $rg_k[\alpha]$ denote the register $\alpha$ of round $k$. The set of registers of round $k$ is written $\text{Reg}_k$, and we let $\text{Reg} = \bigcup_{k \in \mathbb{N}} \text{Reg}_k$. The size of a protocol is $|\mathcal{P}| = |Q| + |D| + |\Delta| + v + \dim$. A given process is described by its state and round, formalized by a pair $(q, k) \in Q \times \mathbb{N}$ called location. Let $\text{Loc} := Q \times \mathbb{N}$ denote the set of locations. A concrete configuration describes the number of processes in each location along with the value of each register. Formally, a concrete configuration is a pair $\langle \mu, \vec{d} \rangle$ with $\mu \in \mathbb{N}^{\text{Loc}}$ such that $0 < \sum_{(q,k) \in \text{Loc}} \mu(q, k) < \infty$ and $\vec{d} \in \mathbb{D}^{\text{Reg}}$. For $\gamma = \langle \mu, \vec{d} \rangle$, we write $\text{loc}(\gamma) := \mu$ and $\text{data}(\gamma) := \vec{d}$. Again, we write $\Gamma$ for the set of concrete configurations. The set of initial configurations is $\text{Init}_c := \{\gamma \in \Gamma \mid \text{data}(\gamma) = d_0^{\text{Reg}} \text{ and } \forall (q, k) \notin Q_0 \times \{0\}, \text{loc}(\gamma)(q, k) = 0\}$.
<figure><img src="image_7.png" /><figcaption>Figure 4 An example of round-based register protocol</figcaption></figure>

A *move* is a pair $\theta \in \Delta \times \mathbb{N}$: move $(\delta, k)$ expresses that transition $\delta$ is taken by a process at round $k$; we write $\text{Moves} := \Delta \times \mathbb{N}$ for the set of all moves. A move $\theta$ has *effect* on round $k$ when $\theta$ is at round $k$ or $\theta$ is an increment at round $k-1$. We define a step as follows: for $\theta = ((q, a, q'), k) \in \text{Moves}$, $\gamma \xrightarrow{\theta} \gamma'$ when $(q, k) \in \text{loc}(\gamma)$ and:

- if $a = \text{read}_\alpha^{-i}(d)$, $\text{loc}(\gamma') = (\text{loc}(\gamma) \ominus \{(q, k)\}) \oplus \{(q', k)\}$, $\text{data}(\gamma)(\text{rg}_{k-i}[\alpha]) = d$ and $\text{data}(\gamma') = \text{data}(\gamma)$;

- if $a = \text{write}_\alpha(d)$, $\text{loc}(\gamma') = (\text{loc}(\gamma) \ominus \{(q, k)\}) \oplus \{(q', k)\}$, $\text{data}(\gamma')(\text{rg}_k[\alpha]) = d$ and for all $r \neq \text{rg}_k[\alpha]$, $\text{data}(\gamma')(r) = \text{data}(\gamma)(r)$;

- if $a = \text{Inc}$, $\text{loc}(\gamma') = (\text{loc}(\gamma) \ominus \{(q, k)\}) \oplus \{(q', k+1)\}$ and $\text{data}(\gamma') = \text{data}(\gamma)$.

A step is at round $k$ when the corresponding move is of the form $(\delta, k)$. Note that action $\text{read}_\alpha^{-i}(d)$ is only possible for processes at rounds $k \ge i$. The notions of execution, of reachability and of coverability are defined as in the roundless case.

**Example 15.** Consider the round-based protocol $\mathcal{P}$ from Figure 4, with $\dim = 1$, $v = 1$, $Q_0 = \{q_0\}$ and $D = \{d_0, a, b\}$. In this protocol, state $q_f$ cannot be covered. By contradiction, consider an execution $\pi: \gamma_0 \xrightarrow{\delta} \gamma$ with $\gamma_0 \in \text{Init}_c$ and $\text{loc}(\gamma)(q_f, k) > 0$ for some $k \in \mathbb{N}$. We have that, at some point in $\pi$, $(E, k)$ is populated and $b$ is in $\text{rg}[k]$. Therefore, some process went from $(A, k)$ to $(B, k)$, which implies that $\text{rg}[k]$ lost value $d_0$ before $\text{rg}[k-1]$; this in turn implies that $\pi$ does not send any process to $(E, k)$ which is a contradiction. $\quad$

Since round-based register protocols enjoy the same monotonicity properties as roundless register protocols, we define the same non-counting abstraction. Note that this abstraction differs from the one in [6] which was designed specifically for COVER. The set of abstract configurations is $\Sigma := 2^{\text{Loc}} \times D^{\text{Reg}}$; the abstract semantics are defined as in Subsection 2.3. Again, $\sigma \xrightarrow{\delta} \sigma$ if and only if there exist $\gamma, \gamma' \in \Gamma$, $\gamma \xrightarrow{\delta} \gamma'$ and $\text{abst}(\gamma) = \sigma$, $\text{abst}(\gamma') = \sigma'$. All the properties of Subsection 2.3 apply to round-based abstract semantics. In particular, we have the soundness and completeness of the abstraction:

**Proposition 16 (Soundness and completeness of the abstraction).** For all $L \subseteq \text{Loc}$, $\vec{d} \in D^{\text{Reg}}$:
$(\exists \gamma \in \text{Reach}_c(\text{Init}_c) : \text{supp}(\gamma)=L, \text{data}(\gamma)=\vec{d}) \iff (\exists \sigma \in \text{Reach}_a(\text{Init}_a) : \text{loc}(\sigma)=L, \text{data}(\sigma)=\vec{d})$.

## 4.2 Presence Reachability Problem

COVER is extended to round-based protocols by asking whether some reachable configuration has a process on $q_f$ on some round $k$, and TARGET by asking whether some reachable configuration has no process on states $q \neq q_f$ on any round $k$. Formally, one asks whether there exists $\gamma \in \text{Reach}_c(\text{Init}_c)$ such that $\gamma \models \psi$ where $\psi = \exists k \in \mathbb{N}, (q, k) \in \text{loc}(\gamma)$" for COVER and $\psi = \forall k \in \mathbb{N}, \forall q \neq q_f, (q, k) \notin \text{loc}(\gamma)$" for TARGET. We will now extend roundless PRP to round-based PRP, where the formula is allowed to have non-nested quantification over rounds.
Presence constraints are first-order formulas (quantifying over the rounds) without any nested quantifiers. See Appendix B.1 for the full definition.

**► Example 17.** "$(\exists k (q_2, k) \text{ populated}) \lor (\forall k ((q_0, k+2) \text{ populated}) \land \mathrm{rg}_1[1] \text{ contains a})$" is an example of presence constraint.

Let $\gamma := ((q_0, 0) \oplus (q_1, 1), d_0^{\mathrm{Reg}})$ with $q_0 \neq q_1$, $\dim = 1$. One has $\gamma \models (\mathrm{rg}_0[1] \text{ contains } d_0) \land (\exists k (q_1, k+1) \text{ populated})$ but $\gamma \not\models \forall k (((q_0, k) \text{ populated}) \lor \neg((q_1, k) \text{ populated}))$. ◀

We define the *round-based presence reachability problem* (round-based PRP):

**ROUND-BASED PRP**

**Input:** A round-based register protocol $\mathcal{P}$, a presence constraint $\psi$

**Question:** Does there exist $\gamma \in \mathrm{Reach}_c(\mathrm{Init}_c)$ such that $\gamma \models \psi$?

**► Example 18.** Consider $\mathcal{P}$ from Example 15. If $\psi := \exists k, (q_f, k) \text{ populated}$, then $(\mathcal{P}, \psi)$ is a negative instance of round-based PRP. If $\psi' := \exists k, ((E, k) \text{ populated}) \land ((E, k+1) \text{ populated})$, then $(\mathcal{P}, \psi')$ is also negative. However, if $\psi'' := ((E, 2) \text{ populated}) \land [\forall k, (\mathrm{rg}[k+1] \text{ contains b}) \lor (\mathrm{rg}[k+1] \text{ contains } d_0)]$, then $(\mathcal{P}, \psi'')$ is positive: a witness execution sends a process to $(B, 1)$, writes $a$ to $\mathrm{rg}[0]$ then $b$ to $\mathrm{rg}[1]$ and finally sends a process from $(q_0, 2)$ to $(E, 2)$. ◀

COVER and TARGET for round-based register protocols are special cases of PRP.
The following lower bound hence applies to all these problems:

**► Proposition 19 ([6, Theorem 23]).** *COVER for round-based register protocols is PSPACE-hard, even in the uninitialized case with $v = 0$ and $\dim = 1$.*

Note that, in the round-based setting, $\dim = 1$ means one register *per round*, therefore still an unbounded number of registers. $v = 0$ means that a process can only interact with registers of its current round. The previous proposition implies that all problems considered in Figure 3 are PSPACE-hard when working with round-based protocols. In [6], COVER for round-based register protocols is shown to be PSPACE-complete. In the rest of this paper, we establish that the more general round-based PRP lies in the same complexity class:

**► Theorem 20.** *Round-based PRP is PSPACE-complete.*

# 5 A Polynomial-Space Algorithm for Round-Based PRP

In this section, we provide a polynomial-space algorithm for round-based PRP. Thanks to Savitch's theorem, it suffices to find a non-deterministic polynomial-space algorithm. To do so, one wants to guess an execution that reaches a configuration satisfying the presence constraint. However, as shown in [6, Proposition 13], one may need, at a given point along such an execution, the number of active rounds to be exponential (an active round being informally a round on which something has already happened and something else is yet to happen). Thus, storing the execution step by step in polynomial space seems hard; instead, our algorithm will guess the execution round by round. To do this, we define the notion of footprint, which represents the projection of an execution onto a narrow window of rounds.

Thanks to Proposition 7, round-based PRP can be studied directly in the abstraction.
In the rest of the paper, all configurations and executions are implicitly abstract.
## 5.1 Footprints

Let $j \le k$. We write $\text{Loc}[j, k]$ for the set of locations at rounds $\max(j, 0)$ to $k$; similarly, we write $\text{Reg}[j, k]$ for the set of registers of rounds $\max(j, 0)$ to $k$. A local configuration on (rounds) $[j, k]$ is an element of $2^{\text{Loc}[j,k]} \times \text{D}^{\text{Reg}[j,k]}$. The set of local configurations on $[j, k]$ is written $\Sigma[j, k]$. Given $\sigma \in \Sigma$, the local configuration $\text{local}[j, k](\sigma)$ is obtained by removing from $\sigma$ all information that is not about rounds $j$ to $k$. Note that local configurations are local with respect to the rounds, and not with respect to processes.

Given $\lambda, \lambda' \in \Sigma[j, k]$ and a move $\theta$, we write $\lambda \xrightarrow{\theta} \lambda'$ when there exist two configurations $\sigma$ and $\sigma'$ such that $\sigma \xrightarrow{\theta} \sigma'$, $\text{local}[j, k](\sigma) = \lambda$ and $\text{local}[j, k](\sigma') = \lambda'$. In practice:

- if $\theta$ is a move with no effect on rounds $j$ to $k$, then $\lambda \xrightarrow{\theta} \lambda'$ if $\lambda = \lambda'$;

- if $\theta = ((q, \text{lnc}, q'), j-1)$ then $\lambda \xrightarrow{\theta} \lambda'$ holds with no condition that $(q, j-1)$ is populated in $\lambda$, since $j-1$ is outside of $[j, k]$;

- if $\theta = ((q, \text{read}_\alpha^{-b}(d)), l)$ with $l-b < j$ (read from register of round $< j$), there is no condition on the content of the register.

A footprint on (rounds) $[j, k]$ corresponds to the projection of an execution on rounds $[j, k]$. Formally, it is an alternating sequence $\lambda_0, \theta_0, \lambda_1, \dots, \theta_{m-1}, \lambda_m$ where for all $i \in [0, m]$, $\lambda_i \in \Sigma[j, k]$ and for all $i \le m-1$, $\lambda_i \xrightarrow{\theta_i} \lambda_{i+1}$ and $\lambda_i \ne \lambda_{i+1}$.

Let $\rho = \sigma_0, \theta_0, \sigma_1, \dots, \theta_{m-1}, \sigma_m$ be an execution. The footprint of $\rho$ on (rounds) $[j, k]$, written $\text{footprint}[j, k](\rho)$, is the footprint on $[j, k]$ obtained from $\rho$ by replacing $\sigma_i$ by $\lambda_i = \text{local}[j, k](\sigma_i)$ and then removing all useless steps $\lambda_i \xrightarrow{\theta} \lambda_{i+1}$ with $\lambda_i = \lambda_{i+1}$ (by merging $\lambda_i$ and $\lambda_{i+1}$, so $\text{footprint}[j, k](\rho)$ can be shorter than $\rho$). Similarly, for $[j', k'] \supseteq [j, k]$ and $\tau$ a footprint on $[j', k']$, define the projection footprint $[j, k](\tau)$ by the footprint obtained by replacing each local configuration in $\tau$ by its projection on $[j, k]$ and removing useless steps.

The following result provides a sufficient condition for a sequence of footprints to be seen as projections of a single common execution.

**Lemma 21.** Let $K \in \mathbb{N}$, $(\tau_k)_{k \le K}$ and $(T_k)_{k \le K-1}$ such that:

- for all $k \le K$, $\tau_k$ is a footprint on $[k-\mathbf{v}+1, k]$,

- for all $k \le K-1$, $T_k$ is a footprint on $[k-\mathbf{v}+1, k+1]$,

- for all $k \le K-1$, $\text{footprint}[k-\mathbf{v}+1, k](T_k) = \tau_k$,

- for all $k \le K-1$, $\text{footprint}[k-\mathbf{v}+2, k+1](T_k) = \tau_{k+1}$.

There exists an execution $\rho$ such that, for all $k \le K$, $\text{footprint}[k-\mathbf{v}+1, k](\rho) = \tau_k$.

## 5.2 A Polynomial-Space Algorithm for Round-Based PRP

The algorithms guesses the witness execution footprint by footprint, and stops when the presence constraint is satisfied. Algorithm 1 provides the skeleton of this procedure. For the sake of simplicity, we suppose that $\mathbf{v} \ge 1$. If $\mathbf{v} = 0$, we artificially increase $\mathbf{v}$ to 1.

For all $k \in \mathbb{N}$, let $\tau_k$ be the value of $\tau$ at the end of iteration $k$ and $T_k$ the value of $T$ guessed at iteration $k+1$. Thanks to Lemma 21, if the algorithm reaches the end of iteration $K$ then there exists an execution $\rho$ whose projection on $[k-\mathbf{v}, k-1]$ is $\tau_k$ for every $k \le K$.

Handling the round-based presence constraint is technical, so we hide it in functions `NDInit`, `NDComputeIteration` and `TestPresenceConstraint` and postpone the details to Appendix B.3. We guess why $\psi$ is true by guessing satisfied *atomic propositions* of three types: existentially quantified on the round (i.e., of the form "$\exists k \phi$" where $\phi$ has no quantifiers and only $k$ as free variable) which we put in $E$; universally quantified on the round (i.e., of
1 **Input:** A PRP instance $(\mathcal{P}, \psi)$
2 $E, U, C \leftarrow \emptyset$;
3 $\tau \leftarrow \epsilon$; // dummy footprint on rounds $[-v, -1]$
4 Guess the initial set $I \subseteq Q_0$ of populated states at round 0;
5 $NDInit(E, U, C)$;
6 **for** $k$ **from** 0 **to** $+\infty$ **do**
7 &nbsp;&nbsp;&nbsp;&nbsp;Guess $T$ a footprint on $[k-v, k]$ such that footprint$[k-v, k-1](T) = \tau$;
8 &nbsp;&nbsp;&nbsp;&nbsp;Check that $T$ is consistent with the initial configuration;
9 &nbsp;&nbsp;&nbsp;&nbsp;$\lambda \leftarrow$ last configuration in $T$;
10 $NDComputeIteration(E, U, C, \lambda)$;
11 **if** TestPresenceConstraint$(E, U, C, \lambda)$ **then** Accept;
12 $\tau \leftarrow$ footprint$[k-v+1, k](T)$;
7 **do**
8 &nbsp;&nbsp;&nbsp;&nbsp;Guess $T$ a footprint on $[k-v, k]$ such that footprint$[k-v, k-1](T) = \tau$;
9 &nbsp;&nbsp;&nbsp;&nbsp;Check that $T$ is consistent with the initial configuration;
10 $\lambda \leftarrow$ last configuration in $T$;
11 $NDComputeIteration(E, U, C, \lambda)$;
12 $\tau \leftarrow$ footprint$[k-v+1, k](T)$;
**end for**
**return** $\lambda$

the form “$\forall k \phi$” where $\phi$ has no quantifiers and only $k$ as free variable) which we put in $U$; with no quantifier (i.e., of the form “$\phi$” where $\phi$ has no quantifiers and no free variables) which we put in $C$. Formulas in $C$ refer to constant rounds and are checked at these rounds only. Formulas in $U$ are checked at every round. For formulas in $E$, the algorithm guesses at which round the formula is true. Our algorithm is correct with respect to round-based PRP:

**Proposition 22.** $(\mathcal{P}, \psi)$ is a positive instance of round-based PRP if and only if there exists an accepting computation of Algorithm 1 on $(\mathcal{P}, \psi)$.

The integer constants in the presence constraint $\psi$ are encoded in unary, like the visibility range $v$. These two hypotheses are reasonable since practical examples typically use constants of small value (e.g., 1). Under these hypotheses, we obtain a polynomial spatial bound on the size of footprints of a well-chosen witness execution, which in turn gives a polynomial spatial bound for the algorithm:

**Proposition 23.** *Algorithm 1 works in space* $O(|\psi|^3 + |Q|^2 (v+1)^2 \log(\dim |D|))$.

Finally, we need to discuss the termination of the algorithm. According to the pigeonhole principle, after an exponential number of iterations, the elements stored in memory repeat from a previous iteration and we can stop the computation. One can thus use a counter, encoded in polynomial space, to count iterations and return a decision when the counter reaches its largest value. Thanks to the space bounds from Proposition 23, correctness from Proposition 22 and the stopping criterion, our algorithm decides round-based PRP in non-deterministic polynomial space, proving Theorem 20.

Acknowledgements

Many thanks to Nathalie Bertrand, Nicolas Markey and Ocan Sankur for their invaluable advice.

References

1 Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. Parameterized verification under TSO is PSPACE-complete. *Proc. ACM Program. Lang.*, 4(POPL):26:1–26:29, 2020. doi:10.1145/3371094.

2 James Aspnes. Fast deterministic consensus in a noisy environment. *Journal of Algorithms*, 45(1):16–39, 2002. doi:10.1016/S0196-6774(02)00220-1.
XX:14 Checking PRPs on Parameterized Shared-Memory Systems

3 A. R. Balasubramanian, Lucie Guillou, and Chana Weil-Kennedy. Erratum to parameterized analysis of reconfigurable broadcast networks, 2022. https://www.model.in.tum.de/~weilkenn/erratum-fossacs22.pdf.

4 A. R. Balasubramanian, Lucie Guillou, and Chana Weil-Kennedy. Parameterized analysis of reconfigurable broadcast networks (long version). 2022. https://arxiv.org/abs/2201.10432.

5 A. R. Balasubramanian and Chana Weil-Kennedy. Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In *GandALF 2021*, volume 346, pages 18–34, 2021. doi:10.4204/EPTCS.346.2.

6 Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized safety verification of round-based shared-memory systems. In *ICALP 2022*, pages 113:1–113:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.ICALP.2022.113.

7 Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. *Decidability of Parameterized Verification*. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. doi:10.2200/S00658ED1V01Y201508DCT013.

8 Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in networks of register protocols under stochastic schedulers. In *ICALP 2016*, volume 55 of *LIPIcs*, pages 106:1–106:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.ICALP.2016.106.

9 Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the complexity of parameterized reachability in reconfigurable broadcast networks. In *FSTTCS 2012*, volume 18 of *LIPIcs*, pages 289–300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPIcs.FSTTCS.2012.289.

10 Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In *STACS 2014*, volume 25 of *LIPIcs*, pages 1–10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. doi:10.4230/LIPIcs.STACS.2014.1.

11 Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. *Journal of the ACM*, 63(1):10:1–10:48, 2016. doi:10.1145/2842603.

12 Paulin Fournier. *Parameterized verification of networks of many identical processes*. PhD thesis, University of Rennes 1, France, 2015. https://tel.archives-ouvertes.fr/tel-01355847.

13 Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. *Journal of the ACM*, 39(3):675–735, 1992. doi:10.1145/146637.146681.

14 Matthew Hague. Parameterised pushdown systems with non-atomic writes. In *FSTTCS 2011*, volume 13 of *LIPIcs*, pages 457–468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.FSTTCS.2011.457.

15 Richard E. Ladner. The circuit value problem is log space complete for P. *SIGACT News*, 7(1):18–20, 1975. doi:10.1145/990518.990519.

16 Michel Raynal and Julien Stainer. A simple asynchronous shared memory consensus algorithm based on omega and closing sets. In *CISIS 2012*, pages 357–364. IEEE Computer Society, 2012. doi:10.1109/CISIS.2012.198.
# Technical appendix

## A Roundless Register Protocols

Recall that the abstract semantics is non-deterministic due to the choice between $st(\gamma') = (st(\gamma) \setminus \{q\}) \cup \{q'\}$ and $st(\gamma') = st(\gamma) \cup \{q'\}$. The first case is called *deserting*, and the latter *non-deserting*. A deserting step corresponds in the concrete semantics to all processes in $q$ taking the transition at once.

Moreover, given a transition $(q, a, q')$, state $q$ is called the *source* and state $q'$ is called the *destination* of the transition, and similarly for a step.

### A.1 Proof of Proposition 6

**Lemma 6 (Copycat).** Consider $\gamma_1, \gamma_2, q_2$ such that $\gamma_1 \xrightarrow{*} \gamma_2, q_2 \in \text{supp}(\gamma_2)$. There exists $q_1 \in \text{supp}(\gamma_1)$ s.t. $\langle \text{st}(\gamma_1) \oplus q_1, \text{data}(\gamma_1) \rangle \xrightarrow{*} \langle \text{st}(\gamma_2) \oplus q_2, \text{data}(\gamma_2) \rangle$.

**Proof.** We prove the result by induction on the length of the execution. If the execution is of length 0 then one simply considers $q_1 := q_2$. Let $\pi : \gamma_1 \xrightarrow{*} \gamma_2$ and suppose that the property is true for all executions of length $|\pi| - 1$. Decompose $\pi$ into $\gamma_1 \xrightarrow{\delta} \gamma_3 \xrightarrow{*} \gamma_2$. If $q_2$ is not the destination of $\delta$, then $q_2 \in \text{supp}(\gamma_3)$ and we directly apply the induction hypothesis on $\gamma_1 \xrightarrow{*} \gamma_3$ and $q_2$ then conclude by taking $\delta$ to get to $\langle \text{st}(\gamma_2) \oplus q_2, \text{data}(\gamma_2) \rangle$. Assume that $q_2$ is the destination of $\delta$; let $q_3$ the source of $\delta$. We have $q_3 \in \text{supp}(\gamma_3)$, so we apply the induction hypothesis on $\gamma_1 \xrightarrow{*} \gamma_3$ and $q_3$: we obtain that there exists $q_1 \in \text{supp}(\gamma_1)$ such that $\langle \text{st}(\gamma_1) \oplus q_1, \text{data}(\gamma_3) \rangle \xrightarrow{*} \langle \text{st}(\gamma_3) \oplus q_3, \text{data}(\gamma_2) \rangle$. Moreover, we have $\langle \text{st}(\gamma_3) \oplus q_3, \text{data}(\gamma_2) \rangle \xrightarrow{\delta} \langle \text{st}(\gamma_2) \oplus q_3, \text{data}(\gamma_2) \rangle \xrightarrow{\delta} \langle \text{st}(\gamma_2) \oplus q_2, \text{data}(\gamma_2) \rangle$. Indeed, if $\delta$ is a read transition then the symbol is still in the register in $\gamma_2$ and may be read again, and if $\delta$ is write transition, then writing again a symbol to a register does not change its content. ◀

### A.2 Proof of Proposition 7

**Proposition 7 (Soundness and completeness of the abstraction).** For all $S \subseteq Q, \vec{d} \in D^{\text{Reg}}$:
$(\exists \gamma \in \text{Reach}_c(\text{Init}_c) : \text{supp}(\gamma)=S, \text{data}(\gamma)=\vec{d}) \iff (\exists \sigma \in \text{Reach}_a(\text{Init}_a) : \text{st}(\sigma)=S, \text{data}(\sigma)=\vec{d})$.

First, the following lemma states that any concrete execution can easily be transformed into an abstract one.

**Lemma A.1.** Let $\gamma, \gamma' \in \Gamma$ and $\pi : \gamma \xrightarrow{*} \gamma'$. There exists $\rho : \text{abst}(\gamma) \xrightarrow{*} \text{abst}(\gamma')$.

**Proof.** By induction, it suffices to prove it for one step; suppose that $\gamma \xrightarrow{\delta} \gamma'$. Let $(q, a, q') := \delta$; if $q \in \text{st}(\gamma')$, then we consider the non-deserting abstract step with transition $\delta$, otherwise we consider the deserting step with transition $\delta$. Either way, we have $\text{abst}(\gamma) \xrightarrow{\delta} \text{abst}(\gamma')$. ◀

Conversely, from an abstract execution, for a large enough number of processes, using the copycat property one can build a concrete execution with the same final states and data.

**Lemma A.2.** Let $\sigma, \sigma' \in \Sigma$ and $\rho : \sigma \xrightarrow{*} \sigma'$. There exist $\gamma, \gamma'$ such that $\text{abst}(\gamma) = \sigma, \text{abst}(\gamma') = \sigma'$ and $\pi : \gamma \xrightarrow{*} \gamma'$.

**Proof.** The proof is by induction on the number of steps in $\pi$. If $\pi$ has 0 steps, then $\sigma = \sigma'$ and suffices to consider $\gamma = \gamma' := \langle \bigoplus_{q \in \text{st}(\sigma)} q, \text{data}(\sigma) \rangle$.
Assume that $\rho : \sigma_1 \stackrel{*}{\rightarrow} \sigma_2 \stackrel{\delta}{\rightarrow} \sigma_3$ and that the property is true for executions shorter than $\rho$. By induction hypothesis, there exists $\pi : \gamma_1 \stackrel{*}{\rightarrow} \gamma_2$ such that $\text{abst}(\gamma_1) = \sigma_1$, $\text{abst}(\gamma_2) = \sigma_2$. There exists $\gamma_3$ such that $\gamma_2 \stackrel{\delta}{\rightarrow} \gamma_3$; however, it could be that $\gamma_3$ does not have a process on the source state of $\delta$ while $\sigma_3$ does. In that case, we modify $\pi$ to put an additional process on the source state of $\delta$ by using the copycat property and increasing the number of processes by one.

◀

Lemmas A.1 and A.2 together prove Proposition 7.

## A.3 Proof of Proposition 11

**Proposition 11.** *COVER for roundless register protocols is PTIME-complete either when the registers are uninitialized or when dim is fixed.*

### A.3.1 PTIME when the Registers are uninitialized

The algorithm computes the set of coverable states using a fixpoint technique called saturation. The algorithm starts with $S := \{Q_0\}$, then iteratively adds to $S$ all states $q_2$ for which there exist $q_1 \in S$ and an action $a \in A$ such that $(q_1, a, q_2) \in \Delta$ and:

- either $a = \text{write}_\alpha(\text{d})$ with $d \in D$,

- or $a = \text{read}_\alpha(\text{d})$ with $\alpha, d$ s.t. there exist $q_3, q_4 \in S$, $(q_3, \text{write}_\alpha(\text{d}), q_4) \in \Delta$.

We prove that, when a fixpoint is reached, $S$ is exactly the set of coverable states. First, any coverable state is added to $S$ by the algorithm, by induction in the number of steps of the execution. Conversely, we show by induction in the number of iterations of the algorithm that any state added to $S$ is coverable. For the first case, if $(q_1, \text{write}_\alpha(\text{d}), q_2) \in \Delta$ and $q_1$ is coverable then clearly $q_2$ is coverable. For the second case, suppose that we have an execution $\rho$ covering $S \subseteq Q$, and that there exist $q_2 \in Q, q_1, q_3, q_4 \in S, d \in D \setminus \{d_0\}, \alpha \in [1, \text{dim}]$ such that $(q_1, \text{read}_\alpha(\text{d}), q_2), (q_3, \text{write}_\alpha(\text{d}), q_4) \in \Delta$. Because we have an unlimited supply of processes, we use the copycat property to put an extra process on $q_3$ then make that process write $d$ to $\text{rg}[\alpha]$ again, so that a process in state $q_1$ may read $d$ from register $\text{rg}[\alpha]$ and get to $q_2$, which is therefore coverable.

### A.3.2 PTIME when the Number of Registers dim is Fixed

The first write to a register is an irreversible action, as $d_0$ cannot be written again. For that reason, we cannot work with a single saturation phase like in the uninitialized case. We iterate over all possible orders in which registers are first written to (see first-write orders in [6, Definition 15]).

For a given such order $r_1, \dots, r_m$ ($m \le \text{dim}$), we proceed using $m+1$ successive saturation phases, numbered from $i=0$ to $m$. The algorithm starts with $S = \{Q_0\}$. During saturation phase $i$, the algorithm saturates $S$ by iteratively adding all states $q_2$ such that:

- there exists $q_1 \in S$ with $(q_1, \text{read}_r(d_0), q_2)$ and $r \notin \{r_1, \dots, r_i\}$,

- there exists $q_1 \in S$ with $(q_1, \text{write}_{r_j}(d), q_2)$, $j \le i$,

- there exists $q_1 \in S$ with $(q_1, \text{read}_{r_j}(d), q_2)$, $j \le i$, and $d$ may be written to $r_j$ using a transition whose source is in $S$.

First, if there exists an execution covering $q_f$, then it writes to registers for the first time in some order $r_1, \dots, r_m$. When the algorithm considers this first-write order, the set of states
computed includes $q_f$. Conversely, suppose that the algorithm finds that $q_f$ is covered for some first-write order $r_1, \dots, r_m$. Observe that, if two executions share a first-write order $r_1, \dots, r_m$ then they may be merged into a common execution [6, Lemma 17]. Therefore, all the states computed by the algorithm may be covered in a single, big execution and $q_f$ is coverable.

### A.3.3 PTIME-hardness

The proof is similar to the one presented in [9, Proposition 1] for broadcast protocols. It uses a LOGSPACE-reduction for the Circuit Value Problem, which is PTIME-complete for LOGSPACE reductions [15]. This problem consists in determining the output value of an acyclic Boolean circuit with given input values and Boolean gates that can be negations $\neg$, disjunctions $\vee$ and conjunctions $\wedge$.

Consider an instance of the Circuit Value Problem, we write $V$ for the set of input, intermediate and output values of the circuit. A gate is represented as a tuple of the form $(\neg, i, o), (\vee, i_1, i_2, o)$ or $(\wedge, i_1, i_2, o)$ where $i, i_1, i_2 \in V$ denote input(s) and $o \in V$ the output of the gate. We construct an instance $(\mathcal{P}_{CVP}, q_f)$ of COVER with $\dim = 1$. In D, we have $d_0$ (which is never read) along with, for every $v \in V$, symbols $v = \text{T}$ and $v = \text{F}$, denoting that $v$ is respectively true and false. First, $\mathcal{P}_{CVP}$ has a part containing a state in $Q_0$ from which one may write the symbols corresponding to the assignment of the input values of the circuit. Moreover, for every gate of the circuit, there is a part of the protocol corresponding to this gate, which has a state in $Q_0$ from which a process may read the values of the inputs and write the corresponding value of the output. A depiction for gate $(\wedge, i_1, i_2, o)$ may be found in Figure 5. Lastly, state $q_f$ is the destination of the transition writing the symbol corresponding to the output variable of the circuit having the desired value, so that $q_f$ is coverable if and only if this desired value is indeed the output value of the circuit.

<figure><img src="image_8.png" /><figcaption>Figure 5 Part of the protocol $\mathcal{P}_{CVP}$ that corresponds to gate $(\wedge, i_1, i_2, o)$</figcaption></figure>

## A.4 Proof of Proposition 12

* **Proposition 12.** *DNF-PRP for roundless register protocols with $\dim = 1$ is in PTIME.*

We here prove the result in the general case of Proposition 12. We first prove that it suffices to prove the result for uninitialized protocols.

* **Lemma A.3.** *There exists a polynomial-time reduction from initialized DNF-PRP with $\dim = 1$ to uninitialized DNF-PRP with $\dim = 1$.*

*Proof.* Let $\mathcal{P} = \langle Q, Q_0, 1, D, d_0, \Delta \rangle$ a roundless register protocol with a single register. Any execution will be composed of two phases: the phase where the register has value $d_0$ and no
XX:18 Checking PRPs on Parameterized Shared-Memory Systems

write transition is taken and the phase where the register no longer has value $d_0$ and write transitions may be taken. The reduction relies on the observation that, in the first phase, only transitions labeled by read($d_0$) may be taken, and processes do not interact during this phase. Therefore, we can consider as initial any state that may be covered from $Q_0$ with a path of transitions all labeled by read($d_0$).

Consider the graph $G = (Q, E)$ whose vertices are the states of the system and whose edges are the transitions labeled by read($d_0$): $(q_1, q_2) \in E$ if and only if $(q_1, \text{read}(d_0)), (q_2) \in \Delta$. Let $Q'_0 := \{q \in Q | \exists m \ge 0, \exists q_0 \in Q_0, \exists q_1, \dots, q_{m-1}, q_m = q \in Q, \forall i \in [0, m-1], (q_i, q_{i+1}) \in E\}$ the set of states reachable from $Q_0$ in G. $Q'_0$ can trivially be computed in polynomial time. Additionally, let $\Delta' := \Delta \setminus \{(q, \text{read}(d_0), q') | q, q' \in Q\}$. The reduction maps $\mathcal{P}$ to the protocol $\mathcal{P}' = \langle Q, Q'_0, 1, D, d_0, \Delta' \rangle$.

We now prove that $(\mathcal{P}, \psi)$ is a positive instance of DNF-PRP if and only if $(\mathcal{P}', \psi)$ is. First, suppose that, in $\mathcal{P}$, there exists $\rho: \sigma_0 \xrightarrow{\ast} \sigma$ such that $\sigma \models \psi$. We decompose $\rho$ into $\rho_p: \sigma_0 \xrightarrow{\ast} \sigma_1$ and $\rho_s: \sigma_1 \xrightarrow{\ast} \sigma$ where $\text{data}(\sigma_1)(r) = d_0$ and $\rho_s$ either is the empty execution or starts with a write transition. $\rho_p$ only uses transitions labeled by read($d_0$) therefore, for every $q \in \text{st}(\sigma_1)$, there exists a path in G from $Q_0$ to $q$; this proves that $\text{st}(\sigma_1) \subseteq Q'_0$ and therefore that $\sigma_1$ is initial for $\mathcal{P}'$, moreover $\rho_s$ does not use transitions labeled by read($d_0$) hence $\rho_s$ is a witness that $(\mathcal{P}', \psi)$ is positive.

Suppose now that $(\mathcal{P}', \psi)$ is positive. There exists $\rho: \sigma_0 \xrightarrow{\ast} \sigma$ with $\sigma \models \psi$. For every $q \in \text{st}(\sigma_0) \setminus Q_0$, there exists $f(q) \in Q_0$ such that $q$ is reachable from $f(q)$ in G. Let $S := (\text{st}(\sigma_0) \cap Q_0) \cup f(\text{st}(\sigma_0) \setminus Q_0)$, we have $S \subseteq Q_0$. We have that $\langle S, d_0 \rangle \xrightarrow{\ast} \sigma_0$ in $\mathcal{P}$ by only taking transitions appearing in G. Therefore $\langle S, d_0 \rangle \xrightarrow{\ast} \sigma$ with $\sigma \models \psi$ and $\langle S, d_0 \rangle$ is initial for $\mathcal{P}$, which proves that $(\mathcal{P}, \psi)$ is positive. $\quad$

Thanks to the previous lemma, we prove Proposition 12 in the uninitialized case. Consider an instance $(\mathcal{P}, \psi)$ of DNF-PRP where $\mathcal{P}$ is uninitialized and $\text{dim} = 1$. $(\mathcal{P}, \psi)$ is positive if and only if $(\mathcal{P}, C)$ is positive for some clause $C$ of $\psi$. Our algorithm hence iterates over all clauses in $\psi$.

Let $C$ a clause in $\psi$. $C$ is a conjunction of literals, hence it may be seen as a set of atomic propositions that the configuration reached has to satisfy. Let $Q_+(C)$ be the set of states that need to be populated in the final configuration, $Q_-(C)$ the states that need to not be populated, and $D_{\text{ok}}(C)$ the symbols that are allowed in the final configuration. Formally, $Q_+(C) := \{q | \text{"q populated"} \in C\}, Q_-(C) := \{q | \text{"\neg(q populated)"} \in C\}$ and $D_{\text{ok}}(C) := \{d \in D | \text{"\neg(r contains d)"} \notin C \text{ and } \forall d' \neq d, \text{"r contains d'"} \notin C\}$ where r denotes the register. For all $\langle S, d \rangle \in \Sigma$, $\langle S, d \rangle \models C$ if and only if $Q_+(C) \subseteq S \subseteq Q \setminus Q_-(C)$ and $d \in D_{\text{ok}}(C)$. Let

$$ \mathcal{F}(C) := \{S \subseteq Q | Q_+(C) \subseteq S \subseteq Q \setminus Q_-(C)\} $$

denote the collection of all sets of states allowed in the final configuration.

**Lemma A.4.** Any execution $\rho: \sigma_0 \xrightarrow{\ast} \sigma$ with $\sigma_0 \in \text{Init}_a$ may be decomposed in the following form: $\sigma_0 \xrightarrow{\ast} \langle S, d_f \rangle \xrightarrow{\ast} \sigma$ with $S$ containing all states appearing in $\rho$.

**Proof.** Let $\rho: \sigma_0 \xrightarrow{\ast} \sigma$; let $\langle S_f, d_f \rangle := \sigma$. The execution $\sigma_0 \xrightarrow{\ast} \langle S, d_f \rangle$ is obtained by turning into non-deserting all deserting steps in $\rho$, so that all states covered in $\rho$ appear in $S$. For the second execution, we claim that there exists $\rho' : \langle S, d_f \rangle \xrightarrow{\ast} \langle S'_f, d_f \rangle$ that is obtained by mimicking steps of $\rho$ starting from $\langle S, d_f \rangle$. First, $\mathcal{P}$ is uninitialized therefore $\rho$ starts with a write and the register value at the beginning of $\rho$ is irrelevant. Moreover, $\text{st}(\sigma_0) \subseteq S$ by definition of $S$, so that $\rho'$ starts from a configuration with more states that $\rho$. By induction,
for all $n \ge 1$, the $n$-th configuration in $\rho'$ has the same register value as and more states than the $n$-th configuration in $\rho$. This in fact proves that $S_f \subseteq S'_f$. Moreover, for every $q \in S \setminus S_f$, since $q \notin S_f$ the last step in $\rho$ about step $q$ has $q$ as source and is deserting, hence $q$ is also deserted in $\rho'$ which shows that $S'_f \subseteq S_f$. In the end, $\rho'$ goes from $\langle S, d_f \rangle$ to $\langle S_f, d_f \rangle$ which concludes the proof. ◀

We define the following two sets:

$$ \mathbf{C}(\mathcal{P}) := \max\{S \subseteq Q \mid \exists \sigma_0 \in \mathrm{Init}_a, \exists d \in D, \sigma_0 \xrightarrow{*} \langle S, d \rangle\}, $$

$$ \mathbf{BC}(\mathcal{P}, C) = \max\{S \subseteq Q \mid \forall d \in D, \exists d_f \in D_{\mathrm{ok}}(C), \exists S_f \in \mathcal{F}(C), \langle S, d \rangle \xrightarrow{*} \langle S_f, d_f \rangle\}. $$

where the max is for inclusion of sets. Note that for $S \subseteq Q$, it is equivalent that $S$ satisfies the condition $\forall d \in D, \dots$ in the second set and that there exists a witness execution that starts with a write and therefore is applicable from any $\langle S, d \rangle$ with $d \in D$. By convention, we consider that $\max(\emptyset) = \emptyset$, i.e., if $Q_0 = \emptyset$ then $\mathcal{C}(\mathcal{P}, C) = \emptyset$ and if $Q_-(\mathcal{P}, C) = Q$ then $\mathbf{BC}(\mathcal{P}, C) = \emptyset$.

We first prove that both maxima are well-defined because the sets considered are stable under union. Let $\sigma_0, \sigma'_0 \in \mathrm{Init}_a$, $\rho : \sigma_0 \xrightarrow{*} \langle S, d \rangle$, $\rho' : \sigma'_0 \xrightarrow{*} \langle S', d' \rangle$. We show that we can merge $\rho$ and $\rho'$ into a single execution $\langle \mathrm{st}(\sigma_0) \cup \mathrm{st}(\sigma'_0), d_0 \rangle \xrightarrow{*} \langle S \cup S', d' \rangle$. By mimicking $\rho$ (without deserting states from $\mathrm{st}(\sigma'_0)$), we obtain an execution $\langle \mathrm{st}(\sigma_0) \cup \mathrm{st}(\sigma'_0), d_0 \rangle \xrightarrow{*} \langle S \cup \mathrm{st}(\sigma'_0), d \rangle$. By mimicking $\rho'$, we obtain an execution $\langle S \cup \mathrm{st}(\sigma'_0), d \rangle \xrightarrow{*} \langle S \cup S', d' \rangle$ (because $\mathcal{P}$ is uninitialized, $\rho'$ starts with a write). Therefore $S \cup S'$ is in the set $\{S \subseteq Q \mid \exists \sigma_0 \in \mathrm{Init}_a, \exists d \in D, \sigma_0 \xrightarrow{*} \langle S, d \rangle\}$, proving that it is closed under union.

For $\mathbf{BC}(\mathcal{P}, C)$, we suppose that we have $S, S' \subseteq Q$ that satisfy the condition of the set, and we prove that $S \cup S'$ does as well. Let $d \in D$. By hypothesis on $S$ applied with $d$, there exist $S_f, d_f$ such that $\langle S, d \rangle \xrightarrow{*} \langle S_f, d_f \rangle$, and therefore $\langle S \cup S', d \rangle \xrightarrow{*} \langle S_f \cup S', d_f \rangle$. By hypothesis on $S'$ applied with $d_f$, there exist $S'_f, d'_f$ such that $\langle S', d_f \rangle \xrightarrow{*} \langle S'_f, d'_f \rangle$. Therefore we also have $\langle S_f \cup S', d_f \rangle \xrightarrow{*} \langle S_f \cup S'_f, d'_f \rangle$, which combined with the previous execution provides a witness that $S \cup S'$ is in the set.

Algorithm 2 provides functions computing $\mathcal{C}(\mathcal{P}, C)$ and $\mathbf{BC}(\mathcal{C}, \mathcal{P})$ along with the function solving DNF-PRP when the protocol is uninitialized and $\dim = 1$.

First, we prove that Compute_\(\mathcal{C}(\mathcal{P})\) returns $\mathcal{C}(\mathcal{P})$. By induction, any state added in $S$ in Compute_\(\mathcal{C}(\mathcal{P})\) are in $\mathcal{C}(\mathcal{P})$. Indeed, any state that can be covered from a state in $\mathcal{C}(\mathcal{P})$ using a write transition is in $\mathcal{C}(\mathcal{P})$. Similarly, any state that can be covered from a state in $\mathcal{C}(\mathcal{P})$ using a read transition which symbol may be written from $\mathcal{C}(\mathcal{P})$ is in $\mathcal{C}(\mathcal{P})$: first write the corresponding value then read it (all states of $\mathcal{C}(\mathcal{P})$ can be covered in a single, common execution). Conversely, for any execution $\rho : \sigma_0 \xrightarrow{*} \sigma$, every state appearing in $\rho$ is added to $S$. Observe that any execution may be split into phases, where a phase starts with a step writing a symbol then performs some number (possibly zero) of steps reading the symbol. We therefore process by induction on the number of such phases. The initialization comes from $\mathrm{st}(\sigma_0) \subseteq Q_0$. Let $d$ the symbol of the last phase in $\rho$, and suppose that all states appearing before this last phase are added to $S$. The write transition of the phase is detected at line 11 of the iteration and the corresponding destination state is added to $S$. This write transition is now a witness for $d$ at line 12, allowing every read transition appearing in the phase to be detected in this iteration.

We now claim that Compute_\(\mathbf{BC}(\mathcal{P}, C)\) returns $\mathbf{BC}(\mathcal{P}, C)$. If $S$ satisfies the condition in $\mathbf{BC}(\mathcal{P}, C)$ then one can go from $\langle S, \rangle$ to a configuration satisfies the clause with an execution starting with a write. Again, this execution may be split into phases, each phase being composed of a write of a symbol followed by some reads of this symbol. The symbol of the last phase must be in $D_{\mathrm{ok}}$ as the last configuration satisfies $C$. Therefore, by induction,
1 Function DNFPRP-Oneregister_Uninit($\mathcal{P}$):

2 | for $C$ clause of $\psi$ do
3 | &nbsp;&nbsp;&nbsp;&nbsp; $\mathcal{P}_C \leftarrow \mathcal{P}$; // copy of $\mathcal{P}$ that will be modified
4 | Until $Q(\mathcal{P}_C)$ reaches a fixpoint do
5 | &nbsp;&nbsp;&nbsp;&nbsp; $Q(\mathcal{P}_C) \leftarrow Q(\mathcal{P}_C) \cap \mathcal{C}(\mathcal{P}_C) \cap \mathcal{BC}(\mathcal{P}_C, C)$; // modifies $\mathcal{P}_C$
6 | &nbsp;&nbsp;&nbsp;&nbsp; if $Q_+(C) \subseteq Q(\mathcal{P}_C) \neq \emptyset$ then Accept;
7 | Reject;

8 Function Compute_C($\mathcal{P}$):

9 | $S \leftarrow Q_0$;
10 | Until $S$ reaches a fixpoint do
11 | &nbsp;&nbsp;&nbsp;&nbsp; $S \leftarrow S \cup \{q' \mid \exists q \in S, \exists d \in D, (q, \text{write}(d), q') \in \Delta\}$;
12 | &nbsp;&nbsp;&nbsp;&nbsp; $S \leftarrow S \cup \{q' \mid \exists q, q_1, q_2 \in S, \exists d, (q, \text{read}(d), q') \in \Delta, (q_1, \text{write}(d), q_2) \in \Delta\}$;
13 | return $S$;

14 Function Compute_BC($\mathcal{P}, C$):

15 | if PreviousSymbol($Q \setminus Q_-(C), D_{ok}$) \neq "Not found" then
16 | &nbsp;&nbsp;&nbsp;&nbsp; $S \leftarrow PreviousSymbol(Q \setminus Q_-(C), D_{ok})$;
17 | else return $\emptyset$;
18 | Until $S$ reaches a fixpoint do
19 | &nbsp;&nbsp;&nbsp;&nbsp; if PreviousSymbol($S, D \setminus \{d_0\}$) \neq "Not found" then
20 | &nbsp;&nbsp;&nbsp;&nbsp; $S \leftarrow PreviousSymbol(S, D \setminus \{d_0\})$;
21 | return $S$;

21 Function PreviousSymbol($S$, Symbols):

22 | Found \leftarrow False;
23 | for $d \in$ Symbols do
24 | &nbsp;&nbsp;&nbsp;&nbsp; $T \leftarrow S$;
25 | &nbsp;&nbsp;&nbsp;&nbsp; Until $T$ reaches a fixpoint do
26 | &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; $T \leftarrow T \cup \{q \in Q \mid \exists q' \in T, (q, \text{read}(d), q') \in \Delta\}$;
27 | &nbsp;&nbsp;&nbsp;&nbsp; if there exist $q \in Q, q' \in T$ s.t. $(q, \text{write}(d), q') \in \Delta$ then
28 | &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; $S \leftarrow T \cup \{q\}$;
29 | &nbsp;&nbsp;&nbsp;&nbsp; Found \leftarrow True;
30 | if Found then return $S$ else return "Not found";

■ Algorithm 2 A polynomial-time algorithm for DNF-PRP with $\dim = 1$
<figure><img src="image_9.png" /><figcaption>Figure 6 The protocol $\mathcal{P}_{\text{SAT}}(\phi)$ for NP-hardness of uninitialized TARGET.</figcaption></figure>

all states appearing in such an execution appear in some PreviousSymbol computation in Compute\_BC($\mathcal{P}, C$), and the states returned include all states of the execution. Conversely, given a computation of Compute\_BC($\mathcal{P}, C$) that returns $S$, one may by reversed induction build an execution that covers every state in $S$ and ends on a configuration satisfying $C$. All in all, we have proven that Compute\_BC($\mathcal{P}, C$) computes $\mathcal{BC}(\mathcal{P}, C)$.

We will now prove that DNFPRP\_Oneregister\_Uninit of Algorithm 2 solves DNF-PRP for uninitialized protocols with $\dim = 1$. First, suppose that the algorithm accepts during the iteration corresponding to clause $C$. It ends with a protocol $\mathcal{P}_C$ such that $Q_+(C) \subseteq Q(\mathcal{P}_C) = \mathcal{C}(\mathcal{P}_C) \cap \mathcal{BC}(\mathcal{P}_C, C)$. In this protocol, there exist $\sigma_0 \in \text{Init}_a$ and $d \in D$ such that $\sigma_0 \xrightarrow{*} \langle \mathcal{C}(\mathcal{P}_C), d \rangle$; since $\mathcal{C}(\mathcal{P}_C) = \mathcal{BC}(\mathcal{P}_C, C)$ we also have $\langle \mathcal{C}(\mathcal{P}_C), d \rangle \xrightarrow{*} \langle S_f, d_f \rangle \models C$ and the instance is positive.

Suppose now that the instance is positive. There exist a clause $C$ in $\psi$ and a witness execution $\rho : \sigma_0 \xrightarrow{*} \langle S_f, d_f \rangle$ with $d_f \in D_{\text{ok}}(C)$ and $S_f \in \mathcal{F}(C)$. Let $S$ the set of states appearing in $\rho$. By induction, we have that $S \subseteq \mathcal{C}(\mathcal{P}_C) \cap \mathcal{BC}(\mathcal{P}_C, C)$ at every iteration of DNFPRP\_Oneregister\_Uninit, because $\rho$ remains a witness of both inclusions at every iteration. Moreover, $Q_+(C) \subseteq S$ therefore the algorithm accepts.

## A.5 Proof of Proposition 13

► **Proposition 13.** *TARGET for uninitialized roundless register protocols is NP-hard.*

Once again, we provide a reduction from 3-SAT. Consider a 3-CNF formula $\phi = \bigwedge_{i=1}^m l_{i,1} \lor \bigvee_{i,2 \lor i,3} \text{over } n \text{ variables } x_1, \dots, x_n \text{ where, for all } i \in [1, m], \text{ for all } k \in [1, 3], l_{i,k} \in \{x_j, \neg x_j \mid j \in [1, n]\}.$

We define an instance of the uninitialized TARGET $(\mathcal{P}_{\text{SAT}}(\phi), q_f)$ which is positive if and only if $\phi$ is satisfiable. Let $\dim := n$, i.e., the protocol has a register $\text{rg}[i]$ for each $i \in [1, n]$. Each register can have values $\mathcal{T}$ and $\mathcal{F}$ (along with $d_0$ which cannot be read nor written). A depiction of the protocol can be found in Figure 6.

Suppose first that $\phi$ is satisfiable by an assignment $\nu$. For all $i \in [1, m]$, there exists $k(i) \in [1, 3]$ such that $\nu(l_{i,k(i)}) = \text{true}$. Consider the execution that writes symbols according to $\nu$, then deserts $q_0$ to go to $C_1?$, and one by one deserts all $C_i$?-s through states Test($l_{i,k(i)}$). This execution goes from $\langle q_0, \mathbf{d}_0^{\text{Reg}} \rangle$ to $\langle q_f, \vec{d}_f \rangle$ hence the instance of TARGET is positive.
Conversely, suppose that there exists such an execution $\rho : \sigma_0 \stackrel{*}{\rightarrow} \langle q_f, \vec{d} \rangle$. Let $\nu$ be the valuation corresponding to the register values when $\rho$ deserts $q_0$ for the last time. From this point onwards, $\rho$ successively deserts all $C_i?$, hence for all $i \in [1, m]$, there exists $k(i) \in [1, 3]$ such that $\nu(l_{i,k(i)}) = \text{true}$, proving that $\phi$ is satisfied by $\nu$.

## B Round-based Register Protocols

### B.1 Formal Definition of Atomic Presence Constraints

We first define some more precise notions to refer to parts of presence constraints. A term is of the form $m$ or $k+m$ with $m \in \mathbb{N}$ and $k$ a free variable. An atomic proposition is either of the form “$(q, t)$ populated” with $t$ a term and $q \in Q$ or of the form “$rg_t[\alpha]$ contains $d$” with $t$ a term, $\alpha \in [1, \text{dim}]$ and $d \in \mathcal{D}$. A literal is either an atomic proposition or the negation of an atomic proposition. A proposition is a Boolean combination of atomic propositions that has at most one free variable. An atomic presence constraint is either a closed proposition (no free variables), or of the form “$\exists k \phi$” or “$\forall k \phi$” where $\phi$ is a proposition with $k$ as a free variable. A presence constraint is a Boolean combination of atomic presence constraints.

### B.2 Proof of Lemma 21

We prove the following, more general statement.

**Lemma B.5.** Let $K \in \mathbb{N}$, $w \ge \nu-1$, $(\tau_k)_{k \le K}$ and $(T_k)_{k \le K-1}$ such that:

- for all $k \le K$, $\tau_k$ is a footprint on $[k-w, k]$,

- for all $k \le K-1$, $T_k$ is a footprint on $[k-w, k+1]$,

- for all $k \le K-1$, footprint[$k-w, k$]($T_k$) = $\tau_k$,

- for all $k \le K-1$, footprint[$k-w+1, k+1$]($T_k$) = $\tau_k$.

There exists an execution $\rho$ such that, for all $k \le K$, footprint[$k-w, k$]($\rho$) = $\tau_k$.

We start by proving the following lemma:

**Lemma B.6.** Let $w \ge \nu$, $k \in \mathbb{N}$, $\tau_-$ a footprint on $[k-w, k]$ and $\tau_+$ a footprint on $[k-w+1, k+1]$ such that footprint[$k-w+1, k$]($\tau_-$) = footprint[$k-w+1, k$]($\tau_+$). There exists $T$ a footprint on $[k-w, k+1]$ such that footprint[$k-w, k$]($T$) = $\tau_-$ and footprint[$k-w+1, k+1$]($T$) = $\tau_+$.

**Proof.** Let $\tau_{com} := \text{footprint}[k-w+1, k](\tau_-) = \text{footprint}[k-w+1, k](\tau_+)$. We proceed by induction on the number of steps in $\tau_{com}$.

First if $\tau_{com}$ is the dummy footprint with no steps, then all steps in $\tau_-$ are at round $k-w$ and steps in $\tau_+$ are at round $k+1$. It suffices to consider $T$ that first copies the behavior of $\tau_-$ and then the behavior of $\tau_+$: steps at round $k-w$ cannot depend on the information of rounds $> k-w$, and steps at round $k+1$ cannot depend on the information of rounds $< k-w$ because $w \ge \nu$.

Assume that the property is true if $\tau_{com}$ has $m$ steps, and suppose that $\tau_{com}$ has $m+1$ steps. We decompose $\tau_- = t_-, \theta, s_-$ and $\tau_+ = t_+, \theta, s_+$ where $t_-$ and $t_+$ coincide on rounds $k-w+1$ to $k$ and their projection on these rounds has exactly $m$ steps, $\theta$ is the move of the $m+1$-th step of $\tau_{com}$, and $s_-$ and $s_+$ have no step at rounds $k-w+1$ to $k$. By induction hypothesis, there exists $t$ such that footprint[$k-w, k$]($t$) = $t_-$ and footprint[$k-w+1, k+1$]($t$) = $t_+$. By applying the property for $m=0$, there exists $s$ such that footprint[$k-w, k$]($s$) = $s_-$ and footprint[$k-w+1, k+1$]($s$) = $s_+$. Letting $T := t, \theta, s$ (with $\theta$ deserting if and only if it was deserting in $\tau_{com}$) concludes the proof. $\quad$
We now prove Lemma B.5. We proceed by induction on $K$. First, if $K = 0$, footprint $\tau_0$ only has moves at round 0 and may be seen as an execution. Suppose that the property is true for $K$, and consider $(\tau_k)_{k \le K+1}$, $(T_k)_{k \le K}$ satisfying the hypothesis. For all $k \le K-1$, $T_k$ and $T_{k+1}$ both have projection $\tau_{k+1}$ on rounds $[k-w+1, k+1]$, hence thanks to Lemma B.6 applied with $w' := w+1$ and $k' := k+1$, there exists $U_k$ on rounds $[k-w, k+2]$ that projects to $T_k$ and $T_{k+1}$ on $[k-w, k+1]$ and $[k-w+1, k+2]$ respectively. By applying the induction hypothesis on $(T_k)$ and $(U_k)$ with $K' := K-1$, there exists an execution $\rho$ such that, for all $k \le K$, footprint$[k-w, k+1](\rho) = T_k$; this implies that, for all $k \le K+1$, footprint$[k-w, k](\rho) = \tau_k$, concluding the proof of Lemma B.5. Applying Lemma B.5 with $w := v-1$ gives Lemma 21.

## B.3 Technical Details about Algorithm 1

Here, we describe in full details how Algorithm 1 handles the presence constraint. The pseudocode of the three functions used in Algorithm 1 can be found in Algorithm 3.

For $\psi$ a presence constraint, we write $\text{APC}(\psi)$ for the set containing all *atomic presence constraints* in $\psi$ as well as their negations. For $\phi$ a closed proposition, we write $\text{AP}(\phi)$ for the set of *atomic propositions* in $\phi$. Given a set $S$ of propositions or presence constraints, we write $\text{PosOrNeg}(S) := S \cup \{\neg P \mid P \in S\}$ for the set containing all elements in $S$ and the negations of all elements in $S$.

### B.3.1 Function NDInit (Line 1):

At **Line 2**, we guess a partial assignment over atomic presence constraints that makes $\psi$ true. Recall that atomic presence constraints either are closed propositions or of the form $\text{"}\forall l \phi\text{"}$ or $\text{"}\exists l \phi\text{"}$ with $\phi$ a proposition that has $l$ as free variable. We see this assignment as a set of atomic presence constraints which, when set to true, make $\psi$ true. Note that negations of atomic presence constraints are atomic presence constraints. All closed atomic propositions refer to constant rounds; guess which ones are true (**Line 5**). This simplifies all closed propositions in $X$ to either true of false: if any of them is false, we reject (**Line 8**). We put universally quantified element of $X$ in $U$ (**Line 9**) and existentially quantified ones in $E$ (**Line 10**).

### B.3.2 Function NDComputeIteration (Line 11):

The universal atomic presence constraints are checked at every round (**Lines 12 to 14**), while for each existential atomic presence constraints is checked at a round chosen non-deterministically (**Lines 15 to 18**). When checking a proposition, we guess which literals make them true, and put these literals in $C$ to be checked later. Moreover, we check at round $k$ all literals in $C$ that are about round $k$ (at **Lines 19 and 20**). Note that all literals in $C$ are closed formulas hence their terms are constant integers.

### B.3.3 Function TestPresenceConstraint (Line 21):

In this function, we check whether we can stop the execution at round $k$, leaving all rounds $\ge k+1$ untouched. First, we check that $E$ is empty. This means that a round has been guessed for every existential formula that has been in $E$. Moreover, we check that remaining formulas in $C$ and $U$ would be satisfied at rounds $\ge k+1$ if these rounds are left untouched by the execution, which is done in **Lines 23 to 25**. The test is expressed under the condition $\langle\emptyset, d_0^{\text{Reg}}\rangle \models \phi$ (although $\langle\emptyset, d_0^{\text{Reg}}\rangle$ is technically not a configuration as it has zero processes), and is implemented as follows. Any formula $\phi$ that is in $C$ at the end of iteration $k$ is about
1 Function NDInit(E, U, C) :
   1 | /* Sets containing what needs to be checked: U and E contain
   2 | respectively universally and existentially quantified atomic
   3 | presence constraints, C contains closed literals */
   4 | Guess Xsubseteq PosOrNeg(APC( )). s.t. ψ is true when all APCs in X are true ;
   5 | for P in X do
   6 |   for φclosed atomic proposition in P do
   7 |   | /* φ refers to constant rounds only */
   8 |   | if φ guessed to be true then Add φ to C ; Replace φ by true in P ;
   9 |   | else Add neg φ to C ; Replace φ by false in P ;
  10 |   if P is a closed proposition then
  11 |   | Check that P is true with guessed values of atomic propositions ;
  12 |   if P universal then Add P to U ;
  13 |   if P existential then Add P to E ;
  14 |   for "forall φ" in U do
  15 |   | for "exists φ" in E do
  16 |   |   if φ[l ← k] guessed to be true then
  17 |   |   | Guess Lsubseteq PosOrNeg(AP(φ[l → k])) s.t. φ[l ← k] is true when all literals in L
  18 |   |   | are true ;
  19 |   |   | Add all literals in L to C ;
  20 |   |   for φin C about round k do
  21 |   |   // φis of the form (negation of) "(q, k) populated", or (negation
  22 |   |   | of) "rgk[α] contains d"
  23 |   | Check that φis satisfied in λ ; Remove φfrom C ;
  24 |   25 |   return false ;
  26 |   return true ;

■ Algorithm 3 The functions at Line 5, Line 10 and Line 11 of Algorithm 1
round $l \ge k+1$ at this stage, and we check that $\phi$ is either of the form "$\neg((q,l) \text{ populated})$" or of the form "$rg_l[\alpha]$ contains $d_0$". A universal presence constraint $\forall l \phi$ must be satisfied on arbitrarily large rounds $\ge k+1$, and we check that we obtain true by setting in $\phi$ all "$ (q,t) \text{ populated} $" to false, "$rg_t[\alpha]$ contains $d_0$" to true and "$rg_t[\alpha]$ contains $d$" to false for $d \ne d_0$.

**Example B.7.** Consider $\phi_1 := \forall l ((q,l) \text{ populated}) \lor (rg_l[\alpha] \text{ contains } d_0)$ and $\phi_2 := \forall l (rg_l[\alpha] \text{ contains } d) \text{ with } d \neq d_0$. One has $\langle\emptyset, d_0^{\text{Reg}}\rangle \models \text{phi}_1$, but $\langle\emptyset, d_0^{\text{Reg}}\rangle \not\models \phi_2$. There is no hope of finding a $\sigma \in \text{Reach}_a(\text{Init}_a)$ such that $\sigma \models \phi_2$. ◀

## B.4 Proof of Correctness of the Algorithm

**Proposition 22.** ($\mathcal{P}, \psi$) is a positive instance of round-based PRP if and only if there exists an accepting computation of Algorithm 1 on ($\mathcal{P}, \psi$).

First, consider a computation of the algorithm that accepts at round $K \in \mathbb{N}$. For all $k \in [0, K]$, let $\tau_k$ denote the footprint on $[k-v+1, k]$ guessed by the algorithm during iteration $k$. By applying Lemma 21, there exist $\sigma_0 \in \text{Init}_a$ and an execution $\rho: \sigma_0 \xrightarrow{*} \sigma$ such that, for all $k \le K$, $\text{footprint}[k-v+1, k](\rho) = \tau_k$. Moreover, $\rho$ leaves rounds $\ge K$ untouched.

**Lemma B.8.** For every formula $P$ that was in $U$, $E$ or $C$ at any point throughout the computation, one has $\sigma \models P$.

**Proof.** Let $L$ be a literal that has been in $C$ at some point. If it was removed from $C$ at **Line 20**, then $C$ is satisfied by $\lambda$ hence by $\sigma$. If it has remained in $C$ until the end, then it is about round $l \ge K+1$ and $\langle\emptyset, d_0^{\text{Reg}}\rangle \models L$, hence $\sigma \models L$.

Consider "$\exists l \phi$" that has appeared in $E$ at some point; it was added to $E$ at **Line 10**. At some iteration $k$, "$\exists l \phi$" is removed from $E$ at **Line 18**. All literals guessed at **Line 17** are added to $C$ at **Line 18** hence are satisfied by $\sigma$, thus $\sigma \models \phi[l \leftarrow k]$ and $\sigma \models \exists l \phi$.

Similarly, consider "$\forall l \phi$" that has appeared in $U$ at some point. By the same argument, for all $k \le K$, $\sigma \models \phi[l \leftarrow k]$. Also, thanks to the verification at **Lines 23 to 25**, for all $k \ge K+1$, $\sigma \models \phi[l \leftarrow k]$, which proves that $\sigma \models \exists l \phi$. ◀

The previous lemma proves that all APCs guessed at **Line 2** are satisfied by $\sigma$. Note that the simplification at **Lines 5 and 6** does not change the truth value of APC $P$. Finally, we have $\sigma \models \psi$.

We now prove the converse implication: suppose that there exists $\rho: \sigma_0 \xrightarrow{*} \sigma$ with $\sigma \models \psi$. Since $\rho$ is a finite execution, there exists $K$ such that $\sigma$ has no move with effect on rounds $> K$. We build an accepting computation of the algorithm as follows. First, the computation of the algorithm guesses $\sigma_0$ as initial configuration. At **Line 2**, it guesses APCs $P$ such that $\sigma \models P$. At **Line 5**, it guesses the truth value of closed APs in $\sigma$, so that all formulas added to $C$, $E$ and $U$ are satisfied by $\sigma$. In the loop on $k$, it guesses $\rho$ footprint by footprint. At execution $k$, the local configuration $\lambda$ obtained is equal to $\text{footprint}[k-v, k](\sigma)$. Formulas in $E$ and $U$ do not have closed terms, and since quantified terms are of the form $l+m$ with $l$ a free variable, literals added to $C$ at iteration $k$ refer to rounds $\ge k$; thanks to **Lines 19** to **20**, at the end of iteration $k$, all literals in $C$ are about rounds $\ge k+1$. At the end of iteration $K$ (or an earlier iteration), all formulas in $C$ and $U$ are satisfied by $\sigma$ (which is blank after round $K$) hence $\text{TestPresenceConstraint}(E, U, C, \lambda)$ succeeds and the computation accepts. This concluded the proof of Proposition 22.
**B.5 Proof of Proposition 23**

**► Proposition 23.** *Algorithm 1 works in space $O(|\psi|^3 + |Q|^2 (v+1)^2 \log(\dim |D|))$.*

We first prove that footprints may be stored in polynomial space.

**► Lemma B.9.** For all $\sigma \in \Sigma$, $\sigma' \in \text{Reach}_a(\sigma)$, there exists $\rho : \sigma \stackrel{*}{\to} \sigma'$ s.t., for all $k$, footprint[$k-v, k$]($\rho$) is storable in space $O((|Q|^2 (v+1)^2 \log(\dim |D|)))$.

More specifically, we will prove that footprint[$k-v, k$]($\rho$) is storable in space $O((|Q|^2 (v+1)^2 + |Q| (v+1)^2 \log(\dim |D|)))$. Similarly to the roundless case, we introduce a notion of normal form. An execution $\rho$ is in normal form if for every step in $\rho$, one the following conditions is satisfied:

- the step writes a symbol to a register, and this symbol is later read by another step, or

- it deserts the source location, or

- its destination location was not populated before the step and has never been populated before in the execution.

Note that the last two conditions combined imply that a given location is deserted at most once, as it cannot be deserted and then populated again.

**► Lemma B.10.** For all execution $\rho : \sigma \stackrel{*}{\to} \sigma'$, there exists an execution $\rho' : \sigma \stackrel{*}{\to} \sigma'$ that is in normal form.

*Proof.* It suffices to iteratively:

- remove any read or increment that is non-deserting and does not cover a new location,

- remove any write that is non-deserting, does not populate a new location and whose written symbol is never read,

- turn into non-deserting any deserting step that deserts a location which is later populated again.

◄

**► Lemma B.11.** An execution in normal form has at most $|Q|(2v+5)$ steps on a given round $k$.

*Proof.* First, any read or increment step at round $k$ either deserts its source location which is never populated again, or populates its destination (i.e., its destination was not populated before the step). However, each location has at most one step populating the location and one deserting the location. Since steps at round $k$ may only desert locations of round $k$ and populate locations at rounds $k$ and $k+1$, at most $3|Q|$ steps at round $k$ either desert or populate a location, among which at most $2|Q|$ read steps as they may only desert and populate locations of round $k$. Moreover, any write step at round $k$ that does not populate or desert must be read later, and that has to be by a read step on a round between $k$ and $k+v$. Since there are at most $2|Q|(v+1)$ read steps on these rounds, there are at most $2|Q|(v+1)$ writes at round $k$ that do not populate nor desert, hence in total at most $|Q|(2v+5)$ steps at round $k$. ◄

**► Lemma B.12.** If $\rho$ is in normal form and $k \in \mathbb{N}$, then footprint[$k-v, k$]($\rho$) is storable in polynomial space $O((|Q|^2 (v+1)^2 + |Q| (v+1)^2 \log(\dim |D|)))$.
**Proof.** This footprint only has steps at rounds $k-v$ to $k$, hence in total at most $(v+1)|Q|(2v+5)$ steps. Since a move can be stored in $O(\log(|Q|) + \log(D) + \log(v) + \log(\dim))$ and a local configuration in $O((|Q| + \dim \log(|D|))(v+1))$ (storing the relative round instead of the absolute one), a footprint on $[k-v, k]$ can be stored in polynomial space $O((|Q|^2(v+1)^2 + |Q|(v+1)^2 \log(\dim |D|)))$. ◀

Combining Lemmas B.10, B.11 and B.12 proves Lemma B.9. Observe that Lemma B.9 is
only true under the assumption that we do not store the rounds of a footprint in absolute
value but in relative value with respect to $k$; otherwise the space used would depend on $k$.

We now prove Proposition 23.

Thanks to Proposition B.9, one may store $\tau$ and $T$ in polynomial space. $U$ and $E$ are
storable in $O(|\psi|)$, as for every atomic presence constraint $\phi$ in $U$ and $E$, either $\phi$ is present
in $\psi$ or its negation $\neg\phi$ is. Let $M$ be the value of the greatest integer constant in $\psi$, which is
in $O(|\psi|)$ thanks to unary encoding of the terms. A literal can get to $C$ in two different ways:
during the initialization (**Lines 5 and 6**) or while processing a presence constraint from $U$
or $E$ (**Lines 14 and 18**). There are at most $O(|\psi|)$ literals added to $C$ in the initialization.
Consider $L$ a literal that is added to $C$ at **Line 14** or **Line 18** during the computation of
round $k$. Let $r$ be the round appearing in $L$. Either $r$ is a constant from $\psi$, or it was added
at iteration $k' \le k$, hence $r$ is of the form $k' + m$ with $m \le M$. In that case, note that $r \ge k$
because otherwise the literal would have been removed from $C$ at iteration $r$. Either way, one
has $0 \le r - k \le M$, hence a given element in $C$ is storable in $O(|\psi|)$. Also, elements in $C$ at
round $k$ were added to $C$ either at the initialization or at a round in $[k-M, k]$, which bounds
the total number of elements in $C$ by $O(M|\psi|) = O(|\psi|^2)$ at any point in the computation,
and $C$ is storable in $O(|\psi|^3)$.