An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913668444192768 |
|---|---|
| author | Stutz, Felix D'Osualdo, Emanuele |
| author_facet | Stutz, Felix D'Osualdo, Emanuele |
| contents | We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a $π$-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called "tame", for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_16977 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols Stutz, Felix D'Osualdo, Emanuele Programming Languages Formal Languages and Automata Theory We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a $π$-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called "tame", for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection). |
| title | An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols |
| topic | Programming Languages Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2501.16977 |