Complexity of the Soundness Problem of Workflow Nets

• Autorzy: Liu G. J. , Sun J. , Liu Y. , Dong J. S.

Identyfikatory

DOI

10.3233/FI-2014-1005

• Języki publikacji: EN

Abstrakty

EN

Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones.

Słowa kluczowe

EN

workflow nets; soundness; complexity; PSPACE-hardness; co-NP-hardness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 131, nr 1
• Strony: 81--101
• Opis fizyczny: Bibliogr. 27 poz., rys., tab.

Twórcy

autor

Liu G. J.

• Department of Computer Science and Technology, Tongji University, Shanghai 201804, China

autor

Sun J.

• ISTD, Singapore University of Technology and Design, Singapore 138682, Singapore

autor

Liu Y.

• School of Computer Engineering, Nanyang Technological University, Singapore 639798, Singapore

autor

Dong J. S.

• School of Computing, National University of Singapore, Singapore 117417, Singapore

Bibliografia

• [1] van der Aalst, W.: Structural Characterizations of Sound Workflow Nets, Computing science report 96/23, Eindhoven University of Technology, Eindhoven, 1996.
• [2] van der Aalst, W.: Interorganizational Workflows: An Approach Based on Message Sequence Charts and Petri Nets, System Analysis and Modeling, 34, 1999, 335–367.
• [3] van der Aalst, W.: Loosely Coupled Interorganizational Wokflows: Modeling and Analyzing Workflows Crossing Organizational Boundaries, Information and Management, 37, 2000, 67–75.
• [4] van der Aalst, W., van Hee, K., ter Hofstede, A., Sidorova, N., Verbeek, H., Voorhoeve, M., Wynn, M.: Soundness of Workflow Nets: Classification, Decidability, and Analysis, Formal Aspects of Computing, 23, 2011, 333–363.
• [5] Barkaoui, K., Ayed, R. B., Sbai, Z.: Workflow soundness verification based on structure theory of Petri nets, Int. J. Comput. Inf. Sci., 5, 2007, 51–61.
• [6] Cheng, A., Esparza, J., Palsberg, J.: Complexity Results for 1-safe Nets, Theoretical Computer Science, 147, 1995, 117–136.
• [7] Chu, F., Xie, X.: Deadlock Analysis of Petri Nets Using Siphons and Mathematical Programming, IEEE Transactions on Robotics and Automation, 13, 1997, 793C–804.
• [8] Desel, J., Esparza, J.: Free Choice Petri Nets, Cambridge University Press, Cambridge, UK, 1995.
• [9] Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets between Decidability and Undecidability, ICALP (K. Larsen, S. Skyum, G. Winskel, Eds.), LNCS 1433, Springer, 1998.
• [10] Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of Reset P/T Nets, ICALP (J. Wiedermann, P. van emde Boas, M. Nielsen, Eds.), LNCS 1644, Springer, 1999.
• [11] Garey, M., Johnson, D.: Computer and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman and Company, 1976.
• [12] Hack, M.: Petri Net Languages, Technical report 159, Massachusetts Institute of Technology, Cambridge, USA, 1976.
• [13] van Hee, K., Sidorova, N., Voorhoeve, M.: Generalized Soundness of Workflow Nets is Decidable, ICATPN (J. Cortadella, W. Reisig, Eds.), LNCS 3099, Springer, 2004.
• [14] van Hee, K., Sidorova, N., Voorhoeve, M.: Resource-constrained workflow nets, Fundamenta Informaticae, 71, 2006, 243–257.
• [15] Jones, N., Landweber, L., Lien, Y.: Complexity of some problems in Petri nets, Theoretical Computer Science, 4, 1977, 277–299.
• [16] Kang,M., Park, J., Froscher, J.: Access Control Mechanisms for Inter-organizational Workflow, Proceedings of the sixth ACM symposium on Access control models and technologies, 2001.
• [17] Kindler, E.: The ePNK: An Extensible Petri Net Tool for PNML, ICATPN (L. Kristensen, L. Petrucci, Eds.), LNCS 6709, Springer, 2011.
• [18] Kindler, E., Martens, A., Reisig, W.: Inter-operability of Workflow Applications: Local Criteria for Global Soundness, BPMMTES (W. van der Aalst, J. Desel, A. Oberweis, Eds.), LNCS 1806, Springer, 2000.
• [19] Lipton, R. J.: The Reachability Problem Requires Exponential Space, Research report 62, Department of Computer Science, Yale University, 1976.
• [20] Liu, G., Sun, J., Liu, Y., Dong, J.: Complexity of the Soundness Problem of Bounded Workflow Nets, ICATPN (S. Haddad, L. Pomello, Eds.), LNCS 7347, Springer, 2012.
• [21] Murata, T.: Petri nets: properties, analysis, and applications, Proc. of IEEE, 77, 1989, 541–580.
• [22] Ohta, A., Tsuji, K.: NP-hardness of Liveness Problem of Bounded Asymmetric Choice Net, IEICE Trans. Fundamentals, E85-A, 2002, 1071–1074.
• [23] Reisig, W.: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies, Springer-Verlag Berlin Heidelberg, 2013.
• [24] Tiplea, F., Bocaneala, C.: Decidability Results for Soundness Criteria of Resource-Constrained Workflow Nets, IEEE Trans. on Systems, man, and Cybernetics, Part A: Systems and Humans, 42, 2011, 238–249.
• [25] Verbeek, H., van der Aalst, W., ter Hofstede, A.: Verifying Worklows with Cancellation Regions and ORjoins: An Approach Based on Relaxed Soundness and Invariants, Computer Journal, 50, 2007, 294–314.
• [26] Verbeek, H., Wynn, M., van der Aalst, W., ter Hofstede, A.: Reduction Rules for Reset/Inhibitor Nets, Journal of Computer and System Science, 76, 2010, 125–143.
• [27] van der Vlugt, S., Kleijn, J., Koutny, M.: Coverability and Inhibitor Arcs: An Example, Technical report cs-tr-1293, Newcastle University, England, 2011.