Multi-buffer simulations: Decidability and complexity

Autor: Martin Lange, Milka Hutagalung, Dietrich Kuske, Norbert Hundeshagen, Etienne Lozes
Přispěvatelé: Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)
Rok vydání: 2018
Předmět:
Zdroj: Information and Computation
Information and Computation, Elsevier, 2018, 262, pp.280-310. ⟨10.1016/j.ic.2018.09.008⟩
ISSN: 0890-5401
1090-2651
Popis: International audience; Multi-buffer simulation is a refinement of fair simulation between two nonde-terministic B ¨ uchi automata (NBA). It is characterised by a game in which letters get pushed to and taken from FIFO buffers of bounded or unbounded capacity. Games with a single buffer approximate the PSPACE-complete language inclusion problem for NBA. With multiple buffers and a fixed mapping of letters to buffers these games approximate the undecidable inclusion problem between Mazurkiewicz trace languages. We study the decidability and complexity of multi-buffer simulations and obtain the following results: P-completeness for fixed bounded buffers, EXPTIME-completeness in case of a single unbounded buffer and high undecidability (in the analytic hierarchy) with two buffers of which at least one is unbounded. We also consider a variant in which the buffers are kept untouched or flushed and show PSPACE-completeness for the single-buffer case.
Databáze: OpenAIRE