Checking Equality and Regularity for Normed BPA with Silent Moves

Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


The decidability of weak bisimilarity on normed BPA is a long standing open problem. It is proved in this paper that branching bisimilarity, a standard refinement of weak bisimilarity, is decidable for normed BPA and that the associated regularity problem is also decidable.


Transition Rule Check Equality Relative Norm Regularity Problem Silent Action 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BBK87]
    Baeten, J., Bergstra, J., Klop, J.: Decidability of bisimulation equivalence for processes generating context-free languages. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 94–113. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  2. [BCS95]
    Burkart, O., Caucal, D., Steffen, B.: An elementary bisimulation decision procedure for arbitrary context free processes. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 423–433. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  3. [BCS96]
    Burkart, O., Caucal, D., Steffen, B.: Bisimulation collapse and the process taxonomy. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 247–262. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  4. [BGS92]
    Balcazar, J., Gabarro, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Aspects of Computing 4, 638–648 (1992)zbMATHCrossRefGoogle Scholar
  5. [CHL11]
    Czerwiński, W., Hofman, P., Lasota, S.: Decidability of branching bisimulation on normed commutative context-free processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 528–542. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. [CHS92]
    Christensen, S., Hüttel, H., Stirling, C.: Bisimulation equivalence is decidable for all context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 138–147. Springer, Heidelberg (1992)Google Scholar
  7. [CHT95]
    Caucal, D., Huynh, D., Tian, L.: Deciding branching bisimilarity of normed context-free processes is in \(\sigma^p_2\). Information and Computation 118, 306–315 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  8. [Hir96]
    Hirshfeld, Y.: Bisimulation trees and the decidability of weak bisimulations. Electronic Notes in Theoretical Computer Science 5, 2–13 (1996)CrossRefGoogle Scholar
  9. [HJM96]
    Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial algorithm for deciding bisimilarity of normed context free processes. Theoretical Computer Science 158(1-2), 143–159 (1996)MathSciNetzbMATHCrossRefGoogle Scholar
  10. [HS91]
    Hüttel, H., Stirling, C.: Actions speak louder than words: Proving bisimilarity for context-free processes. In: LICS 1991, pp. 376–386 (1991)Google Scholar
  11. [HT94]
    Huynh, T., Tian, L.: Deciding bisimilarity of normed context free processes is in \(\sigma_{2}^{p}\). Theoretical Computer Science 123, 83–197 (1994)MathSciNetCrossRefGoogle Scholar
  12. [Hüt92]
    Hüttel, H.: Silence is golden: Branching bisimilarity is decidable for context free processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 2–12. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  13. [Jan12]
    Jančar, P.: Bisimilarity on basic process algebra is in 2-exptime (2012)Google Scholar
  14. [JE96]
    Jančar, P., Esparza, J.: Deciding finiteness of petri nets up to bisimulation. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 478–489. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  15. [Kie13]
    Kiefer, S.: BPA bisimilarity is exptime-hard. Information Processing Letters 113, 101–106 (2013)MathSciNetzbMATHCrossRefGoogle Scholar
  16. [Kuč96]
    Kučera, A.: Regularity is decidable for normed BPA and normed BPP processes in polynomial time. In: Král, J., Bartosek, M., Jeffery, K. (eds.) SOFSEM 1996. LNCS, vol. 1175, pp. 377–384. Springer, Heidelberg (1996)Google Scholar
  17. [May00]
    Mayr, R.: Process rewrite systems. Information and Computation 156, 264–286 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  18. [May03]
    Mayr, R.: Weak bisimilarity and regularity of BPA is exptime-hard. In: EXPRESS 2003 (2003)Google Scholar
  19. [Srb02]
    Srba, J.: Strong bisimilarity and regularity of basic process algebra is pspace-hard. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 716–727. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  20. [Srb03]
    Srba, J.: Complexity of weak bisimilarity and regularity for BPA and BPP. Mathematical Structures in Computer Science 13, 567–587 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  21. [Stř98]
    Stříbrná, J.: Hardness results for weak bisimilarity of simple process algebras. Electronic Notes in Theoretical Computer Science 18, 179–190 (1998)CrossRefGoogle Scholar
  22. [vGW89]
    van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. In: Information Processing 1989, pp. 613–618. North-Holland (1989)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Yuxi Fu
    • 1
  1. 1.BASICS, Department of Computer Science, MOE-MS Key Laboratory for Intelligent Computing and Intelligent SystemsShanghai Jiao Tong UniversityChina

Personalised recommendations