From infinity to choreographies. Extraction for unbounded systems

DOI10.1007/978-3-031-16767-6_6MaRDI QIDQ6103018zbMATH OpenFDO

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

Publication date 2 June 2023

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2207.08884

zbMATH Keywords

concurrencychoreographymessage passing

Mathematics Subject Classification ID

Distributed systems (68M14) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• The Paths to Choreography Extraction
• Choreographies, logically
• Choreographies, logically
• Choreography synthesis as contract agreement
• Applied Choreographies

Cites work

• A core model for choreographic programming
• Choreographies, logically
• From communicating machines to graphical choreographies
• Introduction to bisimulation and coinduction
• Multiparty Asynchronous Session Types
• Procedural Choreographic Programming
• Synthesising Choreographies from Local Session Types
• The Paths to Choreography Extraction
• πI: A symmetric calculus based on internal mobility

Cited in

(2)

• Security protocols as choreographies
• Choreography synthesis as contract agreement

This page was built for publication: From infinity to choreographies. Extraction for unbounded systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6103018)