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

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TidsskriftElectronic Proceedings in Theoretical Computer Science
Vol/bind222
Sider (fra-til)67-82
Antal sider15
ISSN2075-2180
StatusUdgivet - 2017
BegivenhedCombined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics - Berlin, Tyskland
Varighed: 4 sep. 20174 dec. 2017
https://www.concur2017.tu-berlin.de/express_sos.html

Konference

KonferenceCombined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics
LandTyskland
ByBerlin
Periode04/09/201704/12/2017
Internetadresse

Citer dette

@inproceedings{ada81f433a5b414284d42ac10886dc77,
title = "Using Session Types for Reasoning About Boundedness in the Pi-Calculus",
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.",
author = "Hans Huttel",
year = "2017",
language = "English",
volume = "222",
pages = "67--82",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

Using Session Types for Reasoning About Boundedness in the Pi-Calculus. / Huttel, Hans.

I: Electronic Proceedings in Theoretical Computer Science, Bind 222, 2017, s. 67-82.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

TY - GEN

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

AU - Huttel, Hans

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

M3 - Conference article in Journal

VL - 222

SP - 67

EP - 82

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -