MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
Sung-Shik JONGMANS, Nobuko YOSHIDA
To appear in
29th European Symposium on Programming (ESOP 2020)

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.

@inproceedings{JY2020,
  author = {Sung-Shik Jongmans and Nobuko Yoshida},
  title = {{Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types}},
  booktitle = {29th European Symposium on Programming},
  pages = {--},
  year = 2020
}
@inproceedings{JY2020,
  author = {Sung-Shik Jongmans and Nobuko Yoshida},
  title = {{Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types}},
  booktitle = {29th European Symposium on Programming},
  pages = {--},
  year = 2020
}