论文标题
从无限到编舞：无限系统的提取
From Infinity to Choreographies: Extraction for Unbounded Systems
论文作者
论文摘要
编排是对分布式系统的正式描述，其重点是参与者交流的方式。尽管它们对于分析协议很有用，但在实践系统中，通过指定每个参与者的行为直接编写系统。这创造了对编排提取的需求：获得编排的过程，该编排忠实地描述了分布式协议中所有参与者的集体行为。 先前的工作已经解决了具有预定义的，有限的参与者的系统的问题。在这项工作中，我们展示了如何从系统描述中提取编排，这些参与者总数是未知且无限制的，这是由于在运行时产生新过程的能力。这一扩展是具有挑战性的，因为在执行过程中，以前的算法在很大程度上依赖网络的可能状态。
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.
