Realisability and Complementability of Multiparty Session Types
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916890964656128 |
|---|---|
| author | Di Giusto, Cinzia Lozes, Etienne Urso, Pascal |
| author_facet | Di Giusto, Cinzia Lozes, Etienne Urso, Pascal |
| contents | Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. As a side contribution, we propose a complementation construction for global types with sender-driven choice, and more generally commutation-deterministic, with a linear blowup in the size of the global type. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_17354 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Realisability and Complementability of Multiparty Session Types Di Giusto, Cinzia Lozes, Etienne Urso, Pascal Formal Languages and Automata Theory Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. As a side contribution, we propose a complementation construction for global types with sender-driven choice, and more generally commutation-deterministic, with a linear blowup in the size of the global type. |
| title | Realisability and Complementability of Multiparty Session Types |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2507.17354 |