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, May 29, 2007 - 10:25:15 AM
Last modification on : Monday, October 22, 2018 - 12:56:02 PM
Long-term archiving on : Friday, September 21, 2012 - 3:56:11 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : ensl-00149964, version 1

Collections

Citation

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

Share

Metrics

Record views

5

Files downloads

6