From Infinity to Choreographies: Extraction for Unbounded Systems

Bjørn Angel Kjær, Luís Cruz-Filipe, Fabrizio Montesi [2022].
In CoRR abs/2207.08884.

Abstract

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.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2207-08884,
  author       = {Bj{\o}rn Angel Kj{\ae}r and
                  Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi},
  title        = {From Infinity to Choreographies: Extraction for Unbounded Systems},
  journal      = {CoRR},
  volume       = {abs/2207.08884},
  year         = {2022},
  url          = {https://doi.org/10.48550/arXiv.2207.08884},
  doi          = {10.48550/ARXIV.2207.08884},
  eprinttype    = {arXiv},
  eprint       = {2207.08884},
  timestamp    = {Mon, 25 Jul 2022 14:56:58 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2207-08884.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Peer-reviewed version

Click to show in publication list