Using bisimulation proof techniques for the analysis of distributed abstract machines

Analysis of Distributed Abstract Machines Damien Pous ENS Lyon, France. We illustrate the use of recently developed proof techniques for weak bisimulation sing 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. Key words: weak bisimilarity, up-to techniques, process algebras, distributed machines, forwarders.

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Damien Pous
• Keywords: Abstract Machines, Proof Technique, TCS 2008, Theoretical Computer Science, Weak Bisimulation