Choreography Automata

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....

Descripción completa

Detalles Bibliográficos
Autores principales: Barbanera, Franco, Lanese, Ivan, Tuosto, Emilio
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7282852/
http://dx.doi.org/10.1007/978-3-030-50029-0_6
_version_ 1783544202378870784
author Barbanera, Franco
Lanese, Ivan
Tuosto, Emilio
author_facet Barbanera, Franco
Lanese, Ivan
Tuosto, Emilio
author_sort Barbanera, Franco
collection PubMed
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.
format Online
Article
Text
id pubmed-7282852
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72828522020-06-10 Choreography Automata Barbanera, Franco Lanese, Ivan Tuosto, Emilio Coordination Models and Languages Article 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. 2020-05-13 /pmc/articles/PMC7282852/ http://dx.doi.org/10.1007/978-3-030-50029-0_6 Text en © IFIP International Federation for Information Processing 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Barbanera, Franco
Lanese, Ivan
Tuosto, Emilio
Choreography Automata
title Choreography Automata
title_full Choreography Automata
title_fullStr Choreography Automata
title_full_unstemmed Choreography Automata
title_short Choreography Automata
title_sort choreography automata
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7282852/
http://dx.doi.org/10.1007/978-3-030-50029-0_6
work_keys_str_mv AT barbanerafranco choreographyautomata
AT laneseivan choreographyautomata
AT tuostoemilio choreographyautomata

Ejemplares similares