From Infinity to Choreographies: Extraction for Unbounded Systems

TL;DR

This paper introduces a method for extracting choreographies from distributed systems with an unbounded number of participants, addressing the challenge of infinite state spaces caused by runtime process spawning.

Contribution

It extends choreography extraction techniques to systems with dynamic, unbounded participants, overcoming limitations of previous finite-state algorithms.

Findings

Successfully extracts choreographies from systems with unbounded participants.

Handles infinite state spaces caused by process spawning.

Provides a foundation for analyzing dynamic distributed protocols.

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.