Multi-Buffer Simulations for Trace Language Inclusion
We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1609.04098v1 |
| _version_ | 1811322398922768384 |
|---|---|
| author | Milka Hutagalung Norbert Hundeshagen Dietrich Kuske Martin Lange Etienne Lozes |
| author_facet | Milka Hutagalung Norbert Hundeshagen Dietrich Kuske Martin Lange Etienne Lozes |
| author_sort | Milka Hutagalung |
| collection | DOAJ |
| description | We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers). |
| first_indexed | 2024-04-13T13:35:42Z |
| format | Article |
| id | doaj.art-39f73ffc0f0b4dbc909d69b94230ca7a |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T13:35:42Z |
| publishDate | 2016-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-39f73ffc0f0b4dbc909d69b94230ca7a2022-12-22T02:44:48ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-09-01226Proc. GandALF 201621322710.4204/EPTCS.226.15:18Multi-Buffer Simulations for Trace Language InclusionMilka Hutagalung0Norbert Hundeshagen1Dietrich Kuske2Martin Lange3Etienne Lozes4 Universität Kassel Universität Kassel Technische Universität Ilmenau Universität Kassel ENS Cachan We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers).http://arxiv.org/pdf/1609.04098v1 |
| spellingShingle | Milka Hutagalung Norbert Hundeshagen Dietrich Kuske Martin Lange Etienne Lozes Multi-Buffer Simulations for Trace Language Inclusion Electronic Proceedings in Theoretical Computer Science |
| title | Multi-Buffer Simulations for Trace Language Inclusion |
| title_full | Multi-Buffer Simulations for Trace Language Inclusion |
| title_fullStr | Multi-Buffer Simulations for Trace Language Inclusion |
| title_full_unstemmed | Multi-Buffer Simulations for Trace Language Inclusion |
| title_short | Multi-Buffer Simulations for Trace Language Inclusion |
| title_sort | multi buffer simulations for trace language inclusion |
| url | http://arxiv.org/pdf/1609.04098v1 |
| work_keys_str_mv | AT milkahutagalung multibuffersimulationsfortracelanguageinclusion AT norberthundeshagen multibuffersimulationsfortracelanguageinclusion AT dietrichkuske multibuffersimulationsfortracelanguageinclusion AT martinlange multibuffersimulationsfortracelanguageinclusion AT etiennelozes multibuffersimulationsfortracelanguageinclusion |