Correctness Notions for Petri Nets with Identifiers

• Autorzy: van der Werf, Jan Martijn E. M. , Rivkin, Andrey , Montali, Marco , Polyvyanyy, Artem
• Języki publikacji: EN

Abstrakty

EN

A model of an information system describes its processes and how resources are involved in these processes to manipulate data objects. This paper presents an extension to the Petri nets formalism suitable for describing information systems in which states refer to object instances of predefined types and resources are identified as instances of special object types. Several correctness criteria for resource- and object-aware information systems models are proposed, supplemented with discussions on their decidability for interesting classes of systems. These new correctness criteria can be seen as generalizations of the classical soundness property of workflow models concerned with process control flow correctness.

Słowa kluczowe

EN

information System; verification; data correctness; resource correctness

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2024
• Tom: Vol. 190, nr 2-4
• Strony: 159--207
• Opis fizyczny: Bibliogr. 50 poz., rys.

Twórcy

autor

van der Werf, Jan Martijn E. M.

• Utrecht University,The Netherlands,

autor

Rivkin, Andrey

• Technical University of Denmark,

autor

Montali, Marco

• Free University of Bozen-Bolzano,

autor

Polyvyanyy, Artem

• The University of Melbourne, Australia,

Bibliografia

• [1] Reisig W. Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies. Springer Berlin Heidelberg, 2013. ISBN 978-3-642-33277-7. doi:10.1007/978-3-642-33278-4.
• [2] van Hee KM, Sidorova N, Voorhoeve M, van der Werf JMEM. Generation of Database Transactions with Petri Nets. Fundam. Inform., 2009. 93(1-3):171-184.
• [3] Karp RM, Miller RE. Parallel Program Schemata. J. Comput. Syst. Sci., 1969. 3(2):147-195. doi:10.1016/S0022-0000(69)80011-5.
• [4] Hack M. The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems. In: Proc. of SWAT 1974. IEEE Computer Society, 1974 pp. 156-164. doi:10.1109/SWAT.1974.28.
• [5] van der Aalst WMP. Verification of Workflow Nets. In: Proc. of Petri Nets, volume 1248 of LNCS.Springer, 1997 pp. 407-426. doi:10.1007/3-540-63139-9\ 48.
• [6] Polyvyanyy A, van der Werf JMEM, Overbeek S, Brouwers R. Information Systems Modeling: Language, Verification, and Tool Support. In: Proc. of CAiSE 2019, volume 11483 of LNCS. Springer, 2019 pp. 194-212. doi:10.1007/978-3-030-21290-2\ 13.
• [7] van der Werf JMEM, Polyvyanyy A. The Information Systems Modeling Suite - Modeling the Interplay Between Information and Processes. In: Proc. of Petri Nets 2020, volume 12152 of LNCS. Springer, 2020 pp. 414-425. doi:10.1007/978-3-030-51831-8 22.
• [8] van der Werf JMEM, Polyvyanyy A. An Assignment on Information System Modeling - On Teaching Data and Process Integration. In: Business Process Management Workshops, volume 342 of LNBIP. Springer, 2018 pp. 553-566. doi:10.1007/978-3-030-11641-5\ 44.
• [9] Glabbeek R. The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves. In: CONCUR 1993, volume 715 of LNCS. Springer, 1993 pp. 66-81.
• [10] van Hee KM, Sidorova N, Voorhoeve M. Soundness and Separability of Workflow Nets in the Stepwise Refinement Approach. In: Proc. of Petri Nets 2003, volume 2679 of LNCS. Springer, 2003 pp. 337-356. doi:10.1007/3-540-44919-1 22.
• [11] Fahland D. Describing Behavior of Processes with Many-to-Many Interactions. In: Proc. of Petri Nets 2019. Springer, 2019 pp. 3-24. doi:10.1007/978-3-030-21571-2 1.
• [12] Rosa-Velardo F, de Frutos-Escrig D. Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci., 2011. 412(34):4439-4451. doi:10.1016/j.tcs.2011.05.007
• [13] Rosa-Velardo F, Alonso OM, de Frutos-Escrig D. Mobile Synchronizing Petri Nets: A Choreographic Approach for Coordination in Ubiquitous Systems. Electron. Notes Theor. Comput. Sci., 2006. 150(1):103-126. doi:10.1016/j.entcs.2005.12.026. URL https://doi.org/10.1016/j.entcs.2005.12.026.
• [14] Rosa-Velardo F, de Frutos-Escrig D. Forward Analysis for Petri Nets with Name Creation. In: Applications and Theory of Petri Nets, volume 6128 of LNCS. Springer, Berlin, 2010 pp. 185-205. doi:10.1007/978-3-642-13675-7 12.
• [15] van Hee KM, Sidorova N, van der Werf JMEM. Business Process Modeling Using Petri Nets. Trans. Petri Nets Other Model. Concurr., 2013. 7:116-161. doi:10.1007/978-3-642-38143-0 4.
• [16] Lasota S. Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture. In: Kordon F, Moldt D (eds.), Proc. of Petri Nets 2016, volume 9698 of LNCS. Springer, 2016 pp. 20-36. doi:10.1007/978-3-319-39086-4\ 3.
• [17] Ghilardi S, Gianola A, Montali M, Rivkin A. Petri net-based object-centric processes with read-only data. Inf. Syst., 2022. 107:102011. doi:10.1016/j.is.2022.102011.
• [18] Lasota S. Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture. In: Kordon F, Moldt D (eds.), Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS 2016, Toru´n, Poland, June 19-24, 2016. Proceedings, volume 9698 of LNCS. Springer, 2016 pp. 20-36. doi:10.1007/978-3-319-39086-4 3.
• [19] Martos-Salgado M, Rosa-Velardo F. Dynamic Soundness in Resource-Constrained Workflow Nets. In: Formal Techniques for Distributed Systems. FMOODS FORTE, volume 6722 of LNCS. Springer, 2011 pp. 259-273. doi:10.1007/978-3-642-21461-5 17.
• [20] Montali M, Rivkin A. Model checking Petri nets with names using data-centric dynamic systems. Formal Aspects Comput., 2016. 28(4):615-641. doi:10.1007/s00165-016-0370-6.
• [21] Calvanese D, Giacomo GD, Montali M, Patrizi F. First-order μ-calculus over generic transition systems and applications to the situation calculus. Inf. Comput., 2018. 259(3):328-347. doi:10.1016/j.ic.2017.08.007.
• [22] Calvanese D, Giacomo GD, Montali M, Patrizi F. Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces. In: Raedt LD (ed.), Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022. ijcai.org, 2022 pp. 2553-2560. doi:10.24963/ijcai.2022/354.
• [23] Hariri BB, Calvanese D, Giacomo GD, Deutsch A, Montali M. Verification of relational data-centric dynamic systems with external services. In: Hull R, Fan W (eds.), Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY, USA -June 22 - 27, 2013. ACM, 2013 pp. 163-174. doi:10.1145/2463664.2465221.
• [24] Abiteboul S, Hull R, Vianu V. Foundations of Databases. Addison-Wesley, 1995. ISBN 0-201-53771-0.
• [25] van Hee KM, Oanea O, Post R, Somers LJ, van der Werf JMEM. Yasper: a tool for workflow modeling and analysis. In: Proc. of ACSD 2006. IEEE, 2006 pp. 279-282. doi:10.1109/ACSD.2006.37.
• [26] Montali M, Rivkin A. Model checking Petri nets with names using data-centric dynamic systems. Formal Aspects Comput., 2016. 28(4):615-641. doi:10.1007/s00165-016-0370-6. URL https://doi.org/10.1007/s00165-016-0370-6.
• [27] Leemans SJJ, Fahland D, van der Aalst WMP. Discovering Block-Structured Process Models from Event Logs - A Constructive Approach. In: Proc. of Petri Nets 2013, volume 7927 of LNCS. Springer, 2013 pp. 311-329. doi:10.1007/978-3-642-38697-8\ 17.
• [28] Weidlich M, Polyvyanyy A, Mendling J, Weske M. Causal Behavioural Profiles - Efficient Computation, Applications, and Evaluation. Fundam. Informaticae, 2011. 113(3-4):399-435. doi:10.3233/FI-2011-614.
• [29] van Hee KM, Hidders J, Houben GJ, Paredaens J, Thiran P. On the relationship between workflow models and document types. Information Systems, 2009. 34(1):178-208. doi:10.1016/j.is.2008.06.003.
• [30] Murata T. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 1989. 77(4):541-580.
• [31] Berthelot G. Verification de Reseaux de Petri. Ph.D. thesis, Universit´e Pierre et Marie Curie (Paris), 1978.
• [32] van Hee KM, Sidorova N, Voorhoeve M. Resource-Constrained Workflow Nets. Fundam. Inform., 2006.71(2-3):243-257.
• [33] Lomazova IA, Bashkin VA, Jancar P. Resource Bisimilarity in Petri Nets is Decidable. Fundam. Informaticae, 2022. 186(1-4):175-194. doi:10.3233/FI-222125.
• [34] Fahland D, Denisov V, van der Aalst WMP. Inferring Unobserved Events in Systems with Shared Resources and Queues. Fundam. Informaticae, 2021. 183(3-4):203-242. doi:10.3233/FI-2021-2087.
• [35] van der Aalst WMP. Object-Centric Process Mining: Dealing with Divergence and Convergence in Event Data. In: ¨Olveczky PC, Sala¨un G (eds.), Proc. of SEFM 2019, volume 11724 of Lecture Notes in Computer Science. Springer, 2019 pp. 3-25. doi:10.1007/978-3-030-30446-1\ 1.
• [36] Artale A, Kovtunova A, Montali M, van der Aalst WMP. Modeling and Reasoning over Declarative Data-Aware Processes with Object-Centric Behavioral Constraints. In: Proc. of BPM 2019, volume 11675 of LNCS. Springer, 2019 pp. 139-156. doi:10.1007/978-3-030-26619-6 11.
• [37] Montali M, Calvanese D. Soundness of Data-Aware, Case-Centric Processes. Int. Journal on Software Tools for Technology Transfer, 2016. doi:10.1007/s10009-016-0417-2.
• [38] Ghilardi S, Gianola A, Montali M, Rivkin A. Petri Nets with Parameterised Data - Modelling and Verification. In: Fahland D, Ghidini C, Becker J, Dumas M (eds.), BPM’20, volume 12168 of LNCS. Springer, 2020 pp. 55-74. doi:10.1007/978-3-030-58666-9\ 4.
• [39] Bagheri Hariri B, Calvanese D, Montali M, Deutsch A. State-Boundedness in Data-Aware Dynamic Systems. In: Proc. of KR 2014. AAAI Press, 2014 .
• [40] van der Aalst WMP, Berti A. Discovering Object-centric Petri Nets. Fundam. Informaticae, 2020. 175(1-4):1-40. doi:10.3233/FI-2020-1946.
• [41] Lomazova IA, Mitsyuk AA, Rivkin A. Soundness in Object-centric Workflow Petri Nets. CoRR, 2021.abs/2112.14994.
• [42] de Leoni M, Felli P, Montali M. A Holistic Approach for Soundness Verification of Decision-Aware Process Models. In: ER, volume 11157 of LNCS. Springer, 2018 pp. 219-235. doi:10.1007/978-3-030-00847-5 17.
• [43] Felli P, de Leoni M, Montali M. Soundness Verification of Decision-Aware Process Models with Variable-to-Variable Conditions. In: Proc. of ACSD 2019. IEEE, 2019 pp. 82-91. doi:10.1109/ACSD.2019.00013.
• [44] de Leoni M, Felli P, Montali M. Strategy Synthesis for Data-Aware Dynamic Systems with Multiple Actors. In: KR. 2020 pp. 315-325. doi:10.24963/kr.2020/32.
• [45] Haarmann S, Weske M. Cross-Case Data Objects in Business Processes: Semantics and Analysis. In: BPM (Forum), volume 392 of Lecture Notes in Business Information Processing. Springer, 2020 pp. 3-17. doi:10.1007/978-3-030-58638-6 1.
• [46] Haarmann S, Montali M, Weske M. Technical Report: Refining Case Models Using Cardinality Constraints. CoRR, 2020. abs/2012.02245.
• [47] Barkaoui K, Benayed R, Sbai Z. Workflow Soundness Verification Based on Structure Theory of Petri Nets. International Journal of Computing and Information Sciences (IJCIS), 2007. 5:51-62.
• [48] van Hee KM, Serebrenik A, Sidorova N, Voorhoeve M. Soundness of Resource-Constrained Workflow Nets. In: ICATPN, volume 3536 of LNCS. Springer, 2005 pp. 250-267. doi:10.1007/11494744 15.
• [49] Sidorova N, Stahl C. Soundness for Resource-Constrained Workflow Nets Is Decidable. IEEE Trans. Syst. Man Cybern. Syst., 2013. 43(3):724-729. doi:10.1109/TSMCA.2012.2210415.
• [50] Felli P, Montali M, Winkler S. Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic. In: Proc. of AAAI 2022. AAAI Press, 2022.

Identyfikatory

DOI

10.3233/FI-242169