Parameterized Verification of Algorithms for Oblivious Robots on a Ring

TL;DR

This paper investigates the verification of algorithms for anonymous robots on a ring, demonstrating decidability results for safety properties in certain cases and employing SMT-solvers for automated verification.

Contribution

It is the first to analyze parameterized verification of such algorithms, providing decidability results and encoding techniques using Presburger arithmetic and SMT-solvers.

Findings

Safety verification is undecidable in asynchronous settings.

Safety properties are decidable in synchronous and certain asynchronous cases.

Encoding protocols in Presburger arithmetic enables automated verification.

Abstract

We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be error-prone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameter-ized case. We show that safety and reachability problems are undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the asynchronous case for a particular class of algorithms. Several properties on the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMT-solver. Feasibility of our approach is demonstrated by the encoding of several case studies.

Tables

Table 1. Table 1 : Different types of configurations

$\mathrm{𝗌𝗍𝖺𝖻𝗅𝖾}$ configuration		${𝖱}_{tt}{\mathrm{𝖥𝖱}}_t\mathrm{𝖥𝖥}$
$\mathrm{𝗆𝗈𝗏𝗂𝗇𝗀𝟣}$ configuration		${\mathrm{𝖥𝖱}}_{tt}{𝖱}_t\mathrm{𝖥𝖥}$
$\mathrm{𝗆𝗈𝗏𝗂𝗇𝗀𝟤}$ configuration		${\mathrm{𝖥𝖱}}_{tt}{\mathrm{𝖥𝖱}}_t𝖥$
$\mathrm{𝗆𝗈𝗏𝗂𝗇𝗀𝟥}$ configuration		${\mathrm{𝖥𝖱}}_{tt}{\mathrm{𝖥𝖥𝖱}}_t$
$\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗓𝗂𝗇𝗀𝟣}$ configuration		${𝖱}_{tt}{\mathrm{𝖥𝖥𝖥𝖱}}_t$
$\mathrm{𝗌𝗍𝖺𝖻𝗂𝗅𝗂𝗓𝗂𝗇𝗀𝟤}$ configuration		${𝖱}_{tt}{\mathrm{𝖥𝖥𝖱}}_t𝖥$

Equations

$$\mathit{move}(\phi,V)=\left\{\begin{array}[]{ll}\{+1\}&\mbox{if }\mathbf{V}\models\phi\mbox{ and }\mathbf{V}\neq\overleftarrow{\mathbf{V}}\\ \{-1\}&\mbox{if }\overleftarrow{\mathbf{V}}\models\phi\mbox{ and }{\mathbf{V}}\neq\overleftarrow{\mathbf{V}}\\ \{-1,+1\}&\mbox{if }{\mathbf{V}}\models\phi\mbox{ and }{\mathbf{V}}=\overleftarrow{\mathbf{V}}\\ \{0\}&\mbox{otherwise}\end{array}\right.$$

$$\begin{array}[]{c}\mathtt{ConfigView}_{i}(y,p_{1},\dots,p_{k},d_{1},\dots,d_{k}):=\\ \exists d^{\prime}_{1},\dots,d^{\prime}_{k-1}\cdot\bigwedge_{j=1}^{k-2}d^{\prime}_{j}\leq d^{\prime}_{j+1}\wedge\\ \bigwedge_{j=1,j\neq i}^{k}(\bigvee_{\ell=1}^{k-1}p_{j}=(p_{i}+d^{\prime}_{\ell})\mod y)\wedge\\ \bigwedge_{\ell=1}^{k}(\bigvee_{j=1,j\neq i}^{k}p_{j}=(p_{i}+d^{\prime}_{\ell})\mod y))\wedge\\ 0<d^{\prime}_{1}\wedge\bigwedge_{j=1}^{k-1}d^{\prime}_{j}\leq y\wedge\\ d_{1}=d^{\prime}_{1}\wedge\bigwedge_{j=2}^{k-1}d_{j}=d^{\prime}_{j}-d^{\prime}_{j-1}\wedge d_{k}=y-d^{\prime}_{k-1},\end{array}$$

$$\begin{array}[]{c}\mathtt{ViewSym}(d_{1},\dots,d_{k},d^{\prime}_{1},\dots,d^{\prime}_{k}):=\\ \bigvee_{j=1}^{k}(\bigwedge_{\ell=j+1}^{k}(d_{\ell}=0\wedge d^{\prime}_{\ell}=0)\wedge\bigwedge_{\ell=1}^{j}d^{\prime}_{\ell}=d_{j-\ell+1})\end{array}$$

$$\begin{array}[]{c}\mathtt{Move}^{\phi}_{i}(y,p_{1},\dots,p_{k},p^{\prime}):=\\ \exists d_{1},\dots,d_{k},d^{\prime}_{1},\cdots,d^{\prime}_{k}\cdot\\ \mathtt{ConfigView}_{i}(y,p_{1},\dots,p_{k},d_{1},\dots,d_{k})\wedge\\ \mathtt{ViewSym}(d_{1},\dots,d_{k},d^{\prime}_{1},\dots,d^{\prime}k)\wedge\\ \Bigl{[}\Bigl{(}\phi(d_{1},\dots,d_{k})\wedge\bigl{(}(p_{i}<y-1\wedge p^{\prime}=p_{i}+1)\\ \vee(p_{i}=y-1\wedge p^{\prime}=0)\bigr{)}\Bigr{)}\vee\\ \Bigl{(}\phi(d^{\prime}_{1},\dots,d^{\prime}_{k})\wedge\bigl{(}(p_{i}>0\wedge p^{\prime}=p_{i}-1)\\ \vee(p_{i}=0\wedge p^{\prime}=y-1)\bigr{)}\Bigr{)}\\ \vee\Bigl{(}\neg\phi(d_{1},\dots,d_{k})\wedge\neg\phi(d^{\prime}_{1},\dots,d^{\prime}_{k})\wedge(p^{\prime}=p_{i})\Bigr{)}\Bigr{]}\end{array}$$

$$\begin{array}[]{c}\mathtt{SemiSyncPost}_{\phi}(y,p_{1},\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k}):=\\ \bigvee_{i=1}^{k}\bigr{(}\mathtt{Move}^{\phi}_{i}(y,p_{1},\dots,p_{k},p^{\prime}_{i})\wedge\\ \bigwedge_{j=1,j\neq i}^{k}((p^{\prime}_{j}=p_{j})\vee\mathtt{Move}^{\phi}_{j}(y,p_{1},\dots,p_{k},p^{\prime}_{j}))\bigr{)}\\ {\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}aa}\\ \mathtt{SyncPost}_{\phi}(y,p_{1},\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k}):=\\ \bigwedge_{i=1}^{k}\mathtt{Move}^{\phi}_{i}(y,p_{1},\dots,p_{k},p^{\prime}_{i})\end{array}$$

$$\begin{array}[]{c}\mathtt{SyncPost}_{\phi}(y,p_{1},\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k})\wedge\\ \texttt{Ring}(y)\wedge\neg\texttt{Bad}(p_{1},\ldots,p_{k})\wedge\\ \texttt{Bad}(p^{\prime}_{1},\ldots,p^{\prime}_{k})\end{array}$$

$$\begin{array}[]{c}\mathtt{AsyncPost}_{\phi}:=\exists d_{1},\dots,d_{k}\cdot\\ \bigvee_{i=1}^{k}\Bigr{(}\bigwedge_{j\neq i}(p^{\prime}_{j}=p_{j}\wedge s^{\prime}_{j}=s_{j}\wedge v^{\prime}_{j}=v_{j})\wedge\\ s^{\prime}_{i}=1-s_{i}\wedge\bigl{(}(s_{i}=0\wedge v^{\prime}_{i}=\langle d_{1},\dots,d_{k}\rangle\wedge\\ \mathtt{ConfigView}_{i}(n,p_{1},\dots,p_{k},d_{1},\dots,d_{k})\wedge p^{\prime}_{i}=p_{i})\vee\\ (s_{i}=1\wedge v^{\prime}_{i}=v_{i}\wedge\mathtt{Move}_{i}^{\phi}(n,p_{1},\dots,p_{k},p^{\prime}_{i})\bigr{)}\Bigr{)}\end{array}$$

$$\begin{array}[]{c}\texttt{UniqSeq}_{\phi}:=\neg\exists y.p_{1},\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k}\cdot\\ \bigvee_{i\neq j,1\leq i,j\leq k}(\mathtt{Move}^{\phi}_{i}(n,p_{1},\dots,p_{k},p^{\prime}_{i})\wedge\mathtt{Move}^{\phi}_{j}(n,p_{1},\dots,p_{k},p^{\prime}_{j})\\ \wedge p^{\prime}_{i}\neq p_{i}\wedge p^{\prime}_{j}\neq p_{j}.\end{array}$$

$${\mathsf{B}}_3{\mathsf{R}}_{c_1}{\mathsf{F}}^K{\mathsf{B}}_4{\mathsf{R}}_{c_2}{\mathsf{F}}^K{\mathsf{B}}_5{\mathsf{R}}_c{\mathsf{F}}^K{\mathsf{B}}_6{\mathsf{R}}_{\ell }{\mathsf{F}}^{|L|}{\mathsf{B}}_7{\mathsf{R}}_{{\ell }^{\prime }}{\mathsf{F}}^{|L|}{\mathsf{B}}_8{\mathsf{R}}_{tt}\mathsf{F}{\mathsf{R}}_t\mathsf{F}{\mathsf{R}}_g\mathsf{F}{\mathsf{R}}_d,$$

Full text

1 Introduction

We consider sets of mobile oblivious robots evolving in a discrete space (modeled as a ring shaped graph). For our purpose, rings are seen as discrete graphs whose vertices represent the different positions available to host a robot, and edges model the possibility for a robot to move from one position to another. Robots follow the seminal model by Suzuki and Yamashita [23]: they do not remember their past actions, they cannot communicate explicitly, and are disoriented.

However, they can sense their environment and detect the positions of the other robots on the ring. If several robots share the same position on the ring (forming a tower, or multiplicity point), other robots may or may not detect the tower. If robots have weak multiplicity detection, they are assumed to sense a tower on a position, but are not able to count the actual number of robots in this tower. With strong multiplicity detection, they are able to count the exact number of robots on a given position. In case they have no multiplicity detection, robots simply detect occupied positions. In this paper, we assume strong multiplicity detection is available to all robots.

Robots are anonymous and execute the same deterministic algorithm to achieve together a given objective. Different objectives for ring shaped discrete spaces have been studied in the literature [17]: gathering – starting from any initial configuration, all the robots must gather on the same node, not known beforehand, and then stop [18], exploration with stop – starting from any initial configuration, the robots reach a configuration where they all are idle and, in the meanwhile, all the positions of the ring have been visited by a robot [16], exclusive perpetual exploration – starting from any tower-free configuration, each position of the ring is visited infinitely often and no multiplicity point ever appears [6, 11].

Each robot behaves according to the following cycle: it takes a snapshot of its environment, then it computes its next move (either stay idle or move to an adjacent node in the ring), and at the end of the cycle, it moves according to its computation. Such a cycle is called a look-compute-move cycle.

Since robots cannot rely on a common sense of direction, directions that are computed in the compute phase are only relative to the robot. To tell apart its two sides, a robot relies on a description of the ring in both clockwise and counter-clockwise direction, which gives it two views of the configuration. There are two consequences to this fact. First, if its two views are identical, meaning that the robot is on an axis of symmetry, it cannot distinguish the two directions and thus either decides to stay idle, or to move. In the latter case, the robot moves becomes a non-deterministic choice between the two available directions. Second, when two robots have the same two views of the ring, the protocol commands them to move in the same relative direction, but this might result in moves in actual opposite directions for the two robots. Such a symmetrical situation is pictured in Figure 1.

Existing execution models consider different types of synchronization for the robots: in the fully synchronous model (FSYNC), all robots evolve simultaneously and complete a full look-compute-move cycle. The semi-synchronous model (SSYNC) consider runs that evolve in phases: at each phase, an arbitrary subset of the robots is scheduled for a full look-compute-move cycle, which is executed simultaneously by all robots of the subset. Finally, in the asynchronous model (ASYNC), robots evolve freely at their own pace: In particular, a robot can move according to a computation based on an obsolete observation of its environment, as others robots may have moved in between. Algorithms in the literature are typically parameterized by the number of robots and/or number of positions in the ring. In this work we focus on formally verifying algorithms parameterized by the number of ring positions only, assuming a a fixed number of robots.

1.1 Related work

Designing and proving mobile robot protocols is notoriously difficult. Formal methods encompass a long-lasting path of research that is meant to overcome errors of human origin. Unsurprisingly, this mechanized approach to protocol correctness was successively used in the context of mobile robots [7, 13, 5, 2, 20, 9, 4, 22, 3].

When robots are not constrained to evolve on a particular topology (but instead are allowed to move freely in a bidimensional Euclidian space), the Pactole (http://pactole.lri.fr) framework has been proven useful. Developed for the Coq proof assistant, Pactole enabled the use of high-order logic to certify impossibility results [2] for the problem of convergence: for any positive $\epsilon$, robots are required to reach locations that are at most $\epsilon$ apart. Another classical impossibility result that was certified with Pactole is the impossibility of gathering starting from a bivalent configuration [9]. Recently, positive certified results for SSYNC gathering with multiplicity detection [10], and for FSYNC gathering without multiplicity detection [3] were provided. However, as of now, no Pactole library is dedicated to robots that evolve on discrete spaces.

In the discrete setting that we consider in this paper, model-checking proved useful to find bugs in existing literature [5, 14] and assess formally published algorithms [13, 5, 22]. Automatic program synthesis (for the problem of perpetual exclusive exploration in a ring-shaped discrete space) is due to Bonnet et al. [7], and can be used to obtain automatically algorithms that are “correct-by-design”. The approach was refined by Millet et al. [20] for the problem of gathering in a discrete ring network. As all aforementioned approaches are designed for a bounded setting where both the number of locations and the number of robots are known, they cannot permit to establish results that are valid for any number of locations.

Recently, Aminof et al. [22] presented a general framework for verifying properties about mobile robots evolving on graphs, where the graphs are a parameter of the problem. While our model could be encoded in their framework, their undecidability proof relies on persistent memory used by the robots, hence is not applicable to the case of oblivious robots we consider here. Also, they obtain decidability in a subcase that is not relevant for robot protocols like those we consider. Moreover, their decision procedure relies on MSO satisfiability, which does not enjoy good complexity properties and cannot be implemented efficiently for the time being.

1.2 Contributions

In this work, we tackle the more general problem of verifying protocols for swarms of robots for any number of locations.

We provide a formal definition of the problem, where the protocol can be described as a quantifier free Presburger formula. This logic, weak enough to be decidable, is however powerful enough to express existing algorithms in the literature. Objectives of the robots are also described by Presburger formulae and we consider two problems: when the objective of the robots is a safety objective – robots have to avoid the configurations described by the formula ($\mathsf{SAFE}$), and when it is a reachability objective ($\mathsf{REACH}$). We show that if $\mathsf{REACH}$ is undecidable in any semantics, $\mathsf{SAFE}$ is decidable in FSYNC and SSYNC. We also show that when the protocol is uniquely-sequentializable, safety properties become decidable even in the asynchronous case.

Finally, we show practical applicability of this approach by using an SMT-solver to verify safety properties for some algorithms from the literature.

Hence, we advocate that our formalism should be used when establishing such protocols, as a formal and non-ambiguous description, instead of the very informal and sometimes unclear definitions found in the literature. Moreover, if totally automated verification in the parameterized setting seems unfeasible, our method could be used as a “sanity check” of the protocol, and to automatically prove intermediate lemmas, that can then be used as formally proved building blocks of a handmade correction proof.

Due to lack of space, some proofs are given in the appendices.

2 Model of Robots Evolving on a Ring

2.1 Formal model

In this section we present the formal language to describe mobile robots protocols as well as the way it is interpreted.

2.1.1 Preliminaries

For $a,b\in\mathbb{Z}$ such that $a\leq b$, we denote by $[a,b]$ the set $\{c\in\mathbb{Z}\mid a\leq c\leq b\}$. For $a\in\mathbb{Z}$ and $b\in\mathbb{N}$, we write $a\odot b$ the natural $d\in[0,(b-1)]$ such that there exists $j\in\mathbb{Z}$ and $a=b.j+d$ (for instance $-1\odot 3=2$). Note that $\odot$ corresponds to the modulo operator, but for sake of clarity we recall its definition when $a$ is negative.

We recall the definition of Existential Presburger (EP) formulae. Let $Y$ be a countable set of variables. First we define the grammar for terms $\mathtt{t}::=x~{}\mid~{}\mathtt{t}+\mathtt{t}~{}\mid~{}a\cdot\mathtt{t}~{}\mid~{}\mathtt{t}\mod a$, where $a\in\mathbb{N}$ and $x\in Y$ and then the grammar for formulae is given by $\phi::=\mathtt{t}\bowtie b~{}\mid~{}\phi\wedge\phi~{}\mid~{}\phi\vee\phi~{}\mid~{}\exists x.\phi$ where ${\bowtie}\in\{=,\leq,\geq,<,>\}$, $x\in Y$ and $b\in\mathbb{N}$. We sometimes write a formula $\phi$ as $\phi(x_{1},\ldots,x_{k})$ to underline that $x_{1},\ldots,x_{k}$ are the free variables of $\phi$. The set of Quantifier Free Presburger (QFP) formulae is obtained by the same grammar deleting the elements $\exists x.\phi$. Note that when dealing with QFP formulae, we allow as well negations of formulae.

We say that a vector $V=\langle d_{1},\dots,d_{k}\rangle$ satisfies an EP formula $\phi(x_{1},\ldots,x_{k})$, denoted by $V\models\phi$, if the formula obtained by replacing each $x_{i}$ by $d_{i}$ holds. Given a formula $\phi$ with free variables ${x_{1},\dots,x_{k}}$, we write $\phi(d_{1},\dots,d_{k})$ the formula where each $x_{i}$ is replaced by $d_{i}$. We let $\left[\!\left[\phi(x_{1},\ldots,x_{k})\right]\!\right]=\{\langle d_{1},\dots,d_{k}\rangle\in\mathbb{N}^{k}\mid\phi(x_{1},\ldots,x_{k})\models\phi\}$ be the set of models of the formula. In the sequel, we use Presburger formulae to describe configurations of the robots, as well as protocols.

2.1.2 Configurations and robot views

In this paper, we consider a fixed number $k>0$ of robots and, except when stated otherwise, we assume the identities of the robots are $\mathcal{R}=\{R_{1},\ldots,R_{k}\}$. We may sometimes identify $\mathcal{R}$ with the set of indices $\{1,\ldots,k\}$. On a ring of size $n\geq k$, a (k,n)-configuration of the robots (or simply a configuration if $n$ and $k$ are clear from the context) is given by a vector $\mathbf{p}\in[0,n-1]^{k}$ associating to each robot $R_{i}$ its position $\mathbf{p}(i)$ on the ring. We assume w.l.o.g. that positions are numbered in the clockwise direction.

A view of a robot on this configuration gives the distances between the robots, starting from its neighbor, i.e. the robot positioned on the next occupied node (a distance equals to [math] meaning that two robots are on the same node). A view $\mathbf{V}=\langle d_{1},\dots,d_{k}\rangle\in[0,n]^{k}$ is a $k$-tuple such that $\sum_{i=1}^{k}d_{i}=n$ and $d_{1}\neq 0$. We let $\mathcal{V}_{n,k}$ be the set of possible views for $k$ robots on a ring of size $n$. Notice that all the robots sharing the same position should have the same view. For instance, suppose that, on a ring of size 10, 2 robots $R_{1}$, and $R_{2}$ are on the same position of the ring (say position 1), $R_{3}$ is at position 4, $R_{4}$ is at position 8, and $R_{5}$ is at position 9 (see Figure 1(b)). Then, the view of $R_{1}$ and $R_{2}$ is $\langle 3,4,1,2,0\rangle$. It is interpreted by the fact that there is a robot at a distance $3$ (it is $R_{3}$), a robot a at distance $3+4$ (it is $R_{4}$) and so on. We point out that all the robots at the same position share the same view. We as well suppose that in a view, the first distance is not [math] (this is possible by putting [math] at the ‘end’ of the view instead). As a matter of fact in the example of Figure 1(b), there is a robot at distance $3+4+1+2=10$ from $R_{1}$ (resp. $R_{2}$), which is $R_{2}$ (resp. $R_{1}$). The sum of the $d_{i}$ corresponds always to the size of the ring and here the fact that in the view of $R_{1}$ we have as last element [math] signifies that there is a distance [math] between the last robot (here $R_{2}$) and $R_{1}$. When looking in the opposite direction, their view becomes: $\langle 2,1,4,3,0\rangle$. Formally, for a view $\mathbf{V}=\langle d_{1},\dots,d_{k}\rangle\in[0,n]^{k}$, we note $\overleftarrow{\mathbf{V}}=\langle d_{j},\dots,d_{1},d_{k},\dots,d_{j-1}\rangle$ the corresponding view when looking at the ring in the opposite direction, where $j$ is the greatest index such that $d_{j}\neq 0$.

Given a configuration $\mathbf{p}\in[0,n-1]^{k}$ and a robot $R_{i}\in\mathcal{R}$, the view of robot $R_{i}$ when looking in the clockwise direction, is given by $\mathbf{V}_{\mathbf{p}}[i\rightarrow]=\langle d_{i}(i_{1}),d_{i}(i_{2})-d_{i}(i_{1}),\dots,n-d_{i}(i_{k-1})\rangle$, where, for all $j\neq i$, $d_{i}(j)\in[1,n]$ is such that $(\mathbf{p}(i)+d_{i}(j))\odot n=\mathbf{p}(j)$ and $i_{1},\dots,i_{k}$ are indexes pairwise different such that $0<d_{i}(i_{1})\leq d_{i}(i_{2})\leq\dots\leq d_{i}(i_{k-1})$. When robot $R_{i}$ looks in the opposite direction, its view according to the configuration $\mathbf{p}$ is $\mathbf{V}_{\mathbf{p}}[\leftarrow i]=\overleftarrow{\mathbf{V}_{\mathbf{p}}[i\rightarrow]}$.

2.1.3 Protocols

In our context, a protocol for networks of $k$ robots is given by a QFP formula respecting some specific constraints.

Definition 1** (Protocol)**

A protocol is a QFP formula $\phi(x_{1},\ldots,x_{k})$ such that for all views $\mathbf{V}$ the following holds: if $\mathbf{V}\models\phi$ and $\mathbf{V}\neq\overleftarrow{\mathbf{V}}$ then $\overleftarrow{\mathbf{V}}\not\models\phi$

A robot uses the protocol to know in which direction it should move according to the following rules. As we have already stressed, all the robots that share the same position have the same view of the ring. Given a configuration $\mathbf{p}$ and a robot $R_{i}\in\mathcal{R}$, if $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\models\phi$, then the robot $R_{i}$ moves in the clockwise direction, if $\mathbf{V}_{\mathbf{p}}[\leftarrow i]\models\phi$ then it moves in the opposite direction, if none of $\mathbf{V}_{\mathbf{p}}[i\rightarrow]$ and $\mathbf{V}_{\mathbf{p}}[\leftarrow i]$ satisfies $\phi$ then the robot should not move. The conditions expressed in Definition 1 imposes hence a direction when $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\neq\mathbf{V}_{\mathbf{p}}[\leftarrow i]$. In case $\mathbf{V}_{\mathbf{p}}[i\rightarrow]=\mathbf{V}_{\mathbf{p}}[\leftarrow i]$, the robot is disoriented and it can hence move in one direction or the other. For instance, consider the configuration $\mathbf{p}$ pictured on Figure 1(a). Here, $\mathbf{V}_{\mathbf{p}}[1\rightarrow]=\langle 3,1,3\rangle=\mathbf{V}_{\mathbf{p}}[\leftarrow 1]$. Note that such a semantics enforces that the behavior of a robot is not influenced by its direction. In fact consider two symmetrical configurations $\mathbf{p}$ and $\mathbf{p}^{\prime}$ such that $\mathbf{V}_{\mathbf{p}}[i\rightarrow]=\overleftarrow{\mathbf{V}_{\mathbf{p}^{\prime}}[i\rightarrow]}$ for each robot $R_{i}$. If $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\models\phi$ (resp. $\mathbf{V}_{\mathbf{p}}[\leftarrow i]\models\phi$), then necessarily $\mathbf{V}_{\mathbf{p}^{\prime}}[\leftarrow i]\models\phi$ (resp. $\mathbf{V}_{\mathbf{p}^{\prime}}[i\rightarrow]\models\phi$), and the robot in $\mathbf{p}^{\prime}$ moves in the opposite direction than in $\mathbf{p}$ (and the symmetry of the two configurations is maintained).

We now formalize the way movement is decided. Given a protocol $\phi$ and a view $\mathbf{V}$, the moves of any robot whose clockwise direction view is $\mathbf{V}$ are given by:

[TABLE]

Here $+1$ (resp. $-1$) stands for a movement of the robot in the clockwise (resp. anticlockwise) direction.

2.2 Different possible semantics

We now describe different transition relations between configurations. Robots have a two-phase behavior : (1) look at the ring and (2) according to their view, compute and perform a movement. In this context, we consider three different modes. In the semi-synchronous mode, in one step, some of the robots look at the ring and move. In the synchronous mode, in one step, all the robots look at the ring and move. In the asynchronous mode, in one step a single robot can either choose to look at the ring, if the last thing it did was a movement, or to move, if the last thing it did was to look at the ring. As a consequence, its movement decision is a consequence of the view of the ring it has in its memory. In the remainder of the paper, we fix a protocol $\phi$ and we consider a set $\mathcal{R}$ of $k$ robots.

2.2.1 Semi-synchronous mode

We begin by providing the semantics in the semi-synchronous case. For this matter we define the transition relation $\hookrightarrow_{\phi}\subseteq[0,n-1]^{k}\times[0,n-1]^{k}$ (simply noted $\hookrightarrow$ when $\phi$ is clear from the context) between configurations. We have $\mathbf{p}\hookrightarrow\mathbf{p}^{\prime}$ if there exists a subset $I\subseteq\mathcal{R}$ of robots such that, for all $i\in I$, $\mathbf{p}^{\prime}(i)=(\mathbf{p}(i)+m)\odot n$, where $m\in\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$, and for all $i\in\mathcal{R}\setminus I$, $\mathbf{p}^{\prime}(i)=\mathbf{p}(i)$.

2.2.2 Synchronous mode

The transition relation $\Rightarrow_{\phi}\subseteq[0,n-1]^{k}\times[0,n-1]^{k}$ (simply noted $\Rightarrow$ when $\phi$ is clear from the context) describing synchronous movements is very similar to the semi-synchronous case, except that all the robots have to move. Then $\mathbf{p}\Rightarrow\mathbf{p}^{\prime}$ if $\mathbf{p}^{\prime}(i)=(\mathbf{p}(i)+m)\odot n$ with $m\in \mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$ for all $i\in\mathcal{R}$.

2.2.3 Asynchronous mode

The definition of transition relation for the asynchronous mode is a bit more involved, for two reasons: first, the move of each robot does not depend on the current configuration, but on the last view of the robot. Second, in one step a robot either look or move. As a consequence, an asynchronous configuration is a tuple $(\mathbf{p},\mathbf{s},\mathbf{V})$ where $\mathbf{p}\in[0,n-1]^{k}$ gives the current configuration, $\mathbf{s}\in\{\mathbf{L},\mathbf{M}\}^{k}$ gives, for each robot, its internal state ($\mathbf{L}$ stands for ready to look and and $\mathbf{M}$ stands for compute and move) and $\mathbf{V}\in\mathcal{V}_{n,k}^{k}$ stores, for each robot, the view (in the clockwise direction) it had the last time it looked at the ring.

The transition relation for asynchronous mode is hence defined by a binary relation $\leadsto_{\phi}$ (or simply $\leadsto$) working on $[0,n-1]^{k}\times\{\mathbf{L},\mathbf{M}\}^{k}\times\mathcal{V}_{n,k}^{k}$ and defined as follows: $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle\leadsto\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle$ iff there exist $R_{i}\in\mathcal{R}$ such that the following conditions are satisfied:

• •

for all $R_{j}\in\mathcal{R}$ such that $j\neq i$, $\mathbf{p}^{\prime}(j)=\mathbf{p}(j)$, $\mathbf{s}^{\prime}(j)=\mathbf{s}(j)$ and $\mathbf{V}^{\prime}(j)=\mathbf{V}(j)$,

• •

if $\mathbf{s}(i)=\mathbf{L}$ then $\mathbf{s}^{\prime}(i)=\mathbf{M}$, $\mathbf{V}^{\prime}(i)=\mathbf{V}_{\mathbf{p}}[i\rightarrow]$ and $\mathbf{p}^{\prime}(i)=\mathbf{p}(i)$, i.e. if the robot that has been scheduled was about to look, then the configuration of the robots won’t change, and this robot updates its view of the ring according to the current configuration and change its internal state,

• •

if $\mathbf{s}(i)=\mathbf{M}$ then $\mathbf{s}^{\prime}(i)=\mathbf{L}$, $\mathbf{V}^{\prime}(i)=\mathbf{V}(i)$ and $\mathbf{p}^{\prime}(i)=(\mathbf{p}(i)+m)\odot n$, with $m\in\mathit{move}(\phi,\mathbf{V}(i))$, i.e. if the robot was about to move, then it changes its internal state and moves according to the protocol, and its last view of the ring.

2.2.4 Runs

A semi-synchronous (resp. synchronous) $\phi$-run (or a run according to a protocol $\phi$) is a (finite or infinite) sequence of configurations $\rho=\mathbf{p}_{0}\mathbf{p}_{1}\dots$ where, for all $0\leq i<|\rho|$, $\mathbf{p}_{i}\hookrightarrow_{\phi}\mathbf{p}_{i+1}$ (resp. $\mathbf{p}_{i}\Rightarrow_{\phi}\mathbf{p}_{i+1}$). Moreover, if $\rho=\mathbf{p}_{0}\cdots\mathbf{p}_{n}$ is finite, then there is no $\mathbf{p}$ such that $\mathbf{p}_{n}\hookrightarrow_{\phi}\mathbf{p}$ (respectively $\mathbf{p}_{n}\Rightarrow_{\phi}\mathbf{p}$). An asynchronous $\phi$-run is a (finite or infinite) sequence of asynchronous configurations $\rho=\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\cdots$ where, for all $0\leq i<|\rho|$, $\langle\mathbf{p}_{i},\mathbf{s}_{i},\mathbf{V}_{i}\rangle\leadsto_{\phi}\langle\mathbf{p}_{i+1},\mathbf{s}_{i+1},\mathbf{V}_{i+1}\rangle$ and such that $\mathbf{s}_{0}(i)=\mathbf{L}$ for all $i\in[1,k]$. Observe that the value of $\mathbf{V}_{0}$ has no influence on the actual asynchronous run.

We let $\textbf{Post}_{\mathrm{ss}}(\phi,\mathbf{p})=\{\mathbf{p}^{\prime}\mid\mathbf{p}\hookrightarrow_{\phi}\mathbf{p}^{\prime}\}$, $\textbf{Post}_{\mathrm{s}}(\phi,\mathbf{p})=\{\mathbf{p}^{\prime}\mid\mathbf{p}\Rightarrow_{\phi}\mathbf{p}^{\prime}\}$ and $\textbf{Post}_{\mathrm{as}}(\phi,\mathbf{p})=\{\mathbf{p}^{\prime}\mid\textrm{ there exist }\mathbf{V},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\textrm{ s.t. }\langle\mathbf{p},\mathbf{s}_{0},\mathbf{V}\rangle\leadsto_{\phi}\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle\}$, with $\mathbf{s}_{0}(i)=\mathbf{L}$ for all $i\in[1,k]$. Note that in the asynchronous case we impose all the robots to be ready to look. We respectively write $\hookrightarrow_{\phi}^{*}$, $\Rightarrow_{\phi}^{*}$ and $\leadsto_{\phi}^{*}$ for the reflexive and transitive closure of the relations $\hookrightarrow_{\phi}$, $\Rightarrow_{\phi}$ and $\leadsto_{\phi}$ and we define $\mathbf{Post}_{\mathrm{ss}}^{*}(\phi,\mathbf{p})$, $\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p})$ and $\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})$ by replacing in the definition $\textbf{Post}_{\mathrm{ss}}(\phi,\mathbf{p})$,$\textbf{Post}_{\mathrm{s}}(\phi,\mathbf{p})$ and $\textbf{Post}_{\mathrm{as}}(\phi,\mathbf{p})$ the relations $\hookrightarrow_{\phi}$, $\Rightarrow_{\phi}$ and $\leadsto_{\phi}$ by their reflexive and transitive closure accordingly.

We now come to our first result that shows that when the protocols have a special shape, the three semantics are identical.

Definition 2

A protocol $\phi$ is said to be uniquely-sequentializable if, for all configuration $\mathbf{p}$, there is at most one robot $R_{i}\in\mathcal{R}$ such that $\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])\neq\{0\}$.

When $\phi$ is uniquely-sequentializable at any moment at most one robot moves. Consequently, in that specific case, the three semantics are equivalent as stated by the following theorem.

Theorem 1

If a protocol $\phi$ is uniquely-sequentializable, then for all configuration $\mathbf{p}$, $\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p})=\mathbf{Post}_{\mathrm{ss}}^{*}(\phi,\mathbf{p})=\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})$.

2.3 Problems under study

In this work, we aim at verifying properties on protocols where we assume that the number of robots is fixed (equals to $k>0$) but the size of the rings is parameterized and satisfies a given property. Note that when executing a protocol the size of the ring never changes. For our problems, we consider a ring property that is given by a QFP formula $\texttt{Ring}(y)$, a set of bad configurations given by a QFP formula $\texttt{Bad}(x_{1},\ldots,x_{k})$ and a set of good configurations given by a QFP formula $\texttt{Goal}(x_{1},\ldots,x_{k})$. We then define two general problems to address the verification of such algorithms: the $\mathsf{SAFE}_{m}$ problem, and the $\mathsf{REACH}_{m}$ problem, with $m\in\{\mathrm{ss},\mathrm{s},\mathrm{as}\}$.

The $\mathsf{SAFE}_{m}$ problem is to decide, given a protocol $\phi$ and two formulae Ring and Bad whether there exists a size $n\in\mathbb{N}$ with $n\in\left[\!\left[\texttt{Ring}\right]\!\right]$, and a $(k,n)$-configuration $\mathbf{p}$ with $\mathbf{p}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\mathbf{Post}_{m}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$.

The $\mathsf{REACH}_{m}$ problem is to decide given a protocol $\phi$ and two formulae Ring and Goal whether there exists a size $n\in\mathbb{N}$ with $n\in\left[\!\left[\texttt{Ring}\right]\!\right]$ and a $(k,n)$-configuration $\mathbf{p}$, such that $\mathbf{Post}_{m}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Goal}\right]\!\right]=\emptyset$. Note that the two problems are not dual due to the quantifiers.

As an example, we can state in our context the $\mathsf{SAFE}_{m}$ problem that consists in checking that a protocol $\phi$ working with three robots never leads to collision (i.e. to a configuration where two robots are on the same position on the ring) for rings of size strictly bigger than $6$. In that case we have $\texttt{Ring}:=y>6$ and $\texttt{Bad}:=x_{1}=x_{2}~{}\vee~{}x_{2}=x_{3}~{}\vee~{}x_{1}=x_{3}$.

3 Undecidability results

In this section, we present undecidability results for the two aforementioned problems. The proofs rely on the encoding of a deterministic $k$-counter machine run. A deterministic $k$-counter machine consists of $k$ integer-valued registers (or counters) called $c_{1}$, …, $c_{k}$, and a finite list of labelled instructions $L$. Each instruction is either of the form $\ell:c_{i}=c_{i}+1;\texttt{goto }\ell^{\prime}$, or $\ell:\texttt{if }c_{i}>0\texttt{ then }c_{i}=c_{i}-1;\texttt{goto }\ell^{\prime};\texttt{else goto }\ell^{\prime\prime}$, where $i\in[1,k]$. We also assume the existence of a special instruction $\ell_{h}:\texttt{halt}$. Configurations of a $k$-counter machine are elements of $L\times\mathbb{N}^{k}$, giving the current instruction and the current values of the registers. The initial configuration is $(\ell_{0},0,\dots,0)$, and the set of halting configurations is $\mathsf{HALT}=\{\ell_{h}\}\times\mathbb{N}^{k}$. Given a configuration $(\ell,n_{1},\dots,n_{k})$, the successor configuration $(\ell^{\prime},n^{\prime}_{1},\dots,n^{\prime}_{k})$ is defined in the usual way and we note $(\ell,n_{1},\dots,n_{k})\vdash(\ell^{\prime},n^{\prime}_{1},\dots,n^{\prime}_{k})$. A run of a $k$-counter machine is a (finite or infinite) sequence of configurations $(\ell_{0},n^{0}_{1},\dots,n^{0}_{k}),(\ell_{1},n^{1}_{1},\dots,n^{1}_{k})\cdots$, where $(\ell_{0},n^{0}_{1},\dots,n^{0}_{k})$ is the initial configuration, and, for all $i\geq 0$, $(\ell_{i},n^{i}_{1},\dots,n^{i}_{k})\vdash(\ell_{i+1},n^{i+1}_{1},\dots,n^{i+1}_{k})$. The run is finite if and only if it ends in a halting configuration, i.e. in a configuration in $\mathsf{HALT}$.

Theorem 2

$\mathsf{SAFE}_{\mathrm{as}}$* is undecidable.*

Sketch of proof.   

The proof relies on a reduction from the halting problem of a deterministic two-counter machine $M$ to $\mathsf{SAFE}_{\mathrm{as}}$ with $k=42$ robots. It is likely that an encoding using less robots might be used for the proof, but for the sake of clarity, we do not seek the smallest possible amount of robots. The halting problem is to decide whether the run of a given deterministic two-counter machine is finite; this problem is undecidable [21]. The idea is to simulate the run of $M$ in a way that ensures that a collision occurs if and only if $M$ halts. Positions of robots on the ring are used to encode values of counters and the current instruction of the machine. The $k$-protocol makes sure that movements of the robots simulate correctly the run of $M$. Moreover, one special robot moves only when the initial configuration is encoded, and another only when the final configuration is encoded. The collision is ensured in the following sequence of actions of the robots: when the initial configuration is encoded, the first robot computes its action but does not move immediately. When the halting configuration is reached, the second robot computes its action and moves, then the first robot finally completes its move, entailing the collision. Note that if the ring is not big enough to simulate the counter values then the halting configuration is never reached and there is no collision.

Instead of describing configurations of the robots by applications giving positions of the robots on the ring, we use a sequence of letters $\mathsf{F}$ or $\mathsf{R}$, representing respectively a free node and a node occupied by a robot. When a letter $\textsf{A}\in\{\mathsf{F},\mathsf{R}\}$ is repeated $i$ times, we use the notation $\textsf{A}^{i}$, when it is repeated an arbitrary number or times (including 0), we use $\textsf{A}^{*}$. To distinguish between the two representations of the configurations, we use respectively the terms configurations or word-configurations. The correspondence between a configuration and a word-configuration is obvious. A machine-like (word-)configuration is a configuration of the form:

\mathsf{B}_{3}\mathsf{F}^{*}\mathsf{R}\mathsf{F}^{*}\mathsf{B}_{4}\mathsf{F}^{*}\mathsf{R}\mathsf{F}^{*}\mathsf{B}_{5}\mathsf{F}^{*}\mathsf{R}\mathsf{F}^{*}\mathsf{B}_{6}\mathsf{F}^{*}\mathsf{R}\mathsf{F}^{*}\mathsf{B}_{7}\mathsf{F}^{*}\mathsf{R}\mathsf{F}^{*}\mathsf{B}_{8}$$P_{1}$$P_{2}$$P_{3}$$P_{4}$$P_{5} $\mathsf{R}\mathsf{F}\mathsf{R}$

where $\mathsf{B}_{i}$ is a shorthand for $\mathsf{F}\mathsf{R}^{i}\mathsf{F}$, and $P_{1}P_{2}\in\{\mathsf{R}\mathsf{F},\mathsf{F}\mathsf{R}\}$ and exactly one $P_{i}=\mathsf{R}$ for $i\in\{3,4,5\}$, $P_{j}=\mathsf{F}$ for $j\in\{3,4,5\}\setminus\{i\}$ (see Table 1 for a graphic representation of the section $P_{1}P_{2}P_{3}P_{4}P_{5}$ of the ring). Observe that the different blocks $\mathsf{B}_{i}$ yield for every robot in the ring a distinct view. Hence, in the rest of the proof we abuse notations and describe the protocol using different names for the different robots, according to their position in the ring, even if they are formally anonymous. We let $\mathcal{R}$ be the set of robots involved. A machine-like (word-)configuration \mathsf{B}_{3}$$\mathsf{F}^{n_{1}}$$\mathsf{R}_{c_{1}}$$\mathsf{F}^{*}$$\mathsf{B}_{4}$$\mathsf{F}^{n_{2}}$$\mathsf{R}_{c_{2}}$$\mathsf{F}^{*}$$\mathsf{B}_{5}$$\mathsf{F}^{m}$$\mathsf{R}_{c}$$\mathsf{F}^{n}$$\mathsf{B}_{6}$$\mathsf{F}^{i}$$\mathsf{R}_{\ell}$$\mathsf{F}^{i^{\prime}}$$\mathsf{B}_{7}$$\mathsf{F}^{p}$$\mathsf{R}_{\ell^{\prime}}$$\mathsf{F}^{r}$$\mathsf{B}_{8} \mathsf{R}_{tt}$$\mathsf{F}$$\mathsf{R}_{t}$$\mathsf{F}$$\mathsf{F}$$\mathsf{R}_{g}$$\mathsf{F}$$\mathsf{R}_{d} is said to be stable because of the positions of robots $\mathsf{R}_{t}$ and $\mathsf{R}_{tt}$ (see Table 1). Moreover, it encodes the configuration $(\ell_{i},n_{1},n_{2})$ of $M$ (due to the relative positions of robots $\mathsf{R}_{c_{1}}$, $\mathsf{R}_{c_{2}}$ and $\mathsf{R}_{\ell}$ respectively to $\mathsf{B}_{3}$, $\mathsf{B}_{4}$ and $\mathsf{B}_{6}$). We say that a configuration $\mathbf{p}$ is machine-like, $\mathsf{stable}$, etc. if its corresponding word-configuration is machine-like, $\mathsf{stable}$, etc. In the following, we distinguish configurations of the 2-counter machine, and configurations of the robots, by calling them respectively $M$-configurations and $\phi$-(word)-configurations. For a stable and machine-like $\phi$-configuration $\mathbf{p}$, we let $M(\mathbf{p})$ be the $M$-configuration encoded by $\mathbf{p}$. We first present the part of the algorithm simulating the behavior of $M$. We call this algorithm $\phi^{\prime}$. Since the machine is deterministic, only one instruction is labelled by $\ell_{i}$, known by every robot. The simulation follows different steps, according to the positions of the robots $\mathsf{R}_{t}$ and $\mathsf{R}_{tt}$, as pictured in Table 1.

We explain the algorithm $\phi^{\prime}$ on the configuration $(\ell_{i},n_{1},n_{2})$ with the transition $\ell_{i}:\texttt{if }c_{1}>0\texttt{ then }c_{1}=c_{1}-1;\texttt{goto }\ell_{j};\texttt{else goto }\ell_{j^{\prime}}$.

• •

When in a $\mathsf{stable}$ configuration, robot $\mathsf{R}_{tt}$ first moves to obtain a $\mathsf{moving1}$ configuration.

• •

In a $\mathsf{moving1}$ configuration, robot $\mathsf{R}_{c}$ moves until it memorizes the current value of $c_{1}$. More precisely, in a $\mathsf{moving1}$ configuration where $n_{1}\neq m$, robot $\mathsf{R}_{c}$ moves : if $n_{1}>m$, and $n\neq 0$, $\mathsf{R}_{c}$ moves towards $\mathsf{B}_{6}$, if $n_{1}<m$, it moves towards $\mathsf{B}_{5}$, if $n_{1}>m$ and $n=0$, it does not move.

• •

In a $\mathsf{moving1}$ configuration where $n_{1}=m$, $\mathsf{R}_{t}$ moves to obtain a $\mathsf{moving2}$ configuration.

• •

In a $\mathsf{moving2}$ configuration, if $n_{1}=m\neq 0$, then $\mathsf{R}_{c_{1}}$ moves towards $\mathsf{B}_{3}$, hence encoding the decrementation of $c_{1}$.

• •

In a $\mathsf{moving2}$ configuration, if $n_{1}=m=0$ or if $n_{1}\neq m$, (then the modification of $c_{1}$ is either impossible, or already done), robot $\mathsf{R}_{\ell^{\prime}}$ moves until it memorizes the position of robot $\mathsf{R}_{\ell}$: if $p<i$, and $r\neq 0$, $\mathsf{R}_{\ell^{\prime}}$ moves towards $\mathsf{B}_{8}$; if $p>i$, $\mathsf{R}_{\ell^{\prime}}$ moves towards $\mathsf{B}_{7}$.

• •

In a $\mathsf{moving2}$ configuration, if $p=i$, then $\mathsf{R}_{t}$ moves to obtain a $\mathsf{moving3}$ configuration.

• •

In a $\mathsf{moving3}$ configuration, if $n_{1}=m=0$, and robot $\mathsf{R}_{\ell^{\prime}}$ encodes $\ell_{i}$ (i.e. $p=i$), then $c_{1}=0$ and robot $\mathsf{R}_{\ell}$ has to move until it encodes $\ell_{j^{\prime}}$. If on the other hand $n_{1}<m$, then robot $\mathsf{R}_{\ell}$ moves until it encodes $\ell_{j}$. More precisely, if $n_{1}=m=0$, and the position encoded by $\mathsf{R}_{\ell}$ is smaller than $j^{\prime}$ ($i<j^{\prime}$), and if $i^{\prime}\neq 0$, then $\mathsf{R}_{\ell}$ moves towards $\mathsf{B}_{7}$. If $n_{1}=m=0$, and the position encoded by $\mathsf{R}_{\ell}$ is greater than $j^{\prime}$, $\mathsf{R}_{\ell}$ moves towards $\mathsf{B}_{6}$. If $n_{1}\neq m$, then robot $\mathsf{R}_{\ell}$ moves in order to reach a position where it encodes $\ell_{j}$ (towards $\mathsf{B}_{6}$ if $i>j$, towards $\mathsf{B}_{7}$ if $i<j$ and $i^{\prime}\neq 0$).

• •

In a $\mathsf{moving3}$ configuration, if the position encoded by $\mathsf{R}_{\ell^{\prime}}$ is $\ell_{i}$, if $n_{1}=m=0$ and the position encoded by $\mathsf{R}_{\ell}$ is $\ell_{j^{\prime}}$, or if $n_{1}\neq m$, and the position encoded by $\mathsf{R}_{\ell}$ is $\ell_{j}$, then the transition has been completely simulated : the counters have been updated and the next transition is stored. The robots then return to a $\mathsf{stable}$ configuration: robot $\mathsf{R}_{tt}$ moves to obtain a $\mathsf{stabilizing1}$ configuration.

• •

In a $\mathsf{stabilizing1}$ configuration, robot $\mathsf{R}_{t}$ moves to obtain a $\mathsf{stabilizing2}$ configuration.

• •

In a $\mathsf{stabilizing2}$ configuration, robot $\mathsf{R}_{t}$ moves to obtain a $\mathsf{stable}$ configuration.

For other types of transitions, the robots move similarly. When in a $\mathsf{stable}$ configuration encoding a configuration in $\mathsf{HALT}$, no robot moves. We describe now the algorithm $\phi$ that simply adds to $\phi^{\prime}$ the two following rules. Robot $\mathsf{R}_{g}$ (respectively $\mathsf{R}_{d}$) moves in the direction of $\mathsf{R}_{d}$ (respectively in the direction of $\mathsf{R}_{g}$) if and only if the robots are in a $\mathsf{stable}$ machine-like configuration, and the encoded configuration of the machine is $(\ell_{0},0,0)$ (respectively is in $\mathsf{HALT}$), (since the configuration is machine-like, the distance between $\mathsf{R}_{g}$ and $\mathsf{R}_{d}$ is 2).

On all configurations that are not machine-like, the algorithm makes sure that no robot move. This implies that once $\mathsf{R}_{g}$ or $\mathsf{R}_{d}$ has moved, no robot with a view up-to-date ever moves. One can easily be convinced that the algorithm can be expressed by a QFP formula $\phi$.

Let the formulae \texttt{Bad}(\mathbf{p}_{1},\dots,\mathbf{p}_{42})=\bigvee_{\text{\scriptsize\begin{tabular}[t]{@{}l@{}}i,j\in[1,42]$\\$i\neq j\end{tabular}}}(\mathbf{p}_{i}=\mathbf{p}_{j}) that is satisfied by all the configurations where two robots share the same position and $\texttt{Ring}(y)=y\geq 0$. We can show that $M$ halts if and only if there exits a size $n\in\left[\!\left[\texttt{Ring}\right]\!\right]$, a $(42,n)$-configuration $\mathbf{p}$ with $\mathbf{p}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$.

$\Box$

Theorem 3

$\mathsf{REACH}_{m}$* is undecidable, for $m\in\{\mathrm{ss},\mathrm{s},\mathrm{as}\}$.*

Sketch of proof.   

The proof relies on a reduction from the repeated reachability problem of a deterministic three-counter zero-initializing bounded-strongly-cyclic machine $M$, which is undecidable [19]. A counter machine is zero-initializing if from the initial instruction $\ell_{0}$ it first sets all the counters to 0. Moreover, an infinite run is said to be space-bounded if there is a value $K\in\mathbb{N}$ such that all the values of all the counters stay below $K$ during the run. A counter machine $M$ is bounded-strongly-cyclic if every space-bounded infinite run starting from any configuration visits $\ell_{0}$ infinitely often. The repeated reachability problem we consider is expressed as follows: given a 3-counter zero-initializing bounded-strongly-cyclic machine $M$, does there exist an infinite space-bounded run of $M$? A configuration of $M$ is encoded in the same fashion than in the proof of Theorem 2, with 3 robots encoding the values of the counters. A transition of $M$ is simulated by the algorithm in the same way than above except that if a counter is to be increased, the corresponding robot moves accordingly even if there is no room to do it, yielding a collision.

$\Box$

4 Decidability results and case study

In this section, we show that even if $\mathsf{SAFE}_{\mathrm{as}}$, $\mathsf{REACH}_{\mathrm{as}}$, $\mathsf{REACH}_{\mathrm{ss}}$ and $\mathsf{REACH}_{\mathrm{s}}$ are undecidable, the other cases $\mathsf{SAFE}_{\mathrm{s}}$ and $\mathsf{SAFE}_{\mathrm{ss}}$ can be reduced to the satisfiability problem for EP formulae, which is decidable and NP-complete [8].

4.1 Reducing safety to successor checking

The first step towards decidability is to remark that to solve $\mathsf{SAFE}_{\mathrm{s}}$ and $\mathsf{SAFE}_{\mathrm{ss}}$ it is enough to look at the one-step successor. Let $\phi$ be a protocol over $k$ robots and Ring and Bad be respectively a ring property and a set of bad configurations. We have then the following lemma.

Lemma 1

Let $n\in\mathbb{N}$ such that $n\in\left[\!\left[\texttt{Ring}\right]\!\right]$ and $m\in\{\mathrm{s},\mathrm{ss}\}$. There exists a $(k,n)$-configuration $\mathbf{p}$ with $\mathbf{p}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\mathbf{Post}_{m}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$ iff there exists a $(k,n)$-configuration $\mathbf{p}^{\prime}$ with $\mathbf{p}^{\prime}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\textbf{Post}_{m}(\phi,\mathbf{p}^{\prime})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$.

This last result may seems strange at a first sight but it can easily be explained by the fact that robots protocols are most of the time designed to work without any assumption on the initial configuration, except that it is not a bad configuration.

4.2 Encoding successor computation in Presburger

We now describe various EP formulae to be used to express the computation of the successor configuration in synchronous and semi-synchronous mode.

First we show how to express the view of some robot $R_{i}$ in a configuration $\mathbf{p}$, with the following formula:

[TABLE]

Note that this formula only expresses in the syntax of Presburger arithmetic the definition of $\mathbf{V}_{\mathbf{p}}[i\rightarrow]$ where the variable $y$ is used to store the length of the ring, $p_{1},\ldots,p_{k}$ represent $\mathbf{p}$ and the variables $d_{1},\ldots,d_{k}$ represent the view.

We also use the formula $\mathtt{ViewSym}(d_{1},\dots,d_{k},d^{\prime}_{1},\dots,d^{\prime}_{k})$ that is useful to compute the symmetric of a view.

[TABLE]

We are now ready to introduce the formula $\mathtt{Move}^{\phi}_{i}(y,p_{1},\dots,p_{k},p^{\prime})$, which is true if and only if, on a ring of size $n$ (represented by the variable $y$), the move of robot $R_{i}$ according to the protocol $\phi$ from the configuration $\mathbf{p}$ yields to the new position $p^{\prime}$. Here the variables $p_{1},\ldots,p_{k}$ characterizes $\mathbf{p}$. .

[TABLE]

Now, given two $(k,n)$-configurations $\mathbf{p}$ and $\mathbf{p}^{\prime}$, and a $k$-protocol $\phi$, it is easy to express the fact that $\mathbf{p}^{\prime}$ is a successor configuration of $\mathbf{p}$ according to $\phi$ in a semi-synchronous run (resp. synchronous run); for this we define the two formulae $\mathtt{SemiSyncPost}_{\phi}(y,p_{1},\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k})$ and $\mathtt{SyncPost}_{\phi}(y,p_{1}\dots,p_{k},p^{\prime}_{1},\dots,p^{\prime}_{k})$) as follows:

[TABLE]

Lemma 2

For all $n\in\mathbb{N}$ and all $(k,n)$-configurations $\mathbf{p}$ and $\mathbf{p}^{\prime}$, we have:

$\mathbf{p}\hookrightarrow\mathbf{p}^{\prime}$* if and only if $n,\mathbf{p},\mathbf{p}^{\prime}\models\mathtt{SemiSyncPost}_{\phi}$,* 2. 2.

$\mathbf{p}\Rightarrow\mathbf{p}^{\prime}$* if and only if $n,\mathbf{p},\mathbf{p}^{\prime}\models\mathtt{SyncPost}_{\phi}$.*

4.3 Results

Now since to solve $\mathsf{SAFE}_{\mathrm{ss}}$ and $\mathsf{SAFE}_{\mathrm{s}}$, we only need to look at the successor in one step, as stated by Lemma 1, and thanks to the formulae $\mathtt{SemiSyncPost}_{\phi}$ and $\mathtt{SyncPost}_{\phi}$ and their properties expressed by Lemma 2, we deduce that these two problems can be expressed in Presburger arithmetic.

Theorem 4

$\mathsf{SAFE}_{\mathrm{s}}$* and $\mathsf{SAFE}_{\mathrm{ss}}$ are decidable and in NP.*

Proof: We consider a ring property $\texttt{Ring}(y)$, a protocol $\phi$ for $k$ robots (which is a QFP formula) and a set of bad configurations given by a QFP formula $\texttt{Bad}(x_{1},\ldots,x_{k})$. We know that there exists a size $n\in\mathbb{N}$ with $n\in\left[\!\left[\texttt{Ring}\right]\!\right]$, and a $(k,n)$-configuration $\mathbf{p}$ with $\mathbf{p}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$ if and only if there exists a $(k,n)$-configuration $\mathbf{p}^{\prime}$ with $\mathbf{p}^{\prime}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\textbf{Post}_{m}(\phi,\mathbf{p}^{\prime})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$. By Lemma 2, this latter property is true if and only if the following formula is satisfiable:

[TABLE]

For the semi-synchronous case, we replace the formula $\mathtt{SyncPost}_{\phi}$ by $\mathtt{SemiSyncPost}_{\phi}$. The NP upper bound is obtained by the fact that the built formula is an EP formula.

$\Box$

When the protocol $\phi$ is uniquely-sequentializable, i.e. when in each configuration at most one robot make the decision to move then Theorem 1 leads us to the following result.

Corollary 1

When the protocol $\phi$ is uniquely-sequentializable, $\mathsf{SAFE}_{\mathrm{as}}$ is decidable.

4.4 Expressing other interesting properties

Not only the method consisting in expressing the successor computation in Presburger arithmetic allows us to obtain the decidability for $\mathsf{SAFE}_{\mathrm{s}}$ and $\mathsf{SAFE}_{\mathrm{ss}}$, but they also allow us to express other interesting properties. For instance, we can compute the successor configuration in asynchronous mode for a protocol $\phi$ working over $k$ robots thanks to the formula $\mathtt{AsyncPost}_{\phi}(y,p_{1},\ldots,p_{k},s_{1},\ldots,s_{k},\linebreak[0]v_{1}\ldots,v_{k},p^{\prime}_{1},\ldots,p^{\prime}_{k},s^{\prime}_{1},\ldots,s^{\prime}_{k},v^{\prime}_{1},\ldots,v^{\prime}_{k})$, which is given by:

[TABLE]

To prove the correctness of this formula for an asynchronous configuration $(\mathbf{p},\mathbf{s},\mathbf{V})$ with $k$ robots we make the analogy between the flags $\mathbf{L}$ and $\mathbf{M}$ and the naturals [math] and $1$, which means that in the definition of the vector $\mathbf{s}\in\{\mathbf{L},\mathbf{M}\}^{k}$, we encode $\mathbf{L}$ by [math] and $\mathbf{M}$ by $1$ and we then apply the definition of $\rightarrow_{\textit{as}}$.

One can also express the fact that one configuration is a predecessor of the other in a straightforward way.

It is as well possible to check whether a protocol $\phi$ over $k$ robots fits into the hypothesis of Corollary 1, i.e. whether it is uniquely-sequentializable. We define the formula $\texttt{UniqSeq}_{\phi}$ that is satisfiable if and only if $\phi$ is uniquely-sequentializable.

[TABLE]

Hence we deduce the following statement.

Theorem 5

Checking whether a protocol $\phi$ is uniquely-sequentializable is decidable.

4.5 Applications

We have considered the exclusive perpetual exploration algorithms proposed by Blin et al. [6], and generated the formulae to check that no collision are encountered for different cases. We have used the SMT solver Z3 [12] to verify whether the generated formulae were satisfiable or not. We have been able to prove that, in the synchronous case, the algorithm using a minimum of $3$ robots was safe for any ring of size greater than $10$ and changing a rule of the algorithm has allowed us to prove that we could effectively detect bugs in the Algorithm. In fact, in this buggy case, the SMT solver provides a configuration leading to a collision after one step. We have then looked for absence of collision for the algorithms using a maximum number of robots, always in the synchronous case. Here, the verification was not parametric as the size of the ring is fixed and depends on the number of robots (it is exactly $5$ plus the number of robots). The objective was to see whether our approach could be applied for a large number of robots. In that case, we have been able to prove that the algorithm for $6$ robots was safe, but we found some bugs for $5$, $7$, $8$, $9$, $10$ and $12$ robots. It was stated in [6] that the algorithm was not working for $5$ robots however the other cases are new bugs. Note however that for $11$ robots, the SMT solver Z3 was taking more than 10 minutes and we did not let him finish its computation. We observe that when there is a bug, the SMT solver goes quite fast to generate a bad configuration but it takes much more time when the algorithm is correct, as for instance with $6$ robots. The files containing the SMT formulae are all available on the webpage [15] in the SMTLIB format.

5 Conclusion

We have addressed two main problems concerning formal verification of protocols of mobile robots, and answered the open questions regarding decidability of the verification of such protocols, when the size of the ring is given as a parameter of the problem. Note that in such algorithms, robots can start in any position on the ring. Simple modifications of the proofs in this paper allow to obtain undecidability of both the reachability and the safety problem in any semantics, when the starting configuration of the robots is given. Hence we give a precise view of what can be achieved in the automated verification of protocols for robots in the parameterized setting, and provide a means of partially verifying them. Of course, to fully demonstrate the correctness of a tentative protocol, more properties are required (like, all nodes are visited infinitely often) that are not handled with our approach. Nevertheless, as intermediate lemmas (for arbitrary $n$) are verified, the whole process of proof writing is both eased and strengthened.

An application of Corollary 1 and Theorem 5 deals with robot program synthesis as depicted in the approach of Bonnet et al. [7]. To simplify computations and save memory when synthesizing mobile robot protocols, their algorithm only generates uniquely-sequentializable protocols (for a given $k$ and $n$). Now, given a protocol description for a given $n$, it becomes possible to check whether this protocol remains uniquely-sequentializable for any $n$. Afterwards, regular safety properties can be devised for this tentative protocol, for all models of computation (that is, FSYNC, SSYNC, and ASYNC). Protocol design is then driven by the availability of a uniquely-serializable solution, a serious asset for writing handwritten proofs (for the properties that cannot be automated).

Last, we would like to mention possible applications of our approach for problems whose core properties seem related to reachability only. One such problem is exploration with stop [5]: robots have to explore and visit every node in a network, then stop moving forever, assuming that all robots initial positions are distinct. All of the approaches published for this problem make use of towers, that is, locations that are occupied by at least two robots, in order to distinguish the various phases of the exploration process (initially, as all occupied nodes are distinct, there are no towers). Our approach still makes it possible to check if the number of created towers remains acceptable (that is below some constant, typically 2 per block of robots that are equally spaced) from any given configuration in the algorithm, for any ring size $n$. As before, such automatically obtained lemmas are very useful when writing the full correctness proof.

Appendix A Proof of Theorem 1

Let $\phi$ be a protocol and $\mathbf{p}$ a configuration. From the definitions, it is obvious that $\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p})\subseteq\mathbf{Post}_{\mathrm{ss}}^{*}(\phi,\mathbf{p})\subseteq\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})$.

We show that, in case $\phi$ is uniquely-sequentializable, we also have $\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})\subseteq\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p})$. We first prove the following property $(P)$ of uniquely-sequentializable runs: for all uniquely-sequentializable protocol $\phi$, for all configuration $\mathbf{p}_{o}$, for all runs $\rho=\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\cdots\in\mathbf{Runs}_{\mathrm{as}}(\phi)$, for all $0\leq k<|\rho|$, for all robot $i$, if $\mathbf{V}_{k}(i)\neq\mathbf{V}_{\mathbf{p}_{k}}[i\rightarrow]$ and $\mathbf{s}_{k}(i)=\mathbf{M}$ then $\mathit{move}(\phi,\mathbf{V}_{k}(i))=\{0\}$. To prove $(P)$, let $\rho\in\mathbf{Runs}_{\mathrm{as}}(\phi)$. We show $(P)$ by induction on $k$. For $k=0$, it is obvious since $\mathbf{s}_{0}(i)=\mathbf{L}$ for all robot $i$. Let $\rho=\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle\cdots\langle\mathbf{p}_{k},\mathbf{s}_{k},\mathbf{V}_{k}\rangle\langle\mathbf{p}_{k+1},\mathbf{s}_{k+1},\mathbf{V}_{k+1}\rangle$ a prefix of a run in $\mathbf{Runs}_{\mathrm{as}}(\phi)$. Let $i$ be a robot such that $\mathbf{s}_{k+1}(i)=\mathbf{M}$ and $\mathbf{V}_{k+1}(i)\neq\mathbf{V}_{\mathbf{p}_{k+1}}[i\rightarrow]$. If $\mathbf{s}_{k}(i)=\mathbf{L}$, then $\mathbf{V}_{k+1}(i)=\mathbf{V}_{\mathbf{p}_{k}}[i\rightarrow]$ and $\mathbf{p}_{k}=\mathbf{p}_{k+1}$, which is impossible. Hence, $\mathbf{s}_{k}(i)=\mathbf{M}$ and $\mathbf{V}_{k}(i)=\mathbf{V}_{k+1}(i)$. Moreover, either $\mathbf{V}_{k}(i)\neq\mathbf{V}_{\mathbf{p}_{k}}[i\rightarrow]$ and by induction hypothesis, $\mathit{move}(\phi,\mathbf{V}_{k}(i))=\mathit{move}(\phi,\mathbf{V}_{k+1}(i))=\{0\}$. Either $\mathbf{V}_{k}(i)=\mathbf{V}_{\mathbf{p}_{k}}[i\rightarrow]\neq\mathbf{V}_{\mathbf{p}_{k+1}}[i\rightarrow]$. Hence there exists another robot $j\neq i$ such that $\mathbf{s}_{k}(j)=\mathbf{M}$ and $\mathbf{s}_{k+1}(j)=\mathbf{L}$ and $\mathit{move}(\phi,\mathbf{V}_{k}(j))\neq\{0\}$. Since $\phi$ is uniquely-sequentializable, $\mathit{move}(\phi,\mathbf{V}_{k}(i))=\mathit{move}(\phi,\mathbf{V}_{k+1}(i))=\{0\}$.

We show now by induction on $n$ that if $\langle\mathbf{p},\mathbf{s}_{0},\mathbf{V}\rangle\leadsto^{n}\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle$ then $p^{\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\phi)$. For $n=0$, it is obvious. Let now $n\in\mathbb{N}$ and let $\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime},\mathbf{p}^{\prime\prime},\mathbf{s}^{\prime\prime}$, and $\mathbf{V}^{\prime\prime}$ such that $\langle\mathbf{p},\mathbf{s}_{0},\mathbf{V}\rangle\leadsto^{n}\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle\leadsto\langle\mathbf{p}^{\prime\prime},\mathbf{s}^{\prime\prime},\mathbf{V}^{\prime\prime}\rangle$. By induction hypothesis, $\mathbf{p}^{\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\mathbf{p})$. Let $i$ be such that $\mathbf{s}^{\prime\prime}(i)\neq\mathbf{s}^{\prime}(i)$. If $s^{\prime}(i)=L$ then by definition, $\mathbf{p}^{\prime\prime}=\mathbf{p}^{\prime}$ and $\mathbf{p}^{\prime\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\mathbf{p})$. Otherwise, if $\mathbf{V}_{\mathbf{p}^{\prime}}[i\rightarrow]\neq\mathbf{V}^{\prime}(i)$, then by $(P)$, $\mathit{move}(\phi,\mathbf{V}^{\prime}(i))=\{0\}$ and then $\mathbf{p}^{\prime}=\mathbf{p}^{\prime\prime}$. If $\mathbf{V}_{\mathbf{p}^{\prime}}[i\rightarrow]=\mathbf{V}^{\prime}(i)$, either $\mathit{move}(\phi,\mathbf{V}^{\prime}(i))=\{0\}$ and $\mathbf{p}^{\prime\prime}=\mathbf{p}^{\prime}$ or, $\mathit{move}(\phi,\mathbf{V}^{\prime}(i))\neq\{0\}$ and, since $\phi$ is uniquely-sequentializable, for all $j\neq i$, $\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}^{\prime}}[j\rightarrow])=\{0\}$ and $\mathbf{p}^{\prime}\Rightarrow\mathbf{p}^{\prime\prime}$. Hence $\mathbf{p}^{\prime\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\mathbf{p})$.

Appendix B Proof of Theorem 2

We show that $M$ halts if and only if there exits a size $n\in\mathbb{N}$, a $(42,n)$-configuration $\mathbf{p}$ with $\mathbf{p}\notin\left[\!\left[\texttt{Bad}\right]\!\right]$, such that $\mathbf{Post}_{\mathrm{as}}^{*}(\phi,\mathbf{p})\cap\left[\!\left[\texttt{Bad}\right]\!\right]\neq\emptyset$.

For that matter, we use several claims about $\phi^{\prime}$. First observe that $\phi^{\prime}$ is uniquely-sequentializable.

Claim 1

Let $\mathbf{p}$ be a machine-like $\phi$-configuration. Then for all configuration $\mathbf{p}^{\prime}\in\mathbf{Post}_{\mathrm{as}}^{*}(\phi^{\prime},\mathbf{p})=\mathbf{Post}_{\mathrm{s}}^{*}(\phi^{\prime},\mathbf{p})$, $\mathbf{p}^{\prime}$ is machine-like.

Claim 2

Let $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle$ be a $\mathsf{stable}$ and machine-like asynchronous $\phi$-configuration corresponding to the following word-configuration: \mathsf{B}_{3}$$\mathsf{F}^{n_{1}}$$\mathsf{R}_{c_{1}}$$\mathsf{F}^{n^{\prime}_{1}}$$\mathsf{B}_{4}$$\mathsf{F}^{n_{2}}$$\mathsf{R}_{c_{2}}$$\mathsf{F}^{n^{\prime}_{2}}$$\mathsf{B}_{5}$$\mathsf{F}^{m}$$\mathsf{R}_{c}$$\mathsf{F}^{n}$$\mathsf{B}_{6}$$\mathsf{F}^{i}$$\mathsf{R}_{\ell}$$\mathsf{F}^{i^{\prime}}$$\mathsf{B}_{7}$$\mathsf{F}^{p}$$\mathsf{R}_{\ell^{\prime}}$$\mathsf{F}^{r}$$\mathsf{B}_{8} \mathsf{R}_{tt}$$\mathsf{F}$$\mathsf{R}_{t}$$\mathsf{F}$$\mathsf{F}$$\mathsf{R}_{g}$$\mathsf{F}$$\mathsf{R}_{d}. Let $M(\mathbf{p})=(\ell_{i},n_{1},n_{2})$ a non-halting $M$-configuration. Assume that $\mathbf{p}$ has the following properties. $(i)$ if $n_{1}>m$ then $n\geq n_{1}-m$ (if $\ell_{i}$ modifies $c_{1}$) or if $n_{2}>m$ then $n\geq n_{2}-m$ (if $\ell_{i}$ modifies $c_{2}$), $(ii)$ if $\ell_{i}$ increments $c_{1}$ (resp. $c_{2}$) then $n^{\prime}_{1}>0$ (resp. $n^{\prime}_{2}>0$), and $(iii)$ $i+i^{\prime}=p+r=|L|$. Then $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle\leadsto^{*}_{\phi^{\prime}}\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle$ with $\mathbf{p}^{\prime}$ $\mathsf{stable}$ and machine-like, such that $M(\mathbf{p})\vdash M(\mathbf{p}^{\prime})$.

Claim 3

Let $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle$ and $\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle$ be two asynchronous configurations, with $\mathbf{p}$ and $\mathbf{p}^{\prime}$ $\mathsf{stable}$. If there exists $k>0$ such that $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle\leadsto^{k}_{\phi^{\prime}}\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle$ and for all $0<j<k$, if $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle\leadsto^{j}_{\phi^{\prime}}\langle\mathbf{p}^{\prime\prime},\mathbf{s}^{\prime\prime},\mathbf{V}^{\prime\prime}\rangle$ we have $\mathbf{p}^{\prime\prime}$ not $\mathsf{stable}$, then $M(\mathbf{p})\vdash M(\mathbf{p}^{\prime})$.

Assume that $M$ halts. There is then a finite bound $K\in\mathbb{N}$ on the values of the counter during the run. We show hereafter an asynchronous $\phi$-run leading to a collision. Let $\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle$ be the initial configuration of the run, with $\mathbf{p}_{0}$ a $\phi$-configuration corresponding to the word-configuration

[TABLE]

hence such that $M(\mathbf{p}_{0})=(\ell_{0},0,0)$, and $\mathbf{s}_{0}(i)=\mathbf{L}$ for all $i\in\mathcal{R}$. Then $\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle\leadsto\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle$ where $\mathbf{p}_{1}=\mathbf{p}_{0}$, $\mathbf{s}_{1}(g)=\mathbf{M}$, $\mathbf{V}_{1}(g)=\mathbf{V}_{\mathbf{p}_{0}}[g\rightarrow]$, and $\mathbf{s}_{1}(i)=\mathbf{s}_{0}(i)$ and $\mathbf{V}_{1}(i)=\mathbf{V}_{0}(i)$ for all $i\in\mathcal{R}\setminus\{g\}$. It is easy to check that, at each step of a run starting from $\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle$, the conditions $(i)$, $(ii)$ and $(iii)$ of Claim 2 are satisfied. Then, since $M$ halts, by applying iteratively Claim 2, we have $\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\leadsto^{*}_{\phi^{\prime}}\langle\mathbf{p}_{n},\mathbf{s}_{n},\mathbf{V}_{n}\rangle$ with $M(\mathbf{p}_{n})$ a halting configuration. Now, the $\phi$-run continues with robot $d$ being scheduled to look, and then robots $g$ and $d$ moving, leading to a collision. Formally : $\langle\mathbf{p}_{n},\mathbf{s}_{n},\mathbf{V}_{n}\rangle\leadsto\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle\leadsto\langle\mathbf{p}^{\prime},\mathbf{s}^{\prime},\mathbf{V}^{\prime}\rangle\leadsto\langle\mathbf{p}^{\prime\prime},\mathbf{s}^{\prime\prime},\mathbf{V}^{\prime\prime}\rangle$, with $\mathbf{p}_{n}=\mathbf{p}$, $\mathbf{s}(d)=\mathbf{M}$, and $\mathbf{V}(d)=\mathbf{V}_{\mathbf{p}_{n}}[d\rightarrow]$, $\mathbf{p}^{\prime}(d)=\mathbf{p}(d)-1$ since $\mathbf{V}(d)$ memorizes the encoding of a halting configuration, with distance between $\mathsf{R}_{g}$ and $\mathsf{R}_{d}$ equal to 2. Last, $\mathbf{p}^{\prime\prime}(g)=\mathbf{p}(g)+1$ since $\mathbf{V}(g)$ memorizes the encoding of the initial configuration, with distance between $\mathsf{R}_{g}$ and $\mathsf{R}_{d}$ equal to 1. Hence, $\mathbf{p}^{\prime\prime}(g)=\mathbf{p}^{\prime\prime}(d)$ and $\mathbf{p}^{\prime\prime}\in\mathbf{Post}_{as}^{*}(\phi,\mathbf{p}_{0})\cap\left[\!\left[\texttt{Bad}\right]\!\right]$.

Conversely assume there is an asynchronous $\phi$-run $\rho$ leading to a collision. By Claim 1, if $\rho$ is in fact a $\phi^{\prime}$ asynchronous run, there is no collision (either $\rho$ starts in a non machine-like configuration and no robot moves, or it starts in a machine-like configuration and it never reaches a collision, since machine-like configurations are collision-free by construction). Hence $\rho$ contains moves from $\mathsf{R}_{g}$ and/or $\mathsf{R}_{d}$. Assume $\mathsf{R}_{d}$ moves in this run. Hence, there is a configuration $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle$ in this run where $\mathsf{R}_{d}$ has just been scheduled to move and is hence such that $\mathbf{s}(\mathsf{R}_{d})=\mathbf{M}$, $\mathbf{V}(\mathsf{R}_{d})=\mathbf{V}_{\mathbf{p}}[\mathsf{R}_{d}\rightarrow]$, with $\mathit{move}(\phi,\mathbf{V}(\mathsf{R}_{d}))\neq 0$. Hence, by definition of $\phi$, $\mathbf{p}$ is machine-like, $\mathsf{stable}$ and $M(\mathbf{p})$ is a halting $M$-configuration. Let $j\neq\mathsf{R}_{g}$ a robot such that $\mathbf{s}(j)=\mathbf{M}$. If $\mathit{move}(\phi,V(j))\neq\{0\}$, by Proposition (P) from the proof of Theorem 1 and since $\mathit{move}(\phi,V(j))=\mathit{move}(\phi^{\prime},V(j))$, $V(j)=\mathbf{V}_{\mathbf{p}}[j\rightarrow]$, and it is impossible since $M(\mathbf{p})$ is a halting configuration. Hence, from $\langle\mathbf{p},\mathbf{s},\mathbf{V}\rangle$ the only robots that can move are $\mathsf{R}_{d}$ and $\mathsf{R}_{g}$. If $\mathsf{R}_{g}$ does not move, then all the following configurations in the run is $\mathbf{p}^{\prime}$ with $\mathbf{p}^{\prime}(i)=\mathbf{p}(i)$ for all $i\neq\mathsf{R}_{d}$ and $\mathbf{p}^{\prime}(\mathsf{R}_{d})=\mathbf{p}(\mathsf{R}_{d})+1$. Hence, $\rho$ does not lead to a collision.

Assume now that $\mathsf{R}_{g}$ moves in $\rho$. Let $\rho^{\prime}\cdot\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\langle\mathbf{p}_{2},\mathbf{s}_{2},\mathbf{V}_{2}\rangle$ be a prefix of $\rho$ such that $\mathbf{p}_{2}(\mathsf{R}_{g})=\mathbf{p}_{1}(\mathsf{R}_{g})-1$ and $\mathbf{p}_{2}(i)=\mathbf{p}_{1}(i)$ for all $i\neq\mathsf{R}_{g}$, and $\rho^{\prime}\cdot\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle$ is a prefix of a $\phi^{\prime}$-run. Then $\mathbf{p}_{1}$ is a machine-like configuration and again by Proposition (P) of the proof of Theorem 1, there is at most one robot $i\notin\{\mathsf{R}_{g},\mathsf{R}_{d}\}$ such that $\mathit{move}(\phi^{\prime},\mathbf{V}_{1}(i))=\mathit{move}(\phi^{\prime},\mathbf{V}_{2}(i))\neq\{0\}$. Hence if $\mathsf{R}_{d}$ does not move in $\rho$ then $\rho=\rho^{\prime}\cdot\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\langle\mathbf{p}_{2},\mathbf{s}_{2},\mathbf{V}_{2}\rangle\langle\mathbf{p}_{3},\mathbf{s}_{3},\mathbf{V}_{3}\rangle\cdot\rho^{\prime\prime}$ with $\mathbf{p}_{3}(i)=\mathbf{p}_{2}(i)$ for all the robots $i$ but possibly one, and then $\mathbf{p}_{3}$ being the only configuration appearing in $\rho^{\prime\prime}$. According to $\phi^{\prime}$, $\mathbf{p}_{3}$ is collision free, so such a run could not yield a collision.

Hence, we know that in $\rho$ both $\mathsf{R}_{g}$ and $\mathsf{R}_{d}$ moves. Moreover, from the above reasonings we deduce that in $\rho$, at some point $\mathsf{R}_{g}$ has been scheduled to look, then later on, $\mathsf{R}_{d}$ has been scheduled to look, and just after, $\mathsf{R}_{g}$ and $\mathsf{R}_{d}$ have moved provoking a collision. Formally, $\rho$ is in the following form: $\rho=\rho^{\prime}\cdot\langle\mathbf{p}_{0},\mathbf{s}_{0},\mathbf{V}_{0}\rangle\langle\mathbf{p}_{1},\mathbf{s}_{1},\mathbf{V}_{1}\rangle\cdot\rho^{\prime\prime}\cdot\langle\mathbf{p}_{2},\mathbf{s}_{2},\mathbf{V}_{2}\rangle\langle\mathbf{p}_{3},\mathbf{s}_{3},\mathbf{V}_{3}\rangle\langle\mathbf{p}_{4},\mathbf{s}_{4},\mathbf{V}_{4}\rangle\langle\mathbf{p}_{5},\mathbf{s}_{5},\mathbf{V}_{5}\rangle$ with $\rho^{\prime},\rho^{\prime\prime}$ asynchronous $\phi^{\prime}$-runs, $\mathbf{s}_{0}(\mathsf{R}_{g})=\mathbf{L}$, $\mathbf{s}_{1}(\mathsf{R}_{g})=\mathbf{M}$, and for all other robots $i$, $\mathbf{s}_{0}(i)=\mathbf{s}_{1}(i)$, and $\mathbf{p}_{0}=\mathbf{p}_{1}$, and $\mathit{move}(\phi,\mathbf{V}_{1}(\mathsf{R}_{g}))\neq\{0\}$, $\mathbf{p}_{2}=\mathbf{p}_{3}$, $\mathbf{s}_{2}(\mathsf{R}_{d})=\mathbf{L}$, $\mathbf{s}_{3}(\mathsf{R}_{d})=\mathbf{M}$, $\mathit{move}(\phi,\mathbf{V}_{3}(\mathsf{R}_{d}))\neq\{0\}$, and either $\mathbf{p}_{4}(\mathsf{R}_{d})=\mathbf{p}_{3}(\mathsf{R}_{d})+1$, and for all $i\neq\mathsf{R}_{d}$, $\mathbf{p}_{3}(i)=\mathbf{p}_{4}(i)$ and $\mathbf{p}_{5}(\mathsf{R}_{g})=\mathbf{p}_{4}(\mathsf{R}_{g})-1$ and for all $i\neq\mathsf{R}_{g}$, $\mathbf{p}_{4}(i)=\mathbf{p}_{5}(i)$, or $\mathbf{p}_{4}(\mathsf{R}_{g})=\mathbf{p}_{3}(\mathsf{R}_{g})-1$, and for all $i\neq\mathsf{R}_{g}$, $\mathbf{p}_{3}(i)=\mathbf{p}_{4}(i)$ and $\mathbf{p}_{5}(\mathsf{R}_{d})=\mathbf{p}_{4}(\mathsf{R}_{d})-1$ and for all $i\neq\mathsf{R}_{d}$, $\mathbf{p}_{4}(i)=\mathbf{p}_{5}(i)$. In both cases, we deduce that since $\mathit{move}(\phi,\mathbf{V}_{1}(\mathsf{R}_{g}))\neq\{0\}$, then $\mathbf{p}_{0}$ is a machine-like $\mathsf{stable}$ configuration such that $M(\mathbf{p}_{0})=C_{0}$, and since $\mathit{move}(\phi,\mathbf{V}_{3}(\mathsf{R}_{d}))\neq\{0\}$, then $\mathbf{p}_{2}$ is a machine-like $\mathsf{stable}$ configuration encoding a halting $M$-configuration $C_{h}$. Hence, from Claim 3, since $\mathbf{p}_{0}\leadsto^{*}\mathbf{p}_{2}$ then $C_{0}\vdash\cdots\vdash C_{h}$ and $M$ halts.

Appendix C Proof of Theorem 3

The proof relies on a reduction from the repeated reachability problem of a deterministic three-counter zero-initializing bounded-strongly-cyclic machine $M$, which is undecidable [19]. A counter machine is zero-initializing if from the initial instruction $\ell_{0}$ it first sets all the counters to 0. Moreover, an infinite run is said to be space-bounded if there is a value $K\in\mathbb{N}$ such that all the values of all the counters stay below $K$ during the run. A counter machine $M$ is bounded-strongly-cyclic if every space-bounded infinite run starting from any configuration visits $\ell_{0}$ infinitely often. The repeated reachability problem we consider is expressed as follows: given a 3-counter zero-initializing bounded-strongly-cyclic machine $M$, does there exist an infinite space-bounded run of $M$? A configuration of $M$ is encoded in the same fashion than in the proof of Theorem 2, with 3 robots encoding the values of the counters. A transition of $M$ is simulated by the algorithm in the same way than above except that if a counter is to be increased, the corresponding robot moves accordingly even if there is no room to do it, yielding a collision.

We use the following claims, reminiscent of the claims used in the proof of Theorem 2:

Claim 4

Let $\mathbf{p}$ be a machine-like configuration. Then, for all configuration $\mathbf{p}^{\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p})$, $\mathbf{p}^{\prime}\in\left[\!\left[\texttt{Machine\_like}\vee\texttt{Collision}\right]\!\right]$.

Claim 5

*Let $\mathbf{p}$ be a $\mathsf{stable}$ and machine-like synchronous $\overline{\phi}$-configuration corresponding to the following word-configuration: $\mathsf{B}_{3}\mathsf{F}^{n_{1}}\mathsf{R}_{c_{1}}\mathsf{F}^{n^{\prime}_{1}}\mathsf{B}_{4}\mathsf{F}^{n_{2}}\mathsf{R}_{c_{2}}\mathsf{F}^{n^{\prime}_{2}}\mathsf{B}_{5}\mathsf{F}^{n_{3}}\mathsf{R}_{c_{3}}\mathsf{F}^{n^{\prime}_{3}}\mathsf{B}_{6}\mathsf{F}^{m}\mathsf{R}_{c}\mathsf{F}^{n}\mathsf{B}_{7}\mathsf{F}^{i}\mathsf{R}_{\ell}\mathsf{F}^{i^{\prime}}\mathsf{B}_{8}$

$\mathsf{F}^{p}\mathsf{R}_{\ell^{\prime}}\mathsf{F}^{r}\mathsf{B}_{9}\mathsf{R}_{tt}\mathsf{F}\mathsf{R}_{t}\mathsf{F}\mathsf{F}.$ Let $M(\mathbf{p})=(\ell_{i},n_{1},n_{2},n_{3})$ be a non-halting $M$-configuration. Assume that $\mathbf{p}$ has the following properties. $(i)$ if $n_{1}>m$ (respectively $n-2>m$, $n-3>m$), then $n\geq n_{1}-m$ (respectively $n\geq n_{2}-m$, $n\geq n_{3}-m$)(if $\ell_{i}$ modifies $c_{1}$ - respectively $c_{2}$ or $c_{3}$), $(ii)$ if $\ell_{i}$ increments $c_{1}$ (resp. $c_{2}$ or $c_{3}$) then $n^{\prime}_{1}>0$ (resp. $n^{\prime}_{2}>0$, or $n^{\prime}_{3}>0$), and $(iii)$ $i+i^{\prime}=p+r=|L|$. Then $\mathbf{p}\leadsto^{*}_{\overline{\phi}}\mathbf{p}^{\prime}$ with $\mathbf{p}^{\prime}$ $\mathsf{stable}$ and machine-like, such that $M(\mathbf{p})\vdash M(\mathbf{p}^{\prime})$.*

Claim 6

Let $\mathbf{p},\mathbf{p}^{\prime}$ be two $\mathsf{stable}$, machine-like configurations. If there exists some $k>0$ such that $\mathbf{p}\Rightarrow_{\overline{\phi}}^{k}\mathbf{p}^{\prime}$ and that for all $0<j<k$, if $\mathbf{p}\Rightarrow_{\overline{\phi}}^{j}\mathbf{p}^{\prime\prime}$ then $\mathbf{p}^{\prime\prime}$ is not $\mathsf{stable}$, then $M(\mathbf{p})\vdash M(\mathbf{p}^{\prime})$.

Claim 7

Let $\mathbf{p}$ be a machine-like configuration, which is not $\mathsf{stable}$. Then, either $|\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p})|$ is finite, or there exists $\mathbf{p}^{\prime}\in\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p})$ with $\mathbf{p}^{\prime}$ $\mathsf{stable}$.

If there is an infinite space-bounded run of $M$, we let $K\in\mathbb{N}$ be the maximal values of all the counters during this run. Let $\mathbf{p}_{0}$ be the $\phi$-configuration having the following word-representation: $\mathsf{B}_{3}\mathsf{R}_{c_{1}}\mathsf{F}^{K}\mathsf{B}_{4}\mathsf{R}_{c_{2}}\mathsf{F}^{K}\mathsf{B}_{5}\mathsf{R}_{c_{3}}\mathsf{F}^{K}\mathsf{B}_{6}\mathsf{R}_{c}\mathsf{F}^{K}\mathsf{B}_{7}\mathsf{R}_{\ell}\mathsf{F}^{i^{\prime}}\mathsf{B}_{8}\mathsf{F}^{p}\mathsf{R}_{\ell^{\prime}}\mathsf{F}^{r}\mathsf{B}_{9}$

$\mathsf{R}_{tt}\mathsf{F}\mathsf{R}_{t}\mathsf{F}\mathsf{R}_{g}\mathsf{F}\mathsf{R}_{d}$. Hence $M(\mathbf{p}_{0})$ is the initial configuration of $M$. It is easy to show that, for all $\mathbf{p}\in\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p}_{0})$, $\mathbf{p}$ satisfies conditions $(i)$, $(ii)$, and $(iii)$ of Claim 5. Hence, by applying iteratively Claim 5, we can build an infinite $\overline{\phi}$-run $\rho=\mathbf{p}_{0}\mathbf{p}_{1}\cdots$ such that $\mathbf{p}_{i}\notin\left[\!\left[\texttt{Collision}\vee\texttt{Halting}\right]\!\right]$ for all $i\geq 0$. Hence, by Claim 4, $\mathbf{p}_{i}\in\left[\!\left[\texttt{Machine\_like}\right]\!\right]$ for all $i\geq 0$, and $\mathbf{p}_{i}\notin\left[\!\left[\texttt{Goal}\right]\!\right]$ for all $i\geq 0$. Moreover, for all machine-like configuration $\mathbf{p}$, for all $i\in\mathcal{R}$, $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\neq\mathbf{V}_{\mathbf{p}}[\leftarrow i]$, then it can have at most one successor, and $\rho$ is the only $\phi$-run starting from $\mathbf{p}_{0}$. Hence, $\mathbf{Post}_{\mathrm{s}}^{*}(\phi,\mathbf{p}_{0})\cap\left[\!\left[\texttt{Goal}\right]\!\right]=\emptyset$.

Conversely, assume that there is $n\in\mathbb{N}$ and a $(k,n)$-$\phi$-configuration $\mathbf{p}_{0}$ such that $\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p}_{0})\cap\left[\!\left[\texttt{Goal}\right]\!\right]=\emptyset$. Hence, for all $\mathbf{p}\in\mathbf{Post}_{\mathrm{s}}^{*}(\overline{\phi},\mathbf{p}_{0})$, $\mathbf{p}\in\left[\!\left[\texttt{Machine\_like}\right]\!\right]$. Then, according to the definition of the protocol, there is a unique synchronous $\overline{\phi}$-run starting from $\mathbf{p}_{0}$. Assume for the sake of contradiction that this run is finite. Let $\rho=\mathbf{p}_{0}\cdots\mathbf{p}_{m}$ be such a run. Then $\mathbf{p}_{m}\notin\left[\!\left[\texttt{Goal}\right]\!\right]$ hence $M(\mathbf{p}_{m})$ is not a halting configuration and $\mathbf{p}_{m}$ is collision-free. If it is not $\mathsf{stable}$, $\textbf{Post}_{\mathrm{s}}(\overline{\phi},\mathbf{p}_{m})\neq\emptyset$, from the definition of the protocol. If $\mathbf{p}_{m}$ is $\mathsf{stable}$, either $M(\mathbf{p}_{m})=(\ell_{h},n_{1},n_{2},n_{3})$ for some $n_{1},n_{2},n_{3}\in\mathbb{N}$, but then $\mathbf{p}_{m}\in\left[\!\left[\texttt{Halting}\right]\!\right]\subseteq\left[\!\left[\texttt{Goal}\right]\!\right]$, which is not possible, or there exists a configuration $\mathbf{p}_{m+1}$ such that $\mathbf{p}_{m}\Rightarrow\mathbf{p}_{m+1}$ and $\rho$ can be continued. Hence let $\rho=\mathbf{p}_{0}\mathbf{p}_{1}\cdots$ be the infinite synchronous $\overline{\phi}$-run starting from $\mathbf{p}_{0}$. Assume that $\mathbf{p}_{0}$ is not $\mathsf{stable}$. Then, by Claim 7, there exists $i\geq 0$, such that $\mathbf{p}_{i}$ is $\mathsf{stable}$. By definition of $\overline{\phi}$, $\mathbf{p}_{i+1}$ is not $\mathsf{stable}$, but by Claim 7 and Claim 6, there exists $j>i+1$ such that $\mathbf{p}_{j}$ is $\mathsf{stable}$ and $M(\mathbf{p}_{i})\vdash M(\mathbf{p}_{j})$. By iterating this reasoning, we can in fact build an infinite run of $M$ starting in $M(\mathbf{p}_{i})$. Let $K$ be the maximal number of positions between respectively $\mathsf{B}_{3}$ and $\mathsf{B}_{4}$, $\mathsf{B}_{4}$ and $\mathsf{B}_{5}$, $\mathsf{B}_{5}$ and $\mathsf{B}_{6}$ and $\mathsf{B}_{6}$ and $\mathsf{B}_{7}$ in $\mathbf{p}_{0}$. It is easy to see that this distance is an invariant of any $\overline{\phi}$-run. Hence, for any $k\geq 0$ such that $\mathbf{p}_{k}$ is $\mathsf{stable}$, $M(\mathbf{p}_{k})=(\ell,n_{1},n_{2},n_{3})$ with $n_{i}\leq K$ for $i\in\{1,2,3\}$, and the infinite run of $M$ is indeed space-bounded. Let $C_{0}\vdash C_{1}\cdots$ be such a run. Since $M$ is bounded-strongly-cyclic, there exists $i\geq 0$ such that $C_{i}=(\ell_{0},n_{1},n_{2},n_{3})$ with $n_{i}\in\mathbb{N}$ for $i=\{1,2,3\}$, and since $M$ is zero-initializing, then there exists $j\geq i$ such that $C_{j}=(\ell_{0},0,0,0)$. Hence, $M$ has an infinite space-bounded run from $(\ell_{0},0,0,0)$.

Appendix D Correction of the Presburger formulae

Lemma 3

For all $i\in[1,k]$, we have $n,\mathbf{p},\mathbf{V}\models\mathtt{ConfigView}_{i}$ if and only if $\langle d_{1},\dots,d_{k}\rangle=\mathbf{V}_{\mathbf{p}}[i\rightarrow]$ on a ring of size $n$ .

Proof: Assume $n,\mathbf{p},\mathbf{V}\models\mathtt{ConfigView}_{i}$. Then, there exist $k-1$ variables, $d^{\prime}_{1},\dots,d^{\prime}_{k-1}\in[1,n]$ such that $0<d^{\prime}_{1}\leq d^{\prime}_{2}\leq\dots\leq d^{\prime}_{k-1}$. Moreover, there exists a bijection $f:[1,k-1]\rightarrow[1,k-1]$ such that, for all $j\neq i$, $p_{j}=(p_{i}+d^{\prime}_{f(j)})\mod n$. Finally, $d_{1}=d^{\prime}_{1}$ and for all $j\in[2,n-1]$, $d_{j}=d^{\prime}_{j}-d^{\prime}_{j-1}$ and $d_{k}=n-d^{\prime}_{k-1}$. Hence, if we consider the configuration $\mathbf{p}$ defined by $\mathbf{p}(j)=p_{j}$ for all $j\in[1,n]$, then $\langle d_{1},\dots,d_{k}\rangle=\mathbf{V}_{\mathbf{p}}[i\rightarrow]$. Conversely, let $\mathbf{p}$ be a $(k,n)$-configuration and $\mathbf{V}_{\mathbf{p}}[i\rightarrow]=\langle d_{1},\dots,d_{k}\rangle$. Then, $n,\mathbf{p},\mathbf{V}\models\mathtt{ConfigView}_{i}$. Indeed, by definition of the view, we let $d_{i}(j)\in[1,n]$ be such that $(\mathbf{p}(i)+d_{i}(j))\odot n=\mathbf{p}(j)$ for all $j\neq i$ and we let $i_{1},\dots,i_{k}$ be a permutation of positions such that $0<d_{i}(i_{1})\leq d_{i}(i_{2})\leq\dots\leq d_{i}(i_{k-1})$. Then, for all $j\in[2,k-1]$, $d_{j}=d_{i}(i_{j})-d_{i}(i_{j-1})$, $d_{1}=d_{i}(i_{1})$ and $d_{k}=n-d_{i}(i_{k-1})$. By interpreting the variables $d^{\prime}_{1},\dots,d^{\prime}_{k}$ by respectively $d_{i}(i_{1}),\dots,d_{i}(i_{k})$, it is easy to see that the formula is satisfied.

$\Box$

Lemma 4

For all $n\in\mathbb{N}$, for all views $\mathbf{V},\mathbf{V}^{\prime}\in[0,n]^{k}$, we have $\mathbf{V},\mathbf{V^{\prime}}\models\mathtt{ViewSym}$ if and only if $\mathbf{V}^{\prime}=\overleftarrow{\mathbf{V}}$.

Proof: Given $n\in\mathbb{N}$, $d_{1},\dots,d_{k},d^{\prime}_{1},\dots,d^{\prime}_{k}\in[0,n]$ such that $d_{1}\neq 0$ we have $\langle d^{\prime}_{1},\dots,d^{\prime}_{k}\rangle=\overleftarrow{\langle d_{1},\dots,d_{k}\rangle}$ if and only if there exists $1\leq j\leq k$ such that $d_{\ell}=0$ for all $j+1\leq\ell\leq k$ and $d^{\prime}_{1}=d_{j}$, …, $d^{\prime}_{j}=d_{1}$ and $d^{\prime}\ell=0$ for all $j+1\leq\ell\leq k$ (by definition), if and only if $d_{1},\ldots,d_{k},d^{\prime}_{1},\ldots,d^{\prime}_{k}\models\mathtt{ViewSym}$.

$\Box$

Lemma 5

For all $n\in\mathbb{N}$ and a $(k,n)$-configurations $\mathbf{p}$ and $p^{\prime}\in[0,n-1]$, we have $n,\mathbf{p},\mathbf{p}^{\prime}\models\mathtt{Move}^{\phi}_{i}$ if and only if $p^{\prime}=(\mathbf{p}(i)+m)\odot n$ with $m\in\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$.

Proof: We have $n,\mathbf{p},\mathbf{p}^{\prime}\models\mathtt{Move}^{\phi}_{i}$ if and only if there exist $d_{1},\dots,d_{k},d^{\prime}_{1},\dots,d^{\prime}_{k}\in[0,n]$ such that $\langle d_{1},\dots,d_{k}\rangle=\mathbf{V}_{\mathbf{p}}[i\rightarrow]$ (by Lemma 3) and $\langle d^{\prime}_{1},\dots,d^{\prime}_{k}\rangle=\overleftarrow{\langle d_{1},\dots,d_{k}\rangle}=\mathbf{V}_{\mathbf{p}}[\leftarrow i]$ (by Lemma 4) and either $(i)$ $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\models\phi$ and $p^{\prime}=(p_{i}+1)\odot n$, or $(ii)$ $\mathbf{V}_{\mathbf{p}}[\leftarrow i]\models\phi$ and $p^{\prime}=(p_{i}-1)\odot n$, or $(iii)$ $\mathbf{V}_{\mathbf{p}}[i\rightarrow]\not\models\phi$, $\mathbf{V}_{\mathbf{p}}[\leftarrow i]\not\models\phi$ and $p^{\prime}=p_{i}$, if and only if either $(i)$ $1\in\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$ and $p^{\prime}=(p_{i}+1)\odot n$ or $(ii)$ $-1\in\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$ and $p^{\prime}=(p_{i}-1)\odot n$ or $(iii)$ $\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])=\{0\}$ and $p^{\prime}=p_{i}$ if and only if $p^{\prime}=(p_{i}+m)\odot n$ with $m\in\mathit{move}(\phi,\mathbf{V}_{\mathbf{p}}[i\rightarrow])$.

$\Box$