Automata models are well-established in many areas of computer science and are supported by a wealth of theoretical results including a wide range of algorithms and techniques to specify and analyse systems. We introduce choreography automata for the choreographic modelling of communicating systems. The projection of a choreography automaton yields a system of communicating finite-state machines. We consider both the standard asynchronous semantics of communicating systems and a synchronous variant of it. For both, the projections of well-formed automata are proved to be live as well as lock- and deadlock-free.
CITATION STYLE
Barbanera, F., Lanese, I., & Tuosto, E. (2020). Choreography automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12134 LNCS, pp. 86–106). Springer. https://doi.org/10.1007/978-3-030-50029-0_6
Mendeley helps you to discover research relevant for your work.