Using Bisimulation Proof Techniques for the Analysis of Distributed Algorithms

Damien Pous (1, 2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages

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.

Mots clés: Abstract machines; Weak bisimilarity; Up-to techniques

Domaines: Calcul parallèle, distribué et partagé [cs.DC]; Autre [cs.OH]

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⟩