Skip to content
Snippets Groups Projects
Pierre Courtieu's avatar
Pierre Courtieu authored
Every author should fill his part.
506d4ea9

Content

This repository stores the Coq code of the Pactole (https://pactole.liris.cnrs.fr/) project, 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 a very abstract and parametrized formal model and a lot of case studies. The structure of the repository is describe below.

Support

It was financially supported by the following propject:

  • The Pactole project started as Digiteo Project #2009-38HD.
  • SAPPORO is 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 the to the Coq standard library that are not specific to Pactole
  • Core/: The core the 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 the following case studies. Each case study (say casestudy.v) has a companion file called casestudy_Assuptions.v whose only purpose is to call Print Assumption on the main theorem of the case study. The reason why this command is not included in the case study itself is for allowing fast compilation of the case study.

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 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 robot enjoy strong multiplicity detection.
    • InR/ case studies for the gathering on the enclidean line
      • Impossibility.v: Impossibility of gathering on the line in SSYNC.
      • Algorithm.v: Gathering one the line in SSYNC with strong multiplicity detection, from non bivalent configurations.
    • InR2/ case studies for the gathering on the enclidean plane
      • Peleg.v: Formalization of a protocol for gathering with lights due to Peleg.
      • Viglietta.v: Formalization of a protocol for gathering with lights due to Viglietta.
      • FSyncFlexNoMultAlgorithm.v: Gathering in FSYNC and non rigid moves with weak mutliplicity detection.
      • Algorithm.v: Gathering in R2 in SSYNC with strong multiplicity detection, from non bivalent configurations.
  • Exploration/: Exploration of a ring with stop

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

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.