Using Session Types for Reasoning About Boundedness in the Pi-Calculus

Hans Hüttel
(Department of Computer Science, Aalborg University, Denmark)

The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction sequence for P contains successor processes with at most k active nested restrictions. P is name-bounded at level k if every reduction sequence for P contains successor processes with at most k active bound names. Membership of these classes of processes is undecidable. In this paper we use binary session types to decise two type systems that give a sound characterization of the properties: If a process is well-typed in our first system, it is depth-bounded. If a process is well-typed in our second, more restrictive type system, it will also be name-bounded.

In Kirstin Peters and Simone Tini: Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS 2017), Berlin, Germany, 4th September 2017, Electronic Proceedings in Theoretical Computer Science 255, pp. 67–82.
Published: 31st August 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.255.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org