On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping

Mario Bravetti 1, 2 Marco Carbone 3 Gianluigi Zavattaro 2, 1
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asyn-chronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.
Document type :
Journal articles
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01921168
Contributor : Mario Bravetti <>
Submitted on : Tuesday, November 13, 2018 - 4:24:27 PM
Last modification on : Friday, April 12, 2019 - 10:18:10 AM
Long-term archiving on : Thursday, February 14, 2019 - 3:41:38 PM

File

tcs.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Mario Bravetti, Marco Carbone, Gianluigi Zavattaro. On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping. Theoretical Computer Science, Elsevier, 2018, 722, pp.19-51. ⟨10.1016/j.tcs.2018.02.010⟩. ⟨hal-01921168⟩

Share

Metrics

Record views

42

Files downloads

76