Composition of choreography automata
Formal Languages and Automata Theory
2021-07-15 v1 Logic in Computer Science
Abstract
Choreography automata are an automata-based model of choreographies, that we show to be a compositional one. Choreography automata represent global views of choreographies (and rely on the well-known model of communicating finite-state machines to model local behaviours). The projections of well-formed global views are live as well as lock- and deadlock-free. In the class of choreography automata we define an internal operation of {\em composition}, which connects two global views via roles acting as interfaces. We show that under mild conditions the composition of well-formed choreography automata is well-formed. The composition operation enables for a flexible modular mechanism at the design level.
Cite
@article{arxiv.2107.06727,
title = {Composition of choreography automata},
author = {Franco Barbanera and Ivan Lanese and Emilio Tuosto},
journal= {arXiv preprint arXiv:2107.06727},
year = {2021}
}