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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Electronic Proceedings in Theoretical Computer Science |
Vol/bind | 222 |
Sider (fra-til) | 67-82 |
Antal sider | 15 |
ISSN | 2075-2180 |
Status | Udgivet - 2017 |
Begivenhed | Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics - Berlin, Tyskland Varighed: 4 sep. 2017 → 4 dec. 2017 https://www.concur2017.tu-berlin.de/express_sos.html |
Konference
Konference | Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics |
---|---|
Land/Område | Tyskland |
By | Berlin |
Periode | 04/09/2017 → 04/12/2017 |
Internetadresse |