×

zbMATH — the first resource for mathematics

Complexity of deciding bisimilarity between normed BPA and normed BPP. (English) Zbl 1209.68338
Summary: We present a polynomial-time algorithm deciding bisimilarity between a normed BPA process and a normed BPP process, with running time \(O(n^{7})\). This improves the previously known exponential upper bound. We first suggest an \(O(n^{3})\) transformation of the BPP process into “prime form”. Our algorithm then relies on a polynomial bound for a “finite-state core” of the transition system generated by the (transformed) BPP process.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification on infinite structures, (), 545-623, (Chapter 9) · Zbl 1035.68067
[2] J. Srba, Roadmap of infinite results, in: Current Trends in Theoretical Computer Science, The Challenge of the New Century Formal Models and Semantics, vol. 2, World Scientific Publishing Co., 2004, pp. 337-350 (see an updated version at http://www.brics.dk/srba/roadmap). · Zbl 1065.68073
[3] Y. Hirshfeld, M. Jerrum, Bisimulation equivalence is decidable for normed process algebra, in: Proceedings of 26th International Colloquium on Automata, Languages and Programming (ICALP’99), Lecture Notes in Computer Science, vol. 1644, Springer-Verlag, 1999, pp. 412-421. · Zbl 0941.68574
[4] O. Burkart, D. Caucal, B. Steffen, An elementary decision procedure for arbitrary context-free processes, in: Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS’95), Lecture Notes in Computer Science, vol. 969, Springer-Verlag, 1995, pp. 423-433. · Zbl 1193.68172
[5] J. Srba, Strong bisimilarity and regularity of Basic Process Algebra is PSPACE-hard, in: Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP’02), Lecture Notes in Computer Science, vol. 2380, Springer, 2002, pp. 716-727. · Zbl 1057.68071
[6] P. Jančar, Strong bisimilarity on Basic Parallel Processes is PSPACE-complete, in: Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS 2003), IEEE Computer Society, 2003, pp. 218-227.
[7] J. Srba, Strong bisimilarity and regularity of Basic Parallel Processes is PSPACE-hard, in: Proceedings of 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2002), Lecture Notes in Computer Science, vol. 2285, Springer, 2002, pp. 535-546. · Zbl 1054.68096
[8] Hirshfeld, Y.; Jerrum, M.; Moller, F., A polynomial algorithm for deciding bisimilarity of normed context-free processes, Theor. comput. sci., 158, 143-159, (1996) · Zbl 0871.68086
[9] S. Lasota, W. Rytter, Faster algorithm for bisimulation equivalence of normed context-free processes, in: Proceedings of 31st International Symposium on Mathematical Foundations of Computer Science (MFCS 2006), Lecture Notes in Computer Science, vol. 4162, Springer-Verlag, 2006, pp. 646-657. · Zbl 1132.68498
[10] Hirshfeld, Y.; Jerrum, M.; Moller, F., A polynomial-time algorithm for deciding bisimulation equivalence of normed basic parallel processes, Math. struct. comput. sci., 6, 251-259, (1996) · Zbl 0857.68042
[11] P. Jančar, M. Kot, Bisimilarity on normed Basic Parallel Processes can be decided in time \(O(n^3)\), in: Proceedings of the Third International Workshop on Automated Verification of Infinite-State Systems (AVIS 2004), 2004.
[12] Černá, I.; Křetínský, M.; Kučera, A., Comparing expressibility of normed BPA and normed BPP processes, Acta inform., 36, 233-256, (1999) · Zbl 0947.68109
[13] P. Jančar, A. Kučera, F. Moller, Deciding bisimilarity between BPA and BPP processes, in: Proceedings of the 14th International Conference on Concurrency Theory (CONCUR 2003), Lecture Notes in Computer Science, vol. 2761, Springer-Verlag, 2003, pp. 159-173. · Zbl 1274.68236
[14] Kučera, A.; Mayr, R., Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, Theor. comput. sci., 270, 667-700, (2002) · Zbl 0988.68118
[15] P. Jančar, M. Kot, Z. Sawa, Normed BPA vs. normed BPP revisited, in: Proceedings of the 19th International Conference on Concurrency Theory (CONCUR 2008), Lecture Notes in Computer Science, vol. 5201, Springer, 2008, pp. 434-446.
[16] A. Kučera, R. Mayr, A generic framework for checking semantic equivalences between pushdown automata and finite-state automata, in: IFIP TCS, Kluwer, 2004, pp. 395-408. · Zbl 1094.68050
[17] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pac. J. math., 5, 2, 285-309, (1955) · Zbl 0064.26004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.