Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F16%3A86100159" target="_blank" >RIV/61989100:27240/16:86100159 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence

Popis výsledku v původním jazyce

The problem if a given configuration of a pushdown automaton (PDA) is bisimilar with some (unspecified) finite-state process is shown to be decidable. The decidability is proven in the framework of first-order grammars, which are given by finite sets of labelled rules that rewrite roots of first-order terms. The framework is equivalent to PDA where also deterministic popping epsilon-steps are allowed, i.e. To the model for which Sénizergues showed an involved procedure deciding bisimilarity (FOCS 1998). Such a procedure is here used as a black-box part of the algorithm. For deterministic PDA the regularity problem was shown decidable by Valiant (JACM 1975) but the decidability question for nondeterministic PDA, answered positively here, had been open (as indicated, e.g., by Broadbent and Goeller, FSTTCS 2012).

Název v anglickém jazyce

Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence

Popis výsledku anglicky

The problem if a given configuration of a pushdown automaton (PDA) is bisimilar with some (unspecified) finite-state process is shown to be decidable. The decidability is proven in the framework of first-order grammars, which are given by finite sets of labelled rules that rewrite roots of first-order terms. The framework is equivalent to PDA where also deterministic popping epsilon-steps are allowed, i.e. To the model for which Sénizergues showed an involved procedure deciding bisimilarity (FOCS 1998). Such a procedure is here used as a black-box part of the algorithm. For deterministic PDA the regularity problem was shown decidable by Valiant (JACM 1975) but the decidability question for nondeterministic PDA, answered positively here, had been open (as indicated, e.g., by Broadbent and Goeller, FSTTCS 2012).

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

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í

2016

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 58

ISBN

978-3-95977-016-3

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

13

Strana od-do

"52:1-"-"-52:13"

Název nakladatele

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Místo vydání

Wadern

Místo konání akce

Krakov

Datum konání akce

22. 8. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

—