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

TL;DR

This paper introduces a refined type system for Pi-calculus processes that accurately analyzes parallel complexity by incorporating sized types and usages, providing upper bounds on execution time in concurrent programs.

Contribution

It develops a novel type system combining sized types and usages with time annotations, improving precision over previous methods for analyzing parallel complexity.

Findings

Type derivations give upper bounds on parallel complexity.

The system handles non-linear channels more precisely.

Provides a formal proof of complexity bounds.

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 Baillot and Ghyselen 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 new variant of usages we define accounts for the various ways a channel is employed and relies on time annotations to track under which conditions processes can synchronize. We prove that a type derivation for a process provides an upper bound on its parallel complexity.