Univ Rennes, Inria, CNRS, IRISA<EMAIL_ADDRESS>Nicolas
Waldburger [500]Theory of computation Verification by model checking
[300]Theory of computation Distributed algorithms

# Checking Presence Reachability Properties on Parameterized Shared-Memory
Systems

Nicolas Waldburger

###### 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 -complete.
Moreover, for the roundless model with finitely many registers, we prove that
the complexity drops down to -complete and we provide several natural
restrictions that make the problem solvable in polynomial time.

###### keywords:

Verification, Parameterized models, Distributed algorithms

###### category:

###### keywords:

Verification, Parameterized models, Distributed algorithms

##  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 -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 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 -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 -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 -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 -complete and to decrease to 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 -complete.
When the constraints cannot count processes, this problem is analogous to our
presence reachability problem; for RBN, it is shown to be -complete, a
complexity that we also obtain in our setting. Finally, this complexity drops
down to 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 -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 $\textsf{Pre}^{*}$ and $\textsf{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 2.1 (Roundless register protocols).

A _roundless register protocol_ is a tuple $=\nobreak{\langle\penalty
10000Q,Q_{0},\penalty-1000\mathsf{dim},\penalty-1000{\rm
D},\penalty-1000\mathsf{d}_{0},\Delta\penalty 10000\rangle}$ where

  * •

$Q$ is a finite set of _states_ with a distinguished subset of _initial
states_ $Q_{0}\subseteq Q$;

  * •

$\mathsf{dim}\in\mathds{N}$ is the number of shared _registers_ ;

  * •

${\rm D}$ is a finite _data alphabet_ containing the initial symbol
$\mathsf{d}_{0}$;

  * •

$\Delta\subseteq Q\times\times Q$ is the set of _transitions_ , where
$:=\\{\mathsf{read}_{\alpha}(\mathsf{d})\mid\alpha\in[1,\mathsf{dim}],\allowbreak\mathsf{d}\in{\rm
D}\\}\cup\\{\mathsf{write}_{\alpha}(\mathsf{d})\mid\alpha\in[1,\mathsf{dim}],\mathsf{d}\in{\rm
D}\setminus\\{\mathsf{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 $\mathsf{dim}$ shared registers;
$\mathsf{d}\in{\rm D}$ denotes the symbol and $\alpha$ indicates the register
on which the action is performed. Each register stores one _symbol_ from the
finite set ${\rm 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 is defined as
$||:=|Q|+|{\rm D}|+|\Delta|+\mathsf{dim}$. For all
$\alpha\in[1,\mathsf{dim}]$, we write $\mathsf{rg}[\alpha]$ for the register
of index $\alpha$. We also write $\mathsf{Reg}$ for the set
$\\{\mathsf{rg}[\alpha]\mid\alpha\in[1,\mathsf{dim}]\\}$ of all registers.

Processes are assumed to have no identifiers so they are identical anonymous
agents. Therefore, a _configuration_ is a pair $\gamma=\langle\penalty
10000\mu,\vec{d}\penalty 10000\rangle\in\mathds{N}^{Q}\times{\rm
D}^{\mathsf{Reg}}$ such that $0<\sum_{q\in Q}\mu(q)<\infty$. Let
$\mathsf{st}(\gamma):=\mu$ which indicates the number of processes in each
state, and $\mathsf{data}(\gamma):=\vec{d}$ mapping to each register its
symbol: for all $\mathsf{r}\in\mathsf{Reg}$,
$\mathsf{data}(\gamma)(\mathsf{r})$ is the symbol contained in register
$\mathsf{r}$ in $\gamma$. Let $\Gamma:=\mathds{N}^{Q}\times{\rm
D}^{\mathsf{Reg}}$ denote the set of all configurations. Let
$\mathsf{supp}(\gamma):=\\{q\in Q\mid\mathsf{st}(\gamma)(q)>0\\}$ denote the
support of the multiset $\mathsf{st}(\gamma)$. We write $\immediate\oplus$ and
$\immediate\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 $\mathsf{d}_{0}$. We denote by
$\mathsf{Init_{c}}$ the set of initial configurations (the letter $\mathsf{c}$
stands for “concrete” as opposed to “abstract” configurations defined later).
Formally, $\mathsf{Init_{c}}:=\\{\gamma\mid\mathsf{st}(\gamma)\subseteq
Q_{0},\,\mathsf{data}(\gamma)=\mathsf{d}_{0}^{\mathsf{Reg}}\\}$.

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

  * •

if $a=\mathsf{read}_{\alpha}(\mathsf{d})$ then
$\mathsf{data}(\gamma)(\mathsf{rg}[\alpha])=\mathsf{d}$ and
$\mathsf{data}(\gamma^{\prime})=\mathsf{data}(\gamma)$,

  * •

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

In that case, we write $\gamma$ or simply $\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}$. We write $\gamma_{0}$ for the existence
of such an execution. $\gamma^{\prime}$ is _reachable from $\gamma$_ when
$\gamma$. Given a set $C$ of configurations, we write
$\mathsf{Reach_{c}}(C):=\\{\gamma^{\prime}\mid\exists\gamma\in C,\,\gamma$. A
configuration is _reachable_ when it is in
$\mathsf{Reach_{c}}(\mathsf{Init_{c}}{})$.

######  Example 2.8.

Figure 1 provides an example of a roundless register protocol with ${\rm
D}=\\{\mathsf{d}_{0},\mathsf{a},\mathsf{b},\mathsf{c}\\}$, $Q_{0}=\\{q_{0}\\}$
and $\mathsf{dim}=1$, hence read and write actions are implicitly on register
$\alpha=1$. The red and blue labels are to be ignored for now.

The set of initial configurations is $\mathsf{Init_{c}}:=\\{\langle\penalty
10000q_{0}^{n},\mathsf{d}_{0}\penalty 10000\rangle\mid n\geq 1\\}$. The
following execution with two processes witnesses that $\langle\penalty
10000q_{f}\oplus C,\mathsf{a}\penalty
10000\rangle\in\mathsf{Reach_{c}}(\mathsf{Init_{c}}{})$:
$\langle\penalty 10000q_{0}^{2},\mathsf{d}_{0}\penalty 10000\rangle$.

$q_{0}$$B$$A$$C$$q_{f}$$\mathsf{read}(\mathsf{d}_{0}$)$\mathsf{write}(\mathsf{c})$$\mathsf{read}(\mathsf{d}_{0})$$\mathsf{read}(\mathsf{c})$$\mathsf{read}(\mathsf{a})$$\mathsf{write}(\mathsf{b})$$\mathsf{read}(\mathsf{b})$$\mathsf{write}(\mathsf{a})$$\mathsf{read}(\mathsf{c})$$\mathsf{write}(\mathsf{a})$
Figure 1: An example of a protocol

###  2.2 Reachability Problems

Our first problem of interest is the _coverability problem_ ():

for roundless register protocols Input: A roundless register protocol ,
$q_{f}\in Q$ Question: Does there exist
$\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ such that
$\mathsf{st}(\gamma)(q_{f})>0$?

Note that, because the model is parameterized, a witness execution of 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_ () where
processes must synchronize at $q_{f}$ :

for roundless register protocols Input: A roundless register protocol ,
$q_{f}\in Q$ Question: Does there exist
$\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ s.t. for all $q\neq q_{f}$,
$\mathsf{st}(\gamma)(q)=0$?

######  Remark 2.14.

is harder than : 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 $\land$, $\lor$ and
$\neg$) of atomic propositions of the form “$q\mathrel{\mathsf{populated}}$”
with $q\in Q$, or of the form
“$\mathsf{r}\mathrel{\mathsf{contains}}\mathsf{d}$” with
$\mathsf{r}\in\mathsf{Reg}$ and $\mathsf{d}\in{\rm D}$. A presence constraint
is interpreted over a configuration $\gamma$ by interpreting
“$q\mathrel{\mathsf{populated}}$” as true if and only if
$\mathsf{st}(\gamma)(q)>0$ and
“$\mathsf{r}\mathrel{\mathsf{contains}}\mathsf{d}$” as true if and only if
$\mathsf{data}(\gamma)(\mathsf{r})=\mathsf{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 2.15.

If $Q=\\{q_{1},q_{2},q_{3}\\}$, $\mathsf{dim}=2$, ${\rm
D}=\\{\mathsf{d}_{0},a,b\\}$ and
$\phi:=(q_{1}\mathrel{\mathsf{populated}})\lor((q_{2}\mathrel{\mathsf{populated}})\land(\mathsf{rg}[1]\mathrel{\mathsf{contains}}a))$
then $\langle\penalty 10000q_{1}\oplus q_{3},\mathsf{d}_{0}^{2}\penalty
10000\rangle\models\phi$, $\langle\penalty 10000q_{2}^{2},(a,b)\penalty
10000\rangle\models\phi$ but $\langle\penalty 10000q_{2}^{2},b^{2}\penalty
10000\rangle\not\models\phi$.

The _Presence Reachability Problem_ () generalizes both and . It corresponds
to the cardinality reachability problem for cardinality constraints restricted
to CC[$\geq 1,=0$] studied for broadcast protocols [9].

for roundless register protocols Input: A roundless register protocol , a
presence constraint $\phi$ Question: Does there exist
$\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ such that
$\gamma\models\phi$?

The formula $\phi$ automatically makes -hard, since one can encode the
problem. Therefore, we also consider the _DNF Presence Reachability Problem_
(DNF-PRP), in which $\phi$ is in _disjunctive normal form_. and are special
cases of DNF-PRP, with $\phi=(q_{f}\mathrel{\mathsf{populated}})$ for and
$\phi=\bigwedge_{q\neq q_{f}}\neg(q\mathrel{\mathsf{populated}})$ for .

######  Example 2.16.

Consider again the protocol defined in Figure 1. $(,q_{f})$ is a positive
instance of , as proved in Example 2.8. Let blue be the protocol obtained from
by changing to $\mathsf{read}(\mathsf{c})$ the label of the transition from
$q_{0}$ to $B$ (in blue in Figure 1). $(_{\mathsf{blue}},q_{f})$ is a negative
instance of . In fact, a process can only get to $B$ if $\mathsf{c}$ has been
written to the register, and then $\mathsf{d}_{0}$ can no longer be read so no
process may go to state $C$, $\mathsf{a}$ cannot be written and no process may
go from $A$ to $q_{f}$.

$(,q_{f})$ is a negative instance of : to leave $A$, one needs to read
$\mathsf{a}$, hence must have a process on state $C$, and to leave $C$, one
must read $\mathsf{b}$ which would force us to send a process to $A$. Let red
be the protocol obtained from by changing to $\mathsf{write}(\mathsf{a})$ the
label of the transition from $C$ to $A$ (in red in Figure 1).
$(_{\mathsf{red}},q_{f})$ is a positive instance of : $\langle\penalty
10000q_{0}^{2},\mathsf{d}_{0}\penalty 10000\rangle$.

Let
$\phi:=\neg(C\mathrel{\mathsf{populated}})\land((\mathsf{rg}\mathrel{\mathsf{contains}}\mathsf{a})\lor[(\mathsf{rg}\mathrel{\mathsf{contains}}\mathsf{b})\land\neg(A\mathrel{\mathsf{populated}})])$.
$\phi$ is a presence constraint and $(,\phi)$ is a negative instance of .
Indeed, if $\mathsf{a}$ is in the register, then $C$ must be populated and if
$\mathsf{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 . 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 2.23 (Copycat).

Consider $\gamma_{1}$, $\gamma_{2}$, $q_{2}$ such that $\gamma_{1}$,
$q_{2}\in\mathsf{supp}(\gamma_{2})$. There exists
$q_{1}\in\mathsf{supp}(\gamma_{1})$ s.t. $\langle\penalty
10000\mathsf{st}(\gamma_{1})\oplus q_{1},\mathsf{data}(\gamma_{1})\penalty
10000\rangle$.

An _abstract configuration_ is a pair $\sigma=\langle\penalty
10000\mathsf{st}(\sigma),\mathsf{data}(\sigma)\penalty 10000\rangle\in
2^{Q}\times{\rm D}^{\mathsf{Reg}}$ such that
$\mathsf{st}(\sigma)\neq\emptyset$. The set of _initial configurations_ is
$\mathsf{Init_{a}}:=\\{\langle\penalty
10000S,\mathsf{d}_{0}^{\mathsf{dim}}\penalty 10000\rangle\mid S\subseteq
Q_{0}\\}$. Given a concrete configuration $\gamma$, the projection
$\mathsf{abst}(\gamma)$ is the abstract configuration $\langle\penalty
10000\mathsf{supp}(\gamma),\mathsf{data}(\gamma)\penalty 10000\rangle$. Let
$\Sigma:=2^{Q}\times{\rm D}^{\mathsf{Reg}}$ denote the set of abstract
configurations. For $\sigma,\sigma^{\prime}\in\Sigma$, $\sigma^{\prime}$ is
the _successor_ of $\sigma$ when there exists
$\delta=(q,a,q^{\prime})\in\Delta$ such that $q\in\mathsf{st}(\gamma)$, either
$\mathsf{st}(\gamma^{\prime})=\mathsf{st}(\gamma)\cup\\{q^{\prime}\\}$ or
$\mathsf{st}(\gamma^{\prime})=(\mathsf{st}(\gamma)\setminus\\{q\\})\cup\\{q^{\prime}\\}$,
and: if $a=\mathsf{read}_{\alpha}(\mathsf{d})$ then
$\mathsf{data}(\gamma)(\mathsf{rg}[\alpha])=\mathsf{d}$ and
$\mathsf{data}(\sigma)=\mathsf{data}(\sigma^{\prime})$, and if
$a=\mathsf{write}_{\alpha}(\mathsf{d})$ then
$\mathsf{data}(\sigma^{\prime})(\mathsf{rg}[\alpha])=\mathsf{d}$ and for all
$\alpha^{\prime}\neq\alpha$,
$\mathsf{data}(\sigma^{\prime})(\mathsf{rg}[\alpha^{\prime}])=\mathsf{data}(\sigma)(\mathsf{rg}[\alpha^{\prime}])$.
Again, we denote such a step by $\sigma$ or $\sigma$. Note that one could
equivalently define $\sigma$ by: $\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^{\prime\prime}\neq\sigma^{\prime}$ such that $\sigma$ and $\sigma$.
This alternative corresponds to whether all processes in $q$ take the
transition
($\mathsf{st}(\gamma^{\prime})=(\mathsf{st}(\gamma)\setminus\\{q\\})\cup\\{q^{\prime}\\}$)
or only some
($\mathsf{st}(\gamma^{\prime})=\mathsf{st}(\gamma)\cup\\{q^{\prime}\\}$). We
define _abstract executions_ similarly to concrete ones, and denote them using
$\rho$. We also define the _reachability set_ $\mathsf{Reach_{a}}(A)$ and the
notion of _coverability_ as in the concrete case. This abstraction is sound
and complete for :

######  Proposition 2.33 (Soundness and completeness of the abstraction).

For all $S\subseteq Q$, $\vec{d}\in{\rm D}^{\mathsf{Reg}}$:

$(\exists\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}}{}):\mathsf{supp}(\gamma){=}S,\,\mathsf{data}(\gamma){=}\vec{d})\
\Longleftrightarrow\\\
(\exists\sigma\in\mathsf{Reach_{a}}(\mathsf{Init_{a}}{}):\
\mathsf{st}(\sigma){=}S,\,\mathsf{data}(\sigma){=}\vec{d}).$

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 $\mathsf{abst}(\gamma)\models\phi$. Indeed, $\gamma$ and
$\mathsf{abst}(\gamma)$ have the same populated states and register values.
Therefore, there exists $\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ such
that $\gamma\models\phi$ if and only if there exists
$\sigma\in\mathsf{Reach_{a}}(\mathsf{Init_{a}})$ such that
$\sigma\models\phi$: one can consider 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 -Completeness of the General Case

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

######  Proposition 3.1.

, , DNF-PRP and for roundless register protocols are all -complete.

######  Proof 3.2.

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

Let $\rho:\sigma_{0}$ an abstract execution, we simply prove the existence of
$\rho^{\prime}:\sigma_{0}$ of length at most $4|Q|$. To obtain $\rho^{\prime}$
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^{\prime}$, 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 , we can
look for an execution of length less than $4|Q|$ which can be guessed in
polynomial time.

$q_{0}$$C_{1}?$$C_{2}?$…$C_{m}?$$q_{f}$$\mathsf{Test}(l_{1,1})$$\mathsf{Test}(l_{1,2})$$\mathsf{Test}(l_{1,3})$$\mathsf{Test}(l_{m,1})$$\mathsf{Test}(l_{m,2})$$\mathsf{Test}(l_{m,3})$$\mathsf{Test}(l)$$:=$$\forall
j\in[1,n]$
$\mathsf{write}_{\mathsf{rg}(x_{j})}(\mathsf{T})$$\mathsf{write}_{\mathsf{rg}(\neg
x_{j})}(\mathsf{T})$$\forall
j\in[1,n]$$\mathsf{read}_{\mathsf{rg}(l)}(\mathsf{T})$$\mathsf{read}_{\mathsf{rg}(\neg
l)}(\mathsf{d}_{0})$

Figure 2: The protocol $(\phi)$ for -hardness of .

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

The proof is by a reduction from 3-. Consider a 3-CNF formula
$\phi=\bigwedge_{i=1}^{m}l_{i,1}\lor l_{i,2}\lor 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 $(\phi)$ with a distinguished state $q_{f}$ which is
coverable if and only if $\phi$ is satisfiable. In $(\phi)$, one has ${\rm
D}=\\{\mathsf{d}_{0},\mathsf{T}\\}$ and $\mathsf{dim}=2n$, there are two
registers for each variable $x_{i}$, $\mathsf{rg}(x_{i})$ and
$\mathsf{rg}(\neg x_{i})$. The protocol is represented on Figure 2.

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

Suppose that the instance of 3-is positive, _i.e._ , $\phi$ is satisfiable by
some assignment $\nu$. Consider an execution that writes $\mathsf{T}$ exactly
to all $\mathsf{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 is positive.
Conversely, if the instance is positive, there exists an execution
$\rho:\sigma_{0}$ with $\sigma_{0}\in\mathsf{Init_{a}}$ and
$q_{f}\in\mathsf{st}(\sigma)$. Consider $\nu$ that assigns to each variable
$x$ value true if $\mathsf{rg}(x)$ is written before $\mathsf{rg}(\neg x)$ in
$\rho$ and false otherwise. Given a litteral $l$, $\rho$ may only go through
$\mathsf{Test}(l)$ if $\nu(l)$ is true; because $\rho$ covers $q_{f}$, this
proves that $\nu\models\phi$.

######  Remark 3.6.

In [11], the authors prove -completeness of in a similar model, but with a
leader: in the -hardness reduction, the leader make non-determinstic 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 -complete, they are sometimes
tractable under appropriate restrictions on the protocols. We will consider
two restrictions on the protocols. The first one is having $\mathsf{dim}=1$,
_i.e._ , a single register. The second restriction is the _uninitialized case_
where processes are not allowed to read the initial value $\mathsf{d}_{0}$
from the registers. Formally, a protocol is _uninitialized_ if its set of
transitions $\Delta$ does not contain an action reading symbol
$\mathsf{d}_{0}$: in uninitialized protocols, it is structurally impossible to
read from an unwritten register. One might object that forbidding transitions
that read $\mathsf{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 $\mathsf{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 , the formula itself always makes the problem -hard.

######  Proposition 3.7.

for roundless register protocols is -hard even with $\mathsf{dim}=1$ and the
register uninitialized.

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

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

In [11, Theorem 9.2], uninitialized is proved to be -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 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 is tractable as well.

######  Proposition 3.8.

for roundless register protocols is -complete either when the registers are
uninitialized or when $\mathsf{dim}$ is fixed.

For DNF-PRP, we provide a algorithm in the more restrictive case of
$\mathsf{dim}=1$.

######  Proposition 3.9.

DNF-PRP for roundless register protocols with $\mathsf{dim}=1$ is in .

######  Proof 3.10 (Proof sketch).

We give here the proof for . 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 with $\mathsf{dim}=1$
to uninitialized with $\mathsf{dim}=1$. It proceeds as follows. Consider the
graph $G=(Q,E)$ when $(q_{1},q_{2})\in E$ when there exists
$(q_{1},\mathsf{read}(\mathsf{d}_{0}),q_{2})\in\Delta$. Let $I\subseteq Q$ the
set of states that are reachable in $G$ from $Q_{0}$. The reduction simply
replaces $Q_{0}$ by $I$ as set of initial states.

Any (abstract) execution $\rho:\sigma_{0}$, called _synchronizing execution_ ,
can be rearranged into $\rho_{+}:\sigma_{0}$ and $\rho_{-}:\langle\penalty
10000S,\mathsf{d}\penalty 10000\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 $\mathsf{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

$\displaystyle\mathcal{C}():=$ $\displaystyle\max\\{S\subseteq
Q\mid\exists\mathsf{d}\in{\rm
D},\,\exists\sigma_{0}\in\mathsf{Init_{a}},\,\sigma_{0}$
$\displaystyle\mathcal{BC}():=$ $\displaystyle\max\\{S\subseteq
Q\mid\forall\mathsf{d}\in{\rm D},\,\exists\mathsf{\mathsf{d}_{f}}\in{\rm
D},\,\langle\penalty 10000S,\mathsf{d}\penalty 10000\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}()$
corresponds to the set of coverable sets, and $\mathcal{BC}()$ to the set of
backward coverable states. In the decomposition $\rho_{+}:\sigma_{0}$,
$\rho_{-}:\langle\penalty 10000S,\mathsf{d}\penalty 10000\rangle$, $\rho_{+}$
is a witness that $S\subseteq\mathcal{C}()$ and $\rho_{-}$ that
$S\subseteq\mathcal{BC}()$ (because $\rho_{-}$ starts with a write action, for
every $\mathsf{d}^{\prime}\in{\rm D}$ one has $\langle\penalty
10000S,\mathsf{d}^{\prime}\penalty 10000\rangle$).

$\mathcal{C}()$ and $\mathcal{BC}()$ can be computed in polynomial time. For
$\mathcal{C}()$, we use a saturation technique. For $\mathcal{BC}()$, 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 ${\rm D}$, trying to pick the symbol that was in the register
before $S$ could be reached. For each $\mathsf{d}\in{\rm D}$, we saturate $S$
with backward transitions reading $\mathsf{d}$, then check if $\mathsf{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 states that are not in
$\mathcal{C}()\cap\mathcal{BC}()$. Indeed, states that are not in
$\mathcal{C}()\cap\mathcal{BC}()$ cannot appear in any synchronizing
execution. If it ends up with $Q()=\emptyset$, then there is no synchronizing
execution and the algorithm rejects. If it ends up with
$\mathcal{C}()=\mathcal{BC}()=Q()\neq\emptyset$, then applying the definitions
of $\mathcal{C}()$ and $\mathcal{BC}()$ gives a synchronizing execution, and
the algorithm accepts.

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

Unlike , and therefore DNF-PRP are not tractable under the uninitialized
hypothesis. For , 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
$\mathsf{r}$ can only be written from a given state $q$, the last process to
leave $q$ will fix the value in register $\mathsf{r}$.

######  Proposition 3.19.

for uninitialized roundless register protocols is -hard.

|  |  | DNF-PRP |
---|---|---|---|---
General case |  black!8-complete |  black!8-complete |  black!8 -complete |  black!8 -complete
black!8(Prop. 3.1 ) |  black!8(Prop. 3.1 ) |  black!8(Prop. 3.1 ) |  black!8(Prop. 3.1)
Uninitialized | -complete |  black!8 -complete |  black!8 -complete |  black!8 -complete
(Prop. 3.8) |  black!8(Prop. 3.1 & 3.19) |  black!8(Prop. 3.1 & 3.19) |  black!8(Prop. 3.1 & 3.7)
$\mathsf{dim}=1$ (one register) | -complete | -complete | -complete |  black!8 -complete
(Prop. 3.8) |  (Prop. 3.9 & 3.8) |  (Prop. 3.9 & 3.8) |  black!8(Prop. 3.1 & 3.7)
Figure 3: Summary of complexity results for roundless register protocols

##  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 . Thus, the abstract semantics developed here differs from [6].

###  4.1 Definitions

In round-based settings, there is a fresh set of $\mathsf{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 4.1 (Round-based register protocols).

A _round-based register protocol_ is a tuple $=\langle\penalty
10000Q,Q_{0},\penalty-1000\mathsf{dim},\penalty-1000{\rm
D},\penalty-1000\mathsf{d}_{0},\penalty-1000\mathsf{v},\Delta\penalty
10000\rangle$ where

  * •

$Q$ is a finite set of states with a distinguished subset of initial states
$Q_{0}\subseteq Q$;

  * •

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

  * •

${\rm D}$ is a finite data alphabet with an initial symbol $\mathsf{d}_{0}$;

  * •

$\mathsf{v}$ is the visibility range;

  * •

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

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

Let $\mathsf{rg}_{k}[\alpha]$ denote the register $\alpha$ of round $k$. The
set of registers of round $k$ is written $\mathsf{Reg}_{k}$, and we let
$\mathsf{Reg}=\bigcup_{k\in\mathds{N}}\mathsf{Reg}_{k}$. The size of a
protocol is $||=|Q|+|{\rm D}|+|\Delta|+\mathsf{v}+\mathsf{dim}$. A given
process is described by its state and round, formalized by a pair $(q,k)\in
Q\times\mathds{N}$ called _location_. Let $\mathsf{Loc}:=Q\times\mathds{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\penalty 10000\mu,\vec{d}\penalty
10000\rangle$ with $\mu\in\mathds{N}^{\mathsf{Loc}}$ such that
$0<\sum_{(q,k)\in\mathsf{Loc}}\mu(q,k)<\infty$ and $\vec{d}\in{\rm
D}^{\mathsf{Reg}}$. For $\gamma=\langle\penalty 10000\mu,\vec{d}\penalty
10000\rangle$, we write $\mathsf{loc}(\gamma):=\mu$ and
$\mathsf{data}(\gamma):=\vec{d}$. Again, we write $\Gamma$ for the set of
concrete configurations. The set of initial configurations is
$\mathsf{Init_{c}}:=\\{\gamma\in\Gamma\mid\mathsf{data}(\gamma)=\mathsf{d}_{0}^{\mathsf{Reg}}\text{
and }\forall(q,k)\notin Q_{0}\times\\{0\\},\,\mathsf{loc}(\gamma)(q,k)=0\\}$.

A _move_ is a pair $\theta\in\Delta\times\mathds{N}$: move $(\delta,k)$
expresses that transition $\delta$ is taken by a process at round $k$; we
write $\mathsf{Moves}:=\Delta\times\mathds{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^{\prime}),k)\in\mathsf{Moves}$, $\gamma$ when
$(q,k)\in\mathsf{loc}(\gamma)$ and:

  * •

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

  * •

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

  * •

if $a=\mathsf{Inc}$,
$\mathsf{loc}(\gamma^{\prime})=(\mathsf{loc}(\gamma)\ominus\\{(q,k)\\})\oplus\\{(q^{\prime},k{+}1)\\}$
and $\mathsf{data}(\gamma^{\prime})=\mathsf{data}(\gamma)$.

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

######  Example 4.3.

$q_{0}$$A$$B$$C$$D$$E$$q_{f}$$\mathsf{Inc}$$\mathsf{write}(\mathsf{a})$$\mathsf{read}^{-1}(\mathsf{d}_{0})$$\mathsf{read}^{-1}(\mathsf{a})$$\mathsf{write}(\mathsf{b})$$\mathsf{read}^{-1}(\mathsf{b})$$\mathsf{read}^{0}(\mathsf{d}_{0})$$\mathsf{read}^{0}(\mathsf{b})$

Figure 4: An example of round-based register protocol

Consider the round-based protocol from Figure 4, with $\mathsf{dim}=1$,
$\mathsf{v}=1$, $Q_{0}=\\{q_{0}\\}$ and ${\rm
D}=\\{\mathsf{d}_{0},\mathsf{a},\mathsf{b}\\}$. In this protocol, state
$q_{f}$ cannot be covered. By contradiction, consider an execution
$\pi:\gamma_{0}$ with $\gamma_{0}\in\mathsf{Init_{c}}$ and
$\mathsf{loc}(\gamma)(q_{f},k)>0$ fo some $k\in\mathds{N}$. We have that, at
some point in $\pi$, $(E,k)$ is populated and $\mathsf{b}$ is in
$\mathsf{rg}[k]$. Therefore, some process went from $(A,k)$ to $(B,k)$, which
implies that $\mathsf{rg}[k]$ lost value $\mathsf{d}_{0}$ before
$\mathsf{rg}[k{-}1]$; this in turn implies that $\pi$ does not send any
process to $(E,k)$ which is a contradiction.

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 . The set of _abstract configurations_ is
$\Sigma:=2^{\mathsf{Loc}}\times{\rm D}^{\mathsf{Reg}}$; the abstract semantics
are defined as in Subsection 2.3. Again, $\sigma$ if and only if there exist
$\gamma,\gamma^{\prime}\in\Gamma,\,\gamma$ and
$\mathsf{abst}(\gamma)=\sigma,\mathsf{abst}(\gamma^{\prime})=\sigma^{\prime}.$
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 4.7 (Soundness and completeness of the abstraction).

For all $L\subseteq\mathsf{Loc}$, $\vec{d}\in{\rm D}^{\mathsf{Reg}}$:

$(\exists\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}}{}):\mathsf{supp}(\gamma){=}L,\,\mathsf{data}(\gamma){=}\vec{d})\
\Longleftrightarrow\ \\\
(\exists\sigma\in\mathsf{Reach_{a}}(\mathsf{Init_{a}}{}):\
\mathsf{loc}(\sigma){=}L,\,\mathsf{data}(\sigma){=}\vec{d}).$

###  4.2 Presence Reachability Problem

is extended to round-based protocols by asking whether some reachable
configuration has a process on $q_{f}$ on some round $k$, and 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\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ such that $\gamma\models\psi$
where $\psi=$“$\exists k\in\mathds{N},(q,k)\in\mathsf{loc}(\gamma)$” for and
$\psi=$“$\forall k\in\mathds{N},\forall q\neq
q_{f},(q,k)\notin\mathsf{loc}(\gamma)$” for . We will now extend roundless to
round-based , 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 4.8.

“$(\exists k\,(q_{2},k)\mathrel{\mathsf{populated}})\lor(\forall
k\,((q_{0},k{+}2)\mathrel{\mathsf{populated}})\land\mathsf{rg}_{1}[1]\mathrel{\mathsf{contains}}\mathsf{a})$”
is an example of presence constraint.
Let $\gamma:=((q_{0},0)\oplus(q_{1},1),\mathsf{d}_{0}^{\mathsf{Reg}})$ with
$q_{0}\neq q_{1}$, $\mathsf{dim}=1$. One has
$\gamma\models(\mathsf{rg}_{0}[1]\mathrel{\mathsf{contains}}\nobreak\mathsf{d}_{0})\land(\exists
k\,(q_{1},k{+}1)\mathrel{\mathsf{populated}})$ but $\gamma\not\models\forall
k\,(((q_{0},k)\mathrel{\mathsf{populated}})\lor\neg((q_{1},k)\mathrel{\mathsf{populated}}))$.

We define the _round-based presence reachability problem_ (round-based ):

Round-based  Input: A round-based register protocol , a presence constraint
$\psi$ Question: Does there exist
$\gamma\in\mathsf{Reach_{c}}(\mathsf{Init_{c}})$ such that
$\gamma\models\psi$?

######  Example 4.9.

Consider from Example 4.3. If $\psi:=\exists
k,(q_{f},k)\mathrel{\mathsf{populated}}$, then $(,\psi)$ is a negative
instance of round-based . If $\psi^{\prime}:=\exists
k,((E,k)\mathrel{\mathsf{populated}})\allowbreak\land((E,k{+}1)\mathrel{\mathsf{populated}})$,
then $(,\psi^{\prime})$ is also negative. However, if
$\psi^{\prime\prime}:=((E,2)\mathrel{\mathsf{populated}})\allowbreak\land[\forall
k,(\mathsf{rg}[k+1]\mathrel{\mathsf{contains}}\mathsf{b})\lor(\mathsf{rg}[k+1]\mathrel{\mathsf{contains}}\mathsf{d}_{0})]$,
then $(,\psi^{\prime\prime})$ is positive: a witness execution sends a process
to $(B,1)$, writes $\mathsf{a}$ to $\mathsf{rg}[0]$ then $\mathsf{b}$ to
$\mathsf{rg}[1]$ and finally sends a process from $(q_{0},2)$ to $(E,2)$.

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

######  Proposition 4.10 ([6, Theorem 23]).

for round-based register protocols is -hard, even in the uninitialized case
with $\mathsf{v}=0$ and $\mathsf{dim}=1$.

Note that, in the round-based setting, $\mathsf{dim}=1$ means one register
_per round_ , therefore still an unbounded number of registers. $\mathsf{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
-hard when working with round-based protocols. In [6], for round-based
register protocols is shown to be -complete. In the rest of this paper, we
establish that the more general round-based lies in the same complexity class:

######  Theorem 4.11.

Round-based is -complete.

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

In this section, we provide a polynomial-space algorithm for round-based .
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 2.33, round-based 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\leq k$. We write $\mathsf{Loc}{[j,k]}$ for the set of locations at
rounds $\max(j,0)$ to $k$; similarly, we write $\mathsf{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^{\mathsf{Loc}{[j,k]}}\times{\rm
D}^{\mathsf{Reg}{[j,k]}}$. The set of local configurations on $[j,k]$ is
written $\mathsf{\Sigma}{[j,k]}$. Given $\sigma\in\Sigma$, the local
configuration $\mathsf{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^{\prime}\in\mathsf{\Sigma}{[j,k]}$ and a move $\theta$,
we write $\lambda$ when there exist two configurations $\sigma$ and
$\sigma^{\prime}$ such that $\sigma$, $\mathsf{local}{[j,k]}(\sigma)=\lambda$
and $\mathsf{local}{[j,k]}(\sigma^{\prime})=\lambda^{\prime}$. In practice:

  * •

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

  * •

if $\theta=((q,\mathsf{Inc},q^{\prime}),j{-}1)$ then $\lambda$ holds with no
condition that $(q,j{-}1)$ is populated in $\lambda$, since $j{-}1$ is outside
of $[j,k]$;

  * •

if $\theta=((q,\mathsf{read}_{\alpha}^{-b}(\mathsf{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\mathsf{\Sigma}{[j,k]}$ and for all $i\leq
m-1$, $\lambda_{i}$ and $\lambda_{i}\neq\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
$\mathsf{footprint}{[j,k]}(\rho)$, is the footprint on $[j,k]$ obtained from
$\rho$ by replacing $\sigma_{i}$ by
$\lambda_{i}=\mathsf{local}{[j,k]}(\sigma_{i})$ and then removing all useless
steps $\lambda_{i}$ with $\lambda_{i}=\lambda_{i{+}1}$ (by merging
$\lambda_{i}$ and $\lambda_{i{+}1}$, so $\mathsf{footprint}{[j,k]}(\rho)$ can
be shorter than $\rho$). Similarly, for
$[j^{\prime},k^{\prime}]\supseteq[j,k]$ and $\tau$ a footprint on
$[j^{\prime},k^{\prime}]$, define the _projection_
$\mathsf{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 5.7.

Let $K\in\mathds{N}$, $(\tau_{k})_{k\leq K}$ and $(T_{k})_{k\leq K{-}1}$ such
that:

  * •

for all $k\leq K$, $\tau_{k}$ is a footprint on $[k{-}\mathsf{v}{+}1,k]$,

  * •

for all $k\leq K{-}1$, $T_{k}$ is a footprint on $[k{-}\mathsf{v}{+}1,k{+}1]$,

  * •

for all $k\leq K{-}1$,
$\mathsf{footprint}{[k{-}\mathsf{v}{+}1,k]}(T_{k})=\tau_{k}$,

  * •

for all $k\leq K{-}1$,
$\mathsf{footprint}{[k{-}\mathsf{v}{+}2,k{+}1]}(T_{k})=\tau_{k{+}1}$.

There exists an execution $\rho$ such that, for all $k\leq K$,
$\mathsf{footprint}{[k{-}\mathsf{v}{+}1,k]}(\rho)=\tau_{k}$.

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

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 $\mathsf{v}\geq
1$. If $\mathsf{v}=0$, we artificially increase $\mathsf{v}$ to $1$.

1 Input: A instance $(,\psi)$

2 $E,U,C\shortleftarrow\emptyset$ ;

$\tau\shortleftarrow\epsilon$ ;

// dummy footprint on rounds $[-\mathsf{v},-1]$

3 Guess the initial set $I\subseteq Q_{0}$ of populated states at round $0$ ;

4 NDInit(_$E,U,C$_) ;

5 for  _$k$ from $0$ to $+\infty$ _ do

6 Guess $T$ a footprint on $[k{-}\mathsf{v},k]$ such that
$\mathsf{footprint}{[k{-}\mathsf{v},k{-}1]}(T)=\tau$ ;

7 Check that $T$ is consistent with the initial configuration ;

8 $\lambda\shortleftarrow$ last configuration in $T$ ;

9 NDComputeIteration(_$E,U,C,\lambda$_) ;

10 if  _TestPresenceConstraint(_$E,U,C,\lambda$_) _ then Accept ;

11 $\tau\shortleftarrow\mathsf{footprint}{[k{-}\mathsf{v}{+}1,k]}(T)$ ;

12

Algorithm 1 Non-deterministic algorithm for round-based

For all $k\in\mathds{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 5.7, if the algorithm reaches the end of iteration $K$ then
there exists an execution $\rho$ whose projection on $[k{-}\mathsf{v},k-1]$ is
$\tau_{k}$ for every $k\leq 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 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 :

######  Proposition 5.8.

$(,\psi)$ is a positive instance of round-based if and only if there exists an
accepting computation of Algorithm 1 on $(,\psi)$.

The integer constants in the presence constraint $\psi$ are encoded in unary,
like the visibility range $\mathsf{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 5.9.

Algorithm 1 works in space
$O(|\psi|^{3}+|Q|^{2}\,(\mathsf{v}{+}1)^{2}\,\log(\mathsf{dim}\,|{\rm 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 5.9, correctness from Proposition
5.8 and the stopping criterion, our algorithm decides round-based in non-
deterministic polynomial space, proving Theorem 4.11.

##### 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.
  * [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

##  Appendix A Roundless Register Protocols

Recall that the abstract semantics is non-deterministic due to the choice
between
$\mathsf{st}(\gamma^{\prime})=(\mathsf{st}(\gamma)\setminus\\{q\\})\cup\\{q^{\prime}\\}$
and $\mathsf{st}(\gamma^{\prime})=\mathsf{st}(\gamma)\cup\\{q^{\prime}\\}$.
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^{\prime})$, state $q$ is called the
_source_ and state $q^{\prime}$ is called the _destination_ of the transition,
and similarly for a step.

###  A.1 Proof of Proposition 2.23

See 2.23

######  Proof A.1.

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}$ and suppose that the property is true for all executions of
length $|\pi|-1$. Decompose $\pi$ into $\gamma_{1}$. If $q_{2}$ is not the
destination of $\delta$, then $q_{2}\in\mathsf{supp}(\gamma_{3})$ and we
directly apply the induction hypothesis on $\gamma_{1}$ and $q_{2}$ then
conclude by taking $\delta$ to get to $\langle\penalty
10000\mathsf{st}(\gamma_{2})\oplus q_{2},\mathsf{data}(\gamma_{2})\penalty
10000\rangle$. Assume that $q_{2}$ is the destination of $\delta$; let $q_{3}$
the source of $\delta$. We have $q_{3}\in\mathsf{supp}(\gamma_{3})$, so we
apply the induction hypothesis on $\gamma_{1}$ and $q_{3}$: we obtain that
there exists $q_{1}\in\mathsf{supp}(\gamma_{1})$ such that $\langle\penalty
10000\mathsf{st}(\gamma_{1})\oplus q_{1},\mathsf{data}(\gamma_{3})\penalty
10000\rangle$ Moreover, we have $\langle\penalty
10000\mathsf{st}(\gamma_{3})\oplus q_{3},\mathsf{data}(\gamma_{2})\penalty
10000\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 2.33

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

######  Lemma A.10.

Let $\gamma,\gamma^{\prime}\in\Gamma$ and $\pi:\gamma$. There exists
$\rho:\mathsf{abst}(\gamma)$.

######  Proof A.13.

By induction, it suffices to prove it for one step; suppose that $\gamma$. Let
$(q,a,q^{\prime}):=\delta$; if $q\in\mathsf{st}(\gamma^{\prime})$, then we
consider the non-deserting abstract step with transition $\delta$, otherwise
we consider the deserting step with transition $\delta$. Either way, we have
$\mathsf{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.16.

Let $\sigma,\sigma^{\prime}\in\Sigma$ and $\rho:\sigma$. There exist
$\gamma,\gamma^{\prime}$ such that $\mathsf{abst}(\gamma)=\sigma$,
$\mathsf{abst}(\gamma^{\prime})=\sigma^{\prime}$ and $\pi:\gamma$.

######  Proof A.19.

The proof is by induction on the number of steps in $\pi$. If $\pi$ has $0$
steps, then $\sigma=\sigma^{\prime}$ and suffices to consider
$\gamma=\gamma^{\prime}:=\langle\penalty
10000\bigoplus_{q\in\mathsf{st}(\sigma)}q,\mathsf{data}(\sigma)\penalty
10000\rangle$.

Assume that $\rho:\sigma_{1}$ and that the property is true for executions
shorter than $\rho$. By induction hypothesis, there exists $\pi:\gamma_{1}$
such that $\mathsf{abst}(\gamma_{1})=\sigma_{1}$,
$\mathsf{abst}(\gamma_{2})=\sigma_{2}$. There exists $\gamma_{3}$ such that
$\gamma_{2}$; 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.10 and A.16 together prove Proposition 2.33.

###  A.3 Proof of Proposition 3.8

See 3.8

####  A.3.1 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$ such that $(q_{1},a,q_{2})\in\Delta$ and:

  * •

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

  * •

or $a=\mathsf{read}_{\alpha}(\mathsf{d})$ with $\alpha,\mathsf{d}$ s.t. there
exist $q_{3},q_{4}\in S$,
$(q_{3},\mathsf{write}_{\alpha}(\mathsf{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},\mathsf{write}_{\alpha}(\mathsf{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$, $\mathsf{d}\in{\rm
D}\setminus\\{\mathsf{d}_{0}\\}$, $\alpha\in[1,\mathsf{dim}]$ such that
$(q_{1},\mathsf{read}_{\alpha}(\mathsf{d}),q_{2}),(q_{3},\mathsf{write}_{\alpha}(\mathsf{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 $\mathsf{d}$
to $\mathsf{rg}[\alpha]$ again, so that a process in state $q_{1}$ may read
$\mathsf{d}$ from register $\mathsf{rg}[\alpha]$ and get to $q_{2}$, which is
therefore coverable.

####  A.3.2 when the Number of Registers $\mathsf{dim}$ is Fixed

The first write to a register is an irreversible action, as $\mathsf{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 $\mathsf{r}_{1},\dots,\mathsf{r}_{m}$
($m\leq\mathsf{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},\mathsf{read}_{\mathsf{r}}(\mathsf{d}_{0}),q_{2})$ and
$\mathsf{r}\notin\\{\mathsf{r}_{1},\dots,\mathsf{r}_{i}\\}$,

  * •

there exists $q_{1}\in S$ with
$(q_{1},\mathsf{write}_{\mathsf{r}_{j}}(\mathsf{d}),q_{2})$, $j\leq i$,

  * •

there exists $q_{1}\in S$ with
$(q_{1},\mathsf{read}_{\mathsf{r}_{j}}(\mathsf{d}),q_{2})$, $j\leq i$, and
$\mathsf{d}$ may be written to $\mathsf{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
$\mathsf{r}_{1},\dots,\mathsf{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 $\mathsf{r}_{1},\dots,\mathsf{r}_{m}$. Observe that, if two executions
share a first-write order $\mathsf{r}_{1},\dots,\mathsf{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 -hardness

The proof is similar to the one presented in [9, Proposition 1] for broadcast
protocols. It uses a -reduction for the Circuit Value Problem, which is
-complete for 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 $\lor$ and conjunctions $\land$.

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)$, $(\lor,i_{1},i_{2},o)$ or
$(\land,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 $(_{\textsc{CVP}},q_{f})$
of with $\mathsf{dim}=1$. In ${\rm D}$, we have $\mathsf{d}_{0}$ (which is
never read) along with, for every $v\in V$, symbols $v=\mathsf{T}$ and
$v=\mathsf{F}$, denoting that $v$ is respectively true and false. First,
${}_{\textsc{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 $(\land,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.

$\mathsf{read}(i_{1}=\mathsf{F})$$\mathsf{read}(i_{2}=\mathsf{F})$$\mathsf{write}(o=\mathsf{F})$$\mathsf{read}(i_{1}=\mathsf{T})$$\mathsf{read}(i_{2}=\mathsf{T})$$\mathsf{write}(o=\mathsf{T})$
Figure 5: Part of the protocol ${}_{\textsc{CVP}}$ that corresponds to gate
$(\land,i_{1},i_{2},o)$

###  A.4 Proof of Proposition 3.9

See 3.9

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

######  Lemma A.24.

There exists a polynomial-time reduction from initialized DNF-PRP with
$\mathsf{dim}=1$ to uninitialized DNF-PRP with $\mathsf{dim}=1$.

######  Proof A.25.

Let $=\langle\penalty 10000Q,Q_{0},\penalty-10001,\penalty-1000{\rm
D},\penalty-1000\mathsf{d}_{0},\Delta\penalty 10000\rangle$ a roundless
register protocol with a single register. Any execution will be composed of
two phases: the phase where the register has value $\mathsf{d}_{0}$ and no
write transition is taken and the phase where the register no longer has value
$\mathsf{d}_{0}$ and write transitions may be taken. The reduction relies on
the observation that, in the first phase, only transitions labeled by
$\mathsf{read}(\mathsf{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
$\mathsf{read}(\mathsf{d}_{0})$.

Consider the graph $G=(Q,E)$ whose vertices are the states of the system and
whose edges are the transitions labeled by $\mathsf{read}(\mathsf{d}_{0})$:
$(q_{1},q_{2})\in E$ if and only if
$(q_{1},\mathsf{read}(\mathsf{d}_{0}),q_{2})\in\Delta$. Let
$Q_{0}^{\prime}:=\\{q\in Q\mid\exists m\geq 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}^{\prime}$ can
trivially be computed in polynomial time. Additionally, let
$\Delta^{\prime}:=\Delta\setminus\\{(q,\mathsf{read}(\mathsf{d}_{0}),q^{\prime})\mid
q,q^{\prime}\in Q\\}$. The reduction maps to the protocol
${}^{\prime}=\langle\penalty
10000Q,Q_{0}^{\prime},\penalty-10001,\penalty-1000{\rm
D},\penalty-1000\mathsf{d}_{0},\Delta^{\prime}\penalty 10000\rangle$.

We now prove that $(,\psi)$ is a positive instance of DNF-PRP if and only if
$(^{\prime},\psi)$ is. First, suppose that, in , there exists
$\rho:\sigma_{0}$ such that $\sigma\models\psi$. We decompose $\rho$ into
$\rho_{p}:\sigma_{0}$ and $\rho_{s}:\sigma_{1}$ where
$\mathsf{data}(\sigma_{1})(\mathsf{r})=\mathsf{d}_{0}$ and $\rho_{s}$ either
is the empty execution or starts with a write transition. $\rho_{p}$ only uses
transitions labeled by $\mathsf{read}(\mathsf{d}_{0})$ therefore, for every
$q\in\mathsf{st}(\sigma_{1})$, there exists a path in $G$ from $Q_{0}$ to $q$;
this proves that $\mathsf{st}(\sigma_{1})\subseteq Q_{0}^{\prime}$ and
therefore that $\sigma_{1}$ is initial for ′, moreover $\rho_{s}$ does not use
transitions labeled by $\mathsf{read}(\mathsf{d}_{0})$ hence $\rho_{s}$ is a
witness that $(^{\prime},\psi)$ is positive.

Suppose now that $(^{\prime},\psi)$ is positive. There exists
$\rho:\sigma_{0}$ with $\sigma\models\psi$. For every
$q\in\mathsf{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:=(\mathsf{st}(\sigma_{0})\cap Q_{0})\cup f(\mathsf{st}(\sigma_{0})\setminus
Q_{0})$, we have $S\subseteq Q_{0}$. We have that $\langle\penalty
10000S,\mathsf{d}_{0}\penalty 10000\rangle$ in by only taking transitions
appearing in $G$. Therefore $\langle\penalty 10000S,\mathsf{d}_{0}\penalty
10000\rangle$ with $\sigma\models\psi$ and $\langle\penalty
10000S,\mathsf{d}_{0}\penalty 10000\rangle$ is initial for , which proves that
$(,\psi)$ is positive.

Thanks to the previous lemma, we prove Proposition 3.9 in the uninitialized
case. Consider a instance $(,\psi)$ of DNF-PRP where is uninitialized and
$\mathsf{dim}=1$. $(,\psi)$ is positive if and only if $(,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
${\rm D}_{\mathsf{ok}}(C)$ the symbols that are allowed in the final
configuration. Formally,
$Q_{+}(C):=\\{q\mid\text{``$q\mathrel{\mathsf{populated}}$''}\in C\\}$,
$Q_{-}(C):=\\{q\mid\text{``$\neg(q\mathrel{\mathsf{populated}})$''}\in C\\}$
and ${\rm D}_{\mathsf{ok}}(C):=\\{\mathsf{d}\in{\rm
D}\mid\text{``$\neg(\mathsf{r}\mathrel{\mathsf{contains}}\mathsf{d})$''}\notin
C\text{ and
}\forall\mathsf{d}^{\prime}\neq\mathsf{d},\,\text{``$\mathsf{r}\mathrel{\mathsf{contains}}\mathsf{d}^{\prime}$''}\notin
C\\}$ where $\mathsf{r}$ denotes the register. For all $\langle\penalty
10000S,\mathsf{d}\penalty 10000\rangle\in\Sigma$, $\langle\penalty
10000S,\mathsf{d}\penalty 10000\rangle\models C$ if and only if
$Q_{+}(C)\subseteq S\subseteq Q\setminus Q_{-}(C)$ and $\mathsf{d}\in{\rm
D}_{\mathsf{ok}}(C)$. Let

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

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

######  Lemma A.32.

Any execution $\rho:\sigma_{0}$ with $\sigma_{0}\in\mathsf{Init_{a}}$ may be
decomposed in the following form: $\sigma_{0}$ with $S$ containing all states
appearing in $\rho$.

######  Proof A.36.

Let $\rho:\sigma_{0}$; let $\langle\penalty
10000S_{f},\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle:=\sigma$. The
execution $\sigma_{0}$ 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^{\prime}:\langle\penalty
10000S,\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle$ that is obtained by
mimicking steps of $\rho$ starting from $\langle\penalty
10000S,\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle$. First, is uninitialized
therefore $\rho$ starts with a write and the register value at the beginning
of $\rho$ is irrelevant. Moreover, $\mathsf{st}(\sigma_{0})\subseteq S$ by
definition of $S$, so that $\rho^{\prime}$ starts from a configuration with
more states that $\rho$. By induction, for all $n\geq 1$, the $n$-th
configuration in $\rho^{\prime}$ 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}^{\prime}$. 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^{\prime}$ which shows
that $S_{f}^{\prime}\subseteq S_{f}$. In the end, $\rho^{\prime}$ goes from
$\langle\penalty 10000S,\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle$ to
$\langle\penalty 10000S_{f},\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle$
which concludes the proof.

We define the following two sets:

  * •

$\mathcal{C}():=\max\\{S\subseteq
Q\mid\exists\sigma_{0}\in\mathsf{Init_{a}},\exists\mathsf{d}\in{\rm
D},\,\sigma_{0}$,

  * •

$\mathcal{BC}(,C)=\max\\{S\subseteq Q\mid\forall\mathsf{d}\in{\rm
D},\exists\mathsf{\mathsf{d}_{f}}\in{\rm D}_{\mathsf{ok}}(C),{\exists
S_{f}\in\mathcal{F}(C),\,\langle\penalty 10000S,\mathsf{d}\penalty
10000\rangle\step{*}\langle\penalty 10000S_{f},\mathsf{\mathsf{d}_{f}}\penalty
10000\rangle}\\}$.

where the $\max$ is for inclusion of sets. Note that for $S\subseteq Q$, it is
equivalent that $S$ satisfies the condition $\forall\mathsf{d}\in{\rm
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\penalty
10000S,\mathsf{d}\penalty 10000\rangle$ with $\mathsf{d}\in{\rm D}$. By
convention, we consider that $\max(\emptyset)=\emptyset$, _i.e._ , if
$Q_{0}=\emptyset$ then $\mathcal{C}(,C)=\emptyset$ and if $Q_{-}(,C)=Q$ then
$\mathcal{BC}(,C)=\emptyset$.

We first prove that both maxima are well-defined because the sets considered
are stable under union. Let
$\sigma_{0},\sigma_{0}^{\prime}\in\mathsf{Init_{a}}$, $\rho:\sigma_{0}$,
$\rho^{\prime}:\sigma^{\prime}_{0}$. We show that we can merge $\rho$ and
$\rho^{\prime}$ into a single execution $\langle\penalty
10000\mathsf{st}(\sigma_{0})\cup\mathsf{st}(\sigma_{0}^{\prime}),\mathsf{d}_{0}\penalty
10000\rangle$. By mimicking $\rho$ (without deserting states from
$\mathsf{st}(\sigma_{0}^{\prime})$), we obtain an execution $\langle\penalty
10000\mathsf{st}(\sigma_{0})\cup\mathsf{st}(\sigma_{0}^{\prime}),\mathsf{d}_{0}\penalty
10000\rangle$. By mimicking $\rho^{\prime}$, we obtain an execution
$\langle\penalty 10000S\cup\mathsf{st}(\sigma_{0}^{\prime}),\mathsf{d}\penalty
10000\rangle$ (because is uninitialized, $\rho^{\prime}$ starts with a write).
Therefore $S\cup S^{\prime}$ is in the set $\\{S\subseteq
Q\mid\exists\sigma_{0}\in\mathsf{Init_{a}},\exists\mathsf{d}\in{\rm
D},\,\sigma_{0}$, proving that it is closed under union.

For $\mathcal{BC}(,C)$, we suppose that we have $S,S^{\prime}\subseteq Q$ that
satisfy the condition of the set, and we prove that $S\cup S^{\prime}$ does as
well. Let $\mathsf{d}\in{\rm D}$. By hypothesis on $S$ applied with
$\mathsf{d}$, there exist $S_{f}$, $\mathsf{\mathsf{d}_{f}}$ such that
$\langle\penalty 10000S,\mathsf{d}\penalty 10000\rangle$, and therefore
$\langle\penalty 10000S\cup S^{\prime},\mathsf{d}\penalty 10000\rangle$. By
hypothesis on $S^{\prime}$ applied with $\mathsf{\mathsf{d}_{f}}$, there exist
$S_{f}^{\prime}$, $\mathsf{\mathsf{d}_{f}}^{\prime}$ such that
$\langle\penalty 10000S^{\prime},\mathsf{\mathsf{d}_{f}}\penalty
10000\rangle$. Therefore we also have $\langle\penalty 10000S_{f}\cup
S^{\prime},\mathsf{\mathsf{d}_{f}}\penalty 10000\rangle$, which combined with
the previous execution provides a witness that $S\cup S^{\prime}$ is in the
set.

1 Function  _DNFPRP_Oneregister_Uninit(__)_ :

2 for  _$C$ clause of $\psi$_ do

${}_{C}\shortleftarrow$ ;

// copy of that will be modified

3 Until  _$Q(_{C})$_ reaches a fixpoint do

$Q(_{C})\shortleftarrow Q(_{C})\cap\mathcal{C}(_{C})\cap\mathcal{BC}(_{C},C)$
;

// modifies C

4

5 if  _$Q_{+}(C)\subseteq Q(_{C})\neq\emptyset$_ then Accept;

6

7 Reject ;

8

9Function  _Compute_ $\mathcal{C}()$_:

10 $S\shortleftarrow Q_{0}$ ;

11 Until  _$S$_ reaches a fixpoint do

12 $S\shortleftarrow S\cup\\{q^{\prime}\mid\exists q\in
S,\exists\mathsf{d}\in{\rm
D},\,(q,\mathsf{write}(\mathsf{d}),q^{\prime})\in\Delta\\}$ ;

13 $S\shortleftarrow S\cup\\{q^{\prime}\mid\exists q,q_{1},q_{2}\in
S,\exists\mathsf{d},\,(q,\mathsf{read}(\mathsf{d}),q^{\prime})\in\Delta,(q_{1},\mathsf{write}(\mathsf{d}),q_{2})\in\Delta\\}$
;

14

15 return $S$ ;

16

17Function  _Compute_ $\mathcal{BC}(,C)$_:

18 if  _PreviousSymbol(_$Q\setminus Q_{-}(C),{\rm D}_{\mathsf{ok}}$_) $\neq$
“Not found”_ then $S\shortleftarrow$PreviousSymbol(_$Q\setminus Q_{-}(C),{\rm
D}_{\mathsf{ok}}$_);

19 else return $\emptyset$ ;

20 Until  _$S$_ reaches a fixpoint do

21 if  _PreviousSymbol(_$S,{\rm D}\setminus\\{\mathsf{d}_{0}\\}$_)$\neq$“Not
found”_ then

22 $S\shortleftarrow$PreviousSymbol(_$S,{\rm
D}\setminus\\{\mathsf{d}_{0}\\}$_) ;

23

24 return $S$;

25

26Function  _PreviousSymbol(_$S,\mathsf{Symbols}$_)_:

27 $\mathsf{Found}\shortleftarrow\mathsf{False}$ ;

28 for  _$\mathsf{d}\in\mathsf{Symbols}$_ do

29 $T\shortleftarrow S$;

30 Until  _$T$_ reaches a fixpoint do

31 $T\shortleftarrow T\cup\\{q\in Q\mid\exists q^{\prime}\in
T,(q,\mathsf{read}(\mathsf{d}),q^{\prime})\in\Delta\\}$ ;

32

33 if  _there exist $q\in Q$, $q^{\prime}\in T$ s.t.
$(q,\mathsf{write}(\mathsf{d}),q^{\prime})\in\Delta$_ then

34 $S\shortleftarrow T\cup\\{q\\}$ ;

35 $\mathsf{Found}\shortleftarrow\mathsf{True}$ ;

36

37 if  _$\mathsf{Found}$_ then return $S$ else return “Not found” ;

38

Algorithm 2 A polynomial-time algorithm for DNF-PRP with $\mathsf{dim}=1$

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

First, we prove that Compute_$\mathcal{C}()$ returns $\mathcal{C}()$. By
induction, any state added in $S$ in Compute_$\mathcal{C}()$ are in
$\mathcal{C}()$. Indeed, any state that can be covered from a state in
$\mathcal{C}()$ using a write transition is in $\mathcal{C}()$. Similarly, any
state that can be covered from a state in $\mathcal{C}()$ using a read
transition which symbol may be written from $\mathcal{C}()$ is in
$\mathcal{C}()$: first write the corresponding value then read it (all states
of $\mathcal{C}()$ can be covered in a single, common execution). Conversely,
for any execution $\rho:\sigma_{0}$, 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
$\mathsf{st}(\sigma_{0})\subseteq Q_{0}$. Let $\mathsf{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
2 of the iteration and the corresponding destination state is added to $S$.
This write transition is now a witness for $\mathsf{d}$ at line 2, allowing
every read transition appearing in the phase to be detected in this iteration.

We now claim that Compute_$\mathcal{BC}(,C)$ returns $\mathcal{BC}(,C)$. If
$S$ satisfies the condition in $\mathcal{BC}(,C)$ then one can go from
$\langle\penalty 10000S,*\penalty 10000\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
${\rm D}_{\mathsf{ok}}$ as the last configuration satisfies $C$. Therefore, by
induction, all states appearing in such an execution appear in some
PreviousSymbol computation in Compute_$\mathcal{BC}(,C)$, and the states
returned include all states of the execution. Conversely, given a computation
of Compute_$\mathcal{BC}(,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_$\mathcal{BC}(,C)$
computes $\mathcal{BC}(,C)$.

We will now prove that DNFPRP_Oneregister_Uninit of Algorithm 2 solves DNF-PRP
for uninitialized protocols with $\mathsf{dim}=1$. First, suppose that the
algorithm accepts during the iteration corresponding to clause $C$. It ends
with a protocol C such that $Q_{+}(C)\subseteq
Q(_{C})=\mathcal{C}(_{C})\cap\mathcal{BC}(_{C},C)$. In this protocol, there
exist $\sigma_{0}\in\mathsf{Init_{a}}$ and $\mathsf{d}\in{\rm D}$ such that
$\sigma_{0}$; since $\mathcal{C}(_{C})=\mathcal{BC}(_{C},C)$ we also have
$\langle\penalty 10000\mathcal{C}(_{C}),\mathsf{d}\penalty 10000\rangle$ 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}$ with $\mathsf{\mathsf{d}_{f}}\in{\rm
D}_{\mathsf{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}(_{C})\cap\mathcal{BC}(_{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 3.19

See 3.19

Once again, we provide a reduction from 3-. Consider a 3-CNF formula
$\phi=\bigwedge_{i=1}^{m}l_{i,1}\lor l_{i,2}\lor 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 an instance of the uninitialized $((\phi),q_{f})$ which is positive
if and only if $\phi$ is satisfiable. Let $\mathsf{dim}:=n$, _i.e._ , the
protocol has a register $\mathsf{rg}[i]$ for each $i\in[1,n]$. Each register
can have values $\mathsf{T}$ and $\mathsf{F}$ (along with $\mathsf{d}_{0}$
which cannot be read nor written). A depiction of the protocol can be found in
Figure 6.

$q_{0}$$C_{1}?$$C_{2}?$…$C_{m}?$$q_{f}$$\mathsf{Test}(l_{1,1})$$\mathsf{Test}(l_{1,2})$$\mathsf{Test}(l_{1,3})$$\mathsf{Test}(l_{m,1})$$\mathsf{Test}(l_{m,2})$$\mathsf{Test}(l_{m,3})$$\mathsf{Test}(x_{j})$$\mathsf{Test}(\neg
x_{j})$$:=$$:=$$\forall j\in[1,n]$
$\mathsf{write}_{\mathsf{rg}[j]}(\mathsf{T})$$\mathsf{write}_{\mathsf{rg}[j]}(\mathsf{F})$
$\forall
j\in[1,n]$$\mathsf{read}_{\mathsf{rg}[j]}(\mathsf{T})$$\mathsf{read}_{\mathsf{rg}[j]}(\mathsf{F})$

Figure 6: The protocol $(\phi)$ for -hardness of uninitialized .

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)})=\mathsf{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 $\mathsf{Test}(l_{i,k(i)})$. This
execution goes from $\langle\penalty
10000q_{0},\mathsf{d}_{0}^{\mathsf{Reg}}\penalty 10000\rangle$ to
$\langle\penalty 10000q_{f},\vec{d}_{f}\penalty 10000\rangle$ hence the
instance of is positive. Conversely, suppose that there exists such an
execution $\rho:\sigma_{0}$. 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)})=\mathsf{true}$, proving
that $\phi$ is satisfied by $\nu$.

##  Appendix 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\mathds{N}$ and
$k$ a free variable. An _atomic proposition_ is either of the form
“$(q,t)\mathrel{\mathsf{populated}}$” with $t$ a term and $q\in Q$ or of the
form “$\mathsf{rg}_{t}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}$” with $t$
a term, $\alpha\in[1,\mathsf{dim}]$ and $\mathsf{d}\in{\rm 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 5.7

We prove the following, more general statement.

######  Lemma B.1.

Let $K\in\mathds{N}$, $w\geq\mathsf{v}{-}1$, $(\tau_{k})_{k\leq K}$ and
$(T_{k})_{k\leq K{-}1}$ such that:

  * •

for all $k\leq K$, $\tau_{k}$ is a footprint on $[k{-}w,k]$,

  * •

for all $k\leq K{-}1$, $T_{k}$ is a footprint on $[k{-}w,k{+}1]$,

  * •

for all $k\leq K{-}1$, $\mathsf{footprint}{[k{-}w,k]}(T_{k})=\tau_{k}$,

  * •

for all $k\leq K{-}1$,
$\mathsf{footprint}{[k{-}w{+}1,k{+}1]}(T_{k})=\tau_{k}$.

There exists an execution $\rho$ such that, for all $k\leq K$,
$\mathsf{footprint}{[k{-}w,k]}(\rho)=\tau_{k}$.

We start by proving the following lemma:

######  Lemma B.2.

Let $w\geq\mathsf{v}$, $k\in\mathds{N}$, $\tau_{-}$ a footprint on $[k{-}w,k]$
and $\tau_{+}$ a footprint on $[k{-}w{+}1,k{+}1]$ such that
$\mathsf{footprint}{[k{-}w{+}1,k]}(\tau_{-})=\mathsf{footprint}{[k{-}w{+}1,k]}(\tau_{+})$.
There exists $T$ a footprint on $[k{-}w,k{+}1]$ such that
$\mathsf{footprint}{[k{-}w,k]}(T)=\tau_{-}$ and
$\mathsf{footprint}{[k{-}w{+}1,k{+}1]}(T)=\tau_{+}$.

######  Proof B.3.

Let
$\tau_{com}:=\mathsf{footprint}{[k{-}w{+}1,k]}(\tau_{-})=\mathsf{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\geq\mathsf{v}$.

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
$\mathsf{footprint}{[k{-}w,k]}(t)=t_{-}$ and
$\mathsf{footprint}{[k{-}w{+}1,k{+}1]}(t)=t_{+}$. By applying the property for
$m=0$, there exists $s$ such that $\mathsf{footprint}{[k{-}w,k]}(s)=s_{-}$ and
$\mathsf{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.

We now prove Lemma B.1. 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\leq K{+}1}$, $(T_{k})_{k\leq K}$ satisfying the hypothesis. For
all $k\leq 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.2 applied with
$w^{\prime}:=w{+}1$ and $k^{\prime}:=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^{\prime}:=K{-}1$, there exists an execution
$\rho$ such that, for all $k\leq K$,
$\mathsf{footprint}{[k{-}w,k{+}1]}(\rho)=T_{k}$; this implies that, for all
$k\leq K{+}1$, $\mathsf{footprint}{[k{-}w,k]}(\rho)=\tau_{k}$, concluding the
proof of Lemma B.1. Applying Lemma B.1 with $w:=\mathsf{v}{-}1$ gives Lemma
5.7.

###  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 $\mathsf{APC(\psi)}$ for the set
containing all _atomic presence constraints_ in $\psi$ as well as their
negations. For $\phi$ a closed proposition, we write $\mathsf{AP}(\phi)$ for
the set of _atomic propositions_ in $\phi$. Given a set $S$ of propositions or
presence constraints, we write $\mathsf{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$.

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

\begin{picture}(0.0,0.0)\put(0.0,1.1){\put(0.0,0.0){\put(-0.05,-1.18){}}}\end{picture}

1 Function  _NDInit(_$E,U,C$_) _:

/* Sets containing what needs to be checked: $U$ and $E$ contain respectively
universally and existentially quantified _atomic presence constraints_ , $C$
contains closed literals */

2 Guess $X\subseteq\mathsf{PosOrNeg}(\mathsf{APC(\psi)})$ s.t. $\psi$ is true
when all APCs in $X$ are true ;

3

4 for  _$P$ in $X$_ do

5 for  _$\phi$ closed atomic proposition in $P$ _ do

/* $\phi$ refers to constant rounds only */

6 if  _$\phi$ guessed to be true _ then Add $\phi$ to $C$ ; Replace $\phi$ by
true in $P$ ;

7 else Add $\neg\phi$ to $C$ ; Replace $\phi$ by false in $P$ ;

8

9 if  _$P$ is a closed proposition_ then

10 Check that $P$ is true with guessed values of atomic propositions ;

11

12 if  _$P$ universal_ then Add $P$ to $U$ ;

13 if  _$P$ existential_ then Add $P$ to $E$ ;

14

15Function  _NDComputeIteration(_$E,U,C,\lambda$_) _:

16 for  _“ $\forall l\,\phi$” in $U$ _ do

17 Guess
$\mathcal{L}\subseteq\mathsf{PosOrNeg}(\mathsf{AP}(\phi[l\shortleftarrow k]))$
s.t. $\phi[l\shortleftarrow k]$ is true when all literals in $\mathcal{L}$ are
true ;

18 Add all literals in $\mathcal{L}$ to $C$ ;

19

20 for  _“ $\exists l\,\phi$” in $E$ _ do

21 if  _$\phi[l\shortleftarrow k]$ guessed to be true _ then

22 Guess
$\mathcal{L}\subseteq\mathsf{PosOrNeg}(\mathsf{AP}(\phi[l\shortrightarrow
k]))$ s.t. $\phi[l\shortleftarrow k]$ is true when all literals in
$\mathcal{L}$ are true ;

23 Add all literals in $\mathcal{L}$ to $C$ ; Remove “$\exists l\,\phi$” from
$E$ ;

24

25 for  _$\phi$ in $C$ about round $k$ _ do

// $\phi$ is of the form (negation of)
‘‘$(q,k)\mathrel{\mathsf{populated}}$’’, or (negation of)
‘‘$\mathsf{rg}_{k}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}$’’

26 Check that $\phi$ is satisfied in $\lambda$ ; Remove $\phi$ from $C$ ;

27

28Function  _TestPresenceConstraint(_$E,U,C,\lambda$_) _:

29 if  _$E\neq\emptyset$ _ then return false ;

30 for  _$\phi\in C$ or “$\forall l\,\phi$” in $U$ _ do

31 if  _$\langle\penalty 10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty
10000\rangle\not\models\phi$_ then

return false ;

// Execution cannot stop at round $k$

32

33 return true ;

34

Algorithm 3 The functions at Line 1, Line 1 and Line 1 of Algorithm 1

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

At Line 3, 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 “$\forall l\,\phi$” or “$\exists l\,\phi$” 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 3). This simplifies all closed propositions in $X$
to either true of false: if any of them is false, we reject (Line 3). We put
universally quantified element of $X$ in $U$ (Line 3) and existentially
quantified ones in $E$ (Line 3).

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

The universal atomic presence constraints are checked at every round (Lines 3
to 3), while for each existential atomic presence constraints is checked at a
round chosen non-deterministically (Lines 3 to 3). 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 3 and 3). Note that all literals in $C$ are
closed formulas hence their terms are constant integers.

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

In this functon, we check whether we can stop the execution at round $k$,
leaving all rounds $\geq 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 $\geq k{+}1$ if these rounds are left untouched
by the execution, which is done in Lines 3 to 3. The test is expressed under
the condition $\langle\penalty
10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty 10000\rangle\models\phi$
(although $\langle\penalty
10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty 10000\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 round $l\geq k{+}1$ at this stage, and we check that $\phi$ is either of
the form “$\neg((q,l)\mathrel{\mathsf{populated}})$” or of the form
“$\mathsf{rg}_{l}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}_{0}$”. A
universal presence constraint $\forall l\,\phi$ must be satisfied on
arbitrarily large rounds $\geq k{+}1$, and we check that we obtain true by
setting in $\phi$ all “$(q,t)\mathrel{\mathsf{populated}}$” to false,
“$\mathsf{rg}_{t}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}_{0}$” to true
and “$\mathsf{rg}_{t}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}$” to false
for $\mathsf{d}\neq\mathsf{d}_{0}$.

######  Example B.4.

Consider $\phi_{1}:=\forall
l\,((q,l)\mathrel{\mathsf{populated}})\lor(\mathsf{rg}_{l}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d}_{0})$
and $\phi_{2}:=\forall
l\,(\mathsf{rg}_{l}[\alpha]\mathrel{\mathsf{contains}}\mathsf{d})$ with
$\mathsf{d}\neq\mathsf{d}_{0}$. One has $\langle\penalty
10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty 10000\rangle\models
phi_{1}$, but $\langle\penalty
10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty
10000\rangle\not\models\phi_{2}$. There is no hope of finding a
$\sigma\in\mathsf{Reach_{a}}(\mathsf{Init_{a}})$ such that
$\sigma\models\phi_{2}$.

###  B.4 Proof of Correctness of the Algorithm

See 5.8

First, consider a computation of the algorithm that accepts at round
$K\in\mathds{N}$. For all $k\in[0,K]$, let $\tau_{k}$ denote the footprint on
$[k{-}\mathsf{v}{+}1,k]$ guessed by the algorithm during iteration $k$. By
applying Lemma 5.7, there exist $\sigma_{0}\in\mathsf{Init_{a}}$ and an
execution $\rho:\sigma_{0}$ such that, for all $k\leq K$,
$\mathsf{footprint}{[k{-}\mathsf{v}{+}1,k]}(\rho)=\tau_{k}$. Moreover, $\rho$
leaves rounds $\geq K$ untouched.

######  Lemma B.6.

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

######  Proof B.7.

Let $L$ be a literal that has been in $C$ at some point. If it was removed
from $C$ at Line 3, then $C$ is satisfied by $\lambda$ hence by $\sigma$. If
it has remained in $C$ until the end, then it is about round $l\geq K{+}1$ and
$\langle\penalty 10000\emptyset,\mathsf{d}_{0}^{\mathsf{Reg}}\penalty
10000\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 3. At some iteration $k$, “$\exists l\,\phi$” is removed
from $E$ at Line 3. All literals guessed at Line 3 are added to $C$ at Line 3
hence are satisfied by $\sigma$, thus $\sigma\models\phi[l\shortleftarrow 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\leq K$,
$\sigma\models\phi[l\shortleftarrow k]$. Also, thanks to the verification at
Lines 3 to 3, for all $k\geq K{+}1$, $\sigma\models\phi[l\shortleftarrow k]$,
which proves that $\sigma\models\exists l\,\phi$.

The previous lemma proves that all APCs guessed at Line 3 are satisfied by
$\sigma$. Note that the simplification at Lines 3 and 3 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}$ 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 3, it guesses APCs $P$ such that $\sigma\models P$. At
Line 3, 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
$\mathsf{footprint}{[k{-}\mathsf{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
$\geq k$; thanks to Lines 3 to 3, at the end of iteration $k$, all literals in
$C$ are about rounds $\geq 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 TestPresenceConstraint$(E,U,C,\lambda)$ succeeds
and the computation accepts. This concluded the proof of Proposition 5.8.

###  B.5 Proof of Proposition 5.9

See 5.9

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

######  Lemma B.9.

For all $\sigma\in\Sigma,\sigma^{\prime}\in\mathsf{Reach_{a}}(\sigma)$, there
exists $\rho:\sigma$ s.t., for all $k$,
$\mathsf{footprint}{[k{-}\mathsf{v},k]}(\rho)$ is storable in space
$O((|Q|^{2}\,(\mathsf{v}{+}1)^{2}\,\log(\mathsf{dim}\,|{\rm D}|)))$.

More specifically, we will prove that
$\mathsf{footprint}{[k{-}\mathsf{v},k]}(\rho)$ is storable in space
$O((|Q|^{2}\,(\mathsf{v}{+}1)^{2}+|Q|\,(\mathsf{v}{+}1)^{2}\,\log(\mathsf{dim}\,|{\rm
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.11.

For all execution $\rho:\sigma$, there exists a execution
$\tilde{\rho}:\sigma$ that is in normal form.

######  Proof B.14.

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.15.

An execution in normal form has at most $|Q|(2\mathsf{v}{+}5)$ steps on a
given round $k$.

######  Proof B.16.

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{+}\mathsf{v}$. Since there
are at most $2|Q|(\mathsf{v}{+}1)$ read steps on these rounds, there are at
most $2|Q|(\mathsf{v}{+}1)$ writes at round $k$ that do not populate nor
desert, hence in total at most $|Q|(2\mathsf{v}{+}5)$ steps at round $k$.

######  Lemma B.17.

If $\rho$ is in normal form and $k\in\mathds{N}$, then
$\mathsf{footprint}{[k{-}\mathsf{v},k]}(\rho)$ is storable in polynomial space
$O((|Q|^{2}\,(\mathsf{v}{+}1)^{2}+|Q|\,(\mathsf{v}{+}1)^{2}\,\log(\mathsf{dim}\,|{\rm
D}|)))$.

######  Proof B.18.

This footprint only has steps at rounds $k{-}\mathsf{v}$ to $k$, hence in
total at most $(\mathsf{v}{+}1)|Q|(2\mathsf{v}{+}5)$ steps. Since a move can
be stored in $O(\log(|Q|)+\log({\rm D})+\log(\mathsf{v})+\log(\mathsf{dim}))$
and a local configuration in $O((|Q|+\mathsf{dim}\,\log(|{\rm
D}|))(\mathsf{v}{+}1))$ (storing the relative round instead of the absolute
one), a footprint on $[k{-}\mathsf{v},k]$ can be stored in polynomial space
$O((|Q|^{2}\,(\mathsf{v}{+}1)^{2}+|Q|\,(\mathsf{v}{+}1)^{2}\,\log(\mathsf{dim}\,|{\rm
D}|)))$.

Combining Lemmas B.11, B.15 and B.17 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 5.9.

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
3 and 3) or while processing a presence constraint from $U$ or $E$ (Lines 3
and 3). There are at most $O(|\psi|)$ literals added to $C$ in the
initialization. Consider $L$ a literal that is added to $C$ at Line 3 or Line
3 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^{\prime}\leq k$, hence $r$ is of the form $k^{\prime}+m$ with $m\leq M$. In
that case, note that $r\geq k$ because otherwise the literal would have been
removed from $C$ at iteration $r$. Either way, one has $0\leq r-k\leq 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})$.