Contextual equivalence for the pi-calculus that can stop
- The pi-calculus is a well-analyzed model for mobile processes and mobile computations. While a lot of other process and lambda calculi that are core languages of higher-order concurrent and/or functional programming languages use a contextual semantics observing the termination behavior of programs in all program contexts, traditional program equivalences in the pi-calculus are bisimulations and barbed testing equivalences, which observe the communication capabilities of processes under reduction and in contexts. There is a distance between these two approaches to program equivalence which makes it hard to compare the pi-calculus with other languages. In this paper we contribute to bridging this gap by investigating a contextual semantics of the synchronous pi-calculus with replication and without sums. To transfer contextual equivalence to the pi-calculus we add a process Stop as constant which indicates success and is used as the base to define and analyze the contextual equivalence which observes may- and should-convergence of processes. We show as a main result that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus. This implies that results on contextual equivalence can be directly transferred to the (Stop-free) pi-calculus with barbed testing equivalence. We analyze the contextual ordering, prove some nontrivial process equivalences, and provide proof tools for showing contextual equivalences. Among them are a context lemma, and new notions of sound applicative similarities for may- and should-convergence.
Author: | David SabelORCiDGND, Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-336082 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/ |
Parent Title (German): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 53 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (53) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
Place of publication: | Frankfurt [am Main] |
Document Type: | Working Paper |
Language: | English |
Date of Publication (online): | 2014/03/10 |
Date of first Publication: | 2014/03/10 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2014/06/24 |
Page Number: | 22 |
First Page: | 1 |
Last Page: | 22 |
HeBIS-PPN: | 344371301 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Licence (German): | Deutsches Urheberrecht |