2020
Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
Publication
Publication
A key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-030-44914-8_10 | |
| Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence | |
| European Symposium on Programming | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Jongmans, S., & Yoshida, N. (2020). Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types. In European Symposium on Programming, ESOP 2020 (pp. 251–279). doi:10.1007/978-3-030-44914-8_10 |
|
