Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms - Archive ouverte HAL Access content directly
Journal Articles Theoretical Computer Science Year : 2008

Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
main.pdf (336.32 Ko) Télécharger le fichier
Vignette du fichier
LIP-RR2007-31.pdf (336.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Loading...

Dates and versions

ensl-00149964 , version 1 (29-05-2007)
ensl-00149964 , version 2 (19-06-2007)
ensl-00149964 , version 3 (13-12-2007)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More