From infinity to choreographies: Extraction for unbounded Systems

Bjørn Angel Kjær, Luís Cruz-Filipe*, Fabrizio Montesi

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

3 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation : 32nd International Symposium, LOPSTR 2022, Proceedings
EditorsAlicia Villanueva
PublisherSpringer Science+Business Media
Publication date11. Sept 2022
ISBN (Print)9783031167669
Publication statusPublished - 11. Sept 2022
Event32nd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2022 - Tbilisi, Georgia
Duration: 21. Sept 202223. Sept 2022


Conference32nd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2022
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13474 LNCS


  • Choreography
  • Concurrency
  • Extraction
  • Message passing


Dive into the research topics of 'From infinity to choreographies: Extraction for unbounded Systems'. Together they form a unique fingerprint.

Cite this