Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types

Sung-Shik Jongmans*, Nobuko Yoshida

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

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
Title of host publicationProgramming Languages and Systems
Subtitle of host publication29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings
EditorsPeter Müller
Place of PublicationCham
PublisherSpringer Open
Chapter10
Pages251-279
Number of pages29
ISBN (Electronic)978-3-030-44914-8
ISBN (Print)978-3-030-44913-1
DOIs
Publication statusPublished - 2020
Event(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020
Conference number: 26
https://etaps.org/2020/tacas
https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Publication series

SeriesLecture Notes in Computer Science (LNCS) series
Volume12075
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues (LNCS subseries)
Volume12075

Conference

Conference(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated titleTACAS 2020
CountryIreland
CityDublin
Period25/04/2030/04/20
Internet address

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

Cite this