DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.33

Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata

Authors: Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, and Damien Regnault

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract

We study the complexity relationship between three models of unbounded memory automata: nu-automata (ν-A), Layered Memory Automata (LaMA)and History-Register Automata (HRA). These are all extensions of finite state automata with unbounded memory over infinite alphabets. We prove that the membership problem is NP-complete for all of them, while they fall into different classes for what concerns non-emptiness. The problem of non-emptiness is known to be Ackermann-complete for HRA, we prove that it is PSPACE-complete for ν-A.

Cite as

Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel, and Damien Regnault. Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2023.33,
  author =	{Bertrand, Cl\'{e}ment and Di Giusto, Cinzia and Klaudel, Hanna and Regnault, Damien},
  title =	{{Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{33:1--33:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.33},
  URN =		{urn:nbn:de:0030-drops-190277},
  doi =		{10.4230/LIPIcs.CONCUR.2023.33},
  annote =	{Keywords: memory automata, \nu-automata, LaMA, HRA, complexity, non-emptiness, membership}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.14

A Unifying Framework for Deciding Synchronizability

Authors: Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.

Cite as

Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2021.14,
  author =	{Bollig, Benedikt and Di Giusto, Cinzia and Finkel, Alain and Laversa, Laetitia and Lozes, Etienne and Suresh, Amrita},
  title =	{{A Unifying Framework for Deciding Synchronizability}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.14},
  URN =		{urn:nbn:de:0030-drops-143917},
  doi =		{10.4230/LIPIcs.CONCUR.2021.14},
  annote =	{Keywords: communicating finite-state machines, message sequence charts, synchronizability, MSO logic, special tree-width}
}

Search Results

Documents authored by Di Giusto, Cinzia

Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata

Abstract

Cite as

A Unifying Framework for Deciding Synchronizability

Abstract

Cite as

Thanks for your feedback!

Could not send message