Published June 15, 2020
| Version v1
Conference paper
Choreography Automata
- Creators
- Barbanera, Franco
- Lanese, Ivan
- Tuosto, Emilio
- Others:
- University of Catania [Italy]
- Foundations of Component-based Ubiquitous Systems (FOCUS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)
- Alma Mater Studiorum University of Bologna (UNIBO)
- Gran Sasso Science Institute (GSSI) ; Istituto Nazionale di Fisica Nucleare (INFN)
- University of Leicester
- European Project: 778233,H2020-EU.1.3.3. - Stimulating innovation by means of cross-fertilisation of knowledge ,778233,BEHAPI(2018)
Description
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.
Abstract
Online event due to covid
Abstract
International audience
Additional details
- URL
- https://hal.inria.fr/hal-03005377
- URN
- urn:oai:HAL:hal-03005377v1
- Origin repository
- UNICA