arXiv:1706.05193v1 [cs.DC] 16 Jun 2017

Parameterized Verification of Algorithms for Oblivious
Robots on a Ring
Arnaud Sangnier∗

Nathalie Sznajder⋆
Sébastien Tixeuil⋆

Maria Potop-Butucaru⋆

∗

⋆

IRIF - Univ Paris Diderot - Paris, France
Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6, F-75005, Paris,
France
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 parameterized 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.

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
1

R1

R3

R2

(a) A disoriented robot R1
R1 , R2
R5
R4

R3

(b) A configuration with a tower

Figure 1
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-computemove 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
2

fully synchronous model (FSYNC), all robots evolve simultaneously and complete a full lookcompute-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 ε, robots are required to reach locations that are at most ε 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.

3

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 (SAFE), and when
it is a reachability objective (REACH). We show that if REACH is undecidable in any semantics,
SAFE is decidable in FSYNC and SSYNC. We also show that when the protocol is uniquelysequentializable, 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 ∈ Z such that a ≤ b, we denote by [a, b] the set {c ∈ Z | a ≤ c ≤ b}. For a ∈ Z and b ∈ N,
we write a ⊙ b the natural d ∈ [0, (b − 1)] such that there exists j ∈ Z and a = b. j + d (for instance
−1 ⊙ 3 = 2). Note that ⊙ 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 t ::= x | t + t | a · t | t mod a, where a ∈ N
and x ∈ Y and then the grammar for formulae is given by φ ::= t ⊲⊳ b | φ ∧ φ | φ ∨ φ | ∃x.φ
where ⊲⊳ ∈ {=, ≤, ≥, <, >}, x ∈ Y and b ∈ N. We sometimes write a formula φ as φ(x1 , . . . , xk ) to
underline that x1 , . . . , xk are the free variables of φ. The set of Quantifier Free Presburger (QFP)
formulae is obtained by the same grammar deleting the elements ∃x.φ. Note that when dealing
with QFP formulae, we allow as well negations of formulae.

4

We say that a vector V = hd1 , . . . , dk i satisfies an EP formula φ(x1 , . . ., xk ), denoted by V |= φ,
if the formula obtained by replacing each xi by di holds. Given a formula φ with free variables
x1 , . . ., xk , we write φ(d1 , . . ., dk ) the formula where each xi is replaced by di . We let [[φ(x1 , . . ., xk )]] =
{hd1 , . . ., dk i ∈ Nk | φ(x1 , . . ., xk ) |= φ} 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 R = {R1 , . . . , Rk }. We may sometimes identify R with the
set of indices {1, . . ., k}. On a ring of size n ≥ 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 p ∈ [0, n − 1]k associating
to each robot Ri its position 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 0 meaning
that two robots are on the same node). A view V = hd1 , . . ., dk i ∈ [0, n]k is a k-tuple such that
∑ki=1 di = n and d1 6= 0. We let Vn,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 R1 , and R2 are on the same position of the ring (say
position 1), R3 is at position 4, R4 is at position 8, and R5 is at position 9 (see Figure 1b). Then,
the view of R1 and R2 is h3, 4, 1, 2, 0i. It is interpreted by the fact that there is a robot at a distance
3 (it is R3 ), a robot a at distance 3 + 4 (it is R4 ) 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 0
(this is possible by putting 0 at the ‘end’ of the view instead). As a matter of fact in the example
of Figure 1b, there is a robot at distance 3 + 4 + 1 + 2 = 10 from R1 (resp. R2 ), which is R2 (resp.
R1 ). The sum of the di corresponds always to the size of the ring and here the fact that in the view
of R1 we have as last element 0 signifies that there is a distance 0 between the last robot (here
R2 ) and R1 . When looking in the opposite direction, their view becomes: h2, 1, 4, 3, 0i. Formally,
←
−
for a view V = hd1 , . . . , dk i ∈ [0, n]k , we note V = hd j , . . . , d1 , dk , . . ., d j−1 i the corresponding view
when looking at the ring in the opposite direction, where j is the greatest index such that d j 6= 0.
Given a configuration p ∈ [0, n − 1]k and a robot Ri ∈ R , the view of robot Ri when looking in
the clockwise direction, is given by Vp [i →] = hdi (i1), di (i2 ) − di (i1 ), . . ., n − di (ik−1 )i, where, for
all j 6= i, di ( j) ∈ [1, n] is such that (p(i) + di ( j)) ⊙ n = p( j) and i1 , . . . , ik are indexes pairwise different such that 0 < di (i1 ) ≤ di (i2) ≤ · · · ≤ di (ik−1 ). When robot Ri looks in the opposite direction,
←−−−−−
its view according to the configuration p is Vp [← i] = Vp [i →].
2.1.3 Protocols
In our context, a protocol for networks of k robots is given by a QFP formula respecting some
specific constraints.

5

Definition 1 (Protocol) A protocol is a QFP formula φ(x1 , . . . , xk ) such that for all views V the
←
−
←
−
following holds: if V |= φ and V 6= V then V 6|= φ
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 p and a robot Ri ∈ R , if Vp [i →] |= φ, then the robot Ri
moves in the clockwise direction, if Vp [← i] |= φ then it moves in the opposite direction, if none
of Vp [i →] and Vp [← i] satisfies φ then the robot should not move. The conditions expressed in
Definition 1 imposes hence a direction when Vp [i →] 6= Vp [← i]. In case Vp [i →] = Vp [← i], the
robot is disoriented and it can hence move in one direction or the other. For instance, consider
the configuration p pictured on Figure 1a. Here, Vp [1 →] = h3, 1, 3i = Vp [← 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 p and p′ such that Vp [i →] = Vp′ [i →] for each robot Ri . If Vp [i →
] |= φ (resp. Vp [← i] |= φ), then necessarily Vp′ [← i] |= φ (resp. Vp′ [i →] |= φ), and the robot
in p′ moves in the opposite direction than in p (and the symmetry of the two configurations is
maintained).
We now formalize the way movement is decided. Given a protocol φ and a view V, the moves
of any robot whose clockwise direction view is V are given by:

←
−

{+1}
if V |= φ and V 6= V


←
−
←
−

{−1}
if V |= φ and V 6= V
move(φ,V ) =
←
−

{−1, +1} if V |= φ and V = V



{0}
otherwise
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 φ and we consider a set 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 ֒→φ ⊆ [0, n − 1]k × [0, n − 1]k (simply noted ֒→ when φ is clear from the context)
6

between configurations. We have p ֒→ p′ if there exists a subset I ⊆ R of robots such that, for all
i ∈ I, p′ (i) = (p(i) + m) ⊙ n, where m ∈ move(φ, Vp [i →]), and for all i ∈ R \ I, p′ (i) = p(i).
2.2.2 Synchronous mode
The transition relation ⇒φ ⊆ [0, n − 1]k × [0, n − 1]k (simply noted ⇒ when φ 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 p ⇒ p′ if p′ (i) = (p(i) + m) ⊙ n with m ∈ move(φ, Vp [i →])
for all i ∈ 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 (p, s, V) where p ∈ [0, n − 1]k gives the current configuration,
s ∈ {L, M}k gives, for each robot, its internal state (L stands for ready to look and and M stands
k stores, for each robot, the view (in the clockwise direction) it
for compute and move) and V ∈ Vn,k
had the last time it looked at the ring.
The transition relation for asynchronous mode is hence defined by a binary relation φ (or
k and defined as follows: hp, s, Vi
simply ) working on [0, n − 1]k × {L, M}k × Vn,k
hp′ , s′ , V′ i
iff there exist Ri ∈ R such that the following conditions are satisfied:
• for all R j ∈ R such that j 6= i, p′ ( j) = p( j), s′ ( j) = s( j) and V′ ( j) = V( j),
• if s(i) = L then s′ (i) = M, V′ (i) = Vp [i →] and p′ (i) = 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 s(i) = M then s′ (i) = L, V′ (i) = V(i) and p′ (i) = (p(i) + m) ⊙ n, with m ∈ move(φ, 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) φ-run (or a run according to a protocol φ) is a (finite or
infinite) sequence of configurations ρ = p0 p1 . . . where, for all 0 ≤ i < |ρ|, pi ֒→φ pi+1 (resp. pi ⇒φ
pi+1 ). Moreover, if ρ = p0 · · · pn is finite, then there is no p such that pn ֒→φ p (respectively pn ⇒φ
p). An asynchronous φ-run is a (finite or infinite) sequence of asynchronous configurations ρ =
hp0 , s0, V0 ihp1 , s1 , V1 i · · · where, for all 0 ≤ i < |ρ|, hpi , si , Vi i φ hpi+1 , si+1 , Vi+1 i and such that
s0 (i) = L for all i ∈ [1, k]. Observe that the value of V0 has no influence on the actual asynchronous
run.
We let Postss (φ, p) = {p′ | p ֒→φ p′ }, Posts (φ, p) = {p′ | p ⇒φ p′ } and Postas (φ, p) = {p′ |
there exist V, s′ , V′ s.t. hp, s0 , Vi φ hp′ , s′ , V′ i}, with s0 (i) = L for all i ∈ [1, k]. Note that in the
7

asynchronous case we impose all the robots to be ready to look. We respectively write ֒→∗φ , ⇒∗φ
and ∗φ for the reflexive and transitive closure of the relations ֒→φ , ⇒φ and φ and we define
Post∗ss (φ, p), Post∗s (φ, p) and Post∗as (φ, p) by replacing in the definition Postss (φ, p),Posts (φ, p) and
Postas (φ, p) the relations ֒→φ , ⇒φ and φ 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 φ is said to be uniquely-sequentializable if, for all configuration p, there
is at most one robot Ri ∈ R such that move(φ, Vp[i →]) 6= {0}.
When φ 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 φ is uniquely-sequentializable, then for all configuration p, Post∗s (φ, p) =
Post∗ss (φ, p) = Post∗as (φ, 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 Ring(y), a set of bad configurations
given by a QFP formula Bad(x1 , . . . , xk ) and a set of good configurations given by a QFP formula
Goal(x1 , . . ., xk ). We then define two general problems to address the verification of such algorithms: the SAFEm problem, and the REACHm problem, with m ∈ {ss, s, as}.
The SAFEm problem is to decide, given a protocol φ and two formulae Ring and Bad whether
there exists a size n ∈ N with n ∈ [[Ring]], and a (k, n)-configuration p with p ∈
/ [[Bad]], such that
/
Post∗m (φ, p) ∩ [[Bad]] 6= 0.
The REACHm problem is to decide given a protocol φ and two formulae Ring and Goal whether
there exists a size n ∈ N with n ∈ [[Ring]] and a (k, n)-configuration p, such that Post∗m (φ, p) ∩
/ Note that the two problems are not dual due to the quantifiers.
[[Goal]] = 0.
As an example, we can state in our context the SAFEm problem that consists in checking that
a protocol φ 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 Ring := y > 6 and Bad := x1 = x2 ∨ x2 = x3 ∨ x1 = x3 .

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 c1 , . . . , ck , and a finite list of labelled instructions L. Each instruction is either of the form ℓ : ci = ci + 1; goto ℓ′ , or ℓ : if ci >
8

0 then ci = ci − 1; goto ℓ′ ; else goto ℓ′′ , where i ∈ [1, k]. We also assume the existence of
a special instruction ℓh : halt. Configurations of a k-counter machine are elements of L × Nk ,
giving the current instruction and the current values of the registers. The initial configuration is
(ℓ0 , 0, . . ., 0), and the set of halting configurations is HALT = {ℓh } × Nk . Given a configuration
(ℓ, n1, . . . , nk ), the successor configuration (ℓ′ , n′1 , . . ., n′k ) is defined in the usual way and we note
(ℓ, n1, . . . , nk ) ⊢ (ℓ′ , n′1 , . . ., n′k ). A run of a k-counter machine is a (finite or infinite) sequence of
configurations (ℓ0 , n01 , . . . , n0k ), (ℓ1, n11 , . . ., n1k ) · · · , where (ℓ0 , n01 , . . ., n0k ) is the initial configuration,
i+1
and, for all i ≥ 0, (ℓi , ni1 , . . . , nik ) ⊢ (ℓi+1 , ni+1
1 , . . . , nk ). The run is finite if and only if it ends in a
halting configuration, i.e. in a configuration in HALT.
Theorem 2 SAFEas is undecidable.
Sketch of proof. The proof relies on a reduction from the halting problem of a deterministic twocounter machine M to SAFEas 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 F or R, representing respectively a free node and a node
occupied by a robot. When a letter A ∈ {F, R} is repeated i times, we use the notation Ai , when
it is repeated an arbitrary number or times (including 0), we use A∗ . To distinguish between the
two representations of the configurations, we use respectively the terms configurations or wordconfigurations. The correspondence between a configuration and a word-configuration is obvious.
A machine-like (word-)configuration is a configuration of the form:
B3 F∗ RF∗ B4 F∗ RF∗ B5 F∗ RF∗ B6 F∗ RF∗ B7 F∗ RF∗ B8 P1 P2 P3 P4 P5 RFR
where Bi is a shorthand for FRi F, and P1 P2 ∈ {RF, FR} and exactly one Pi = R for i ∈ {3, 4, 5},
Pj = F for j ∈ {3, 4, 5} \ {i} (see Table 1 for a graphic representation of the section P1 P2 P3 P4 P5
of the ring). Observe that the different blocks Bi 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 R be the set of robots involved. A machine-like (word-)configuration
′
B3 Fn1 Rc1 F∗ B4 Fn2 Rc2 F∗ B5 Fm Rc Fn B6 Fi Rℓ Fi B7 F p Rℓ′ Fr B8 Rtt FRt FFRg FRd is said to be stable because of the positions of robots Rt and Rtt (see Table 1). Moreover, it encodes the configuration
9

(ℓi , n1 , n2 ) of M (due to the relative positions of robots Rc1 , Rc2 and Rℓ respectively to B3 , B4
and B6 ). We say that a configuration p is machine-like, stable, etc. if its corresponding wordconfiguration is machine-like, 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 φ-(word)-configurations. For a stable and machine-like φ-configuration p, we let M(p) be the
M-configuration encoded by p. We first present the part of the algorithm simulating the behavior
of M. We call this algorithm φ′ . Since the machine is deterministic, only one instruction is labelled
by ℓi , known by every robot. The simulation follows different steps, according to the positions of
the robots Rt and Rtt , as pictured in Table 1.
Table 1: Different types of configurations
stable configuration

Rtt FRt FF

moving1 configuration

FRtt Rt FF

moving2 configuration

FRtt FRt F

moving3 configuration

FRtt FFRt

stabilizing1 configuration

Rtt FFFRt

stabilizing2 configuration

Rtt FFRt F

We explain the algorithm φ′ on the configuration (ℓi , n1 , n2 ) with the transition ℓi : if c1 >
0 then c1 = c1 − 1; goto ℓ j ; else goto ℓ j′ .
• When in a stable configuration, robot Rtt first moves to obtain a moving1 configuration.
• In a moving1 configuration, robot Rc moves until it memorizes the current value of c1 . More
precisely, in a moving1 configuration where n1 6= m, robot Rc moves : if n1 > m, and n 6= 0,
Rc moves towards B6 , if n1 < m, it moves towards B5 , if n1 > m and n = 0, it does not move.
• In a moving1 configuration where n1 = m, Rt moves to obtain a moving2 configuration.
• In a moving2 configuration, if n1 = m 6= 0, then Rc1 moves towards B3 , hence encoding the
decrementation of c1 .
• In a moving2 configuration, if n1 = m = 0 or if n1 6= m, (then the modification of c1 is either
impossible, or already done), robot Rℓ′ moves until it memorizes the position of robot Rℓ : if
p < i, and r 6= 0, Rℓ′ moves towards B8 ; if p > i, Rℓ′ moves towards B7 .
• In a moving2 configuration, if p = i, then Rt moves to obtain a moving3 configuration.
• In a moving3 configuration, if n1 = m = 0, and robot Rℓ′ encodes ℓi (i.e. p = i), then c1 = 0
and robot Rℓ has to move until it encodes ℓ j′ . If on the other hand n1 < m, then robot Rℓ
moves until it encodes ℓ j . More precisely, if n1 = m = 0, and the position encoded by Rℓ
is smaller than j′ (i < j′ ), and if i′ 6= 0, then Rℓ moves towards B7 . If n1 = m = 0, and the
position encoded by Rℓ is greater than j′ , Rℓ moves towards B6 . If n1 6= m, then robot Rℓ
10

moves in order to reach a position where it encodes ℓ j (towards B6 if i > j, towards B7 if
i < j and i′ 6= 0).
• In a moving3 configuration, if the position encoded by Rℓ′ is ℓi , if n1 = m = 0 and the position
encoded by Rℓ is ℓ j′ , or if n1 6= m, and the position encoded by Rℓ is ℓ 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 stable configuration: robot Rtt moves to obtain a stabilizing1
configuration.
• In a stabilizing1 configuration, robot Rt moves to obtain a stabilizing2 configuration.
• In a stabilizing2 configuration, robot Rt moves to obtain a stable configuration.
For other types of transitions, the robots move similarly. When in a stable configuration encoding a configuration in HALT, no robot moves. We describe now the algorithm φ that simply adds to
φ′ the two following rules. Robot Rg (respectively Rd ) moves in the direction of Rd (respectively in
the direction of Rg ) if and only if the robots are in a stable machine-like configuration, and the encoded configuration of the machine is (ℓ0, 0, 0) (respectively is in HALT), (since the configuration
is machine-like, the distance between Rg and Rd is 2).
On all configurations that are not machine-like, the algorithm makes sure that no robot move.
This implies that once Rg or Rd 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 φ.
W
Let the formulae Bad(p1 , . . . , p42 ) = i, j ∈ [1,42] (pi = p j ) that is satisfied by all the configurai 6= j

tions where two robots share the same position and Ring(y) = y ≥ 0. We can show that M halts
if and only if there exits a size n ∈ [[Ring]], a (42, n)-configuration p with p ∈
/ [[Bad]], such that
∗
/
Postas (φ, p) ∩ [[Bad]] 6= 0.

Theorem 3 REACHm is undecidable, for m ∈ {ss, s, 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 ℓ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 ∈ 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 ℓ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.

11

4 Decidability results and case study
In this section, we show that even if SAFEas , REACHas , REACHss and REACHs are undecidable,
the other cases SAFEs and SAFEss 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 SAFEs and SAFEss it is enough to look
at the one-step successor. Let φ 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 ∈ N such that n ∈ [[Ring]] and m ∈ {s, ss}. There exists a (k, n)-configuration p
with p ∈
/ [[Bad]], such that Post∗m (φ, p) ∩ [[Bad]] 6= 0/ iff there exists a (k, n)-configuration p′ with
/
p′ ∈
/ [[Bad]], such that Postm (φ, p′ ) ∩ [[Bad]] 6= 0.
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 Ri in a configuration p, with the following
formula:
ConfigViewi (y, p1 , . . ., pk , d1 , . . . , dk ) :=
V
′
′
′
∃d1′ , . . ., dk−1
· k−2
j=1 d j ≤ d j+1 ∧
Vk
Wk−1
′
j6=i ( ℓ=1 p j = (pi + dℓ ) mod y)∧
Vkj=1,W
k
′
ℓ=1 ( j=1, j6=i p j = (pi + dℓ ) mod y))∧
V
′
0 < d1′ ∧ k−1
j=1 d j ≤ y∧
V
′
′
′
d1 = d1′ ∧ k−1
j=2 d j = d j − d j−1 ∧ dk = y − dk−1 ,
Note that this formula only expresses in the syntax of Presburger arithmetic the definition of Vp [i →
] where the variable y is used to store the length of the ring, p1 , . . . , pk represent p and the variables
d1 , . . . , dk represent the view.
We also use the formula ViewSym(d1 , . . . , dk , d1′ , . . ., dk′ ) that is useful to compute the symmetric
of a view.
ViewSym(d1 , . . ., dk , d1′ , . . . , dk′ ) :=
Vk
Wk
Vj
′
′
j=1 ( ℓ= j+1 (dℓ = 0 ∧ dℓ = 0) ∧ ℓ=1 dℓ = d j−ℓ+1 )
φ

We are now ready to introduce the formula Movei (y, p1 , . . ., pk , p′ ), which is true if and only if,
on a ring of size n (represented by the variable y), the move of robot Ri according to the protocol φ
12

from the configuration p yields to the new position p′ . Here the variables p1 , . . ., pk characterizes
p. .
φ

Movei (y, p1 , . . ., pk , p′ ) :=
∃d1 , . . . , dk , d1′ , · · · , dk′ ·
ConfigViewi (y, p1 , . . . , pk , d1 , . . . , dk )∧
′
′
h ViewSym(d1 , . . ., dk , d1 , . . . , d k)∧

φ(d1 , . . ., dk ) ∧ (pi < y − 1 ∧ p′ = pi + 1)

′
∨(pi = y − 1 ∧ p = 0) ∨

φ(d1′ , . . ., dk′ ) ∧ (pi > 0 ∧ p′ = pi − 1)

∨(pi = 0 ∧ p′ = y − 1)

i
∨ ¬φ(d1 , . . ., dk ) ∧ ¬φ(d1′ , . . . , dk′ ) ∧ (p′ = pi )
Now, given two (k, n)-configurations p and p′ , and a k-protocol φ, it is easy to express the fact
that p′ is a successor configuration of p according to φ in a semi-synchronous run (resp. synchronous run); for this we define the two formulae SemiSyncPostφ (y, p1 , . . . , pk , p′1 , . . ., p′k ) and
SyncPostφ (y, p1 . . . , pk , p′1 , . . . , p′k )) as follows:
SemiSyncPostφ (y, p1 , . . ., pk , p′1 , . . . , p′k ) :=
Wk
φ
′
i=1 Movei (y, p1 , . . . , pk , pi )∧

Vk
φ
′
′
j=1, j6=i ((p j = p j ) ∨ Move j (y, p1 , . . . , pk , p j ))
aa
SyncPostφ (y, p1 , . . . , pk , p′1 , . . ., p′k ) :=
Vk
φ
′
i=1 Movei (y, p1 , . . . , pk , pi )
Lemma 2 For all n ∈ N and all (k, n)-configurations p and p′ , we have:
1. p ֒→ p′ if and only if n, p, p′ |= SemiSyncPostφ ,
2. p ⇒ p′ if and only if n, p, p′ |= SyncPostφ .

4.3 Results
Now since to solve SAFEss and SAFEs , we only need to look at the successor in one step, as
stated by Lemma 1, and thanks to the formulae SemiSyncPostφ and SyncPostφ and their properties expressed by Lemma 2, we deduce that these two problems can be expressed in Presburger
arithmetic.
Theorem 4 SAFEs and SAFEss are decidable and in NP.
Proof: We consider a ring property Ring(y), a protocol φ for k robots (which is a QFP formula) and a set of bad configurations given by a QFP formula Bad(x1 , . . . , xk ). We know that
13

there exists a size n ∈ N with n ∈ [[Ring]], and a (k, n)-configuration p with p ∈
/ [[Bad]], such that
Post∗s (φ, p) ∩ [[Bad]] 6= 0/ if and only if there exists a (k, n)-configuration p′ with p′ ∈
/ [[Bad]], such
′
/ By Lemma 2, this latter property is true if and only if the following
that Postm (φ, p ) ∩ [[Bad]] 6= 0.
formula is satisfiable:
SyncPostφ (y, p1 , . . ., pk , p′1 , . . . , p′k )∧
Ring(y) ∧ ¬Bad(p1 , . . . , pk )∧
Bad(p′1 , . . . , p′k )
For the semi-synchronous case, we replace the formula SyncPostφ by SemiSyncPostφ . The NP
upper bound is obtained by the fact that the built formula is an EP formula.

When the protocol φ 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 φ is uniquely-sequentializable, SAFEas 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 SAFEs and SAFEss , but they also allow us to express other
interesting properties. For instance, we can compute the successor configuration in asynchronous
mode for a protocol φ working over k robots thanks to the formula AsyncPostφ (y, p1 , . . . , pk , s1 , . . . , sk ,
v1 . . . , vk , p′1 , . . ., p′k , s′1 , . . . , s′k , v′1 , . . . , v′k ), which is given by:
AsyncPostφ := ∃d1 , . . ., dk ·

Wk  V

′
′
′
j6=i (p j = p j ∧ s j = s j ∧ v j = v j )∧
i=1
s′i = 1 − si ∧ (si = 0 ∧ v′i = hd1 , . . ., dk i∧
ConfigViewi (n, p1 , . . . , pk , d1 , . . ., dk ) ∧ p′i = pi )∨

φ
(si = 1 ∧ v′i = vi ∧ Movei (n, p1 , . . . , pk , p′i )

To prove the correctness of this formula for an asynchronous configuration (p, s, V) with k
robots we make the analogy between the flags L and M and the naturals 0 and 1, which means that
in the definition of the vector s ∈ {L, M}k , we encode L by 0 and M by 1 and we then apply the
definition of →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 φ over k robots fits into the hypothesis of
Corollary 1, i.e. whether it is uniquely-sequentializable. We define the formula UniqSeqφ that is
satisfiable if and only if φ is uniquely-sequentializable.
UniqSeqφ := ¬∃y.p1 , . . ., pk , p′1 , . . . , p′k ·
φ
φ
′
′
i6= j,1≤i, j≤k (Movei (n, p1 , . . ., pk , pi ) ∧ Move j (n, p1 , . . ., pk , p j )
∧p′i 6= pi ∧ p′j 6= p j .

W

14

Hence we deduce the following statement.
Theorem 5 Checking whether a protocol φ 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
15

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

References
[1] K. R. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems.
Inf. Process. Lett., 22(6):307–309, 1986.
[2] C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain. Certified Impossibility Results
for Byzantine-Tolerant Mobile Robots. In Proc. of SSS’13, volume 8255 of LNCS, pages
178–186. Springer, 2013.
[3] T. Balabonski, A. Delga, L. Rieg, S. Tixeuil, and X. Urbain. Synchronous gathering without
multiplicity detection: A certified algorithm. In Proc. of SSS’16, volume 10083 of LNCS,
pages 7–19. Springer, 2016.
[4] B. Bérard, P. Courtieu, L. Millet, M. Potop-Butucaru, L. Rieg, N. Sznajder, S. Tixeuil, and
X. Urbain. Formal Methods for Mobile Robots: Current Results and Open Problems. Int. J.
Inform. Soc., 7(3):101–114, 2015. Invited Paper.
[5] B. Bérard, P. Lafourcade, L. Millet, M. Potop-Butucaru, Y. Thierry-Mieg, and S. Tixeuil.
Formal verification of mobile robot protocols. Distr. Comp., 2016.
[6] L. Blin, A. Milani, M. Potop-Butucaru, and S. Tixeuil. Exclusive perpetual ring exploration
without chirality. In Proc. of DISC’10, volume 6343 of LNCS, pages 312–327. Springer,
2010.
[7] F. Bonnet, X. Défago, F. Petit, M. Potop-Butucaru, and S. Tixeuil. Discovering and assessing
fine-grained metrics in robot networks protocols. In Proc. of SRDS’14, pages 50–59. IEEE
Press., 2014.

16

[8] I. Borosh and L. Treybig. Bounds on positive integral solutions of linear Diophantine equations. Amer. Math. Soc., 55:299–304, 1976.
[9] P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Impossibility of Gathering, a Certification.
Inf. Process. Lett., 115:447–452, 2015.
[10] P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Certified universal gathering in \mathbb R
ˆ2 for oblivious mobile robots. In Proc. of DISC’16, volume 9888 of LNCS, pages 187–200.
Springer, 2016.
[11] G. D’Angelo, G. D. Stefano, A. Navarra, N. Nisse, and K. Suchan. A unified approach for
different tasks on rings in robot-based computing systems. In Proc. of IPDPSW’13, pages
667–676. IEEE Press., 2013.
[12] L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS’08, volume 4963 of
LNCS, pages 337–340. Springer, 2008.
[13] S. Devismes, A. Lamani, F. Petit, P. Raymond, and S. Tixeuil. Optimal Grid Exploration by
Asynchronous Oblivious Robots. In Proc. of SSS’12, volume 7596 of LNCS, pages 64–76.
Springer, 2012.
[14] H. T. T. Doan, F. Bonnet, and K. Ogata. Model checking of a mobile robots perpetual exploration algorithm. In Proc. of SOFL+MSVL, Revised Selected Papers, volume 10189 of LNCS,
pages 201–219, 2016.
[15] https://www.irif.fr/˜sangnier/robots.html.
[16] P. Flocchini, D. Ilcinkas, A. Pelc, and N. Santoro. Computing without communicating: Ring
exploration by asynchronous oblivious robots. Algorithmica, 65(3):562–583, 2013.
[17] P. Flocchini, G. Prencipe, and N. Santoro. Distributed Computing by Oblivious Mobile
Robots. Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, 2012.
[18] E. Kranakis, D. Krizanc, and E. Markou. The Mobile Agent Rendezvous Problem in the Ring.
Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, 2010.
[19] R. Mayr. Undecidable problems in unreliable computations. Theoret. Comput. Sci., 297(13):337–354, 2003.
[20] L. Millet, M. Potop-Butucaru, N. Sznajder, and S. Tixeuil. On the synthesis of mobile robots
algorithms: The case of ring gathering. In Proc. of SSS’14, volume 8756 of LNCS, pages
237–251. Springer, 2014.
[21] M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Upper Saddle
River, NJ, USA, 1967.

17

[22] S. Rubin, F. Zuleger, A. Murano, and B. Aminof. Verification of asynchronous mobile-robots
in partially-known environments. In Proc. of PRIMA’15, volume 9387 of LNCS, pages 185–
200. Springer, 2015.
[23] I. Suzuki and M. Yamashita. Distributed anonymous mobile robots: Formation of geometric
patterns. SIAM J. Comput., 28(4):1347–1363, 1999.

18

A Proof of Theorem 1
Let φ be a protocol and p a configuration. From the definitions, it is obvious that Post∗s (φ, p) ⊆
Post∗ss (φ, p) ⊆ Post∗as (φ, p).
We show that, in case φ is uniquely-sequentializable, we also have Post∗as (φ, p) ⊆ Post∗s (φ, p).
We first prove the following property (P) of uniquely-sequentializable runs: for all uniquelysequentializable protocol φ, for all configuration po , for all runs ρ = hp0 , s0 , V0 ihp1 , s1, V1 i · · · ∈
Runsas (φ), for all 0 ≤ k < |ρ|, for all robot i, if Vk (i) 6= Vpk [i →] and sk (i) = M then move(φ, Vk (i)) =
{0}. To prove (P), let ρ ∈ Runsas (φ). We show (P) by induction on k. For k = 0, it is obvious since s0 (i) = L for all robot i. Let ρ = hp0 , s0 , V0 i · · · hpk , sk , Vk ihpk+1 , sk+1 , Vk+1 i a prefix
of a run in Runsas (φ). Let i be a robot such that sk+1 (i) = M and Vk+1 (i) 6= Vpk+1 [i →]. If
sk (i) = L, then Vk+1 (i) = Vpk [i →] and pk = pk+1 , which is impossible. Hence, sk (i) = M and
Vk (i) = Vk+1 (i). Moreover, either Vk (i) 6= Vpk [i →] and by induction hypothesis, move(φ, Vk (i)) =
move(φ, Vk+1 (i)) = {0}. Either Vk (i) = Vpk [i →] 6= Vpk+1 [i →]. Hence there exists another robot
j 6= i such that sk ( j) = M and sk+1 ( j) = L and move(φ, Vk ( j)) 6= {0}. Since φ is uniquelysequentializable, move(φ, Vk (i)) = move(φ, Vk+1 (i)) = {0}.
We show now by induction on n that if hp, s0 , Vi n hp′ , s′ , V′ i then p′ ∈ Post∗s (φ). For n = 0,
it is obvious. Let now n ∈ N and let p′ , s′ , V′ , p′′ , s′′, and V′′ such that hp, s0 , Vi n hp′ , s′ , V′ i
hp′′ , s′′ , V′′ i. By induction hypothesis, p′ ∈ Post∗s (p). Let i be such that s′′ (i) 6= s′ (i). If s′ (i) =
L then by definition, p′′ = p′ and p′′ ∈ Post∗s (p). Otherwise, if Vp′ [i →] 6= V′ (i), then by (P),
move(φ, V′ (i)) = {0} and then p′ = p′′ . If Vp′ [i →] = V′ (i), either move(φ, V′ (i)) = {0} and p′′ = p′
or, move(φ, V′(i)) 6= {0} and, since φ is uniquely-sequentializable, for all j 6= i, move(φ, Vp′ [ j →
]) = {0} and p′ ⇒ p′′ . Hence p′′ ∈ Post∗s (p).

B Proof of Theorem 2
We show that M halts if and only if there exits a size n ∈ N, a (42, n)-configuration p with p ∈
/ [[Bad]],
∗
/
such that Postas (φ, p) ∩ [[Bad]] 6= 0.
For that matter, we use several claims about φ′ . First observe that φ′ is uniquely-sequentializable.
Claim 1 Let p be a machine-like φ-configuration. Then for all configuration p′ ∈ Post∗as (φ′ , p) =
Post∗s (φ′ , p), p′ is machine-like.
Claim 2 Let hp, s, Vi be a stable and machine-like asynchronous φ-configuration corresponding
′
′
′
to the following word-configuration: B3 Fn1 Rc1 Fn1 B4 Fn2 Rc2 Fn2 B5 Fm Rc Fn B6 Fi Rℓ Fi B7 F p Rℓ′ Fr B8
Rtt FRt FFRg FRd . Let M(p) = (ℓi , n1 , n2 ) a non-halting M-configuration. Assume that p has the following properties. (i) if n1 > m then n ≥ n1 − m (if ℓi modifies c1 ) or if n2 > m then n ≥ n2 − m (if ℓi
modifies c2 ), (ii) if ℓi increments c1 (resp. c2 ) then n′1 > 0 (resp. n′2 > 0), and (iii) i+i′ = p+r = |L|.
Then hp, s, Vi ∗φ′ hp′ , s′ , V′ i with p′ stable and machine-like, such that M(p) ⊢ M(p′ ).
Claim 3 Let hp, s, Vi and hp′ , s′ , V′ i be two asynchronous configurations, with p and p′ stable. If
j
there exists k > 0 such that hp, s, Vi kφ′ hp′ , s′ , V′ i and for all 0 < j < k, if hp, s, Vi φ′ hp′′ , s′′ , V′′i
we have p′′ not stable, then M(p) ⊢ M(p′ ).
19

Assume that M halts. There is then a finite bound K ∈ N on the values of the counter during
the run. We show hereafter an asynchronous φ-run leading to a collision. Let hp0 , s0, V0 i be the
initial configuration of the run, with p0 a φ-configuration corresponding to the word-configuration
B3 Rc1 FK B4 Rc2 FK B5 Rc FK B6 Rℓ F|L| B7 Rℓ′ F|L| B8 Rtt FRt FRg FRd ,
hence such that M(p0 ) = (ℓ0 , 0, 0), and s0 (i) = L for all i ∈ R . Then hp0 , s0 , V0 i
hp1 , s1 , V1 i
where p1 = p0 , s1 (g) = M, V1 (g) = Vp0 [g →], and s1 (i) = s0 (i) and V1 (i) = V0 (i) for all i ∈
R \ {g}. It is easy to check that, at each step of a run starting from hp0 , s0 , V0 i, the conditions (i),
(ii) and (iii) of Claim 2 are satisfied. Then, since M halts, by applying iteratively Claim 2, we have
hp1 , s1, V1 i ∗φ′ hpn , sn , Vn i with M(pn ) a halting configuration. Now, the φ-run continues with
robot d being scheduled to look, and then robots g and d moving, leading to a collision. Formally :
hpn , sn, Vn i hp, s, Vi hp′ , s′ , V′ i hp′′ , s′′, V′′ i, with pn = p, s(d) = M, and V(d) = Vpn [d →],
p′ (d) = p(d) − 1 since V(d) memorizes the encoding of a halting configuration, with distance
between Rg and Rd equal to 2. Last, p′′ (g) = p(g) + 1 since V(g) memorizes the encoding of
the initial configuration, with distance between Rg and Rd equal to 1. Hence, p′′ (g) = p′′ (d) and
p′′ ∈ Post∗as (φ, p0 ) ∩ [[Bad]].
Conversely assume there is an asynchronous φ-run ρ leading to a collision. By Claim 1, if
ρ is in fact a φ′ asynchronous run, there is no collision (either ρ 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 ρ contains
moves from Rg and/or Rd . Assume Rd moves in this run. Hence, there is a configuration hp, s, Vi
in this run where Rd has just been scheduled to move and is hence such that s(Rd ) = M, V(Rd ) =
Vp [Rd →], with move(φ, V(Rd )) 6= 0. Hence, by definition of φ, p is machine-like, stable and M(p)
is a halting M-configuration. Let j 6= Rg a robot such that s( j) = M. If move(φ,V ( j)) 6= {0}, by
Proposition (P) from the proof of Theorem 1 and since move(φ,V ( j)) = move(φ′ ,V ( j)), V ( j) =
Vp [ j →], and it is impossible since M(p) is a halting configuration. Hence, from hp, s, Vi the only
robots that can move are Rd and Rg . If Rg does not move, then all the following configurations in
the run is p′ with p′ (i) = p(i) for all i 6= Rd and p′ (Rd ) = p(Rd ) + 1. Hence, ρ does not lead to a
collision.
Assume now that Rg moves in ρ. Let ρ′ · hp1 , s1 , V1 ihp2 , s2 , V2 i be a prefix of ρ such that
p2 (Rg ) = p1 (Rg ) − 1 and p2 (i) = p1 (i) for all i 6= Rg , and ρ′ · hp1 , s1 , V1 i is a prefix of a φ′ -run.
Then p1 is a machine-like configuration and again by Proposition (P) of the proof of Theorem 1,
there is at most one robot i ∈
/ {Rg , Rd } such that move(φ′ , V1 (i)) = move(φ′ , V2 (i)) 6= {0}. Hence if
Rd does not move in ρ then ρ = ρ′ · hp1 , s1 , V1 ihp2 , s2 , V2 ihp3 , s3, V3 i · ρ′′ with p3 (i) = p2 (i) for all
the robots i but possibly one, and then p3 being the only configuration appearing in ρ′′ . According
to φ′ , p3 is collision free, so such a run could not yield a collision.
Hence, we know that in ρ both Rg and Rd moves. Moreover, from the above reasonings we
deduce that in ρ, at some point Rg has been scheduled to look, then later on, Rd has been scheduled
to look, and just after, Rg and Rd have moved provoking a collision. Formally, ρ is in the following
form: ρ = ρ′ · hp0 , s0 , V0 ihp1 , s1 , V1 i · ρ′′ · hp2 , s2 , V2 ihp3 , s3 , V3 ihp4 , s4 , V4 ihp5 , s5 , V5 i with ρ′ , ρ′′
asynchronous φ′ -runs, s0 (Rg ) = L, s1 (Rg ) = M, and for all other robots i, s0 (i) = s1 (i), and p0 = p1 ,
and move(φ, V1(Rg )) 6= {0}, p2 = p3 , s2 (Rd ) = L, s3 (Rd ) = M, move(φ, V3 (Rd )) 6= {0}, and either
20

p4 (Rd ) = p3 (Rd ) + 1, and for all i 6= Rd , p3 (i) = p4 (i) and p5 (Rg ) = p4 (Rg ) − 1 and for all i 6= Rg ,
p4 (i) = p5 (i), or p4 (Rg ) = p3 (Rg ) − 1, and for all i 6= Rg , p3 (i) = p4 (i) and p5 (Rd ) = p4 (Rd ) − 1
and for all i 6= Rd , p4 (i) = p5 (i). In both cases, we deduce that since move(φ, V1 (Rg )) 6= {0}, then
p0 is a machine-like stable configuration such that M(p0 ) = C0 , and since move(φ, V3(Rd )) 6= {0},
then p2 is a machine-like stable configuration encoding a halting M-configuration Ch . Hence, from
Claim 3, since p0 ∗ p2 then C0 ⊢ · · · ⊢ Ch and M halts.

C Proof of Theorem 3
The proof relies on a reduction from the repeated reachability problem of a deterministic threecounter zero-initializing bounded-strongly-cyclic machine M, which is undecidable [19]. A counter
machine is zero-initializing if from the initial instruction ℓ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 ∈ 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 ℓ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 p be a machine-like configuration. Then, for all configuration p′ ∈ Post∗s (φ, p), p′ ∈
[[Machine like ∨ Collision]].
Claim 5 Let p be a stable and machine-like synchronous φ-configuration corresponding to the
′
′
′
′
following word-configuration: B3 Fn1 Rc1 Fn1 B4 Fn2 Rc2 Fn2 B5 Fn3 Rc3 Fn3 B6 Fm Rc Fn B7 Fi Rℓ Fi B8
F p Rℓ′ Fr B9 Rtt FRt FF. Let M(p) = (ℓi , n1 , n2 , n3 ) be a non-halting M-configuration. Assume that p
has the following properties. (i) if n1 > m (respectively n − 2 > m, n − 3 > m), then n ≥ n1 − m
(respectively n ≥ n2 − m, n ≥ n3 − m)(if ℓi modifies c1 - respectively c2 or c3 ), (ii) if ℓi increments
c1 (resp. c2 or c3 ) then n′1 > 0 (resp. n′2 > 0, or n′3 > 0), and (iii) i + i′ = p + r = |L|. Then p φ∗ p′
with p′ stable and machine-like, such that M(p) ⊢ M(p′ ).
Claim 6 Let p, p′ be two stable, machine-like configurations. If there exists some k > 0 such that
j
p ⇒φk p′ and that for all 0 < j < k, if p ⇒φ p′′ then p′′ is not stable, then M(p) ⊢ M(p′ ).
Claim 7 Let p be a machine-like configuration, which is not stable. Then, either |Post∗s (φ, p)| is
finite, or there exists p′ ∈ Post∗s (φ, p) with p′ stable.
If there is an infinite space-bounded run of M, we let K ∈ N be the maximal values of all the
counters during this run. Let p0 be the φ-configuration having the following word-representation:
21

′

B3 Rc1 FK B4 Rc2 FK B5 Rc3 FK B6 Rc FK B7 Rℓ Fi B8 F p Rℓ′ Fr B9
Rtt FRt FRg FRd . Hence M(p0 ) is the initial configuration of M. It is easy to show that, for all
p ∈ Post∗s (φ, p0 ), p satisfies conditions (i), (ii), and (iii) of Claim 5. Hence, by applying iteratively
Claim 5, we can build an infinite φ-run ρ = p0 p1 · · · such that pi ∈
/ [[Collision ∨ Halting]] for
all i ≥ 0. Hence, by Claim 4, pi ∈ [[Machine like]] for all i ≥ 0, and pi ∈
/ [[Goal]] for all i ≥ 0.
Moreover, for all machine-like configuration p, for all i ∈ R , Vp [i →] 6= Vp [← i], then it can have
/
at most one successor, and ρ is the only φ-run starting from p0 . Hence, Post∗s (φ, p0 ) ∩ [[Goal]] = 0.
∗
Conversely, assume that there is n ∈ N and a (k, n)-φ-configuration p0 such that Posts (φ, p0 ) ∩
/ Hence, for all p ∈ Post∗s (φ, p0 ), p ∈ [[Machine like]]. Then, according to the defini[[Goal]] = 0.
tion of the protocol, there is a unique synchronous φ-run starting from p0 . Assume for the sake of
contradiction that this run is finite. Let ρ = p0 · · · pm be such a run. Then pm ∈
/ [[Goal]] hence M(pm )
/ from the
is not a halting configuration and pm is collision-free. If it is not stable, Posts (φ, pm ) 6= 0,
definition of the protocol. If pm is stable, either M(pm ) = (ℓh , n1 , n2 , n3) for some n1 , n2 , n3 ∈ N, but
then pm ∈ [[Halting]] ⊆ [[Goal]], which is not possible, or there exists a configuration pm+1 such
that pm ⇒ pm+1 and ρ can be continued. Hence let ρ = p0 p1 · · · be the infinite synchronous φ-run
starting from p0 . Assume that p0 is not stable. Then, by Claim 7, there exists i ≥ 0, such that pi is
stable. By definition of φ, pi+1 is not stable, but by Claim 7 and Claim 6, there exists j > i + 1 such
that p j is stable and M(pi ) ⊢ M(p j ). By iterating this reasoning, we can in fact build an infinite run
of M starting in M(pi ). Let K be the maximal number of positions between respectively B3 and
B4 , B4 and B5 , B5 and B6 and B6 and B7 in p0 . It is easy to see that this distance is an invariant
of any φ-run. Hence, for any k ≥ 0 such that pk is stable, M(pk ) = (ℓ, n1, n2 , n3 ) with ni ≤ K for
i ∈ {1, 2, 3}, and the infinite run of M is indeed space-bounded. Let C0 ⊢ C1 · · · be such a run.
Since M is bounded-strongly-cyclic, there exists i ≥ 0 such that Ci = (ℓ0, n1 , n2 , n3 ) with ni ∈ N
for i = {1, 2, 3}, and since M is zero-initializing, then there exists j ≥ i such that C j = (ℓ0, 0, 0, 0).
Hence, M has an infinite space-bounded run from (ℓ0, 0, 0, 0).

D Correction of the Presburger formulae
Lemma 3 For all i ∈ [1, k], we have n, p, V |= ConfigViewi if and only if hd1 , . . . , dk i = Vp [i →]
on a ring of size n .
′
Proof: Assume n, p, V |= ConfigViewi . Then, there exist k − 1 variables, d1′ , . . . , dk−1
∈ [1, n] such
′ . Moreover, there exists a bijection f : [1, k − 1] → [1, k − 1] such that,
that 0 < d1′ ≤ d2′ ≤ · · · ≤ dk−1
for all j 6= i, p j = (pi + d ′f ( j) ) mod n. Finally, d1 = d1′ and for all j ∈ [2, n − 1], d j = d ′j − d ′j−1
′ . Hence, if we consider the configuration p defined by p( j) = p for all j ∈ [1, n],
and dk = n − dk−1
j
then hd1 , . . . , dk i = Vp [i →]. Conversely, let p be a (k, n)-configuration and Vp [i →] = hd1 , . . . , dk i.
Then, n, p, V |= ConfigViewi . Indeed, by definition of the view, we let di ( j) ∈ [1, n] be such that
(p(i) + di ( j)) ⊙ n = p( j) for all j 6= i and we let i1 , . . ., ik be a permutation of positions such that
0 < di (i1) ≤ di (i2 ) ≤ · · · ≤ di (ik−1 ). Then, for all j ∈ [2, k − 1], d j = di (i j ) − di (i j−1 ), d1 = di (i1 )
and dk = n − di (ik−1 ). By interpreting the variables d1′ , . . . , dk′ by respectively di (i1), . . . , di (ik ), it is
easy to see that the formula is satisfied.


22

Lemma 4 For all n ∈ N, for all views V, V′ ∈ [0, n]k , we have V, V′ |= ViewSym if and only if
←
−
V′ = V .
←−−−−−−−
Proof: Given n ∈ N, d1 , . . ., dk , d1′ , . . . , dk′ ∈ [0, n] such that d1 6= 0 we have hd1′ , . . ., dk′ i = hd1 , . . ., dk i
if and only if there exists 1 ≤ j ≤ k such that dℓ = 0 for all j + 1 ≤ ℓ ≤ k and d1′ = d j , . . . , d ′j = d1
and d ′ ℓ = 0 for all j + 1 ≤ ℓ ≤ k (by definition), if and only if d1 , . . . , dk , d1′ , . . ., dk′ |= ViewSym.

φ

Lemma 5 For all n ∈ N and a (k, n)-configurations p and p′ ∈ [0, n − 1], we have n, p, p′ |= Movei
if and only if p′ = (p(i) + m) ⊙ n with m ∈ move(φ, Vp [i →]).
φ

Proof: We have n, p, p′ |= Movei if and only if there exist d1 , . . . , dk , d1′ , . . ., dk′ ∈ [0, n] such that
←−−−−−−−
hd1 , . . . , dk i = Vp [i →] (by Lemma 3) and hd1′ , . . ., dk′ i = hd1 , . . . , dk i = Vp [← i] (by Lemma 4) and
either (i) Vp [i →] |= φ and p′ = (pi + 1) ⊙ n, or (ii) Vp [← i] |= φ and p′ = (pi − 1) ⊙ n, or (iii)
Vp [i →] 6|= φ, Vp [← i] 6|= φ and p′ = pi , if and only if either (i) 1 ∈ move(φ, Vp [i →]) and p′ =
(pi + 1) ⊙ n or (ii) −1 ∈ move(φ, Vp [i →]) and p′ = (pi − 1) ⊙ n or (iii) move(φ, Vp [i →]) = {0}
and p′ = pi if and only if p′ = (pi + m) ⊙ n with m ∈ move(φ, Vp [i →]).


23

