diff --git a/CREDIT.md b/CREDIT.md
index 6edbe5b69a9304b123c3e175e49b6ce95d27ff42..dfd9aa608b6e2deaffa29524ca38057fcb4aa21e 100644
--- a/CREDIT.md
+++ b/CREDIT.md
@@ -2,10 +2,10 @@ The following people have contrinuted to the Pactole library. See also
the LICENSE file.
Cédric Auger (2013)
-Thibaut Balabonski(2016-2017)
-Sebastien Bouchard(2021-)
+Thibaut Balabonski (2016-2017)
+Sebastien Bouchard (2021-)
Pierre Courtieu (2013-)
Robin Pelle (2016-2020)
-Lionel Rieg (2019-)
+Lionel Rieg (2014-)
Xavier Urbain (2013-)
diff --git a/README.md b/README.md
index 0b2dc291d766b0c890439a36830a2cb4b55dca36..9f9cb4163c2c871fbc2d098b43975542c673ec9e 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ case studies. The structure of the repository is describe below.
# Support
-It was financially supported by the following propject:
+It was financially supported by the following projects:
- [The Pactole project](https://pactole.liris.cnrs.fr/) started as
Digiteo Project #2009-38HD.
@@ -36,16 +36,15 @@ It was financially supported by the following propject:
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.
+Assumption` on the main theorem(s) 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/](Casestudy/Convergence):
- [Algorithm_noB.v](CaseStudies/Convergence/Algorithm_noB.v):
Convergence without byzantine robots on the euclidean plane.
-
- [Impossibility_2G_1B.v](CaseStudies/Convergence/Impossibility_2G_1B.v):
Impossibility of convergence on the line when 1/3 of robots are
byzantine. Auger, Bouzid, Courtieu, Tixeuil, Urbain. Certified
@@ -56,40 +55,47 @@ Here is a list of the current case studies:
various models
- [Impossibility.v](CaseStudies/Gathering/Impossibility.v):
Impossibility of gathering in SSYNC.
- - [Definitions.v](CaseStudies/Gathering/Definitions.v): Common
- definitions about the gathering problem.
+ - [Definitions.v](CaseStudies/Gathering/Definitions.v):
+ Common definitions about the gathering problem.
- [WithMultiplicity.v](CaseStudies/Gathering/WithMultiplicity.v):
- Common definition on gathering when robot enjoy strong
+ Common definition on gathering when robots enjoy strong
multiplicity detection.
- [InR/](CaseStudies/Gathering/InR) case studies for the gathering
- on the enclidean line
+ on the Euclidean line
- [Impossibility.v](CaseStudies/Gathering/InR/Impossibility.v):
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
non bivalent configurations.
- [InR2/](CaseStudies/Gathering/InR2) case studies for the gathering
- on the enclidean plane
+ on the Euclidean plane
- [Peleg.v](CaseStudies/Gathering/InR2/Peleg.v):
- Formalization of a protocol for gathering with lights 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.
- [FSyncFlexNoMultAlgorithm.v](CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v):
- Gathering in FSYNC and non rigid moves with weak 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):
Gathering in R2 in SSYNC 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.
+ 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.
- [LifeLine/](CaseStudies/LifeLine): Life line connection in the 2D Euclidean plane
- [Algorithm.v](CaseStudies/LifeLineAlgorithm.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
diff --git a/codemeta.json b/codemeta.json
index ebb365b59cec186adf172fc63bd0612d1830ab19..ecffdeeb58f376d52295c3c9bdd50460e0af6dfd 100644
--- a/codemeta.json
+++ b/codemeta.json
@@ -53,6 +53,16 @@
"name": "Université???"
}
}
+ {
+ "@type": "Person",
+ "givenName": "Lionel",
+ "familyName": "Rieg",
+ "email": "lionel.rieg@univ-grenoble-alpes.fr",
+ "affiliation": {
+ "@type": "Organization",
+ "name": "Verimag, Grenoble INP -- UGA"
+ }
+ }
],
"contributor": "TODO: Les stagiaires comme ci-dessus?",
"citation": "TODO un papier décrivant Pactole"