%0 Conference Proceedings
%T Choreography Automata
%+ Università degli studi di Catania = University of Catania (Unict)
%+ Foundations of Component-based Ubiquitous Systems (FOCUS)
%+ Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO)
%+ Gran Sasso Science Institute (GSSI)
%+ University of Leicester
%A Barbanera, Franco
%A Lanese, Ivan
%A Tuosto, Emilio
%Z Online event due to covid
%< avec comité de lecture
%B COORDINATION 2020 - 22nd International Conference on Coordination Models and Languages
%C Valletta, Malta
%P 86 - 106
%8 2020-06-15
%D 2020
%R 10.1007/978-3-030-50029-0_6
%Z Computer Science [cs]/Programming Languages [cs.PL]
%Z Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-03005377/document
%2 https://inria.hal.science/hal-03005377/file/main.pdf
%L hal-03005377
%U https://inria.hal.science/hal-03005377
%~ INRIA
%~ INRIA-SOPHIA
%~ INRIASO
%~ OPENAIRE
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ UNIV-COTEDAZUR
%~ IFIP-LNCS-12134
%~ INRIA-ROYAUMEUNI