On Compositional Reasoning in the Spi-Calculus

Michele Boreale, Daniele Gorla

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


Observational equivalences can be used to reason about the correctness of protocols described in the spi-calculus, but they do not enjoy the same pleasant properties they enjoy in CCS or in pi-calculus. The present paper aims at enriching the set of tools for reasoning on spi-processes by providing a few equational laws for a sensible notion of spi-calculus bisimilarity. We discuss the difficulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Maintainer fossacs02@brics.dk.
Start Conference Manager
Conference Systems