Observing Success in the Pi-Calculus

A contextual semantics – defined in terms of successful termination and may- and shouldconvergence – 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. 1998 ACM Subject Classification F.3.2 Semantics of Programming Languages, D.3.1 Formal Definitions and Theory F.4.2 Grammars and Other Rewriting Systems, Keywords and phrases concurrency, process calculi, pi-calculus, rewriting, semantics Dig...

• Type: Journal
• Year: 2015
• Where: RTA
• Authors: David Sabel, Manfred Schmidt-Schauß
• Keywords: RTA 2015, Theoretical Computer Science