On the k-synchronizability of Systems

We study k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is d...

Descripción completa

Detalles Bibliográficos
Autores principales: Di Giusto, Cinzia, Laversa, Laetitia, Lozes, Etienne
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7788629/
http://dx.doi.org/10.1007/978-3-030-45231-5_9
_version_ 1783633067976425472
author Di Giusto, Cinzia
Laversa, Laetitia
Lozes, Etienne
author_facet Di Giusto, Cinzia
Laversa, Laetitia
Lozes, Etienne
author_sort Di Giusto, Cinzia
collection PubMed
description We study k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.
format Online
Article
Text
id pubmed-7788629
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-77886292021-01-07 On the k-synchronizability of Systems Di Giusto, Cinzia Laversa, Laetitia Lozes, Etienne Foundations of Software Science and Computation Structures Article We study k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata. 2020-04-17 /pmc/articles/PMC7788629/ http://dx.doi.org/10.1007/978-3-030-45231-5_9 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Di Giusto, Cinzia
Laversa, Laetitia
Lozes, Etienne
On the k-synchronizability of Systems
title On the k-synchronizability of Systems
title_full On the k-synchronizability of Systems
title_fullStr On the k-synchronizability of Systems
title_full_unstemmed On the k-synchronizability of Systems
title_short On the k-synchronizability of Systems
title_sort on the k-synchronizability of systems
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7788629/
http://dx.doi.org/10.1007/978-3-030-45231-5_9
work_keys_str_mv AT digiustocinzia ontheksynchronizabilityofsystems
AT laversalaetitia ontheksynchronizabilityofsystems
AT lozesetienne ontheksynchronizabilityofsystems

Ejemplares similares