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 language | English |
---|---|
Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
Volume | 255 |
Pages (from-to) | 67-82 |
Number of pages | 16 |
ISSN | 2075-2180 |
DOIs | |
Publication status | Published - 31 Aug 2017 |
Event | 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017 - Berlin, Germany Duration: 4 Sept 2017 → … |
Conference
Conference | 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017 |
---|---|
Country/Territory | Germany |
City | Berlin |
Period | 04/09/2017 → … |