Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms

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.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2008, 402 (2-3), pp.199-220. 〈10.1016/j.tcs.2008.04.035〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00149964
Contributeur : Damien Pous <>
Soumis le : jeudi 13 décembre 2007 - 21:27:08
Dernière modification le : jeudi 17 mai 2018 - 12:52:03
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 20:03:52

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

126

Téléchargements de fichiers

179