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

Research output: Contribution to journalConference article in JournalResearchpeer-review

Abstract

The classes of depth-bounded and name-bounded processes are fragments of the π -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.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
Volume222
Pages (from-to)67-82
Number of pages15
ISSN2075-2180
Publication statusPublished - 2017
EventCombined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics - Berlin, Germany
Duration: 4 Sep 20174 Dec 2017
https://www.concur2017.tu-berlin.de/express_sos.html

Conference

ConferenceCombined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics
CountryGermany
CityBerlin
Period04/09/201704/12/2017
Internet address

Cite this