A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success. The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
@InProceedings{sabel_et_al:OASIcs.WPTE.2015.31, author = {Sabel, David and Schmidt-Schau{\ss}, Manfred}, title = {{Observing Success in the Pi-Calculus}}, booktitle = {2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)}, pages = {31--46}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-94-1}, ISSN = {2190-6807}, year = {2015}, volume = {46}, editor = {Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.31}, URN = {urn:nbn:de:0030-drops-51808}, doi = {10.4230/OASIcs.WPTE.2015.31}, annote = {Keywords: Concurrency, Process calculi, Pi-calculus, Rewriting, Semantics} }
Feedback for Dagstuhl Publishing