{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T14:42:25Z","timestamp":1768488145582,"version":"3.49.0"},"reference-count":29,"publisher":"Emerald","issue":"1","license":[{"start":{"date-parts":[[2009,2,6]],"date-time":"2009-02-06T00:00:00Z","timestamp":1233878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.emerald.com\/insight\/site-policies"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,2,6]]},"abstract":"<jats:sec><jats:title content-type=\"abstract-heading\">Purpose<\/jats:title><jats:p>The purpose of this paper is to demonstrate that process verification has matured to a level where it can be used in practice. This paper reports on new verification techniques that can be used to assess the correctness of real\u2010life models.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Design\/methodology\/approach<\/jats:title><jats:p>The proposed approach relies on using formal methods to determine the correctness of business processes with cancellation and OR\u2010joins. The paper also demonstrates how reduction rules can be used to improve the efficiency. These techniques are presented in the context of the workflow language yet another workflow language (YAWL) that provides direct support for 20 most frequently used patterns found today (including cancellation and OR\u2010joins). But the results also apply to other languages with these features (e.g. BPMN, EPCs, UML activity diagrams, etc.). An editor has been developed that provides diagnostic information based on the techniques presented in this paper.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Findings<\/jats:title><jats:p>The paper proposes four properties for business processes with cancellation and OR\u2010joins, namely: soundness, weak soundness, irreducible cancellation regions and immutable OR\u2010joins and develop new techniques to verify these properties. Reduction rules have been used as a means of improving the efficiency of the algorithm. The paper demonstrates the feasibility of this verification approach using a realistic and complex business process, the visa application process for general skilled migration to Australia, modelled as a YAWL workflow with cancellation regions and OR\u2010joins.<\/jats:p><\/jats:sec><jats:sec><jats:title content-type=\"abstract-heading\">Originality\/value<\/jats:title><jats:p>Business processes sometimes require complex execution interdependencies to properly complete a process. For instance, it is possible that certain activities need to be cancelled mid\u2010way though the process. Some parallel activities may require complex \u201cwait and see\u201d style synchronisation depending on a given context. These types of business processes can be found in various domains, such as application integration, B2B commerce, web service composition and workflow systems. Even though cancellation and sophisticated join structures are present in many business processes, existing verification techniques are unable to deal with such processes. Hence, this paper plays an important role in making process verification a reality.<\/jats:p><\/jats:sec>","DOI":"10.1108\/14637150910931479","type":"journal-article","created":{"date-parts":[[2009,1,31]],"date-time":"2009-01-31T07:06:04Z","timestamp":1233385564000},"page":"74-92","source":"Crossref","is-referenced-by-count":95,"title":["Business process verification \u2013 finally a reality!"],"prefix":"10.1108","volume":"15","author":[{"given":"M.T.","family":"Wynn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.M.W.","family":"Verbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.M.P.","family":"van der Aalst","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.H.M.","family":"ter Hofstede","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Edmond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","reference":[{"key":"key2022031119474839300_b7","unstructured":"Berthelot, G. (1986), \u201cTransformations and decompositions of nets\u201d, in Brauer, W., Reisig, W. and Rozenberg, G. (Eds), Petri Nets: Central Models and Their Properties, Advances in Petri Nets, Proceedings of an Advanced Course, Part 1, Vol. 254 of Lecture Notes in Computer Science, Springer\u2010Verlag, Bad Honnef, pp. 359\u201076."},{"key":"key2022031119474839300_b8","doi-asserted-by":"crossref","unstructured":"Bi, H. and Zhao, J. (2004), \u201cApplying propositional logic to workflow verification\u201d, Information Technology and Management, Vol. 5 Nos 3\u20104, pp. 293\u2010318.","DOI":"10.1023\/B:ITEM.0000031583.16306.0f"},{"key":"key2022031119474839300_b9","doi-asserted-by":"crossref","unstructured":"Choi, Y. and Zhao, J. (2005), \u201cDecomposition\u2010based verification of cyclic workflows\u201d, in Peled, D. and Tsay, Y.\u2010K. (Eds), Proceedings of Automated Technology for Verification and Analysis (ATVA 2005), Vol. 3707 of Lecture Notes in Computer Science, Springer\u2010Verlag, Taipei, pp. 84\u201098.","DOI":"10.1007\/11562948_9"},{"key":"key2022031119474839300_b10","unstructured":"Dehnert, J. and Rittgen, P. (2001), \u201cRelaxed soundness of business processes\u201d, in Dittrich, K., Geppert, A. and Norrie, M. (Eds), Proceedings of the 13th International Conference on Advanced Information Systems Engineering (CAiSE'01), Vol. 2068 of Lecture Notes in Computer Science, Springer\u2010Verlag, London, pp. 157\u201070."},{"key":"key2022031119474839300_b11","doi-asserted-by":"crossref","unstructured":"Desel, J. and Esparza, J. (1995), Free Choice Petri Nets, Vol. 40 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge.","DOI":"10.1017\/CBO9780511526558"},{"key":"key2022031119474839300_b13","doi-asserted-by":"crossref","unstructured":"Dufourd, C., Finkel, A. and Schnoebelen, P. (1998), \u201cReset nets between decidability and undecidability\u201d, in Larsen, K., Skyum, S. and Winskel, G. (Eds), Proceedings of the 25th International Colloquium on Automata, Languages and Programming, Vol. 1443 of Lecture Notes in Computer Science, Vol. 1443, Springer\u2010Verlag, Aalborg, pp. 103\u201015.","DOI":"10.1007\/BFb0055044"},{"key":"key2022031119474839300_b14","doi-asserted-by":"crossref","unstructured":"Dufourd, C., Jan\u02c7car, P. and Schnoebelen, P. (1999), \u201cBoundedness of reset P\/T nets\u201d, in Wiedermann, J., Boas, P. and Nielsen, M. (Eds), Lectures on Concurrency and Petri Nets, Vol. 1644 of Lecture Notes in Computer Science, Springer\u2010Verlag, Prague, Czech Republic, pp. 301\u201010.","DOI":"10.1007\/3-540-48523-6_27"},{"key":"key2022031119474839300_b15","doi-asserted-by":"crossref","unstructured":"Finkel, A. and Schnoebelen, P. (2001), \u201cWell\u2010structured transition systems everywhere!\u201d, Theoretical Computer Science, Vol. 256 Nos 1\u20102, pp. 63\u201092.","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"key2022031119474839300_b16","unstructured":"Hee, K., Sidorova, N. and Voorhoeve, M. (2004), \u201cGeneralised soundness of workflow nets is decidable\u201d, in Cortadella, J. and Reisig, W. (Eds), Application and Theory of Petri Nets 2004, Vol. 3099 of Lecture Notes in Computer Science, Springer\u2010Verlag, New York, NY."},{"key":"key2022031119474839300_b17","doi-asserted-by":"crossref","unstructured":"Kindler, E., Martens, A. and Reisig, W. (2000), \u201cInter\u2010operability of workflow applications: local criteria for global soundness\u201d, in van der Aalst, W., Desel, J. and Oberweis, A. (Eds), Business Process Management: Models, Techniques, and Empirical Studies, Vol. 1806 of Lecture Notes in Computer Science, Springer\u2010Verlag, Berlin, pp. 235\u201053.","DOI":"10.1007\/3-540-45594-9_15"},{"key":"key2022031119474839300_b18","doi-asserted-by":"crossref","unstructured":"Mendling, J., Moser, M., Neumann, G., Verbeek, H., Dongen, B. and van der Aalst, W. (2006), \u201cFaulty EPCs in the SAP reference model\u201d, in Dustdar, S., Faideiro, J. and Sheth, A. (Eds) International Conference on Business Process Management (BPM 2006), Vol. 4102 of Lecture Notes in Computer Science, Springer\u2010Verlag, pp. 451\u20107.","DOI":"10.1007\/11841760_38"},{"key":"key2022031119474839300_b19","doi-asserted-by":"crossref","unstructured":"Murata, T. (1989), \u201cPetri nets: properties, analysis and applications\u201d, Proceedings of the IEEE, Vol. 77 No. 4, pp. 541\u201080.","DOI":"10.1109\/5.24143"},{"key":"key2022031119474839300_b20","unstructured":"Sadiq, W. and Orlowska, M. (1997), \u201cOn correctness issues in conceptual modeling of workflows\u201d, Proceedings of the 5th European Conference on Information Systems (ECIS' 97), Cork, Ireland, pp. 19\u201021."},{"key":"key2022031119474839300_b21","unstructured":"Sadiq, W. and Orlowska, M. (1999), \u201cApplying graph reduction techniques for identifying structural conflicts in process models\u201d, in Jarke, M. and Oberweis, A. (Eds), Proceedings of the 11th Conference on Advanced Information Systems Engineering (CAiSE 1999), Vol. 1626 of Lecture Notes in Computer Science, Springer\u2010Verlag, Heidelberg, pp. 195\u2010209."},{"key":"key2022031119474839300_b22","doi-asserted-by":"crossref","unstructured":"Sloan, R. and Buy, U. (1996), \u201cReduction rules for time Petri nets\u201d, Acta Informatica, Vol. 33 No. 7, pp. 687\u2010706.","DOI":"10.1007\/s002360050066"},{"key":"key2022031119474839300_b1","doi-asserted-by":"crossref","unstructured":"van der Aalst, W. (1997), \u201cVerification of workflow nets\u201d, in Az\u00e7ema, P. and Balbo, G. (Eds), Proceedings of Application and Theory of Petri Nets, Vol. 1248 of Lecture Notes in Computer Science, Springer\u2010Verlag, Toulouse, pp. 407\u201026.","DOI":"10.1007\/3-540-63139-9_48"},{"key":"key2022031119474839300_b2","doi-asserted-by":"crossref","unstructured":"van der Aalst, W. (1998), \u201cThe application of Petri nets to workflow management\u201d, The Journal of Circuits, Systems and Computers, Vol. 8 No. 1, pp. 21\u201066.","DOI":"10.1142\/S0218126698000043"},{"key":"key2022031119474839300_b3","doi-asserted-by":"crossref","unstructured":"van der Aalst, W. (2000), \u201cWorkflow verification: finding control\u2010flow errors using Petri net\u2010based techniques\u201d, in van der Aalst, W., Desel, J. and Oberweis, A. (Eds), Proceedings of Business Process Management: Models, Techniques and Empirical Studies, Vol. 1806 of Lecture Notes in Computer Science, Springer\u2010Verlag, Berlin, pp. 161\u201083.","DOI":"10.1007\/3-540-45594-9_11"},{"key":"key2022031119474839300_b4","doi-asserted-by":"crossref","unstructured":"van der Aalst, W. and ter Hofstede, A. (2005), \u201cYAWL: yet another workflow language\u201d, Information Systems, Vol. 30 No. 4, pp. 245\u201075.","DOI":"10.1016\/j.is.2004.02.002"},{"key":"key2022031119474839300_b5","doi-asserted-by":"crossref","unstructured":"van der Aalst, W., ter Hofstede, A., Kiepuszewski, B. and Barros, A. (2003), \u201cWorkflow patterns\u201d, Distributed and Parallel Databases, Vol. 14, pp. 5\u201051.","DOI":"10.1023\/A:1022883727209"},{"key":"key2022031119474839300_b6","unstructured":"van der Aalst, W. and van Hee, K. (2004), Workflow Management: Models, Methods and Systems, MIT Press, Cambridge, MA."},{"key":"key2022031119474839300_b12","doi-asserted-by":"crossref","unstructured":"van Dongen, B., van der Aalst, W. and Verbeek, H. (2005), \u201cVerification of EPCs: using reduction rules and Petri nets\u201d, in Pastor, O. and e Cunha, J.F. (Eds), Proceedings of the 17th Conference on Advanced Information Systems Engineering (CAiSE 2005), Vol. 3520 of Lecture Notes in Computer Science, Springer\u2010Verlag, Porto, pp. 372\u201086.","DOI":"10.1007\/11431855_26"},{"key":"key2022031119474839300_b23","unstructured":"Verbeek, H. (2004), \u201cVerification of WF\u2010nets\u201d, PhD thesis, Eindhoven University of Technology, Eindhoven."},{"key":"key2022031119474839300_b24","doi-asserted-by":"crossref","unstructured":"Verbeek, H., Basten, T. and van der Aalst, W. (2001), \u201cDiagnosing workflow processes using Woflan\u201d, The Computer Journal, Vol. 44 No. 4, pp. 246\u201079.","DOI":"10.1093\/comjnl\/44.4.246"},{"key":"key2022031119474839300_b25","doi-asserted-by":"crossref","unstructured":"Verbeek, H., van der Aalst, W. and ter Hofstede, A. (2006), \u201cVerifying workflows with cancellation regions and OR\u2010joins: an approach based on relaxed soundness and invariants\u201d, The Computer Journal, Vol. 50 No. 3, pp. 294\u2010314.","DOI":"10.1093\/comjnl\/bxl074"},{"key":"key2022031119474839300_b26","unstructured":"Wynn, M. (2006), \u201cSemantics, verification, and implementation of workflows with cancellation regions and OR\u2010joins\u201d, PhD thesis, Faculty of Information Technology, Queensland University of Technology, Brisbane."},{"key":"key2022031119474839300_b27","doi-asserted-by":"crossref","unstructured":"Wynn, M., Edmond, D., van der Aalst, W. and ter Hofstede, A. (2005), \u201cAchieving a general, formal and decidable approach to the OR\u2010join in workflow using reset nets\u201d, in Ciardo, G. and Darondeau, P. (Eds), Proceedings of ATPN, Vol. 3536 of Lecture Notes in Computer Science, Springer\u2010Verlag, Miami, FL, pp. 423\u201043.","DOI":"10.1007\/11494744_24"},{"key":"key2022031119474839300_b28","unstructured":"Wynn, M., Verbeek, H., van der Aalst, W., ter Hofstede, A. and Edmond, D. (2006a), \u201cReduction rules for reset workflow nets\u201d, Technical report BPM\u201006\u201025, BPM Center, available at: bpmcenter.org."},{"key":"key2022031119474839300_b29","unstructured":"Wynn, M., Verbeek, H., van der Aalst, W., ter Hofstede, A. and Edmond, D. (2006b), \u201cReduction rules for workflows with cancellation regions and OR\u2010joins\u201d, Technical report BPM\u201006\u201024, BPM Center, availble at: bpmcenter.org."}],"container-title":["Business Process Management Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.emeraldinsight.com\/doi\/full-xml\/10.1108\/14637150910931479","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/14637150910931479\/full\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/14637150910931479\/full\/html","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T00:36:11Z","timestamp":1753403771000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.emerald.com\/bpmj\/article\/15\/1\/74-92\/256886"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,6]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2,6]]}},"alternative-id":["10.1108\/14637150910931479"],"URL":"https:\/\/doi.org\/10.1108\/14637150910931479","relation":{},"ISSN":["1463-7154"],"issn-type":[{"value":"1463-7154","type":"print"}],"subject":[],"published":{"date-parts":[[2009,2,6]]}}}