Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space

TL;DR

This paper demonstrates how model checking can be effectively used to verify the correctness of rendezvous algorithms for robots with lights in continuous environments, ensuring reliability across various synchrony models.

Contribution

It introduces a generic verification model for the SPIN model-checker that handles continuous robot environments and verifies multiple rendezvous algorithms across different synchrony models.

Findings

Model-checking confirms known rendezvous algorithm correctness.

Counter-examples are generated for known failures.

Fundamental theorems about robot memory and algorithm properties.

Abstract

The paper details the first successful attempt at using model-checking techniques to verify the correctness of distributed algorithms for robots evolving in a \emph{continuous} environment. The study focuses on the problem of rendezvous of two robots with lights. There exist many different rendezvous algorithms that aim at finding the minimal number of colors needed to solve rendezvous in various synchrony models (e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically very simple, their analysis and proof of correctness tend to be extremely complex, tedious, and error-prone as impossibility results are based on subtle interactions between robots activation schedules. The paper presents a generic verification model written for the SPIN model-checker. In particular, we explain the subtle design decisions that allow to keep the search space finite and tractable, as well as prove several important theorems that support them. As a sanity check, we use the model to verify several known rendezvous algorithms in six different models of synchrony. In each case, we find that the results obtained from the model-checker are consistent with the results known in the literature. The model-checker outputs a counter-example execution in every case that is known to fail. In the course of developing and proving the validity of the model, we identified several fundamental theorems, including the ability for a well chosen algorithm and ASYNC scheduler to produce an emerging property of memory in a system of oblivious mobile robots, and why it is not a problem for luminous rendezvous algorithms.

Tables

Table 1. Table 1 : Movement resolution. Each tuple represents (position, me.pending, other.pending). Major changes appear in boldface. A bottom value ( ⊥ bottom \bot ) represents the absence of pending moves. Wildcard (*) replaces any value and placeholder (–) retains the original value. Rule precedence is from top to bottom.

from NEAR or SAME
(   ,	Stay ,	* ) $\rightsquigarrow$ (	– ,	$\perp$ ,	– )
(   ,	Miss ,	Stay — $\perp$ ) $\rightsquigarrow$ (	NEAR ,	$\perp$ ,	– )
(   ,	Miss ,	* ) $\rightsquigarrow$ (	NEAR ,	$\perp$ ,	Miss )
(   ,	M2O ,	Stay — $\perp$ ) $\rightsquigarrow$ (	SAME ,	$\perp$ ,	– )
(   SAME ,	M2O ,	* ) $\rightsquigarrow$ (	SAME ,	$\perp$ ,	– )
(   NEAR ,	M2O ,	* ) $\rightsquigarrow$ (	SAME ,	$\perp$ ,	Miss )
(   ,	M2H ,	M2H ) $\rightsquigarrow$ (	– ,	$\perp$ ,	M2O )
(   ,	M2H ,	Stay — $\perp$ ) $\rightsquigarrow$ (	– ,	$\perp$ ,	– )
(   ,	M2H ,	* ) $\rightsquigarrow$ (	– ,	$\perp$ ,	Miss )

Table 2. Table 2: Results of model-checking liveness

			LC-atomic	Move-atomic
Centralized	FSYNC	SSYNC	ASYNC	ASYNC	ASYNC
Non-Rigid Self-Stabilizing
-	-	-	-	-	-	NoMove
-	✓	-	-	-	-	ToHalf
✓	-	-	-	-	-	ToOther
✓	✓	✓	✓	-	-	Vig2Cols
✓	✓	✓	✓	✓	✓	Vig3Cols
✓	✓	✓	✓	✓	✓	Her2Cols
✓	✓	✓	-	-	-	Flo3ColsX
✓	✓	✓	✓	-	-	Oku5ColsX
✓	-	-	-	-	-	Oku4ColsX
✓	-	-	-	-	-	Oku3ColsX
Rigid333This algorithm is supposed to be non-rigid. However, as is shown in the appendix, proving non-rigid, non-self-stabilizing algorithms is a lot trickier and cannot be done by the current version of our model checker. Quasi-Self-Stabilizing
✓	✓	✓	✓	-	-	Oku4Cols QSS333This algorithm is supposed to be non-rigid. However, as is shown in the appendix, proving non-rigid, non-self-stabilizing algorithms is a lot trickier and cannot be done by the current version of our model checker.
Rigid Non-Self-Stabilizing
✓	✓	✓	✓	-	-	Oku3Cols NSS

Table 3. Table 3 : Model Checker runtime performance for the ASYNC scheduler on an Intel i7-8650U running SPIN 6.4.9 on Arch Linux.

	States				Runtime	Memory
	Sorted	Matched	Transitions	Atomic steps	[ms]	[MB]
NoMove	12,080	2,738	17,604	73,027	220	145
ToHalf	6,141	979	10,979	57,152	130	135
ToOther	4,046	57	8,367	34,372	110	134
Vig2Cols	188,010	4,014,448	5,452,656	33,925,728	3,110	151
Vig3Cols	612,209	13,678,976	18,419,016	$114\times {10}^6$	11,200	190
Her2Cols	395,150	8,589,648	11,652,481	72,971,392	6,840	170
Flo3ColsX	13,053	48,509	80,419	440,286	210	135
Oku5ColsX	414,247	8,981,645	12,126,155	73,027,637	7,870	172
Oku4ColsX	307,795	6,607,778	8,936,310	54,718,251	5,080	162
Oku3ColsX	83,072	1,714,653	2,329,400	14,330,584	1,380	142
Oku4Cols QSS	307,793	6,607,778	8,936,308	54,718,251	5,110	162
Oku3Cols NSS	83,070	1,714,653	2,329,398	14,330,584	1,380	142

Table 4. Table 4 : Distance after a full cycle of A 𝐴 A and n 𝑛 n full cycles of B 𝐵 B with an initial distance of X 𝑋 X

	$A$ has a pending Stay	$A$ has a pending M2H	$A$ has a pending M2O
$B$ executes $n$ Stay	$X$	$[\frac{X}{2},X-\delta ]$	$[0,X-\delta ]$
$B$ executes $n$ M2H	$[\frac{X}{2^n},X-n\delta ]$	$[0,X-\left(n+1\right)\delta ]$	$[0,X-\frac{X}{2^n}]$
$B$ executes $n$ M2O	$[0,X-n\delta ]$	$[0,\frac{X}{2}]$	$[0,X]$

Full text

There exist many different rendezvous algorithms that aim at finding the minimal number of colors needed to solve rendezvous in various synchrony models (e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically very simple, their analysis and proof of correctness tend to be extremely complex, tedious, and error-prone as impossibility results are based on subtle interactions between robots activation schedules.

The paper presents a generic verification model written for the SPIN model-checker. In particular, we explain the subtle design decisions that allow to keep the search space finite and tractable, as well as prove several important theorems that support them. As a sanity check, we use the model to verify several known rendezvous algorithms in six different models of synchrony. In each case, we find that the results obtained from the model-checker are consistent with the results known in the literature. The model-checker outputs a counter-example execution in every case that is known to fail.

In the course of developing and proving the validity of the model, we identified several fundamental theorems, including the ability for a well chosen algorithm and ASYNC scheduler to produce an emerging property of memory in a system of oblivious mobile robots, and why it is not a problem for luminous rendezvous algorithms.

1 Introduction

Since the seminal work of Suzuki and Yamashita [33], much research on cooperative mobile robots has aimed at identifying the minimal assumptions (in terms of synchrony, sensing capabilities, environment, etc.) under which basic problems such as gathering or rendezvous can be solved.

Robots are modelled as mathematical points in the 2D Euclidean plane that independently execute their own instance of the same algorithm. In the model we consider, robots are anonymous (i.e., indistinguishable from each-other), oblivious (i.e., no persistent memory of the past is available), and disoriented (i.e., they do not agree on a common coordinate system). The robots operate in Look-Compute-Move cycles. In each cycle a robot “Looks” at its surroundings and obtains (in its own coordinate system) a snapshot containing the locations of all robots. Based on this visual information, the robot “Computes” a destination location (still in its own coordinate system) and then “Moves” towards the computed location. Since the robots are identical, they all follow the same deterministic algorithm. The algorithm is oblivious if the computed destination in each cycle depends only on the snapshot obtained in the current cycle (and not on the past history of execution). The snapshots obtained by the robots are not consistently oriented in any manner (that is, the robots’ local coordinate systems do not share a common direction nor a common chirality111Chirality denotes the ability to distinguish left from right.).

The execution model significantly impacts the ability to solve collaborative tasks. Three different levels of synchronization have been commonly considered. The strongest model is the fully-synchronous (FSYNC) model [33] where each phase of each cycle is performed simultaneously by all robots. The semi-synchronous (SSYNC) model [33] considers that time is discretized into rounds, and that in each round an arbitrary yet non-empty subset of the robots are active. The robots that are active in a particular round perform exactly one atomic Look-Compute-Move cycle in that round. It is assumed that the scheduler (seen as an adversary) is fair in the sense that in each execution, every robot is activated infinitely often. The weakest model is the asynchronous (ASYNC) model [21, 20], which allows arbitrary delays between the Look, Compute and Move phases, and the movement itself may take an arbitrary amount of time.

1.1 Gathering

The gathering problem is one of the benchmarking tasks in mobile robot networks, and has received a considerable amount of attention (e.g., [1, 2, 9, 10, 11, 15, 21, 23, 24, 26, 32, 33, 19]). The gathering task consists in all robots reaching a single point, not known beforehand, in finite time. The particular case of gathering two robots is called rendezvous in the literature. A foundational result [33] shows that in the SSYNC model, no deterministic algorithm can solve rendezvous without additional assumptions. This impossibility result naturally extends to the ASYNC model [21].

To circumvent the aforementioned impossibility result, it was proposed to endow each robot with a light [14], that is, it is capable of emitting one color among a fixed number of available colors, visible to all other robots. This additional capacity allows to solve rendezvous in the most general ASYNC model, provided that lights of robots are capable to emit at least four colors. In the more restricted SSYNC model, Viglietta [34] proved that being able to emit two colors is sufficient to solve the rendezvous problem. In the same paper [34], Viglietta proves [34] that three colors are sufficient in ASYNC. Both solutions in ASYNC [14, 34] and SSYNC [34] output a correct behavior independently of the initial value of the lights’ colors. Recently, Okumura et al. [27] presented an rendezvous algorithm with two colors in ASYNC assuming rigid moves (that is, the move of every robot is never stopped by the scheduler before completion), or assuming non-rigid moves but robots being aware of $\delta$ (the minimum distance before which the scheduler cannot interrupt their move). Also, the solution of Okumura et al. [27] requires lights to have a specific color in the initial configuration. Finally, Heriban et al. [23] show that two colors are necessary and sufficient in ASYNC without extra assumptions.

However, all aforementioned results were proved in an ad-hoc manner (i.e., with handwritten proofs). As they often use case-based reasoning, are lengthy and complex, they are tedious to check and thus to write, hence error-prone.

1.2 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 used in the context of mobile robots [8, 16, 7, 3, 25, 12, 6, 30, 16, 31, 5].

When robots move freely in a continuous two-dimensional Euclidean space (as considered in this paper), to the best of our knowledge the only formal framework available is Pactole.222http://pactole.lri.fr It relies on higher-order logic to certify impossibility results [3, 12, 5], as well as the correctness of algorithms [13, 16] in the FSYNC and SSYNC models, possibly for an arbitrary number of robots (hence in a scalable manner). Pactole was recently extended by Balabonski et al. [4] to handle the ASYNC model, thanks to its modular design. However, in its current form, Pactole lacks automation; that is, in order to prove a result formally, one still has to write the proof (that is automatically verified), which requires expertise both in Coq (the language Pactole is based upon) and about the mathematical and logical arguments one should use to complete the proof.

On the other side, model checking and its derivatives (automatic program synthesis, parameterized model checking) hint at more automation once a suitable model has been defined with the input language of the model checker. In particular, model-checking proved useful to find bugs (usually in the ASYNC setting) [7, 17, 18] and to formally check the correctness of published algorithms [16, 7, 30]. Automatic program synthesis [8, 25] was used to obtain automatically algorithms that are “correct-by-design”. However, those approaches are limited to instances with few robots. Generalizing them to an arbitrary number of robots with similar models is doubtful as Sangnier et al. [31] proved that safety and reachability problems are undecidable in the parameterized case. Another limitation of the above approaches is that they only consider cases where mobile robots evolve in a discrete space (i.e., graph). This limitation is due to the model used, that closely matches the original execution model by Suzuki and Yamashita [33]. As a computer can only model a finite set of locations, a continuous 2D Euclidean space cannot be expressed in this model.

Overall, the only way to obtain automated proofs of correctness in the continuous space context through model checking is to use a more abstract model.

1.3 Our contribution

We present a new formal model and related proof techniques enabling the use of model checking tools for mobile robots evolving in a 2D Euclidean space. Because of the nature of rendezvous, we abstract the Euclidean space into a single line, which is itself discretized into a finite number of well-defined distance states. The number of those states depends on the exact hypotheses of the verified algorithm. Our process relies on the fact that rigid-motion algorithms are, by definition, distance-independent, and so limiting the space model to two states: {gathered, non-gathered} is sufficient to properly model the distance. We also prove that, in the case of self-stabilizing algorithms, rigid and non-rigid motions are equivalent. Proving non-rigid, non-self-stabilizing algorithms is, however, more complex, and we propose a method to check them properly. We propose a way to prove algorithms such as the one presented in Okumura et al. [27].

We also show that proving any algorithm for the ASYNC scheduler is, unsurprisingly, extremely difficult. We prove that for a well-chosen scheduler, algorithm, and initial configuration, it is possible for every configuration in the execution to depend on the initial configuration even when robots are oblivious. However, we point out a structural property satisfied by known rendezvous algorithms that enables reducing the verification space tremendously.

2 Definitions and Terminology

2.1 System model

The system consists of a finite set of dimensionless robots evolving in a boundless 2D Euclidean space, devoid of any landmarks or obstacles. The robots cannot explicitly communicate with each other and do not share any notion of a global coordinate system as defined by a common origin, unit distance, or directions and orientations of the axes. These coordinate systems are not assumed to be consistent during the execution.

Robots are anonymous in that they are unaware of an identity and execute the exact same algorithm consisting of cycles of the basic operations: Look, Compute, Move. We also consider a Wait phase between the end of the Move phase and the beginning of the Look phase. Robots are oblivious in the sense that their new destination only depends on the current snapshot.

Robots’ activations are independent and governed by an adversary scheduler acting according to a synchrony model which can vary from Centralized (where activation cycles execute in mutual exclusion) or FSYNC (fully synchronous; where activation cycles always occur in parallel) to SSYNC (semi-synchronous, where the scheduler can choose between FSYNC and Centralized) and ASYNC (asynchronous; where activation steps occur independently). We also consider the more recent LC-atomic ASYNC and Move-atomic ASYNC schedulers [27], which are variants of the ASYNC for which the Look and Compute, or the entire Move phase, respectively, must happen atomically. The scheduler may also have the ability to influence the movement of robots. In the case of rigid motion, a robot always reaches its target upon completion of its Move phase. In the case of non-rigid motion, the scheduler may stop the robot before it reaches its target, but not before it has travelled a minimum distance of $\delta>0$, usually unknown to the robots.

We also consider a fair scheduler, which activates every robot infinitely often.

Additionally, in this paper we consider that robots are equipped with a light that can emit a color among a fixed number of different colors. A robot can observe the color of all lights during its Look phase and change the color of its light at the end of its Compute phase. During the compute phase, the snapshot may lead to a deterministic change in color. Then, we say the new color is pending until the Compute phase has ended. Similarly, we call target (or pending move) the destination dictated by a robot’s snapshot that it tries to reach in its next Move phase. More specifically, this is called the ”full light” model. Other variants in the literature consider the cases where a robot can only observe the light of the other robots (external light model), or can only observe its own light (internal light model). This paper considers both the full and external light models.

A more detailed model is provided in the appendix.

2.2 Configurations and executions

The union of the local states (position, color, phase, pending move and color) of all robots defines a configuration. An execution is a sequence, possibly infinite, starting in an initial configuration and where each transition corresponds to the activation of a subset of the robots according to the constraints of the scheduler.

2.3 Rendezvous problem

The gathering problem requires that all robots eventually reach the same location from any initial location and regardless of activations decided by the scheduler.

The rendezvous problem is another name for the gathering of two robots. Intuitively, the problem may seem simpler to solve due to the smaller number of robots, but this is actually the opposite, due to symmetry. Indeed, with only two robots and no lights, all configurations are symmetrical and hence convey no information other than distance. Because of the lack of a common coordinate system, this information is limited to the binary {gathered, non-gathered}.

2.4 Self-Stabilization

A rendezvous algorithm is self-stabilizing if robots eventually reach and stay forever at the same location regardless of the initial configuration. Algorithms that set constraints on the initial configuration (e.g., must start with a specific color) are not self-stabilizing. We introduce a more refined definition of self-stabilization.

Definition 1** (Simple Self-Stabilization).**

An algorithm is simply self-stabilizing for problem $\mathcal{P}$ if it solves $\mathcal{P}$ starting from any initial position and any initial color, with all robots in the Wait phase.

Definition 2** (Complete Self-Stabilization).**

An algorithm is completely self-stabilizing for problem $\mathcal{P}$ if it solves $\mathcal{P}$ from any initial position, color, phase, target and pending color.

Following the same terminology, an initial configuration where both robots are in the Wait phase is called a simple initial configuration. Otherwise it is a complete initial configuration. We similarly define simple executions and complete executions. If a complete execution has a common suffix with a simple execution, we say it is simple-reachable.

3 From the system model to the verification model

Implementing the system model we consider into a verification model that can be checked by a model-checker is difficult, as some elements are continuous (position of both robots, pending moves of both robots). This section is dedicated to proving that those problematic elements can be discretized in a way that enables mechanized verification.

3.1 Simple vs. Complete self-stabilization

This subsection is dedicated to proving that pending moves and pending colors can be removed from the verification model in the case of self-stabilizing rendezvous algorithms. This is true for all self-stabilizing algorithms under the FSYNC, Centralized, and SSYNC schedulers (Lemma 2), and true for specific self-stabilizing algorithms under the ASYNC scheduler (Theorem 3).

Lemma 1**.**

Any completely self-stabilizing algorithm is also simply self-stabilizing.

To prove the reverse, we want to prove that every complete execution is simple-reachable. If this is the case, then any complete execution is eventually explored by starting from a simple initial configuration.

Lemma 2**.**

Under the FSYNC, Centralized and SSYNC schedulers, any simply self-stabilizing algorithm is also completely self-stabilizing.

Intuitively, it seems that this also holds for the case of ASYNC algorithms. Since both robots are oblivious, with the exception of color, it seems logical that the system eventually “forgets” its initial configuration, and becomes reachable from a simple initial configuration.

Surprisingly, we show that it is possible, for a well-chosen algorithm, ASYNC scheduling, and complete initial configuration to create an infinite execution that never becomes simple-reachable.

Theorem 1**.**

A simply self-stabilizing algorithm is not necessarily completely self-stabilizing in the ASYNC model.

For a well-chosen algorithm, scheduler, and complete initial configuration, it is possible for the system to have an emerging property of memory. This is because it is possible to have the current configuration depend on the initial configuration indefinitely (see appendix for details).

In practice, most rendezvous algorithms in the literature prevent this behavior by forcing robot $A$ to wait for robot $B$ without being able to change its color or move. As the scheduler relies on its ability to feed outdated information infinitely often to the robot performing the Look to create non-oblivious executions, when synchronization is enforced by the algorithm, the scheduler looses this capability.

We first observe that in the case of oblivious deterministic rendezvous algorithms (that is, algorithms that make use of a single color), simple self-stabilization implies complete self-stabilization.

Theorem 2**.**

If a simply self-stabilizing algorithm achieves rendezvous, it is also a simply self-stabilizing algorithm for rendezvous with arbitrary initial targets.

Because no deterministic solution exists in this setting, we study the case of ASYNC luminous rendezvous algorithms using at least two colors.

To tackle the case of color memory, we consider two luminous ASYNC rendezvous algorithms: Viglietta 3 [34] colors and Heriban 2 colors [23]. For both algorithms, we find a structural condition we prove is sufficient to block the scheduler from creating any color memory execution.

Theorem 3** (Identical Color Condition).**

We define the identical color condition (ICC) as: ”For any pair of robots $A$ and $B$ whose colors are $Color_{A}$ and $Color_{B}$, respectively, $A$ can decide on a new color (different from $Color_{A}$) if and only if its snapshot shows $Color_{A}$ and $Color_{B}$ are identical.” For any luminous rendezvous algorithm, if the algorithm satisfies ICC and is simply self-stabilizing, then is it also completely self-stabilizing.

In this paper, the model checker only uses simple initial configurations. From Theorem 3, we can extend the positive results to complete initial configurations when considering algorithms that satisfy ICC such as Viglietta 3-colors [34] and Heriban 2 colors [23]. Of course, negative results are not impacted, as a counter-example in the simply self-stabilizing context is also a counter-example in the completely self-stabilizing context.

3.2 Self-Stabilization and rigidity

The non-rigid assumption is another source of a continuous variable in the model: when the robot target a point at some distance $d\geq\delta>0$, the scheduler may stop the robot anywhere between $\delta$ and $d$. In this section, we explore under which circumstances we can restrict the verification model to rigid moves only without loosing generality, and show that completely self-stabilizing rendezvous algorithms satisfy the condition (Theorem 4).

Using criteria such as (complete) self-stabilization and rigidity, we can define four different settings for rendezvous algorithms according to the combination of $\{\textit{rigid},\textit{non-rigid\}}$ and $\{\textit{self-stabilizing},\textit{non}$ self-stabilizing}. Studying the literature on rendezvous algorithms, we were not able to find examples of self-stabilizing algorithms requiring rigid moves that failed with non-rigid moves. The following theorem shows that such algorithms cannot exist.

Theorem 4**.**

Any completely self-stabilizing algorithm that achieves rendezvous assuming rigid moves also achieves it assuming non-rigid moves.

Theorem 4 implies that in order to prove complete self-stabilization, it is only necessary to prove the property assuming rigid moves.

3.3 Proving rendezvous algorithms

The last mile to the verification model is to show that the remaining continuous variable of the current configuration (the distance between the two robots) can be abstracted into two states only (Theorem 5)

We first show that, when robots may only move in straight lines, rendezvous algorithms need only use three kinds of movements: stay put, move to the midpoint, or move to the other robot.

Lemma 3**.**

The three types of motion stay put (Stay), move to the midpoint (M2H), and move to the other robot (M2O) are both necessary and sufficient to achieve rendezvous in SSYNC and ASYNC.

Lemma 4**.**

When two robots $A$ and $B$ start from the Wait state, in an infinite fair execution, either the distance between $A$ and $B$ eventually remains constant, or it converges toward [math].

We observe that, for any rendezvous algorithm execution that solely uses the three required movements, and where robots $A$ and $B$ start in the Wait phase, the entire execution happens on the line $(AB)$.

Theorem 5** (Rigid motion model).**

When proving the correctness of a rigid-motion rendezvous algorithm that solely uses the three required movements, only using the two model states gathered and not-gathered is sufficient to properly represent the Euclidean plane.

Thanks to Theorem 5, we now have a finite number of states to model the entire Euclidean plane in the case of rigid rendezvous. Note that this holds for both self-stabilizing and non-self-stabilizing algorithms. In turn, this implies that we may use model checking to verify the validity of a rendezvous algorithm in the particular case of rigid motion. Furthermore, we can verify (simple) self-stabilization by checking all possible pairs of colors, and that this also verifies complete self-stabilization if the algorithm satisfies ICC (by Theorem 3) and non-rigid completely self-stabilizing algorithms (by Theorem 4).

The only remaining family of algorithms is non-rigid, non-self-stabilizing algorithms.

Theorem 6**.**

To prove non-rigid non-self-stabilizing algorithms to achieve rendezvous, verifying rigid behavior is necessary but not sufficient to prove the correctness of the algorithm.

We present a possible approach for checking these algorithms in the appendix. To the best of our knowledge, the 4-color external light algorithm by Okumura et al. [26] is the only known rendezvous algorithm that satisfies these two criteria.

Note that our reasoning is only true in the case where the behavior of the algorithm is the same for any distance between $A$ and $B$ that is greater than zero. Recently, Okumura et al. [28] introduced an algorithm under the additional assumption that robots have the knowledge of $\delta$. Because of this, the behavior of the algorithm is different when the distance is less than $\delta$, and when it is between $\delta$ and $2\delta$, which means that the rigid and the non-rigid behavior of the algorithm are different. To prove such algorithms, we also need to both prove the rigid and non-rigid behaviors.

Theorem 7**.**

To prove completely self-stabilizing rendezvous algorithms whose behavior differs depending whether the distance between $A$ and $B$ is smaller than $\delta$, between $\delta$ and $2\delta$, or greater than $2\delta$, it is sufficient to consider the case where robots are initially $3\delta$ apart.

4 Verification Model

4.1 Position

Our verification model only needs to consider two different positions (called NEAR, SAME) depending on the distance between the two robots. This choice is justified by the definition of the model (two robots, no shared coordinate system, no landmarks, oblivious robots) and Theorem 5

4.2 Activation and synchrony

In the verification model, the activation cycle of a robot $r$ is defined as a sequence of four consecutive atomic events: Look, Compute, $\mbox{{Move}}_{\mbox{{b}}}$, and $\mbox{{Move}}_{\mbox{{e}}}$. Each of the four events is as follows:

Look** (L)**

The robot obtains a snapshot observation of the environment which consists of the color of both robots and the location of the other robot with respect to $r$’s local coordinate system where $r$ is always at the origin.

Compute** (C)**

The robot executes the algorithm which is defined as a function of the latest observation that returns a new color and a move order. In the verification model, we assume that the light of the robot changes as part of the compute event.

$\mbox{{Move}}_{\mbox{{b}}}$** (B)**

The robot begins moving according to the move order. Although it can be observed while moving, the actual position of the robot is actually undefined until the movement is completed with the $\mbox{{Move}}_{\mbox{{e}}}$ event.

However, we assume that the robot moves according to a straight line toward its target (point computed by the algorithm), and that it only progresses forward until reaching the destination of the move (point within the reachable distance $\delta$).

$\mbox{{Move}}_{\mbox{{e}}}$** (E)**

The robot ends its move and has moved a distance of at least $\delta$ towards the target. If the distance to the target was equal or less than $\delta$, the robot has reached its target.

We use this four-events verification model instead of the classical three phases model because of the flexibility it allows when defining variants of the ASYNC model. We can set the Look phase to be instantaneous by linking a Compute event to happen right after each Look event, or set to LC-atomic ASYNC by linking Look, Compute and $\mbox{{Move}}_{\mbox{{b}}}$, or Move-atomic ASYNC by linking $\mbox{{Move}}_{\mbox{{b}}}$ and $\mbox{{Move}}_{\mbox{{e}}}$, and so on.

Theorem 8**.**

The FSYNC scheduler can be properly simulated by activating sequentially the Look phase of robot $A$, the Look phase of robot $B$, the Compute $\mbox{{Move}}_{\mbox{{b}}}$, and $\mbox{{Move}}_{\mbox{{e}}}$ of robot $A$ and finally the Compute $\mbox{{Move}}_{\mbox{{b}}}$, and $\mbox{{Move}}_{\mbox{{e}}}$ of robot $B$, infinitely often.

Theorem 9**.**

Two simultaneous events $E1$ and $E2$ can be properly simulated by exploring both sequences $(E1,E2)$ and $(E2,E1)$.

Theorem 10**.**

Except for non-rigid non-self-stabilizing rendezvous, a fair scheduler can be properly simulated by an 8$N$-bounded scheduler, where $N$ denotes the number of colors available to the algorithm.

Because we check for a maximum of 5 colors, the model checker uses a 40-bounded scheduler.

4.3 Movement resolution

The key to our verification model is the idea of movement resolution. When a robot completes its movement, this translates into a change of the verification model according to specific rules, which are described below.

Stationary moves When the computed move is invariant or stationary (e.g., M2O when the observed position is SAME), its pending move is systematically translated to an equivalent Stay move. A robot that has a Stay pending move is stationary, and hence is not observed as moving between $\mbox{{Move}}_{\mbox{{b}}}$ and $\mbox{{Move}}_{\mbox{{e}}}$.

From NEAR or SAME position The key aspect of the verification model is the case when the robots are in rigid motion (NEAR and SAME), and we only detail the resolution of moves for this combined case.

Stay

No change.

Miss

The pending move is a sure miss. A miss happens for instance if $r$ observes the other robot while it moves. It also happens indirectly during movement resolution. The result of a Miss move is always NEAR (in particular, it can happen if the position was SAME).

M2O

If the position is SAME, then the move is treated as a Stay. If the other robot is either Stay or $\bot$, then the position is now SAME. Else, if the other robot has a pending move, it is converted to a Miss and the position is now SAME.

M2H

If the pending move of the other robot is Stay or $\bot$, then neither the distance nor the pending move of the other robot changes. If the pending move of the other robot is also M2H, then the move is potentially successful and the pending move of the other robot is changed into an M2O move that targets the location just newly reached. Thus, provided that the first robot doesn’t move in the meantime, the movement of the other robot later leads to SAME. Else, the distance is still NEAR and the pending move or the other robot is now Miss.

5 Checking Rendezvous Algorithms

5.1 Rendezvous Algorithms

To assess the verification model, we have checked three trivial baseline algorithms as well as seven known algorithms from the literature. For each of these algorithms, it is widely-known in which models they achieve rendezvous or fail. Unless explicitly stated otherwise, algorithms are non-rigid and self-stabilizing. The latter seven algorithms are detailed in Figure 2 and the code for some of them can be found in the appendix.

“NoMove”: the robots never move and hence the algorithm always fails to achieve rendezvous regardless of the model; 2. 2.

“ToHalf”: the robots always target the midpoint and the algorithm fails in all models but FSYNC. 3. 3.

“ToOther”: the robots always target the other robot’s position and the algorithm fails in all models but Centralized. 4. 4.

“Vig2Cols”: the algorithm (Figure 2(a)) was originally proved correct in SSYNC [34] but was later proved to also achieve rendezvous in LC-atomic ASYNC [27]. The algorithm is known to fail in ASYNC [34]. 5. 5.

“Vig3Cols”: the algorithm (Figure 2(b)) is known to succeed in ASYNC and consequently in all other weaker models [34]. 6. 6.

“Her2Cols”: the algorithm (Figure 2(c)) is an extension of ”Vig2Cols” that uses only two colors but succeeds in ASYNC [23]. The algorithm is optimal in the sense that rendezvous in ASYNC cannot possibly be achieved with fewer colors. 7. 7.

“Flo3ColsX”: the algorithm (Figure 2(d)) achieves rendezvous in SSYNC in a model with external colors. The algorithm is known to succeed in SSYNC and to fail in ASYNC [22]. 8. 8.

“Oku5colsX”: the algorithm achieves rendezvous in LC-atomic ASYNC in a model with external colors. The algorithm is known to succeed in LC-atomic ASYNC and to fail in ASYNC [26]. 9. 9.

“Oku4colsX”: the algorithm achieves rendezvous in LC-atomic ASYNC in a model with external colors. It is quasi-self-stabilizing, meaning in requires the starting colors of the robots to be identical. The algorithm is known to succeed in LC-atomic ASYNC and to fail in ASYNC [26]. 10. 10.

“Oku3colsX”: the algorithm achieves rendezvous in LC-atomic ASYNC in a model with external colors. It is a rigid, non-self-stabilizing algorithm. The algorithm is known to succeed in LC-atomic ASYNC and to fail in ASYNC [26].

5.2 Verification by Model Checking

Given a rendezvous algorithm and a verification model, the SPIN model checker essentially verifies that the following liveness property (expressed in LTL) holds in every possible execution:

ltl gathering { <> [] (position == SAME) }

The formula defines a predicate called gathering with the meaning that there is a time after which the position is always SAME. Concretely, to verify the property, the model checker runs an exhaustive search in the transition graph of configurations such that all initial configurations lead to some cycle such that the predicate gathering holds or, in other words, that the variable position is equal to SAME in every configuration of such cycle(s).

Two of those results were actually unexpected: Oku3colsX [26] and Oku4colsX [26] are not supposed to be self-stabilizing at all, yet are verified to be self-stabilizing under the centralized scheduler by our model checker. However, looking in details at the algorithms, it turns out that the key counter-examples to self-stabilization rely on a simultaneous execution of both robots, which explains the result.

6 Conclusion and Future Work

In this paper, we introduced the first model for continuous space rendezvous algorithms that enables mechanical verification. To achieve this, we designed a new abstraction layer for mobile robots and proved that our new model was sufficient for proving properties that are relevant for our purpose. This lead to unexpected but interesting results for general self-stabilizing robot algorithms, such as the non existence of rigid-only self-stabilizing algorithms, and the possible emergence of memory in a system of oblivious robots due to ASYNC scheduling. Using SPIN as a basis for our work, we were able to confirm known results for ten different rendezvous algorithms proposed in the literature (performance results are presented in Table 3).

Our framework is, however still incomplete and ongoing. While we describe a way to extend our model to non-rigid non-self-stabilizing algorithms, the actual implementation is not complete yet. Also, although the proof arguments sustaining our abstract model are relatively simple, for the sake of having a completely mechanically verified result, we would like to have rewrite them formally using a proof assistant such as CoQ [29].

Appendix A Appendix

A.1 Reminder: Robot System Model

An execution of robot $r$ is defined as a possibly infinite sequence of activation cycles of $r$. A global execution is a sequence of events on both robots, such that the event of each robot $r$ is a robot execution of $r$, and the interleaving of events follows the rules of the activation model:

Centralized

The activation cycle of a robot is atomic. In other words, a single robot is activated at a time and executes a full activation cycle each time (see Figure 1).

FSYNC

The activation cycles of both robots are executed simultaneously. Equivalently, the robots always follows the following atomic sequence: each robot executes a Look event and then, in turn, each robot sequentially execute Compute, $\mbox{{Move}}_{\mbox{{b}}}$, and $\mbox{{Move}}_{\mbox{{e}}}$. This is depicted in Figure 1.

SSYNC

Activation cycles can be either centralized or combined (as FSYNC).

ASYNC

Each event is atomic but there is no atomicity between events (see Figure 1).

LC-atomic ASYNC

Same as ASYNC, but the Look and Compute events execute atomically.

Move-atomic ASYNC

Same as ASYNC, but the $\mbox{{Move}}_{\mbox{{b}}}$ and $\mbox{{Move}}_{\mbox{{e}}}$ events execute atomically.

In this paper, we assume that robots are always activable and that the scheduling is fair. Consequently, both robots are activated infinitely many times.

A.2 Proving lemmas and theorems of Section 3

Proof: Lemma 1.

Since the set of initial configurations allowed for simple self-stabilization is a subset of the one allowed for complete self-stabilization, if all complete initial configurations lead to a successful execution, then all simple starting execution also do. ∎

Proof: Lemma 2.

Under the FSYNC, Centralized and SSYNC scheduler, any complete initial configuration becomes a simple initial configuration after all robots finish their current cycle.∎

Proof: Theorem 1 : Oblivious Robots.

Let us assume two robots $A$ and $B$ running the ToOther algorithm, i.e., the target is always the other robot. Let us also assume an initial configuration where $A$ is in the Wait phase and $B$ is in the Compute phase and has targeted point $P_{1}$ such that $|AP_{1}|=|BP_{1}|=|AB|$. In other words, $ABP_{1}$ is an equilateral triangle. Note that this is a complete, but not simple initial configuration.

We first activate $A$, which is now in its Compute phase and targets the current location of $B$. We then activate $B$ which starts moving towards $P_{1}$. We then activate $B$ again as it reaches $P_{1}$ and is now in its Wait phase.

This current configuration is identical to the initial configuration. Thus, we have an execution that repeats infinitely often while never being reachable from both robots starting in the Wait phase, because starting from the Wait phase cannot yield a target outside the $[AB]$ segment

While this is the simplest example of the behaviour that we could devise, it should be noted that a similar execution could be achieved using a move-to-half algorithm, the only difference being the $ABP_{1}$ would be shrinking with each activation. Similarly, any initial configuration that included a target outside of the line $(AB)$ could lead to a similar execution, given the right algorithm and ASYNC scheduling.

Figure 3 visually shows the execution, with the colored cross showing the target of the robot.

∎

Proof: Theorem 1: Luminous Robots.

Let us assume the three-color algorithm in Figure 4, and an initial configuration of two robots $A$ and $B$, where $A$ starts in color 1, in the Wait phase, and $B$ in color 2, in the Compute phase, with 3 as a pending color.

We then follow the execution described in Figure 5. We see that the last configuration is identical to the first one with $A$ and $B$ swapped, which means the execution can be executed infinitely often.

Let us now prove that this execution cannot be reached from a Wait/Wait initial configuration.

A three-color algorithm allows for 6 different color combinations.

• •

Starting from {1,2}, robot $B$ is stuck in color 2 and robot $A$ turns to color 2. So {1,2} leads to {2,2}

• •

Starting from {2,3}, robot $B$ is stuck in color 3 and robot $A$ turns to color 3. So {2,3} leads to {3,3}

• •

Starting from {3,1}, robot $B$ is stuck in color 1 and robot $A$ turns to color 1. So {3,1} leads to {1,1}

• •

Starting from 1,1, no robot can change color.

• •

Starting from 2,2, no robot can change color.

• •

Starting from 3,3, no robot can change color.

We now see that, if starting from Wait/Wait, no cycle of changing colors can be reached. Therefore, the previously described execution cannot be reached either. ∎

Lemma 5** (Condition of rendezvous in ASYNC).**

To achieve rendezvous in ASYNC, it is necessary that the targets of both robots are eventually always identical.

Proof: Lemma 5.

Let us assume that two robots are currently gathered, that is they occupy the same position, and remain there forever.

Let us assume for the purpose of contradiction that at some point during the execution, their targets become different. Then, there exists an execution where their positions become different. Therefore rendezvous is not actually achieved in this execution, a contradiction. ∎

Lemma 6** (Pending Colors).**

An execution that is not simple-reachable cannot contain a configuration in which all robots have identical pending and visible colors.

Proof: Lemma 6.

Let us assume a configuration in which all robots have identical pending and visible colors.

In this configuration, robots can only be in Wait, Move or Compute with a pending color identical to the visible one. If both robots are in Wait, then this can trivially be reached from a Wait/Wait configuration. If both robots are in Compute, then the following activation turns this configuration into a Compute/Move configuration with no change of color. If both robots are in Move, then the following activation turns this configuration into a Wait/Move configuration.

If one robot is in Wait and the other in Compute, then, after the second robot has reached Wait, the configuration can be reached by starting the second robot in its current color and the first robot in its previous color and activating it. The same reasoning holds if a robot is in Wait and the second in Move or Compute and Move. ∎

Based on Lemma 5 and 6 above, we can now prove Theorem 2.

Proof: Theorem 2.

In the case of oblivious robots, we know that rendezvous is not possible in SSYNC, hence in ASYNC. So, proving that an oblivious algorithm is simply self-stabilizing, means that it is also completely self-stabilizing.

For a luminous algorithm to be simply self-stabilizing, the condition must be true for any pair of colors. To obtain an execution similar to the one described in Figure 3, it is necessary for robots to always move to a target that depends on an outdated position of the other robot. If this behavior is allowed, then gathering is impossible, regardless of the initial target, as robots never have identical targets. ∎

Proof : Theorem 3.

We first prove that complete executions that are not simple-reachable must contain pending colors.

We know that any complete initial configuration must contain at least one pending color different from the current one to be non simple-reachable. Let us first consider the case where one robot $A$ has different pending and visible colors $A1$ and $A0$, and robot $B$ has identical colors $B0$.

We first show that the first activated robot must be $B$, as we see in Figure 6.

We show a possible memory execution in Figure 7

We now note that, if the algorithm follows the identical color condition, in order for $B1$ to be different from $B0$, we require $A0$ to be identical to $B0$. If we do not force change in color and have $B1=B0$, the configuration does not change and the first activation of $A$ leads to the counter example shown in Figure 6. Because of this, the scheduler now has two choices : Either activate $A$ or $B$. These two executions are shown if Figure 9 and 9.

In the case shown in Figure 9, following the condition leads to $A1$ being identical to $A0$, which is a contraction. In the case shown in Figure 9, following the condition leads to $B1$ being identical to $A0$, which we know leads to a simple-reachable configuration.

A similar reasoning can be held for the case where both robots have pending colors. ∎

Proof: Lemma 3.

First, these three motions are obviously sufficient since they are the only ones used by both Heriban et al. [23] and Viglietta [34] with two and three colors, respectively.

Next, we prove that it is necessary to use all of these motions to achieve rendezvous.

Consider the case where both robots are at distinct positions, anonymous and have the same color. As proven by Viglietta [34] in Proposition 4.1: “We may assume that both robots get isometric snapshots at each cycle, so they both turn the same colors, and compute destination points that are symmetric with respect to their midpoint. If they never compute the midpoint and their execution is rigid and fully synchronous, they never gather.” Therefore, Move to Half is necessary.

Similarly, consider now a case where snapshots are not isometric because of different colors. Let us assume that their algorithm makes them target any point between them, but not their own positions.

Because of the case where they are both activated at the same time, their targets need to be identical to gather. We model this as $\dfrac{D}{x}$ for robot $A$ and $\dfrac{(x-1)D}{x}$ for robot $B$, with $D$ the distance between $A$ and $B$ and $x$ is a real positive number. This is mandatory in the case where $A$ and $B$ are activated at the same time.

However, if $A$ and $B$ are activated sequentially for a full cycle and $x\neq 1$, then $A$ and $B$ have different targets. As long as no motion where $x=1$ exists, no rendezvous can happen if $A$ and $B$ are separated. When $x=1$, $A$ uses Move to Other and B uses Stay and rendezvous can be achieved. Therefore, M2O and Stay are both necessary. ∎

Definition 3** (Static Execution).**

We define a static execution as an execution during which the distance between $A$ and $B$ does not decrease.

Proof: Lemma 4.

We only consider three types of motion:

• •

Stay (Stay)

• •

Move to the midpoint (M2H)

• •

Move to the other robot (M2O)

First, it is trivial to see that, using these three types of motion, the distance between $A$ and $B$ cannot increase if both robot start in a Wait phase.

Next, we look at what happens after each robot completes at least one full cycle. The resulting distance is presenting in Table 4.

We note that only three static executions exist:

• •

No robot moves,

• •

Robot $A$ has a pending M2O and robot $B$ reaches robot $A$, either by:

• –

executing at least one M2O,

• –

executing an infinite number of M2H,

We also can notice that all other cases converge towards a distance of 0. This implies that any algorithm which includes only these three motions and no static execution reduces the distance between the two robots towards zero. ∎

Proof: Theorem 4.

For the purpose of contradiction, let us assume the existence of a completely self-stabilizing algorithm that achieves rendezvous with rigid moves, but not with non-rigid moves. This implies that there exists a non-rigid execution that does not lead to rendezvous.

Since the algorithm works in the rigid case, we know that it cannot include any of the static executions we described in Lemma 4 since they would also fail with rigid motion. Since these executions are not part of the algorithm, in the non-rigid case, any execution of the algorithm necessarily decreases the distance towards zero. Therefore the distance between two robots $A$ and $B$ eventually becomes less than $\delta$, with $\delta$ being the distance between $A$ and $B$ below which the behavior becomes rigid.

When that is the case, the behavior of the algorithm is strictly the same as the rigid-motion behavior. Since this execution does not achieve rendezvous, this means that there exists a state, which is part of the states of the rigid-motion behavior that does not achieve rendezvous. Hence, a contradiction. ∎

Proof: Theorem 5.

We know that a single line is sufficient to model the plane for the rendezvous problem in the general case. First, since robots have no common notion of length, the actual distance between the two robots, other than being gathered or not, cannot be used for deciding to move or change their color. We assume robots only use the three required movements. Because the motion is rigid, robots always reach their destinations. Therefore, if an execution leads to rendezvous, changing the initial distance between the two robots does not change the outcome of the execution. ∎

Proof: Theorem 6.

Consider an algorithm that achieves rendezvous with non-rigid moves when both robots start from color $C_{0}$, but fails to do so for any other initial color combination. To achieve rendezvous, the algorithm must work for any initial distance between both robots, including a distance smaller than $\delta$. Therefore, we know that checking the rigid behavior for color $C_{0}$ is necessary to prove non-rigid behavior.

For instance, Vig2Cols [34] achieves rendezvous with rigid moves when starting from color Black. However, we also know this algorithm to fail with non-rigid moves when starting with the same initial colors. Therefore, solely checking the rigid behavior would lead us to incorrectly consider Vig2Cols [34] to be a working non-rigid non-self-stabilizing algorithm. Hence, the condition is not sufficient. ∎

This happens because, after starting from an arbitrary distance, we cannot make any assumption about which configuration the system is in when the distance between robots becomes smaller than $\delta$. This configuration may indeed depend on the initial distance and the activation schedule.

Proof: Theorem 7.

In this particular case, we need to check three things:

That the rigid algorithm achieves rendezvous. 2. 2.

That the farthest non-rigid algorithm leads to the closest. 3. 3.

That the closest non-rigid algorithm leads to the rigid.

The first point is proven in the rigid part of the paper. We now only need to prove the second and third points.

This is easily done by remembering that any algorithm using only the three moves either allows static executions or not. If it does, then the distance is never reduced, and checking at $3\delta$ is equivalent to any other distance. If it does not, then the distance is eventually reduced to zero and hence eventually enters the second behavior. Similarly, we check that the second behavior leads to rigid by reducing distance. We only need to check that this decrease happens once for every initial configuration to ensure that distance is reduced towards rigid behavior. ∎

Proof: Theorem 8.

In the FSYNC model, the Look, Compute, $\mbox{{Move}}_{\mbox{{b}}}$, and $\mbox{{Move}}_{\mbox{{e}}}$ phases of all robots are executed simultaneously. However, since Look is a read-only operation, and Compute a write-only operation, with regards to color, these operations can be executed sequentially as long as no Look happens after a Compute (i.e., all $read$ operations happen before the first $write$ operation). A similar reasoning holds for the $\mbox{{Move}}_{\mbox{{b}}}$ to $\mbox{{Move}}_{\mbox{{e}}}$ being the beginning and end of a continuous write operation. ∎

Proof: Theorem 9.

We consider two cases:

In the first case, one event ($E1$) is a $read$ operation (Look), and one event ($E2$) is a $write$ operation (Compute). Since the same piece of information is being read and written at the same time, the result of the read operation cannot be determined. In the case of mobile robots, where the $write$ operation is a color transition from color $c_{1}$ to color $c_{2}$, we assume that the only colors that can be seen by the Look are $c_{1}$ or $c_{2}$444This assumption is analogous to assuming regularity with registers.. We then need to consider the case where the LOOK saw a $c_{1}$ (E1 then E2) and the case where it saw a $c_{2}$ (E2 then E1). 2. 2.

In any other case, since no read and write operation are happening at the same time, activating E1 and E2 simultaneously is identical to activating either E1 then E2, or E2 then E1.

∎

Proof: Theorem 10.

To properly limit the number of activations of the scheduler, we need to ensure that any change in the configuration made by $A$ that may impact the snapshot of $B$ has been explored. When performing its cycle, there are two such elements: $A$’s color, and the distance between $A$ and $B$.

Since there are only two distance states {SAME, NEAR }, a fixed number $N$ of colors, and it takes 4 activations to perform a cycle, limiting the fair scheduler to an 8$N$-fair scheduler, that is, a fair scheduler that can perform at most 8$N$ activations of robot $A$ between two activations of robot $B$ still ensures that every possible snapshot has been explored. ∎

Appendix B The case of non-rigid, non-self-stabilizing Algorithms

Because of Theorem 6, we cannot directly use our model checker in its current form to check this type of algorithms.

This is because a non-rigid algorithm can reach its rigid behavior in an unpredictable configuration. Our method for solving this issue is to notice that the number of those configurations is finite. More precisely, parameters include:

• •

The current color of each robot

• •

The pending color of each robot

• •

The phase of each robot

• •

The pending move of each robot

This means we have a number $N_{conf}$ of possible configurations.

We use this fact by creating a counter, which starts at 0 and increases up to $N_{conf}$.

We start the validation process in the FAR state. When executing the first movement resolution that leads to NEAR, we create two branches:

In the first branch, the robot reaches NEAR and we continue the process 2. 2.

In the second branch, the robot actually did not reach NEAR and is kept at FAR. We increment the counter by 1.

We repeat this process until the counter reaches $N_{conf}-1$. We have then created $2^{N_{conf}}-1$ branches to verify. However, we have ensured that any possible rigid motion behavior configurations has been checked. Repeating this process for every possible non-rigid motion initial configuration is enough to ensure that any possibly failing execution would have been detected.

B.1 Movement Resolution

The movement resolution rules described in Figure 1 (p. 1) are implemented by the Promela code described in Listing 1 below, during the $\mbox{{Move}}_{\mbox{{e}}}$ phase of the cycle.

In Promela, the meaning of if and the guarded actions guard -> action that follow is different from other languages in the sense that, when several guards are enabled, the execution faces a non-deterministic choice and the exploration of the model checker branches into several executions to explore all enabled guards. The guard else is exclusive in that it is enabled only when no other guards are enabled.

B.2 Verified Algorithms

B.3 Verification Model

B.3.1 State variables

The state of the system is represented by the following explicit variables:

• •

distance $\in\{\mbox{N{\scriptsize{EAR}}},\mbox{S{\scriptsize{AME}}}\}$

The distance between the two robots. NEAR means that it is equal or smaller and they have distinct positions, and SAME that they share the same location. When checking non-rigid non-self-stabilizing algorithm, the distance FAR can also be used.

• •

robot[_].color $\in\{\mbox{{Black}},\mbox{{White}},\mbox{{Red}},\mbox{{Yellow}},\mbox{{Green}}\}$

The observable color of the robot. The color Red is used only in 3 colors, 4 colors, and 5 colors algorithms. The color Yellow is used only in 4 colors and 5 colors algorithms. The color Green is used only in 5 colors algorithms.

and the following implicit variables:

• •

robot[_].phase $\in\{\mbox{{Look}},\mbox{{Compute}},\mbox{{Move}}_{\mbox{{b}}},\mbox{{Move}}_{\mbox{{e}}}\}$

Keeps track of the next event to execute in the activation cycle of the robot. This variable is managed by the scheduler and is particularly important for the ASYNC scheduler.

• •

robot[_].pending_move $\in\{\mbox{{Stay}},\mbox{{M2O}},\mbox{{M2H}},\mbox{{Miss}},\bot\}$

Holds the movement computed by the robot. This is not observable but used to resolve movements during the $\mbox{{Move}}_{\mbox{{e}}}$ phases. The variable is updated during the Look phase, based on the movement computed by the algorithm.

• •

robot[_].pending_color $\in\{\mbox{{Black}},\mbox{{White}},\mbox{{Red}},\mbox{{Yellow}},\mbox{{Green}},\bot\}$

New color for the robot, as computed by the algorithm. The color is computed during the Look phase of the robot and used during the Compute phase to update the visible color of the robot.

Depending on the model and algorithms, this can lead to at most $2*(5*4*5*6)^{2}=720^{\prime}000$ different states.

B.3.2 Activation Phases

Look

Reads the current state of the environment and saves it as an observation. Applies the algorithm to compute the pending move and the new color.

Compute

Updates the color of the robot in the environment.

$\mbox{{Move}}_{\mbox{{b}}}$

Begins moving. Unless the pending move is Stay, the robot’s position is undetermined until $\mbox{{Move}}_{\mbox{{e}}}$ and any that occurs in the interval causes an automatic Miss move for the other robot.

$\mbox{{Move}}_{\mbox{{e}}}$

The pending move is resolved into a new position for the robot and the environment is updated accordingly.

B.4 Verification and compile options

spin -a -DALGO=ALGORITHM -DSCHEDULER=SCHEDULER MainGathering.pml clang -DMEMLIM=1024 -DXUSAFE -DNOREDUCE -O2 -w -o pan pan.c ./pan -m100000 -a -f -E -n gathering

B.4.1 Verification output

Vig2Cols in ASYNC (fails)

Depth= 19582 States= 1e+06 Transitions= 3.86e+06 Memory= 146.311 t= 2.25 R= 4e+05 pan:1: acceptance cycle (at depth 2723) pan: wrote MainGathering.pml.trail

(Spin Version 6.4.9 -- 17 December 2018) Warning: Search not completed

Full statespace search for: never claim + (gathering) assertion violations + (if within scope of claim) acceptance cycles + (fairness enabled) invalid end states - (disabled by -E flag)

State-vector 107 byte, depth reached 25730, errors: 1 189620 states, stored (1.45028e+06 visited) 4046596 states, matched 5496875 transitions (= visited+matched) 34174756 atomic steps hash conflicts: 16160 (resolved)

Stats on memory usage (in Megabytes): 24.413 equivalent memory usage for states (stored*(State-vector + overhead)) 17.660 actual memory usage for states (compression: 72.34%) state-vector as stored = 70 byte + 28 byte overhead 128.000 memory used for hash table (-w24) 6.104 memory used for DFS stack (-m100000) 151.682 total actual memory usage

pan: elapsed time 3.25 seconds pan: rate 446239.69 states/second

After a failed execution, SPIN provides a (very verbose) counter-example that can be investigated with the following command.

spin -t MainGathering.pml

Her2Cols in ASYNC (Succeeds)

Depth= 16958 States= 1e+06 Transitions= 3.84e+06 Memory= 146.115 t= 2.26 R= 4e+05

(Spin Version 6.4.9 -- 17 December 2018)

Full statespace search for: never claim + (gathering) assertion violations + (if within scope of claim) acceptance cycles + (fairness enabled) invalid end states - (disabled by -E flag)

State-vector 107 byte, depth reached 17016, errors: 0 232931 states, stored (1.80493e+06 visited) 5061150 states, matched 6866078 transitions (= visited+matched) 42744752 atomic steps hash conflicts: 30286 (resolved)

Stats on memory usage (in Megabytes): 29.989 equivalent memory usage for states (stored*(State-vector + overhead)) 21.666 actual memory usage for states (compression: 72.25%) state-vector as stored = 70 byte + 28 byte overhead 128.000 memory used for hash table (-w24) 6.104 memory used for DFS stack (-m100000) 155.686 total actual memory usage

pan: elapsed time 4.07 seconds pan: rate 443471.25 states/second