From Infinity to Choreographies - Extraction for Unbounded Systems
Bjørn Angel Kjær, Luís Cruz-Filipe, Fabrizio Montesi
[2022].
In proceedings of LOPSTR 2022, pp. 103-120.
Choreographies are formal descriptions of distributed systems, which focus on the way in which participants communicate. While they are useful for analysing protocols, in practice systems are written directly by specifying each participant’s behaviour. This created the need for choreography extraction: the process of obtaining a choreography that faithfully describes the collective behaviour of all participants in a distributed protocol.
Previous works have addressed this problem for systems with a predefined, finite number of participants. In this work, we show how to extract choreographies from system descriptions where the total number of participants is unknown and unbounded, due to the ability of spawning new processes at runtime. This extension is challenging, since previous algorithms relied heavily on the set of possible states of the network during execution being finite.
@inproceedings{DBLP:conf/lopstr/KjaerCM22,
author = {Bj{\o}rn Angel Kj{\ae}r and
Lu{\'{\i}}s Cruz{-}Filipe and
Fabrizio Montesi},
editor = {Alicia Villanueva},
title = {From Infinity to Choreographies - Extraction for Unbounded Systems},
booktitle = {Logic-Based Program Synthesis and Transformation - 32nd International
Symposium, {LOPSTR} 2022, Tbilisi, Georgia, September 21-23, 2022,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13474},
pages = {103--120},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-16767-6\_6},
doi = {10.1007/978-3-031-16767-6\_6},
timestamp = {Tue, 18 Oct 2022 22:17:04 +0200},
biburl = {https://dblp.org/rec/conf/lopstr/KjaerCM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
A PDF is available (possibly a preprint):