Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
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_ | 1866909622829318144 |
|---|---|
| author | Acclavio, Matteo Manara, Giulia Montesi, Fabrizio |
| author_facet | Acclavio, Matteo Manara, Giulia Montesi, Fabrizio |
| contents | We introduce a novel approach to studying properties of processes in the π-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free π-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the π-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite π-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the paradigm of computation-as-derivation extends the reach of logical methods for the study of concurrency, by bridging important gaps between logic, the expressiveness of the π-calculus, and the expressiveness of choreographic languages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_08928 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version) Acclavio, Matteo Manara, Giulia Montesi, Fabrizio Logic in Computer Science We introduce a novel approach to studying properties of processes in the π-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free π-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the π-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite π-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the paradigm of computation-as-derivation extends the reach of logical methods for the study of concurrency, by bridging important gaps between logic, the expressiveness of the π-calculus, and the expressiveness of choreographic languages. |
| title | Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.08928 |