zbMATH — the first resource for mathematics

Undecidability of performance equivalence of Petri nets. (English) Zbl 1356.68155
Summary: We investigate bisimulation equivalence on Petri nets under durational semantics. Our motivation was to verify the conjecture that in durational setting, the bisimulation equivalence checking problem becomes more tractable than in ordinary setting (which is the case, e.g., over communication-free nets). We disprove this conjecture in three of four proposed variants of durational semantics. The fourth variant remains an intriguing open problem.
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI
[1] Bérard, B.; Labroue, A.; Schnoebelen, Ph., Verifying performance equivalence for timed basic parallel processes, (Proceeding of the 3rd Int. Conf. Foundations of Software Science and Computation Structures, FOSSACS’2000, LNCS, vol. 1784, (2000)), 35-47 · Zbl 0965.68063
[2] Bonnet, R., The reachability problem for vector addition system with one zero-test, (Proceedings of MFCS’11, (2011)), 145-157 · Zbl 1343.68160
[3] Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification on infinite structures, (Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra, (2001), Elsevier Science), 545-623 · Zbl 1035.68067
[4] Christensen, S., Decidability and decomposition in process algebras, (1993), University of Edinburgh, Department of Computer Science, ECS-LFCS-93-278
[5] Corradini, F., On performance congruences for process algebras, Inform. and Comput., 145, 2, 191-230, (1998) · Zbl 0921.68031
[6] Corradini, F.; Gorrieri, R.; Roccetti, M., Performance preorder and competitive equivalence, Acta Inform., 34, 11, 805-835, (1997) · Zbl 0878.68081
[7] de Frutos Escrig, D.; Cuartero Gomez, F.; Valero Ruiz, V., On non-decidability of reachability for timed-arc Petri nets, (Proceedings of the 8th International Workshop on Petri Nets and Performance Models, (1999))
[8] van Glabbeek, R. J., The linear-branching time spectrum, (Beaten, J. C.M.; Klop, J. W., CONCUR’90, LNCS, vol. 458, (1990), Springer Amsterdam), 278-297
[9] Gorrieri, R.; Roccetti, M.; Stancampiano, E., A theory of processes with durational actions, Theoret. Comput. Sci., 140, 1, 73-94, (1995) · Zbl 0874.68113
[10] Jančar, P., Undecidablilty of bisimilarity for Petri nets and some related problems, Theoret. Comput. Sci., 148, 2, 281-301, (1995) · Zbl 0873.68147
[11] Jančar, P., Strong bisimilarity on basic parallel processes is PSPACE-complete, (Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, LICS’03, (2003), IEEE Computer Society Press), 218-227
[12] Lasota, S., Decidability of strong bisimilarity for timed BPP, (Proceedings of CONCUR’02, LNCS, vol. 2421, (2002)), 562-578 · Zbl 1012.68126
[13] Lasota, S., A polynomial-time algorithm for deciding true concurrency equivalences of basic parallel processes, (Proceedings of MFCS’03, LNCS, vol. 2747, (2003)), 521-530 · Zbl 1124.68392
[14] Lasota, S., Decidability of performance equivalence for basic parallel processes, Theoret. Comput. Sci., 360, 172-192, (2006) · Zbl 1099.68070
[15] Lazic, R.; Newcomb, T. C.; Ouaknine, J.; Roscoe, A. W.; Worrell, J., Nets with tokens which carry data, (Proceedings ICATPN’07, (2007)), 301-320 · Zbl 1226.68062
[16] Merlin, P., A study of the recoverability of communication protocols, (1974), Univ. of California, PhD Thesis
[17] Milner, R., Communication and concurrency, (1995), Prentice Hall
[18] Park, D. M.R., Concurrency and automata on infinite sequences, (Proceedings of the 5th GI Conference, LNCS, vol. 104, (1981), Springer-Verlag), 167-183
[19] Ramchamdani, C., Performance evaluation of asynchronous concurrent systems by timed Petri net, (1973), MIT, PhD Thesis
[20] Reinhardt, K., Reachability in Petri nets with inhibitor arcs, Electron. Notes Theor. Comput. Sci., 223, 239-264, (2008) · Zbl 1337.68191
[21] Srba, J., Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard, (Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science, STACS’02, LNCS, vol. 2285, (2002), Springer-Verlag), 535-546 · Zbl 1054.68096
[22] Stirling, C., Bisimulation, model checking and other games, (Notes for Mathfit Instructional Meeting on Games and Computation, Edinburgh, (1997))
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.