zbMATH — the first resource for mathematics

Linearity and bisimulation. (English) Zbl 1077.68719
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 417-433 (2002).
Summary: We introduce a theory of weak bisimilarity for the \(\pi\)-calculus with linear type structure in which we abstract away not only \(\tau\)-actions but also non-\(\tau\) actions which do not affect well-typed environments. This gives an equivalence far larger than the standard bisimilarity while retaining semantic soundness. The congruency of the bisimilarity relies on a liveness property at linear channels ensured by typing. The theory is consistently extendible to settings which involve nontermination, nondeterminism and state. As an application we develop a behavioural theory of secrecy for the \(\pi\)-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach of Yoshids, Honda and Vasconcelos.
For the entire collection see [Zbl 0989.00051].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: Link