Pactole

Networks of Static and/or Mobile sensors (that is, robots) recently received significant attention from mainstream news media. Indeed, the era of expensive robots that are dedicated to a single task is past. Nowadays the tendency is to deploy networked mobile sensors that are able to execute collectively various complex tasks. One possible application of these networks could be for example to optimise the coverage of interest zones under natural or human disaster, and help in search and rescue tasks. In rescue situations, rescue people have to work rapidly to be able to save victims, but they are often limited by insufficient man-power, by their inability to reach confined spaces and by the lack of information about the location and condition of victims. In this context, networked mobile sensors can be a valuable asset to the human search and rescue teams.

The characteristic feature of mobile sensor networks is the extreme dynamism of their structure, content, and load. In these systems, nodes may join, leave and change their physical position at will with a strong impact on the system topology. Moreover, the energy fluctuation of their batteries also induces high system dynamism (that is, the system size and topology are likely to change during any computation that might take place).

Our project aims to propose a formal provable framework based on recent advances in automated proving and related areas in order to prove the correctness of localised distributed protocols in dynamic mobile sensor networks. So far, the correctness of these systems was partially explored either via restrictive simulations and experiments or via analytical tools built on top of restrictive assumptions (for example, the nodes characteristics and status do not change during the whole system execution, etc.). These assumptions may be completely unrealistic in actual networks and thus disastrous in practice. The correctness proofs of aforementioned systems should be based on a well-founded theoretical model, able to encapsulate the dynamic behaviour of these systems that must withstand frequent changes.

The Pactole project started as Digiteo Project #2009-38HD.

Contact: Xavier Urbain.

Framework

Discrete Graphs and Continuous Graphs with Discrete Observation for Coq 8.7
Discrete Graphs and Continuous Graphs with Discrete Observation for Coq 8.6
Explorations in graphs for Coq 8.6.
New version for Coq 8.6 including instances for certification of gathering algorithms in 2D (SSYNC and FSYNC).
Version for Coq 8.5rc1 including instance for certification of a gathering algorithm in 2D.
Version with spectra and instance for certification of a gathering algorithm.
Coq formal framework instance for impossibility of gathering.
Coq formal framework instance for impossibility of Byzantine convergence.

Publications

Potop-Butucaru, Sznajder, Tixeuil, Urbain. Formal Methods for Mobile Robots, chapter in Distributed Computing by Mobile Entities, Current Research in Moving and Computing Flocchini, Prencipe, Santoro. 2019  Link
Balabonski, Courtieu, Pelle, Rieg, Tixeuil, Urbain. Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. NETYS 2019.  
Balabonski, Courtieu, Pelle, Rieg, Tixeuil, Urbain. Manuel de savoir-prouver à l’usage des roboteux et des distributeux. AlgoTel 2019.  
Balabonski, Delga, Rieg, Tixeuil, Urbain. Synchronous Gathering without Multiplicity Detection: A Certified Algorithm Theory of Computing Systems, 63 (2) : 200--218. 2019.  Link
Balabonski, Courtieu, Pelle, Rieg, Tixeuil, Urbain. Brief Announcement: Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. SSS 2018. [Extended in [netys19]]  
Balabonski, Pelle, Rieg, Tixeuil. A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs. ICDCN 2018.  Link
Balabonski, Courtieu, Rieg, Tixeuil, Urbain. Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems.   Link
Balabonski, Delga, Rieg, Tixeuil, Urbain. Synchronous Gathering without Multiplicity Detection: A Certified Algorithm. SSS 2016. [Extended in [ToCS]]  
Courtieu, Rieg, Tixeuil, Urbain. Certified Universal Gathering in ℝ2 for Oblivious Mobile Robots. DISC 2016.  
Courtieu, Rieg, Tixeuil, Urbain. Brief Announcement: Certified Universal Gathering in ℝ2 for Oblivious Mobile Robots. PODC 2016. [Extended in [disc16]]  
Bérard, Courtieu, Millet, Potop-Butucaru, Rieg, Sznajder, Tixeuil, Urbain. Invited Paper: Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society (IJIS) 7(3), 2015.  Link
Courtieu, Rieg, Tixeuil, Urbain. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. Research Report UPMC, 2015.  Link
Courtieu, Rieg, Tixeuil, Urbain. Impossibility of Gathering, a Certification. IPL 115(3), 2015.  
Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. SSS 2013.  
Auger, Bouzid, Courtieu, Tixeuil, Urbain. Brief Annoucement: Certified Impossibility Results for Byzantine-Tolerant Mobile. DISC 2013  
Courtieu, Rieg, Tixeuil, Urbain. Impossibility of Gathering, a Certification. Research Report Cédric-14-3016, 2014.  Link
Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. Research Report LRI 1560, 2013.  
Bouzid. Modèles et algorithmes pour les systèmes émergents. PhD Thesis  
Bouzid, Das, Tixeuil. Brief Annoucement: Wait-Free Gathering of Mobile Robots. DISC 2012.  
Izumi, Bouzid, Tixeuil, Wada. The BG-Simulation for Byzantine Mobile Robots. DISC 2011.  
Bouzid, Lamani. Robot Networks with Homonyms: The Case of Pattern Formation. SSS 2011.  
Bouzid, Dolev, Potop-Butucaru, Tixeuil. RoboCast: Asynchronous Communication in Robot Networks. OPODIS 2010