Relaxed Lazy Soundness Verification for Data Petri Nets
https://doi.org/10.15514/ISPRAS-2025-37(4)-19
Abstract
To represent a model that includes both data and resource perspectives, Data Petri nets could be used. In this formalism, each transition has a constraint that includes input and output conditions on variables. To stay within decidability, the conditions should not contain arithmetic operations, so the resources are usually represented as separate places. Existing correctness criteria such as easy, relaxed and lazy soundness could be adapted to resource-oriented Data Petri nets but deciding them requires solving a reachability problem that is known to have very high complexity even for classical Petri nets. In this paper, we propose a new correctness notion called relaxed lazy soundness that incorporates the main features of the aforementioned properties and that could be decided as a coverability problem, which is known to be less computationally complex than the reachability one. We provide an algorithm to verify this property, prove its correctness, and implement it in the existing soundness verification toolkit. The performance evaluation results confirm the applicability of the algorithm to process models of a moderate size. The algorithm could be used both for verification of resource-oriented models and for preliminary validation of arbitrary process models represented as Data Petri nets.
Keywords
data Petri net,
verification of distributed processes with data,
soundness verification,
transition systems.
Supporting agencies: This study has been supported by the Basic Research Program at HSE University, Russia.
About the Authors
Nikolai Mikhailovich SUVOROV
HSE University
Russian Federation
Russian Federation
Postgraduate student at Doctoral School of Computer Science, HSE University, research fellow at Laboratory of Process-Aware Information Systems, Faculty of Computer Science, HSE University. Research interests: automata theory, distributed processes, and model verification and repair.
Irina Alexandrovna LOMAZOVA
HSE University
Russian Federation
Russian Federation
Dr. Sci. (Phys.-Math.), professor of the faculty of computer science in HSE University, and laboratory head of the Laboratory for Process-Aware Information Systems (PAIS Lab), HSE University. Doctor of Sciences in Theoretical Foundations of Computer Science Russian Academy of Sciences Dorodnitsyn Computation Center since 2002. Research interests mainly include analysis and modeling of business processes, Petri nets, process-oriented information systems, formal models of distributed systems.
References
1. Weske M. Business Process Management: Concepts, Languages, Architectures. Introduction. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 3–23.
2. van der Aalst W. M. P. Verification of workflow nets. In Application and Theory of Petri Nets 1997, 1997, pp. 407–426.
3. Martens A. Analyzing web service based business processes. In Fundamental Approaches to Software Engineering, 2005, pp. 19–33.
4. van Hee K. M., Sidorova N., Voorhoeve M. Soundness and separability of workflow nets in the stepwise refinement approach. In Applications and Theory of Petri Nets, 2003, pp. 337–356.
5. Dehnert J., Rittgen P. Relaxed soundness of business processes. In Advanced Information Systems Engineering, 2001, pp. 157–170.
6. Puhlmann F., Weske M. Investigations on soundness regarding lazy activities. In Business Process Management, 2006, pp. 145–160.
7. van der Aalst W. M. P., van Hee K. M., ter Hofstede A. H. M., Sidorova N., Verbeek H. M. W., Voorhoeve M., Wynn M. T. Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects of Computing, 23(3), 2011, pp. 333–363.
8. de Leoni M., van der Aalst W. M. P. Data-aware process mining: Discovering decisions in processes using alignments. In Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013,
9. pp. 1454–1461.
10. Mannhardt F. Multi-perspective process mining. Ph.D. dissertation, Eindhoven University of Technology, 2018.
11. de Leoni M., Felli P., Montali M. A holistic approach for soundness verification of decision-aware process models. In Conceptual Modeling, 2018, pp. 219–235.
12. Esparza J., Nielsen M. Decidability issues for Petri Nets. Information Processing and Cybernetics, 30(3), 1994, pp. 143-160.
13. Czerwinski W., Lasota S., Lazic R., Leroux J., Mazowiecki F. The reachability problem for Petri nets is not elementary. In STOC 2019, 2019, pp. 24–33.
14. Bazhenova E., Zerbato F., Oliboni B., Weske M. From bpmn process models to dmn decision models. Information Systems, vol. 83, 2019, pp. 69–88.
15. Knuplesch D., Ly L. T., Rinderle-Ma S., Pfeifer H., Dadam P. On enabling data-aware compliance checking of business process models. In Conceptual Modeling, 2010, pp. 332–346.
16. van der Aalst W. M. The application of petri nets to workflow management. Journal of Circuits, Systems and Computers, vol. 8, 1998, pp. 21–66.
17. Awad A., Decker G., Lohmann N. Diagnosing and repairing data anomalies in process models. In Business Process Management Workshops, 2010, pp. 5–16.
18. Sidorova N., Stahl C., Trcka N. Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible. Information Systems, 36(7) , 2011, pp. 1026–1043.
19. Felli P., de Leoni M., Montali M. Soundness verification of decision-aware process models with variable-to-variable conditions. In ACSD 2019, 2019, pp. 82–91.
20. Tao X., Liu G., Yang B., Yan C., Jiang C. Workflow nets with tables and their soundness. IEEE Transactions on Industrial Informatics, 16(3), 2020, pp. 1503–1515.
21. Song J., Liu G, Wang M. Model checking of workflow nets with tables and constraints. ACM Transactions on Autonomous and Adaptive Systems, 2025, 37p.
22. Felli P., Montali M., Winkler S. Soundness of data-aware processes with arithmetic conditions. In Advanced Information Systems Engineering, 2022, pp. 389–406.
23. Suvorov N. M., Lomazova I. A. Verification of data-aware process models: Checking soundness of data petri nets. Journal of Logical and Algebraic Methods in Programming, vol. 138, 100953, 2024.
24. Felli P., de Leoni M., Montali M. Soundness verification of data-aware process models with variable-to-variable conditions. Fundamental Informaticae, 182(1), 2021, pp. 1–29.
25. Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4), pp. 541–580, 1989.
26. Tarski A. A decision method for elementary algebra and geometry. Journal of Symbolic Logic, 14(3), pp. 188–188, 1949.
27. Lu F., Tao R., Du Y., Zeng Q., Bao Y. Deadlock detection-oriented unfolding of unbounded petri nets. Information Sciences, vol. 497, 2019, pp. 1–22.
28. Ding Z., Jiang C., Zhou M. Deadlock checking for one-place unbounded petri nets based on modified reachability trees. IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), 38(3), pp. 881–883, 2008.
29. Puhlmann F. Soundness verification of business processes specified in the pi-calculus. In On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE, GADA, and IS, 2007, pp. 6–23.
30. de Moura L., Bjørner N. Z3: An efficient smt solver. In TACAS, 2008, pp. 337–340.
31. Finkel A., Schnoebelen P. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1), 2001, pp. 63–92.
32. Felli P., Montali M., Winkler S. Repairing soundness properties in data-aware processes. In 2023 5th International Conference on Process Mining (ICPM), 2023, pp. 41–48.
Supplementary files
Review
For citations:
SUVOROV N.M., LOMAZOVA I.A. Relaxed Lazy Soundness Verification for Data Petri Nets. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(4):69-84. https://doi.org/10.15514/ISPRAS-2025-37(4)-19
Email this article 