Document Open Access Logo

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

Author Petr Jancar

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.52.pdf
  • Filesize: 437 kB
  • 13 pages

Document Identifiers

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

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. Petr Jančar. Bisimulation equivalence of first-order grammars. In Proc. ICALP'14 (II), volume 8573 of LNCS, pages 232-243. Springer, 2014. Google Scholar
  5. Petr Jančar. Equivalences of pushdown systems are hard. In Proc. FOSSACS 2014, volume 8412 of LNCS, pages 1-28. Springer, 2014. Google Scholar
  6. 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.
  7. 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. Google Scholar
  8. Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3, 2016. Google Scholar
  9. Géraud Sénizergues. L(A)=L(B)? Decidability results from complete formal systems. Theoretical Computer Science, 251(1-2):1-166, 2001. Google Scholar
  10. Géraud Sénizergues. The bisimulation problem for equational graphs of finite out-degree. SIAM J.Comput., 34(5):1025-1106, 2005. Google Scholar
  11. 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/. Google Scholar
  12. Colin Stirling. Deciding DPDA equivalence is primitive recursive. In Proc. ICALP'02, volume 2380 of LNCS, pages 821-832. Springer, 2002. Google Scholar
  13. 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.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact