Skip to content
Snippets Groups Projects
Select Git revision
  • public default protected
1 result
Compare History
Pierre Courtieu's avatar
Merge branch 'master' into public
Pierre Courtieu authored
f00c59c3
Name Last commit Last update
CaseStudies
Core
Models
Observations
Spaces
Util
dev
minipactole
.gitignore
.gitlab-ci.yml
CREDIT.md
DEV.md
INSTALL.md
LICENSE
Makefile.local
Pactole_all.v
README.md
Setting.v
_CoqProject
codemeta.json
metrics.txt
README.md

Content

This repository stores the Coq code of the Pactole project (https://pactole.liris.cnrs.fr/), dedicated to formal verification of mobile robotic swarm protocols in many variants of the model initially proposed by Suzuki and Yamashita [1] and sometimes called the "look-compute-move model".

It contains an abstract and parametrized formal model and a few case studies. The structure of the repository is described below.

Support

Pactole was financially supported by the following projects:

  • Pactole started as Digiteo Project #2009-38HD.
  • SAPPORO funded by the French National Research Agency (ANR) under the reference 2019-CE25-0005

[1] I. Suzuki and M. Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM Journal of Computing, 28(4):1347–1363, 1999.

Overall Structure

  • Setting.v: All you need to setup a working framework. A good starting point.
  • Util/: Extension to the Coq standard library that are not specific to Pactole.
  • Core/: The core of the Pactole framework, implementing the Look/Compute/Move cycle.
  • Spaces/: Spaces in which robots evolve.
  • Observations/: Types of robot views of the configuration.
  • Models/: Additional properties of some models.
  • CaseStudies/ : Case studies.

Case Studies

The directory CaseStudies contains the following case studies. Each case study (say casestudy.v) has a companion file called casestudy_Assuptions.v the only purpose of which is to call Print Assumption on the main theorem(s) of the case study. This command is not included in the case study itself to allow for fast compilation.

Here is a list of the current case studies:

  • Convergence/:

    • Algorithm_noB.v: Convergence without Byzantine robots on the Euclidean plane.
    • Impossibility_2G_1B.v: Impossibility of convergence on the real line when 1/3 of robots are Byzantine. Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. SSS 2013.

  • Gathering/: Gathering in R or R² for various models

    • Impossibility.v: Impossibility of gathering in SSYNC.
    • Definitions.v: Common definitions about the gathering problem.
    • WithMultiplicity.v: Common definition on gathering when robots enjoy strong multiplicity detection.
    • InR/ case studies for the gathering on the Euclidean line
      • Impossibility.v: Impossibility of gathering on the line in SSYNC. Courtieu, Rieg, Tixeuil, Urbain. Impossibility of gathering, a certification. IPL 115.
      • Algorithm.v: Gathering one the line in SSYNC with strong multiplicity detection, from non bivalent configurations.
    • InR2/ case studies for the gathering on the Euclidean plane
      • Peleg.v: Gathering in FSYNC and non rigid moves with weak mutliplicity detection, due to Peleg. Cohen, Peleg. Convergence Properties of the Gravitational Algorithm in Asynchronous Robot Systems. SIAM Journal of Computing, 34(6):1516–1528, 2005.
      • Viglietta.v: Formalization of a protocol for gathering with lights due to Viglietta. Viglietta. Rendezvous of two robots with visible bits. ALGOSENSORS 2013.
      • FSyncFlexNoMultAlgorithm.v: Gathering in FSYNC and non rigid moves with no mutliplicity detection. Balabonski, Delga, Rieg, Tixeuil, Urbain. Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm. Theory Comput. Syst. 63(2): 200-218 (2019)
      • Algorithm.v: SSYNC Gathering in R² with strong multiplicity detection, from non-bivalent configurations. Courtieu, Rieg, Tixeuil, Urbain. Certified Universal Gathering in R² for Oblivious Mobile Robots. DISC 2016.

  • Exploration/: Exploration of a ring with stop

    • ImpossibilityKDividesN.v: Impossibility of exploration of a ring when the number of robots divides the number of nodes. Balabonski, Pelle, Rieg, Tixeuil. A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs. ICDCN 2018.
    • ExplorationDefs.v: Common definitions on exploration.
    • Tower.v: Exploration with stop on a ring requires forming a tower, in particular a single robot is no enough.

  • LifeLine/: Life line connection in the 2D Euclidean plane

    • Algorithm.v: Connection maintenance protocol on R2. Balabonski, Courtieu, Pelle, Rieg, Tixeuil, Urbain. Computer Aided Formal Design of Swarm Robotics Algorithms. SSS 2021.

Other Related Ressources

A general description of the Pactole library and its use:

Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. Leibniz Transactions on Embedded Systems, 8(2):02:1– 02:36, 2022.