Sciweavers

Share
TCS
2008

Using bisimulation proof techniques for the analysis of distributed abstract machines

8 years 5 months ago
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.
Damien Pous
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Damien Pous
Comments (0)
books