On Büchi one-counter automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F17%3A10237379" target="_blank" >RIV/61989100:27240/17:10237379 - isvavai.cz</a>

Výsledek na webu

<a href="http://drops.dagstuhl.de/opus/volltexte/2017/7019/" target="_blank" >http://drops.dagstuhl.de/opus/volltexte/2017/7019/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.STACS.2017.14" target="_blank" >10.4230/LIPIcs.STACS.2017.14</a>

Jazyk výsledku

angličtina

Název v původním jazyce

On Büchi one-counter automata

Popis výsledku v původním jazyce

Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by Sénizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by Löding. In fact, we show that already the equivalence problem for deterministic Büchi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by Löding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic Büchi pushdown automata) is decidable. Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic Büchi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.

Název v anglickém jazyce

On Büchi one-counter automata

Popis výsledku anglicky

Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by Sénizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by Löding. In fact, we show that already the equivalence problem for deterministic Büchi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by Löding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic Büchi pushdown automata) is decidable. Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic Büchi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA15-13784S" target="_blank" >GA15-13784S: Výpočetní složitost vybraných verifikačních problémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Leibniz International Proceedings in Informatics, LIPIcs. Volume 66

ISBN

978-3-95977-028-6

ISSN

1868-8969

e-ISSN

neuvedeno

Počet stran výsledku

13

Strana od-do

1-13

Název nakladatele

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Místo vydání

Wadern

Místo konání akce

Hannover

Datum konání akce

8. 3. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—