Undecidability of asynchronous session subtyping

Mario Bravetti 1 Marco Carbone 2 Gianluigi Zavattaro 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 used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability of subtyping for session types in asynchronously communicating systems. We first devise a core undecidable subtyping relation that is obtained by imposing limitations on the structure of types. Then, as a consequence of this initial undecidability result, we show that (differently from what stated or conjectured in the literature) the three notions of asynchronous subtyping defined so far for session types are all undecidable. Namely, we consider the asynchronous session subtyping by Mostrous and Yoshida for binary sessions, the relation by Chen et al. for binary sessions under the assumption that every message emitted is eventually consumed, and the one by Mostrous et al. for multiparty session types. Finally, by showing that two fragments of the core subtyping relation are decidable, we evince that further restrictions on the structure of types make our core subtyping relation decidable.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2017, 256, pp.300 - 320. 〈10.1016/j.ic.2017.07.010〉
Liste complète des métadonnées

Contributeur : Mario Bravetti <>
Soumis le : samedi 18 novembre 2017 - 17:13:47
Dernière modification le : jeudi 11 janvier 2018 - 15:49:57




Mario Bravetti, Marco Carbone, Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Information and Computation, Elsevier, 2017, 256, pp.300 - 320. 〈10.1016/j.ic.2017.07.010〉. 〈hal-01637935〉



Consultations de la notice