Two Lower Bounds for BPA

Authors Mingzhang Huang, Qiang Yin

Thumbnail PDF


  • Filesize: 0.67 MB
  • 16 pages

Document Identifiers

Author Details

Mingzhang Huang
Qiang Yin

Cite AsGet 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)


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.
  • BPA
  • branching bisimulation
  • regularity


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


  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:
  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:
  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:
  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:
  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:
  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:
  7. P. Jančar. Branching Bisimilarity of Normed BPA Processes as a Rational Monoid. arXiv preprint, 2016. URL:
  8. P. Jančar and J. Srba. Undecidability of bisimilarity by defender’s forcing. J. ACM, V:1-26, 2008. URL:
  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:
  10. S. Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters, 113(4):101-106, 2013. URL:
  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:
  12. R. Mayr. Process Rewrite Systems. Information and Computation, 156(1):264-286, 2000. URL:
  13. R. Mayr. Weak bisimilarity and regularity of context-free processes is EXPTIME-hard. Theoretical Computer Science, 330(3):553-575, 2005. URL:
  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:
  18. J. Srba. Roadmap of infinite results. Current Trends In Theoretical Computer Science, 2(201):337-350, 2004. updated version at Google Scholar
  19. C. Stirling. The joys of bisimulation. In Mathematical Foundations of Computer Science 1998. Springer Berlin Heidelberg, 1998. URL:
  20. J. Stříbrná. Hardness results for weak bisimilarity of simple process algebras. Electronic Notes in Theoretical Computer Science, 18:179-190, 1998. URL:
  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: