Проверка ослабленной ленивой бездефектности для сетей Петри с данными

Для представления модели, включающей как данные, так и ресурсы, можно использовать сети Петри с данными. Каждому переходу в таких сетях сопоставлено ограничение, включающее условия на входные и выходные значения переменных. Условия на входные значения определяют правила, при которых переход может сработать. Условия на выходные значения определяют правила, согласно которым осуществляется изменение значений переменных при срабатывании перехода. Чтобы оставаться в границах разрешимости, условия не должны содержать арифметические операции, ввиду чего ресурсы обычно представляются как отдельные позиции. Существующие критерии бездефектности, такие как простая, ослабленная и ленивая бездефектность, могут быть адаптированы к ресурсно-ориентированным сетям Петри с данными, но для их вычисления требуется решение проблемы достижимости, имеющей высокую вычислительную сложность даже для классических сетей Петри. В этой статье мы предлагаем новое свойство бездефектности, называемое ослабленной ленивой бездефектностью, которое включает в себя основные характеристики вышеупомянутых свойств и которое может быть определено путем решения проблемы покрытия, имеющей меньшую вычислительную сложность чем проблема достижимости. Мы представляем алгоритм для проверки данного свойства, доказываем его корректность и реализуем его в существующем наборе инструментов проверки бездефектности. Результаты оценки производительности подтверждают применимость алгоритма для верификации моделей среднего размера. Алгоритм можно использовать как для проверки ресурсно-ориентированных моделей, так и для предварительной проверки произвольных моделей, представленных сетями Петри с данными.

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.