Equivalences of pushdown systems are hard

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F14%3A86092899" target="_blank" >RIV/61989100:27240/14:86092899 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-642-54830-7_1" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-642-54830-7_1</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-54830-7_1" target="_blank" >10.1007/978-3-642-54830-7_1</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Equivalences of pushdown systems are hard

Popis výsledku v původním jazyce

Language equivalence of deterministic pushdown automata (DPDA) was shown to be decidable by Senizergues (1997, 2001); Stirling (2002) then showed that the problem is primitive recursive. Senizergues (1998, 2005) also generalized his proof to show decidability of bisimulation equivalence of (nondeterministic) PDA where epsilon-rules can be only deterministic and popping; this problem was shown to be nonelementary by Benedikt, Goeller, Kiefer, and Murawski (2013), even for PDA with no epsilon-rules. Herewe refine Stirling?s analysis and show that DPDA equivalence is in TOWER, i.e., in the ?least? nonelementary complexity class. The basic proof ideas remain the same but the presentation and the analysis are simplified, in particular by using a first-order term framework. The framework of (nondeterministic) first-order grammars, with term root-rewriting rules, is equivalent to the model of PDA with restricted epsilon-rules to which Senizergues?s decidability proof applies. We show that bi

Název v anglickém jazyce

Equivalences of pushdown systems are hard

Popis výsledku anglicky

Language equivalence of deterministic pushdown automata (DPDA) was shown to be decidable by Senizergues (1997, 2001); Stirling (2002) then showed that the problem is primitive recursive. Senizergues (1998, 2005) also generalized his proof to show decidability of bisimulation equivalence of (nondeterministic) PDA where epsilon-rules can be only deterministic and popping; this problem was shown to be nonelementary by Benedikt, Goeller, Kiefer, and Murawski (2013), even for PDA with no epsilon-rules. Herewe refine Stirling?s analysis and show that DPDA equivalence is in TOWER, i.e., in the ?least? nonelementary complexity class. The basic proof ideas remain the same but the presentation and the analysis are simplified, in particular by using a first-order term framework. The framework of (nondeterministic) first-order grammars, with term root-rewriting rules, is equivalent to the model of PDA with restricted epsilon-rules to which Senizergues?s decidability proof applies. We show that bi

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F11%2F0340" target="_blank" >GAP202/11/0340: Modelování a verifikace paralelních systémů</a><br>

Návaznosti

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

Rok uplatnění

2014

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

Lecture Notes in Computer Science. Volume 8412

ISBN

978-3-642-54829-1

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

28

Strana od-do

1-28

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Grenoble

Datum konání akce

4. 4. 2014

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

WRD - Celosvětová akce

Kód UT WoS článku

—