RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model
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. Probabili...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Alexandru Ioan Cuza University of Iasi
2016-12-01
|
| Series: | Scientific Annals of Computer Science |
| Online Access: | http://www.info.uaic.ro/bin/download/Annals/XXVI2/XXVI2_1.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850263320968298496 |
|---|---|
| author | A. Fontaine A. Zemmari |
| author_facet | A. Fontaine A. Zemmari |
| author_sort | A. Fontaine |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-e6e97b1609be4979b4f9ac1279589149 |
| institution | OA Journals |
| issn | 1843-8121 2248-2695 |
| language | English |
| publishDate | 2016-12-01 |
| publisher | Alexandru Ioan Cuza University of Iasi |
| record_format | Article |
| series | Scientific Annals of Computer Science |
| spelling | doaj-art-e6e97b1609be4979b4f9ac12795891492025-08-20T01:54:58ZengAlexandru Ioan Cuza University of IasiScientific Annals of Computer Science1843-81212248-26952016-12-01XXVI215718610.7561/SACS.2016.2.157RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing ModelA. FontaineA. ZemmariDistributed 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.http://www.info.uaic.ro/bin/download/Annals/XXVI2/XXVI2_1.pdf |
| spellingShingle | A. Fontaine A. Zemmari RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model Scientific Annals of Computer Science |
| title | RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model |
| title_full | RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model |
| title_fullStr | RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model |
| title_full_unstemmed | RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model |
| title_short | RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model |
| title_sort | rda a coq library to reason about randomised distributed algorithms in the message passing model |
| url | http://www.info.uaic.ro/bin/download/Annals/XXVI2/XXVI2_1.pdf |
| work_keys_str_mv | AT afontaine rdaacoqlibrarytoreasonaboutrandomiseddistributedalgorithmsinthemessagepassingmodel AT azemmari rdaacoqlibrarytoreasonaboutrandomiseddistributedalgorithmsinthemessagepassingmodel |