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

TL;DR

This paper employs session types to characterize and decide boundedness properties in the pi-calculus, making certain undecidable membership problems decidable through type systems.

Contribution

It introduces two session type systems that provide sound characterizations for depth-boundedness and name-boundedness in pi-calculus processes.

Findings

Well-typed processes in the first system are depth-bounded.

Well-typed processes in the second system are name-bounded.

Type systems enable decidability of boundedness properties.

Abstract

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.