Published in Volume XXVI, Issue 2, 2016, pages 157–186, doi: 10.7561/SACS.2016.2.157

Authors: A. Fontaine, A. Zemmari

Abstract

Distributed algorithms have received considerable attention and were studied intensively in the past few decades. Under some hypotheses on the distributed system, there is no deterministic solution to certain classical problems. Randomised solutions are then needed to solve those problems. Probabilistic algorithms are generally simple to formulate. However, their analysis can become very complex, especially in the field of distributed computing.

Full Text (PDF)

References

[1] P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568–589, 2009. doi: 10.1016/j.scico.2007.09.002.

[2] C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In Stabilization, Safety, and Security of Distributed Systems – 15th International Symposium, SSS 2013, Osaka, Japan, November 13-16, 2013, pages 178–190, 2013. doi:10.1007/978-3-319-03089-0_13.

[3] P. Castéran and V. Filou. Tasks, types and tactics for local computation systems. Studia Informatica Universalis, Hermann, 9(1):39–86, 2011.

[4] C.-T. Chou. Mechanical verification of distributed algorithms in higher- order logic. The Computer Journal, 38:158–176, 1995. doi:10.1007/3-540-58450-1_41.

[5] P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Certified universal gathering in R² for oblivious mobile robots. In Distributed Computing – 30th International Symposium, DISC 2016, Paris, France, September 27- 29, 2016, pages 187–200, 2016. doi:10.1007/978-3-662-53426-7_14.

[6] Deploy European Community Project, www.event-b.org. Event-B and the Rodin Platform.

[7] C. Derman. Finite state Markovian decision processes. Mathematics in science and engineering. Academic Press, Orlando, FL, USA, 1970.

[8] A. Fontaine and A. Zemmari. Rda: A Coq Library on Randomised Distributed Algorithms. www.allyxfontaine.com/rda.

[9] G. Gonthier and A. Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010. doi:10.6092/issn.1972-5787/1979.

[10] J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanized in HOL. Electronic Notes in Theoretical Computer Science, 112:95–111, 2005. doi:10.1016/j.entcs.2004.01.021.

[11] Monads in Haskell. http://www.haskell.org/haskellwiki/monad.

[12] D. E. Knuth. The art of computer programming, volume 2: seminumerical algorithms. Addison-Wesley, Boston, MA, USA, 1981.

[13] P. Küfner, U. Nestmann, and C. Rickmann. Formal verification of distributed algorithms – from pseudo code to checked proofs. In Theoretical Computer Science – 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, Amsterdam, The Netherlands, September 26-28, 2012, pages 209–224, 2012. doi:10.1007/978-3-642-33475-7_15.

[14] M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In Computer Performance Evaluation / TOOLS, pages 200–204, 2002. doi:10.1007/3-540-46029-2_13.

[15] M. Z. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In Computer Aided Verification (CAV’01), pages 194–206, 2001. doi:10.1007/3-540-44585-4_17.

[16] Y. Métivier, N. Saheb, and A. Zemmari. Analysis of a randomized rendez-vous algorithm. Information and Computation, 184(1):109–128, 2003. doi:10.1016/S0890-5401(03)00054-3.

[17] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9.

[18] A. Pogosyants and R. Segala. Formal verification of timed properties for randomized distributed algorithms. In Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing (PODC’95), pages 174–183, 1995. doi:10.1145/224964.224984.

[19] DAMPAS Project. Visidia. http://visidia.labri.fr.

[20] Coq Development Team. The Coq Proof Assistant Reference Manual. coq.inria.fr.

Bibtex

@article{sacscuza:fontaine2016racltrardaitmpm,
  title={RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model},
  author={A. Fontaine and A. Zemmari},
  journal={Scientific Annals of Computer Science},
  volume={26},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2016},
  pages={157–186},
  doi={10.7561/SACS.2016.2.157},
  publisher={``A.I. Cuza'' University Press}
}