On Bisimulation Proofs for the Analysis of Distributed Abstract Machines

Abstract : We illustrate the use of recent, non-trivial proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. The definition of the framework comes from previous works on a specific abstract machine; however, its new presentation, as a labelled transition system, makes it suitable for a wider range of calculi. A first version of the framework 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.
Complete list of metadatas

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00149964
Contributor : Damien Pous <>
Submitted on : Tuesday, June 19, 2007 - 8:29:27 AM
Last modification on : Monday, October 22, 2018 - 12:56:02 PM
Long-term archiving on : Friday, November 25, 2016 - 3:55:18 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : ensl-00149964, version 2

Collections

Citation

Damien Pous. On Bisimulation Proofs for the Analysis of Distributed Abstract Machines. 2007. ⟨ensl-00149964v2⟩

Share

Metrics

Record views

2

Files downloads

8