Deciding Subtyping for Asynchronous Multiparty Sessions

Elaine Li, Felix Stutz, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as implementation model. We address two problems: when can a local implementation safely substitute another, and when does an arbitrary CSM implement a global type? We define safety with respect to a given global type, in terms of subprotocol fidelity and deadlock freedom. Our implementation model subsumes existing work which considers local types with restricted choice. We exploit the connection between MST subtyping and refinement to formulate concise conditions that are directly checkable on the candidate implementations, and use them to show that both problems are decidable in polynomial time.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings
EditorsStephanie Weirich
PublisherSpringer Science and Business Media Deutschland GmbH
Pages176-205
Number of pages30
ISBN (Print)9783031572616
DOIs
StatePublished - 2024
Event33rd European Symposium on Programming, ESOP 2024, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 - Luxembourg City, Luxembourg
Duration: Apr 6 2024Apr 11 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14576 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd European Symposium on Programming, ESOP 2024, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period4/6/244/11/24

Keywords

  • Communicating state machines
  • Multiparty session types
  • Protocol verification
  • Refinement
  • Subtyping

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Deciding Subtyping for Asynchronous Multiparty Sessions'. Together they form a unique fingerprint.

Cite this