Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [20, 23], while still offering compositional verification techniques.

• Type: Journal
• Year: 2007
• Where: JLP
• Authors: Nobuko Yoshida, Kohei Honda, Martin Berger
• Keywords: JLP 2007, Linear Type Structure, Non-τ Actions, Well-typed Observers