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 : Thursday, September 29, 2022 - 2:58:07 PM
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