Linearity and Bisimulation

Nobuko Yoshida, Kohei Honda and Martin Berger

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the pi-calculus in which we abstract away not only tau-actions but also non-tau 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 pi-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [Honda et al. 99, Honda and Yoshida 02], while still offering compositional verification techniques.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Start Conference Manager
Conference Systems