Implementing choreography extraction

TL;DR

This paper demonstrates a practical implementation of a previously theoretical choreography extraction method, optimizing data structures and techniques to handle its exponential complexity effectively in real-world scenarios.

Contribution

It provides the first practical implementation of a theoretical choreography extraction approach, including optimizations and systematic evaluation.

Findings

Implementation is feasible despite theoretical exponential complexity.

Optimizations significantly improve performance.

Systematic evaluation confirms practical usability.

Abstract

Choreography extraction deals with the generation of a choreography (a global description of communication behaviour) from a set of local process behaviours. In this work, we implement a previously proposed theory for extraction and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introduce some optimizations, and perform a systematic practical evaluation.