Abstract
We present a polynomial-time algorithm deciding bisimilarity between a normed BPA process and a normed BPP process. This improves the previously known exponential upper bound by Černá, Křetínský, Kučera (1999). The algorithm relies on a polynomial bound for the “finite-state core” of the transition system generated by the BPP process. The bound is derived from the “prime form” of the underlying BPP system (where bisimilarity coincides with equality); we suggest an original algorithm for the respective transformation.
The authors acknowledge the support by the Czech Ministry of Education, Grant No. 1M0567.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 545–623. Elsevier, Amsterdam (2001)
Srba, J.: Roadmap of infinite results. In: Current Trends In Theoretical Computer Science, The Challenge of the New Century. Formal Models and Semantics, vol. 2, pp. 337–350. World Scientific Publishing Co., Singapore (2004), http://www.brics.dk/~srba/roadmap/
Hirshfeld, Y., Jerrum, M.: Bisimulation equivalence is decidable for normed process algebra. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 412–421. Springer, Heidelberg (1999)
Burkart, O., Caucal, D., Steffen, B.: An elementary 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)
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)
Jančar, P.: Strong bisimilarity on Basic Parallel Processes is PSPACE-complete. In: Proc. 18th LiCS, pp. 218–227. IEEE Computer Society, Los Alamitos (2003)
Srba, J.: Strong bisimilarity and regularity of Basic Parallel Processes is PSPACE-hard. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 535–546. Springer, Heidelberg (2002)
Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science 158, 143–159 (1996)
Lasota, S., Rytter, W.: Faster algorithm for bisimulation equivalence of normed context-free processes. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 646–657. Springer, Heidelberg (2006)
Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. Mathematical Structures in Computer Science 6, 251–259 (1996)
Jančar, P., Kot, M.: Bisimilarity on normed Basic Parallel Processes can be decided in time O(n 3). In: Bharadwaj, R. (ed.) Proceedings of the Third International Workshop on Automated Verification of Infinite-State Systems – AVIS 2004 (2004)
Černá, I., Křetínský, M., Kučera, A.: Comparing expressibility of normed BPA and normed BPP processes. Acta Informatica 36, 233–256 (1999)
Jančar, P., Kučera, A., Moller, F.: Deciding bisimilarity between BPA and BPP processes. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 159–173. Springer, Heidelberg (2003)
Kučera, A., Mayr, R.: Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time. Theoretical Computer Science 270, 667–700 (2002)
Kučera, A., Mayr, R.: A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. In: IFIP TCS, pp. 395–408. Kluwer, Dordrecht (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jančar, P., Kot, M., Sawa, Z. (2008). Normed BPA vs. Normed BPP Revisited. In: van Breugel, F., Chechik, M. (eds) CONCUR 2008 - Concurrency Theory. CONCUR 2008. Lecture Notes in Computer Science, vol 5201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85361-9_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-85361-9_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85360-2
Online ISBN: 978-3-540-85361-9
eBook Packages: Computer ScienceComputer Science (R0)