On Asynchronous Multiparty Session Types for Federated Learning
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915891948552192 |
|---|---|
| author | Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko |
| author_facet | Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko |
| contents | This paper improves the session typing theory to support the modelling and verification of processes that implement federated learning protocols. To this end, we build upon the asynchronous ``bottom-up'' session typing approach by adding support for input/output operations directed towards multiple participants at the same time. We further enhance the flexibility of our typing discipline and allow for safe process replacements by introducing a session subtyping relation tailored for this setting. We formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system. Moreover, we highlight the nuances of our session typing system, which (compared to previous work) reveals interesting interplays and trade-offs between safety, liveness, and the flexibility of the subtyping relation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_21108 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Asynchronous Multiparty Session Types for Federated Learning Prokić, Ivan Prokić, Simona Ghilezan, Silvia Scalas, Alceste Yoshida, Nobuko Logic in Computer Science This paper improves the session typing theory to support the modelling and verification of processes that implement federated learning protocols. To this end, we build upon the asynchronous ``bottom-up'' session typing approach by adding support for input/output operations directed towards multiple participants at the same time. We further enhance the flexibility of our typing discipline and allow for safe process replacements by introducing a session subtyping relation tailored for this setting. We formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system. Moreover, we highlight the nuances of our session typing system, which (compared to previous work) reveals interesting interplays and trade-offs between safety, liveness, and the flexibility of the subtyping relation. |
| title | On Asynchronous Multiparty Session Types for Federated Learning |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.21108 |