Partial Typing for Asynchronous Multiparty Sessions
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913525203468288 |
|---|---|
| author | Barbanera, Franco Dezani-Ciancaglini, Mariangiola de'Liguoro, Ugo |
| author_facet | Barbanera, Franco Dezani-Ciancaglini, Mariangiola de'Liguoro, Ugo |
| contents | Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_00537 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Partial Typing for Asynchronous Multiparty Sessions Barbanera, Franco Dezani-Ciancaglini, Mariangiola de'Liguoro, Ugo Logic in Computer Science F.3.2; F.3.3 Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom. |
| title | Partial Typing for Asynchronous Multiparty Sessions |
| topic | Logic in Computer Science F.3.2; F.3.3 |
| url | https://arxiv.org/abs/2410.00537 |