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/: Convergence of robots in the 2D Euclidean plane
  • Algorithm_noB.v
  • Impossibility_2G_1B.v
• Gathering/: Gathering in R or R² for various models
  • Impossibility.v:
  • Definitions.v: Common definitions about the gathering problem
  • WithMultiplicity.v
  • InR/ case studies for the gathering on the enclidean line
    • Impossibility.v
    • Algorithm.v
  • InR2/ case studies for the gathering on the enclidean plane
    • Peleg.v
    • Viglietta.v
    • FSyncFlexNoMultAlgorithm.v
    • Algorithm.v
    • Algorithm_Assumptions.v
• Exploration/: Exploration of a ring with stop
  • ImpossibilityKDividesN.v
  • ExplorationDefs.v
  • Tower.v
• LifeLine/: Life line connection in the 2D Euclidean plane
  • Algorithm.v

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.