Article ID Journal Published Year Pages File Type
438324 Theoretical Computer Science 2008 22 Pages PDF
Abstract

We illustrate the use of recently developed 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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics