diff --git a/README.md b/README.md
index 7b6fd626d2a0fe84631858cd64561ba69507b336..c92dccf715edd047495d7d610643fe9f4ae1bb2f 100644
--- a/README.md
+++ b/README.md
@@ -1,33 +1,35 @@
# 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".
+The Pactole Repository: *A Framework for Formal Verification of Robotic Swarm Protocols*.
-It contains an abstract and parametrized formal model and a few
-case studies. The structure of the repository is described below.
+This repository houses the Coq implementation of the Pactole project (https://pactole.liris.cnrs.fr/), dedicated to formally verifying distributed protocols for mobile robot swarms. It implements multiple variants of the Look-Compute-Move model, originally introduced by Suzuki and Yamashita [1].
+
+Key Features:
+
+- Provides an abstract, parameterized formal model
+- Includes documented case studies (described below)
+- Supports various model variants
+- Enables rigorous protocol verification
+
+[1] I. Suzuki and M. Yamashita. *Distributed Anonymous Mobile Robots: Formation of Geometric Patterns*. SIAM Journal of Computing, 28(4):1347–1363, 1999.
# Support
Pactole was financially supported by the following projects:
-- [Pactole](https://pactole.liris.cnrs.fr/) started as
+- [Pactole](https://pactole.liris.cnrs.fr/) started as the
Digiteo Project #2009-38HD.
- [SAPPORO](https://sapporo.liris.cnrs.fr/) 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.
+- *Util/*: Extension to the Coq standard library 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.
+- *Spaces/*: Spaces where robots evolve.
+- *Observations/*: Types of robot views on the configuration.
- *Models/*: Additional properties of some models.
- *CaseStudies/* : Case studies.
@@ -35,19 +37,19 @@ Pactole was financially supported by the following projects:
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
+called `casestudy_Assuptions.v` whose only purpose 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/](Casestudy/Convergence):
+- [Convergence/](Casestudy/Convergence): convergency results on different protocols.
- [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v):
- Convergence without Byzantine robots on the Euclidean plane.
+ Convergence on the Euclidean plane without Byzantine robots.
- [Impossibility_2G_1B.v](CaseStudies/Convergence/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 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.
@@ -63,7 +65,7 @@ Here is a list of the current case studies:
- [InR/](CaseStudies/Gathering/InR) case studies for the gathering
on the Euclidean line
- [Impossibility.v](CaseStudies/Gathering/InR/Impossibility.v):
- Impossibility of gathering on the line in SSYNC.
+ *Impossibility of gathering on the line in SSYNC.*
Courtieu, Rieg, Tixeuil, Urbain. Impossibility of gathering, a certification. IPL 115.
- [Algorithm.v](CaseStudies/Gathering/InR/Algorithm.v): Gathering
one the line in SSYNC with strong multiplicity detection, from
@@ -71,36 +73,38 @@ Here is a list of the current case studies:
- [InR2/](CaseStudies/Gathering/InR2) case studies for the gathering
on the Euclidean plane
- [Peleg.v](CaseStudies/Gathering/InR2/Peleg.v):
- Gathering in FSYNC and non rigid moves with weak mutliplicity detection, due to Peleg.
+ *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](CaseStudies/Gathering/InR2/Viglietta.v):
Formalization of a protocol for gathering with lights due to Viglietta.
- Viglietta. Rendezvous of two robots with visible bits. ALGOSENSORS 2013.
+ Viglietta. *Rendezvous of two robots with visible bits.* ALGOSENSORS 2013.
- [FSyncFlexNoMultAlgorithm.v](CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v):
- Gathering in FSYNC and non rigid moves with no mutliplicity detection.
+ *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](CaseStudies/Gathering/InR2/Algorithm.v):
- SSYNC Gathering in R² with strong multiplicity detection, from
- non-bivalent configurations.
+ *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/](CaseStudies/Exploration): Exploration of a ring with stop
- [ImpossibilityKDividesN.v](CaseStudies/Exploration/ImpossibilityKDividesN.v):
- Impossibility of exploration of a ring when the number of robots
- divides the number of nodes.
+ *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](CaseStudies/Exploration/ExplorationDefs.v):
Common definitions on exploration.
- [Tower.v](CaseStudies/Exploration/Tower.v):
- Exploration with stop on a ring requires forming a tower, in particular a single robot is no enough.
+ Exploration with stop on a ring requires forming a tower, in particular one single robot is no enough.
- [LifeLine/](CaseStudies/LifeLine): Life line connection in the 2D Euclidean plane
- [Algorithm.v](CaseStudies/LifeLineAlgorithm.v):
- Connection maintenance protocol on R2.
+ *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–
+ Courtieu, Rieg, Tixeuil, and Urbain. *Swarms of Mobile Robots: Towards
+ Versatility with Safety.* Leibniz Transactions on Embedded Systems (LITES), 8(2):02:1–
+ 02:36, 2022. [link](https://doi.org/10.4230/LITES.8.2.2)
+
02:36, 2022.