Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence

Jancar, Petr

doi:10.4230/LIPIcs.MFCS.2016.52

File

LIPIcs.MFCS.2016.52.pdf

Filesize: 437 kB
13 pages

Document Identifiers

DOI: 10.4230/LIPIcs.MFCS.2016.52
URN: urn:nbn:de:0030-drops-64649

Author Details

Petr Jancar

Cite AsGet BibTex

Petr Jancar. Deciding Semantic Finiteness of Pushdown Processes and First-Order Grammars w.r.t. Bisimulation Equivalence. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 52:1-52:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.MFCS.2016.52

Abstract

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 Senizergues 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).

Keywords

pushdown processes
first-order grammars
bisimulation
regularity

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S. Murawski. Bisimilarity of pushdown automata is nonelementary. In Proc. LICS 2013, pages 488-498. IEEE Computer Society, 2013.
Christopher H. Broadbent and Stefan Göller. On bisimilarity of higher-order pushdown automata: Undecidability at order two. In FSTTCS 2012, volume 18 of LIPIcs, pages 160-172. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.
Bruno Courcelle. Recursive applicative program schemes. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pages 459-492. Elsevier, MIT Press, 1990.
Petr Jančar. Bisimulation equivalence of first-order grammars. In Proc. ICALP'14 (II), volume 8573 of LNCS, pages 232-243. Springer, 2014.
Petr Jančar. Equivalences of pushdown systems are hard. In Proc. FOSSACS 2014, volume 8412 of LNCS, pages 1-28. Springer, 2014.
Petr Jančar and Jiri Srba. Undecidability of bisimilarity by defender’s forcing. J. ACM, 55(1), 2008. URL: http://dx.doi.org/10.1145/1326554.1326559.
Antonín Kučera and Richard Mayr. On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. Inf. Comput., 208(7):772-796, 2010.
Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3, 2016.
Géraud Sénizergues. L(A)=L(B)? Decidability results from complete formal systems. Theoretical Computer Science, 251(1-2):1-166, 2001.
Géraud Sénizergues. The bisimulation problem for equational graphs of finite out-degree. SIAM J.Comput., 34(5):1025-1106, 2005.
Jiri Srba. Roadmap of infinite results. In Current Trends In Theoretical Computer Science, The Challenge of the New Century, volume 2, pages 337-350. World Scientific Publishing Co., 2004. Updated version at http://users-cs.au.dk/srba/roadmap/.
Colin Stirling. Deciding DPDA equivalence is primitive recursive. In Proc. ICALP'02, volume 2380 of LNCS, pages 821-832. Springer, 2002.
Leslie G. Valiant. Regularity and related problems for deterministic pushdown automata. J. ACM, 22(1):1-10, 1975. URL: http://dx.doi.org/10.1145/321864.321865.