Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms

Damien Pous 1, 2
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We illustrate the use of recently developped proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. We first define this framework, and then focus on the algorithm which is used to route messages asynchronously to their destination. A first version of this algorithm can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00149964
Contributor : Damien Pous <>
Submitted on : Thursday, December 13, 2007 - 9:27:08 PM
Last modification on : Wednesday, November 20, 2019 - 7:36:29 AM
Long-term archiving on : Friday, November 25, 2016 - 8:03:52 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Damien Pous. Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms. Theoretical Computer Science, Elsevier, 2008, 402 (2-3), pp.199-220. ⟨10.1016/j.tcs.2008.04.035⟩. ⟨ensl-00149964v3⟩

Share

Metrics

Record views

149

Files downloads

199