Complete Multiparty Session Type Projection with Automata
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913285381554176 |
|---|---|
| author | Li, Elaine Stutz, Felix Wies, Thomas Zufferey, Damien |
| author_facet | Li, Elaine Stutz, Felix Wies, Thomas Zufferey, Damien |
| contents | Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is in PSPACE. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_17079 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Complete Multiparty Session Type Projection with Automata Li, Elaine Stutz, Felix Wies, Thomas Zufferey, Damien Formal Languages and Automata Theory Distributed, Parallel, and Cluster Computing Programming Languages Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is in PSPACE. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance. |
| title | Complete Multiparty Session Type Projection with Automata |
| topic | Formal Languages and Automata Theory Distributed, Parallel, and Cluster Computing Programming Languages |
| url | https://arxiv.org/abs/2305.17079 |