License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2021.34
URN: urn:nbn:de:0030-drops-144111
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14411/
Go to the corresponding LIPIcs Volume Portal

Baillot, Patrick ; Ghyselen, Alexis ; Kobayashi, Naoki

Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes

pdf-format:
LIPIcs-CONCUR-2021-34.pdf (0.9 MB)

Abstract

We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by the first two authors but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The sized types allow us to parametrize the complexity by the size of inputs, and the usages allow us to achieve a kind of rely-guarantee reasoning on the timing each process communicates with its environment. We prove that our new type system soundly estimates the parallel complexity, and show through examples that it is often more precise than the previous type system of the first two authors.

BibTeX - Entry

@InProceedings{baillot_et_al:LIPIcs.CONCUR.2021.34,
  author =	{Baillot, Patrick and Ghyselen, Alexis and Kobayashi, Naoki},
  title =	{{Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{34:1--34:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14411},
  URN =		{urn:nbn:de:0030-drops-144111},
  doi =		{10.4230/LIPIcs.CONCUR.2021.34},
  annote =	{Keywords: Type Systems, Pi-calculus, Process Calculi, Complexity Analysis, Usages, Sized Types}
}

Keywords: Type Systems, Pi-calculus, Process Calculi, Complexity Analysis, Usages, Sized Types
Collection: 32nd International Conference on Concurrency Theory (CONCUR 2021)
Issue Date: 2021
Date of publication: 13.08.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI