44 articles – 42 Notices  [english version]

ensl-00149964, version 3

Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms

Damien Pous () 1

Theoretical Computer Science 402, 2-3 (2008) 199-220

Résumé : 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.

  • 1 :  Laboratoire de l'Informatique du Parallélisme (LIP)
  • Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
  • Domaine : Informatique/Calcul parallèle, distribué et partagé
    Informatique/Autre
  • Mots-clés : Weak bisimilarity – Up-to techniques – Abstract machines
  • Référence interne : LIP Research Report n°2007-31
  • Versions disponibles :  v1 (29-05-2007) v2 (19-06-2007) v3 (14-12-2007)
 
  • ensl-00149964, version 3
  • http://hal-ens-lyon.archives-ouvertes.fr/ensl-00149964
  • oai: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 22 Septembre 2011, 10:07:21