Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
438324 | Theoretical Computer Science | 2008 | 22 Pages |
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