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

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 produced by the author(s)




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⟩



Record views


Files downloads