
arXiv: 2104.07293
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.
FOS: Computer and information sciences, Type Systems, Sized Types, 2012 ACM Subject Classification Theory of computation → Type structures, Computational Complexity (cs.CC), Pi-calculus, 004, Process Calculi, Computer Science - Computational Complexity, Complexity Analysis, Computer Science - Distributed, Parallel, and Cluster Computing, Theory of computation → Process calculi, Software and its engineering → Software verification phrases Type Systems, [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], Distributed, Parallel, and Cluster Computing (cs.DC), Usages, ddc: ddc:004
FOS: Computer and information sciences, Type Systems, Sized Types, 2012 ACM Subject Classification Theory of computation → Type structures, Computational Complexity (cs.CC), Pi-calculus, 004, Process Calculi, Computer Science - Computational Complexity, Complexity Analysis, Computer Science - Distributed, Parallel, and Cluster Computing, Theory of computation → Process calculi, Software and its engineering → Software verification phrases Type Systems, [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], Distributed, Parallel, and Cluster Computing (cs.DC), Usages, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
