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: |
Büchi automata
Discrete mathematics Hardware_MEMORYSTRUCTURES Hierarchy (mathematics) FIFO (computing and electronics) Computer science Büchi automaton 0102 computer and information sciences 02 engineering and technology 01 natural sciences Computer Science Applications Theoretical Computer Science Decidability Undecidable problem Nondeterministic algorithm simulation games Computational Theory and Mathematics 010201 computation theory & mathematics Bounded function 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] 020201 artificial intelligence & image processing Mazurkiewicz traces Information Systems TRACE (psycholinguistics) |
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 |
Externí odkaz: |