Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Networks of mobile robots captured the attention of the distributed computing community, as they promise new application (rescue, exploration, surveillance) in potentially harmful environments. Originally introduced in 1999 by Suzuki and Yamashita [27], the model has been refined since by many authors while growing in popularity (see [20] for a comprehensive textbook). From a theoretical point of view, the interest lies in characterising, for each of these various refinements, the exact conditions under which a particular task can be solved or not.

In the model we consider, all robots are anonymous and operate using the same embedded program through repeated Look-Compute-Move cycles. In each cycle, a robot first “looks” at its environment and obtains a snapshot containing some information about the locations of all robots, expressed in the robot’s own self-centred coordinate system, whose scale and orientation might not be consistent with the other robot’s coordinate systems. Then the robot “computes” a destination, still in its own coordinate system, based only on the snapshot it just obtained. Finally the robot “moves” towards the computed destination.

The general model is agnostic to the shape of the space where the robots operate, which can be the real line, a two dimensional Euclidean space, a discrete space (a.k.a. a graph), or even another space with a more intricate topology. To date, two independent lines of research focused on (i) continuous Euclidean spaces, and (ii) graphs, studying different sets of problems and using distinct algorithmic techniques.

1 Continuous vs. Discrete Spaces

The core problem to solve in the context of mobile robot networks that operate in bidimensional continuous spaces is pattern formation, where robots starting from distinct initial positions have to form a given geometric pattern. Arbitrary patterns can be formed when robots have memory [27] or common knowledge [21], otherwise only a subset of patterns can be achieved. Forming a point as the target pattern is known as gathering [27], where robots have to meet at a single point in space in finite time, not known beforehand. The problem is generally impossible to solve [25] unless the setting is fully synchronous [3] or robots are endowed with multiplicity detection [10]. Recently, researchers considered tridimensional Euclidean spaces [28], where robots must solve plane formation, that is, land on a common plane (not determined beforehand) in finite time. In the context of robots operating on graphs, typical problems are terminating exploration [16, 19], where robots must explore all nodes of a given graph and then stop moving forever, exclusive perpetual exploration [7, 14], where robots must explore all nodes of a graph forever without ever colliding, exclusive searching [6, 13], where robots must capture an intruder in the graph without colliding, and gathering [8, 14, 22, 23], where robots must meet at a given node in finite time.

Although some of the studied problems overlap (e.g. gathering), the algorithmic techniques that enable solving problems are substantially different. On the one hand, robots operating in continuous spaces may typically use fractional distance moves to another robot, or non-straight moves in order to make the algorithm progress, two options that are not possible in the discrete model. On the other hand, in the asynchronous continuous setting, a robot may be seen by another robot as it is moving, hence at some arbitrary position between its source and destination point within a cycle, something that is impossible to observe in the discrete setting. Indeed, all aforementioned works for robots on graph consider that their moves are atomic, even in the ASYNC setting, which may seem unrealistic to a practitioner.

2 Related Works

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 mechanised approach to protocol correctness was successively used in the context of mobile robots.

In the discrete setting, model-checking proved useful to find bugs (usually in the ASYNC setting) in existing literature [5, 17, 18] and formally check the correctness of published algorithms [5, 15]. Automatic program synthesis [9, 24] can be used to obtain automatically algorithms that are “correct-by-design”. However, those approaches are limited to small instances with few robots. Generalising to an arbitrary number of robots with similar approaches is doubtful as Sangnier et al. [26] proved that safety and reachability problems become undecidable in the parameterised case.

When robots move freely in a continuous bidimensional Euclidean space, to the best of our knowledge the only formal framework available is the Pactole framework.Footnote 1 Pactole enabled the use of higher-order logic to certify impossibility results [1, 4, 11] as well as certifying the correctness of algorithms [3, 12], possibly for an arbitrary number of robots (hence in a scalable manner). Pactole was recently extended by Balabonski et al. [4] to handle discrete spaces as well as continuous spaces, thanks to its modular design. However, to this paper, Pactole only allowed one to express specifications and proofs with the FSYNC and SSYNC models.

3 Our Contribution

In this brief announcement, we explore the possibility of establishing a first bridge between the continuous movements and observation vs. discrete movements and observation in the context of autonomous mobile robots. Our position is that the continuous model reflects well the physicality of robots operating in some environment, while the discrete model reflects well the digital nature of autonomous robots, whose sensors and computing capabilities are inherently finite. For this purpose, we consider that robots make continuous, non atomic moves, but only sense in a discrete manner the position of robots. Our approach is certified using the Coq proof assistant and the Pactole framework.

In more details, our full paper [2] first extends the Pactole framework to handle the ASYNC model, preserving its modularity by keeping the operating space and the robots algorithm both abstract. This permits to retain the same formal framework for both continuous and discrete spaces, and the possibility for mobile robots to be faulty (even possibly malicious a.k.a. Byzantine). Then, as an application of the new framework, we formally prove in the full paper [2] the equivalence between atomic moves in a discrete space (the classical model for robots operating on graphs) and non-atomic moves in a continuous unidimensional space when robot vision sensors are discrete (that is, robots are only able to see another robot on a node when they perform the Look phase, but robots can move anywhere between two adjacent nodes), irrespective of the problem being solved. Our effort consolidates the integration between the model, the problem specification, and its proof that is advocated by the Pactole framework.

Pactole and the formal developments of this work are available at http://pactole.lri.fr.