RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model

Scientific Annals of Computer Science

article

A. Fontaine¹  A. Zemmari² 

[1] Universit´e de Guyane, UMR Espace-Dev;Universit´e de Bordeaux, LaBRI UMR CNRS

关键词: Distributed Algorithm;    Randomised Algorithm;    Analyses;    Formal Proof;    Proof Assist;   

DOI  :  10.7561/SACS.2016.2.157

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

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. In this paper, we formally model in Coq a class of randomised distributed algorithms. We develop some tools to help proving impossibility results about classical problems and analysing this class of algorithms. As case studies, we examine the handshake and maximal matching problems. We show how to use our tools to formally prove properties about algorithms solving those problems.

【 授权许可】

CC BY-ND