Resource Bisimilarity in Petri Nets is Decidable

• Autorzy: Lomazova Irina , Bashkin Vladimir , Jančar Petr

Identyfikatory

DOI

10.3233/FI-222125

• Języki publikacji: EN

Abstrakty

EN

Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (a submultiset) of Petri net markings and call two resources equivalent when replacing one of them with another in any marking does not change the observable Petri net behavior. We consider resource similarity and resource bisimilarity, two congruent restrictions of bisimulation equivalence on Petri net markings. Previously it was proved that resource similarity (the largest congruence included in bisimulation equivalence) is undecidable. Here we present an algorithm for checking resource bisimilarity, thereby proving that this relation (the largest congruence included in bisimulation equivalence that is a bisimulation) is decidable. We also give an example of two resources in a Petri net that are similar but not bisimilar.

Słowa kluczowe

EN

labeled Petri nets; bisimulation; congruence; decidability; resource bisimilarity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 186, nr 1-4
• Strony: 175--194
• Opis fizyczny: Bibliogr. 37 poz.

Twórcy

autor

Lomazova Irina

• Dept. of Computer Science, Faculty of Science Palack´y University, Olomouc, Czechia

autor

Bashkin Vladimir

• Dept. of Computer Science, Faculty of Science Palack´y University, Olomouc, Czechia

autor

Jančar Petr

• Dept. of Computer Science, Faculty of Science Palack´y University, Olomouc, Czechia

Bibliografia

• [1] van Glabbeek R. The Linear Time - Branching Time Spectrum. In: Bergstra J, Ponse A, Smolka S (eds.), Handbook of Process Algebra, pp. 3 – 99. Elsevier Science, Amsterdam. ISBN:978-0-444-82830-9, 2001. doi:10.1016/B978-044482830-9/50019-9.
• [2] Park D. Concurrency and automata on infinite sequences. In: Deussen P (ed.), Theoretical Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, 1981 pp. 167–183. ISBN:978-3-540-38561-5.
• [3] Milner R. Communication and Concurrency. Prentice-Hall, Inc., USA, 1989. ISBN:0131150073.
• [4] Jančar P. Undecidability of Bisimilarity for Petri Nets and Some Related Problems. Theor. Comput. Sci., 1995. 148(2):281–301. doi:10.1016/0304-3975(95)00037-W.
• [5] Mayr R. Process Rewrite Systems. Information and Computation, 2000. 156(1):264 – 286. doi:10.1006/inco.1999.2826.
• [6] Christensen S, Hirshfeld Y, Moller F. Bisimulation equivalence is decidable for basic parallel processes. In: Best E (ed.), CONCUR’93. Springer Berlin Heidelberg, Berlin, Heidelberg, 1993 pp. 143–157. ISBN:978-3-540-47968-0.
• [7] Jančar P. Bisimilarity on Basic Parallel Processes. Theor. Comput. Sci., 2022. 903:26–38. doi:10.1016/j.tcs.2021.11.027.
• [8] Baldan P, Bonchi F, Gadducci F, Monreale GV. Modular encoding of synchronous and asynchronous interactions using open Petri nets. Science of Computer Programming, 2015. doi:10.1016/j.scico.2014. 11.019.
• [9] Heckel R. Open petri nets as semantic model for workflow integration. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2003. doi:10.1007/978-3-540-40022-614.
• [10] Dong X, Fu Y, Varacca D. Place bisimulation and liveness for open petri nets. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ISBN: 9783319476766, 2016 doi:10.1007/978-3-319-47677-31.
• [11] Lomazova IA, Romanov IV. Analyzing compatibility of services via resource conformance. In: Fundamenta Informaticae. 2013 doi:10.3233/FI-2013-937.
• [12] Bashkin VA, Lomazova IA. Decidability of k-soundness for workflow nets with an unbounded resource. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ISBN:9783662457290, 2014 doi:10.1007/978-3-662-45730-61.
• [13] Sidorova N, Stahl C. Soundness for resource-constrained workflow nets is decidable. IEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans, 2013. doi:10.1109/TSMCA.2012.2210415.
• [14] Girard JY. Linear logic. Theoretical Computer Science, 1987. doi:10.1016/0304-3975(87)90045-4.
• [15] Farwer B. A Linear Logic view of object Petri Nets. Fundamenta Informaticae, 1999. doi:10.3233/fi-1999-37303.
• [16] Farwer B, Lomazova I. A systematic approach towards object-based petri net formalisms. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ISBN: 354043075X, 2001 doi:10.1007/3-540-45575-226.
• [17] Olderog ER. Strong bisimilarity on nets: A new concept for comparing net semantics. In: de Bakker JW, de Roever WP, Rozenberg G (eds.), Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer Berlin Heidelberg, Berlin, Heidelberg, 1989 pp. 549–573. ISBN:978-3-540-46147-0.
• [18] Autant C, Belmesk Z, Schnoebelen P. Strong Bisimilarity on Nets Revisited. In: Aarts EHL, vaneeuwen J, Rem M (eds.), Parle ’91 Parallel Architectures and Languages Europe. Springer Berlin Heidelberg, Berlin, Heidelberg, 1991 pp. 717–734. ISBN:978-3-662-25209-3.
• [19] Autant C, Schnoebelen P. Place bisimulations in Petri nets, pp. 45–61. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN:978-3-540-47270-4, 1992. doi:10.1007/3-540-55676-13.
• [20] Autant C, Pfister W, Schnoebelen P. Place bisimulations for the reduction of labeled Petri nets with silent moves. In: Proc. 6th Int. Conf. on Computing and Information, Peterborough, Canada. 1994 .
• [21] Quivrin-Pfister W. Des bisimulations de places pour la r´eduction des r´esaux de Petri. Phd thesis, I.N.P. de Grenoble, France, 1995.
• [22] Schnoebelen P, Sidorova N. Bisimulation and the Reduction of Petri Nets, pp. 409–423. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN:978-3-540-44988-1, 2000. doi:10.1007/3-540-44988-423.
• [23] Voorhoeve M. Structural Petri net equivalence. Technical Report 9607, Technische Universiteit Eindhoven, 1996.
• [24] Gorrieri R. Team bisimilarity, and its associated modal logic, for BPP nets. Acta Informatica, 2020. pp. 1–41.
• [25] Gorrieri R. A Study on Team Bisimulations for BPP Nets. In: Janicki R, Sidorova N, Chatain T (eds.), Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham, 2020 pp. 153–175. ISBN:978-3-030-51831-8.
• [26] Bashkin VA, Lomazova IA. Petri nets and resource bisimulation. Fundamenta Informaticae, 2003. 55(2):101–114.
• [27] Corradini F, De Nicola R, Labella A. Models of Nondeterministic Regular Expressions. Journal of Computer and System Sciences, 1999. 59(3):412 – 449. doi:10.1006/jcss.1999.1636.
• [28] Bashkin VA, Lomazova IA. Resource Similarities in Petri Net Models of Distributed Systems, pp. 35–48. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN:978-3-540-45145-7, 2003. doi:10.1007/978-3-540-45145-74.
• [29] Bashkin VA, Lomazova IA. Similarity of Generalized Resources in Petri Nets, pp. 27–41. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. ISBN:978-3-540-31826-2. doi:10.1007/115352943.
• [30] Lomazova IA. Resource Equivalences in Petri Nets. In: van der Aalst W, Best E (eds.), Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham, 2017 pp. 19–34. ISBN:978-3-319-57861-3.
• [31] Aceto L, Ingolfsdottir A, Srba J. The algorithmics of bisimilarity. In: Advanced Topics in Bisimulation and Coinduction. 2011. doi:10.1017/cbo9780511792588.004.
• [32] Hennessy M, Milner R. Algebraic Laws for Nondeterminism and Concurrency. J. ACM, 1985. 32(1):137–161. doi:10.1145/2455.2460.
• [33] Christensen S. Decidability and decomposition in process algebras. Ph.D. thesis, University of Edinburgh, UK, 1993. URL http://hdl.handle.net/1842/410.
• [34] Rédei L. The theory of finitely generated commutative semigroups. Oxford University Press, New-York, 1965.
• [35] Hirshfeld Y. Congruences in commutative semigroups. Technical Report ECS-LFCS-94-291, Department of Computer Science, University of Edinburgh, 1994.
• [36] Bashkin VA, Lomazova IA. Reduction of Coloured Petri Nets based on resource bisimulation. Joint Bulletin of NCC & IIS (Comp. Science), 2000. 13:12–17.
• [37] Srba J. Strong bisimilarity of simple process algebras: complexity lower bounds. Acta Informatica, 2003. 39(6-7):469–499. doi:10.1007/s00236-003-0116-9.