METIVIER_2002-ProvingDistributed
Yves Métivier, Mohamed Mosbah, Affif Sellami. Proving Distributed Algorithms by Graph Relabelling Systems: Examples of Trees in Networks with Processor Identities. In AGT2002, ETAPS, Grenoble, France, April 2002.
Download
Download paper:
Gziped Postscript
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Abstract
In this paper, we argue that graph relabelling systems are well suited for the representation of distributed algorithms as well as for correctness and termination proofs. Various algorithms for computing distributed spanning trees serve as examples. The proofs use techniques that benefit from the high level encoding of distributed algorithms in form of rewriting systems. The result is a formal approach to describe and study distributed algorithms in a unified and simple way.
Contact
Yves Métivier
Mohamed Mosbah
Afif Sellami
BibTex Reference
@InProceedings{METIVIER_2002-ProvingDistributed,
Author = {Métivier, Yves and Mosbah, Mohamed and Sellami, Affif},
Title = {Proving Distributed Algorithms by Graph Relabelling Systems: Examples of Trees in Networks with Processor Identities},
BookTitle = {AGT2002, ETAPS},
Address = {Grenoble, France},
Month = {April},
Year = {2002}
}
EndNote Reference [help]
Get EndNote Reference (.ref)