HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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 metadata

Cited literature [34 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00149964
Contributor : Damien Pous Connect in order to contact the contributor
Submitted on : Thursday, December 13, 2007 - 9:27:08 PM
Last modification on : Saturday, September 11, 2021 - 3:16:55 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

93

Files downloads

238