Document Open Access Logo

Two Lower Bounds for BPA

Authors Mingzhang Huang, Qiang Yin

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.20.pdf
  • Filesize: 0.67 MB
  • 16 pages

Document Identifiers

Author Details

Mingzhang Huang
Qiang Yin

Cite As Get BibTex

Mingzhang Huang and Qiang Yin. Two Lower Bounds for BPA. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.20

Abstract

Branching bisimilarity of normed Basic Process Algebra (nBPA) was claimed to be EXPTIME-hard in previous papers without any explicit proof. Recently it has been pointed out by Petr Jancar that the claim lacked proper justification. In this paper, we develop a new complete proof for the EXPTIME-hardness of branching bisimilarity of nBPA. We also prove that the associated regularity problem of nBPA is PSPACE-hard. This improves previous P-hard result.

Subject Classification

Keywords
  • BPA
  • branching bisimulation
  • regularity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for process generating context-free languages. J. ACM, 40(3):653-682, 1993. URL: http://dx.doi.org/10.1145/174130.174141.
  2. J. Balcázar, J. Gabarró, and M. Sántha. Deciding bisimilarity is P-complete. Formal aspects of computing, 4(1):638-648, 1992. URL: http://dx.doi.org/10.1007/BF03180566.
  3. W. Czerwiński, P. Hofman, and S. Lasota. Decidability of branching bisimulation on normed commutative context-free processes. Theory of Computing Systems, 55(1):136-169, 2014. URL: http://dx.doi.org/10.1007/s00224-013-9505-9.
  4. W. Czerwiński and P. Jančar. Branching bisimilarity of normed BPA processes is in NEXPTIME. In Proc. LICS 2015, pages 168-179. IEEE Computer Society, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.25.
  5. Y. Fu. Checking equality and regularity for normed BPA with silent moves. In Proc. ICALP'13 (II), volume 7966 of LNCS, pages 238-249. Springer-Verlag, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39212-2_23.
  6. C. He and M. Huang. Branching bisimilarity on normed BPA is EXPTIME-complete. In Proc. LICS 2015, pages 180-191. IEEE Computer Society, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.26.
  7. P. Jančar. Branching Bisimilarity of Normed BPA Processes as a Rational Monoid. arXiv preprint, 2016. URL: http://arxiv.org/abs/1602.05151.
  8. P. Jančar and J. Srba. Undecidability of bisimilarity by defender’s forcing. J. ACM, V:1-26, 2008. URL: http://dx.doi.org/10.1145/1326554.1326559.
  9. M. Jurdziński, F. Laroussinie, and J. Sproston. Model checking probabilistic timed automata with one or two clocks. In Proc. TACS'07, pages 170-184. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-71209-1_15.
  10. S. Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters, 113(4):101-106, 2013. URL: http://dx.doi.org/10.1016/j.ipl.2012.12.004.
  11. A. Kučera and P. Jančar. Equivalence-checking with infinite-state systems: Techniques and results. Theory and Practice of Logic Programming, 6(3):227-264, 2006. URL: http://dx.doi.org/10.1017/S1471068406002651.
  12. R. Mayr. Process Rewrite Systems. Information and Computation, 156(1):264-286, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2826.
  13. R. Mayr. Weak bisimilarity and regularity of context-free processes is EXPTIME-hard. Theoretical Computer Science, 330(3):553-575, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.10.008.
  14. J. Srba. Applications of the Existential Quantification Technique. In 4th International Workshop on Verification of Infinite-State Systems, pages 151-152, 2002. Google Scholar
  15. J. Srba. Strong bisimilarity and regularity of Basic Parallel Processes is PSPACE-hard. In Proc. STACS'02, pages 535-546. Springer, 2002. Google Scholar
  16. J. Srba. Strong bisimilarity and regularity of Basic Process Algebra is PSPACE-hard. In Proc. ICALP'02, pages 716-727. Springer, 2002. Google Scholar
  17. J. Srba. Complexity of weak bisimilarity and regularity for BPA and BPP. Mathematical Structures in Computer Science, 13(4):567-587, 2003. URL: http://dx.doi.org/10.1017/S0960129503003992.
  18. J. Srba. Roadmap of infinite results. Current Trends In Theoretical Computer Science, 2(201):337-350, 2004. updated version at http://users-cs.au.dk/srba/roadmap/. Google Scholar
  19. C. Stirling. The joys of bisimulation. In Mathematical Foundations of Computer Science 1998. Springer Berlin Heidelberg, 1998. URL: http://dx.doi.org/10.1007/BFb0055763.
  20. J. Stříbrná. Hardness results for weak bisimilarity of simple process algebras. Electronic Notes in Theoretical Computer Science, 18:179-190, 1998. URL: http://dx.doi.org/10.1016/S1571-0661(05)80259-2.
  21. W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science. In TAPSOFT'93: Theory and Practice of Software Development, pages 559-568. Springer Berlin Heidelberg, 1993. URL: http://dx.doi.org/10.1007/3-540-56610-4_89.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact