Abstract
Classical workflow nets (WF-nets) are an important class of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property that guarantees these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable, and proposed (but not proved) that the soundness problem is EXPSPACE-hard. In this paper, we show that the satisfiability problem of Boolean expression is polynomial time reducible to the liveness problem of bounded WF-nets, and soundness and liveness are equivalent for bounded WF-nets. As a result, the soundness problem of bounded WF-nets is co-NP-hard.
Workflow nets with reset arcs (reWF-nets) are an extension to WF-nets, which enhance the expressiveness of WF-nets. Aalst et al. proved that the soundness problem of reWF-nets is undecidable. In this paper, we show that for bounded reWF-nets, the soundness problem is decidable and equivalent to the liveness problem. Furthermore, a bounded reWF-net can be constructed in polynomial time for every linear bounded automaton (LBA) with an input string, and we prove that the LBA accepts the input string if and only if the constructed reWF-net is live. As a result, the soundness problem of bounded reWF-nets is PSPACE-hard.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Van der Aalst, W.M.P.: Interorganizational Workflows: An Approach Based on Message Sequence Charts and Petri Nets. System Analysis and Modeling 34, 335–367 (1999)
Van der Aalst, W.M.P.: Loosely Coupled Interorganizational Wokflows: Modeling and Analyzing Workflows Crossing Organizational Boundaries. Inf. Manage. 37, 67–75 (2000)
Van der Aalst, W.M.P.: Structural Characterizations of Sound Workflow Nets. Computing Science Report 96/23, Eindhoven University of Technology (1996)
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, 333–363 (2011)
Cheng, A., Esparza, J., Palsberg, J.: Complexity Results for 1-safe Nets. Theoretical Computer Science 147, 117–136 (1995)
Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science, vol. 40. Cambridge University Press, Cambridge (1995)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of Reset P/T Nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)
Garey, M.R., Johnson, D.S.: Computer and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company (1976)
Hack, M.: Petri Net Languages. Technical Report 159. MIT (1976)
van Hee, K.M., Sidorova, N., Voorhoeve, M.: Generalised Soundness of Workflow Nets Is Decidable. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 197–215. Springer, Heidelberg (2004)
Kang, M.H., Park, J.S., Froscher, J.N.: Access Control Mechanisms for Inter-organizational Workflow. In: Proc. of the Sixth ACM Symposium on Access Control Models and Technologies, pp. 66–74. ACM Press, New York (2001)
Kindler, E.: The ePNK: An Extensible Petri Net Tool for PNML. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 318–327. Springer, Heidelberg (2011)
Kindler, E., Martens, A., Reisig, W.: Inter-operability of Workflow Applications: Local Criteria for Global Soundness. In: van der Aalst, W.M.P., Desel, J., Oberweis, A. (eds.) BPM 2000. LNCS, vol. 1806, pp. 235–253. Springer, Heidelberg (2000)
Ohta, A., Tsuji, K.: NP-hardness of Liveness Problem of Bounded Asymmetric Choice Net. IEICE Trans. Fundamentals E85-A, 1071–1074 (2002)
Tiplea, F.L., 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, 238–249 (2011)
Verbeek, H.M.W., Van der Aalst, W.M.P., Ter Hofstede, A.H.M.: Verifying Worklows with Cancellation Regions and OR-joins: An Approach Based on Relaxed Soundness and Invariants. Computer Journal 50, 294–314 (2007)
Verbeek, H.M.W., Wynn, M.T., Van der Aalst, W.M.P., Ter Hofstede, A.H.M.: Reduction Rules for Reset/Inhibitor Nets. BMP Center Report BMP-07-13, BMP-center.org (2007)
Van der Vlugt, S., Kleijn, J., Koutny, M.: Coverability and Inhibitor Arcs: An Example. Technical Report 1293, University of Newcastle Upon Tyne (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, G.J., Sun, J., Liu, Y., Dong, J.S. (2012). Complexity of the Soundness Problem of Bounded Workflow Nets. In: Haddad, S., Pomello, L. (eds) Application and Theory of Petri Nets. PETRI NETS 2012. Lecture Notes in Computer Science, vol 7347. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31131-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-31131-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31130-7
Online ISBN: 978-3-642-31131-4
eBook Packages: Computer ScienceComputer Science (R0)