Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types

Sung-Shik Jongmans, Nobuko Yoshida

Research output: Book/ReportTechnical reportAcademic

70 Downloads (Pure)


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.

Original languageEnglish
PublisherOpen Universiteit Nederland
Number of pages189
Publication statusPublished - 2020

Publication series

SeriesTechnical Report - Computer Science & Information Science (TR-OU-INF)


Dive into the research topics of 'Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types'. Together they form a unique fingerprint.

Cite this