Abstract
Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternative notions of soundness and have suggested to use more expressive languages, e.g., models with cancellations or priorities. This paper provides an overview of the different notions of soundness and investigates these in the presence of different extensions of workflow nets. We will show that the eight soundness notions described in the literature are decidable for workflow nets. However, most extensions will make all of these notions undecidable. These new results show the theoretical limits of workflow verification. Moreover, we discuss some of the analysis approaches described in the literature.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
van der Aalst WMP (1997) Verification of workflow nets. In: Azéma P, Balbo G (eds) Application and theory of Petri nets 1997. Lecture notes in computer science, vol 1248. Springer-Verlag, Berlin, pp 407–426
van der Aalst WMP (1998) The application of Petri nets to workflow management. J Circ Syst Comput 8(1): 21–66
van der Aalst WMP (2000) Workflow verification: finding control-flow errors using Petri-net-based techniques. In: Aalst WMP, Desel J, Oberweis A (eds) Business process management: models, techniques, and empirical studies. Lecture notes in computer science, vol 1806. Springer-Verlag, Berlin, pp 161–183
van der Aalst WMP, van Hee KM (2004) Workflow management: models, methods, and systems. MIT press, Cambridge
van der Aalst WMP, ter Hofstede AHM (2005) YAWL: yet another workflow language. Inf Syst 30(4): 245–275
van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2008) Soundness of workflow nets: classification, decidability, and analysis. Computer Science report no. 08-13. Technische Universiteit Eindhoven, The Netherlands
van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2009) Soundness of workflow nets with reset arcs. In: Jensen K, Billington J, Koutny M (eds) Transactions on Petri nets and other models of Concurrency III. Lecture notes in computer science, vol 5800. Springer-Verlag, Berlin, pp 50–70
van der Aalst WMP, ter Hofstede AHM, Kiepuszewski B, Barros AP (2003) Workflow patterns. Distrib Parallel Databases 14(1): 5–51
van der Aalst WMP, Hirnschall A, Verbeek HMW (2002) An alternative way to analyze workflow graphs. In: Banks-Pidduck A, Mylopoulos J, Woo CC, Ozsu MT (eds) Proceedings of the 14th international conference on advanced information systems engineering (CAiSE’02). Lecture notes in computer science, vol 2348. Springer-Verlag, Berlin, pp 535–552
van der Aalst WMP, Lohmann N, Massuthe P, Stahl C, Wolf K (2008) From public views to private views: correctness-by-design for services. In: Dumas M, Heckel H (eds) Proceedings of the 4th international workshop on Web services and formal methods (WS-FM 2007). Lecture notes in computer science, vol 4937. Springer-Verlag, Berlin, pp 139–153
van der Aalst WMP, Mooij AJ, Stahl C, Wolf K (2009) Service interaction: patterns, formalization, and analysis. In: Bernardo M, Padovani L, Zavattaro G (eds) Formal methods for Web services. Lecture notes in computer science, vol 5569. Springer-Verlag, Berlin, pp 42–88
Basu A, Blanning RW (2000) A formal approach to workflow analysis. Inf Syst Res 11(1): 17–36
Berthelot G (1987) Transformations and decompositions of nets. In: Brauer W, Reisig W, Rozenberg G (eds) Advances in Petri nets 1986. Part I: Petri nets, central models and their properties. Lecture notes in computer science, vol 254. Springer-Verlag, Berlin, pp 360–376
Basu A, Kumar A (2002) Research commentary: workflow management issues in e-business. Inf Syst Res 13(1): 1–14
Barkaoui K, Petrucci L (1998) Structural analysis of workflow nets with shared resources. In: van der Aalst WMP, De Michelis G, Ellis CA (eds) Proceedings of workflow management: net-based concepts, models, techniques and tools (WFM’98), vol 98/7 of Computing science reports, Lisbon, Portugal. Eindhoven University of Technology, Eindhoven, pp 82–95
Bi HH, Zhao JL (2004) Applying propositional logic to workflow verification. Inf Technol Manag 5(3–4): 293–318
Chrzastowski-Wachtel P (1999) Testing undecidability of the reachability in Petri nets with the help of 10th Hilbert problem. In: Donatelli S, Kleijn J (eds) Application and theory of Petri nets. Lecture notes in computer science, vol 1639. Springer-Verlag, Berlin, pp 268–281
Dehnert J, van der Aalst WMP (2004) Bridging the gap between business models and workflow specifications. Int J Coop Inf Syst 13(3): 289–332
Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE ’99: proceedings of the 21st international conference on software engineering, Los Alamitos, CA, USA. IEEE Computer Society Press, pp 411–420
Dumas M, van der Aalst WMP, ter Hofstede AHM (2005) Process-aware information systems: bridging people and software through process technology. Wiley, Hoboken, New Jersey
van Dongen BF, van der Aalst WMP, Verbeek HMW (2005) Verification of EPCs: using reduction rules and Petri nets. In: Pastor O, Falcão e Cunha J (eds) Proceedings of the 17th conference on advanced information systems engineering (CAiSE’05). Lecture notes in computer science, vol 3520. Springer-Verlag, Berlin, pp 372–386
Desel J, Esparza J (1995) Free choice Petri nets. In: Cambridge tracts in theoretical computer science, vol 40. Cambridge University Press, Cambridge
Dufourd C, Finkel A, Schnoebelen Ph (1998) Reset nets between decidability and undecidability. In: Larsen K, Skyum S, Winskel G (eds) Proceedings of the 25th international colloquium on automata, languages and programming. Lecture notes in computer science, vol 1443. Springer-Verlag, Berlin, pp 103–115
Dufourd C, Jančar P, Schnoebelen Ph (1999) Boundedness of reset P/T nets. In: Wiedermann J, Emde Boas P, Nielsen M (eds) Lectures on concurrency and Petri nets Lecture notes. in computer science, vol 1644. Springer-Verlag, Berlin, pp 301–310
Dehnert J, Rittgen P (2001) Relaxed soundness of business processes. In: Dittrich KR, Geppert A, Norrie MC (eds) Proceedings of the 13th international conference on advanced information systems engineering (CAiSE’01). Lecture notes in computer science, vol 2068. Springer-Verlag, Berlin, pp 157–170
Esparza J, Nielsen M (1994) Decidability issues for Petri nets: a survey. J Inf Process Cybern 30: 143–160
Esparza J (1998) Decidability and complexity of Petri net problems: an introduction. In: Reisig W, Rozenberg G (eds) Lectures on Petri nets I: basic models. Lecture notes in computer science, vol 1491. Springer-Verlag, Berlin, pp 374–428
Esparza J (1998) Reachability in live and safe free-choice Petri nets is NP-complete. Theor Comput Sci 198(1–2): 211–224
Fu X, Bultan T, Su J (2002) Formal verification of e-Services and workflows. In: Bussler C, Hull R, McIlraith S, Orlowska M, Pernici B, Yang J (eds) Web services, E-business, and the semantic web, CAiSE 2002 international workshop (WES 2002). Lecture notes in computer science, vol 2512. Springer-Verlag, Berlin, pp 188–202
Fu X, Bultan T, Su J (2004) Analysis of interacting BPEL Web services. In: International World Wide Web conference: proceedings of the 13th international conference on World Wide Web, New York. ACM Press, pp 621–630
Fahland D, Favre C, Jobstmann B, Koehler J, Lohmann N, Voelzer H, Wolf K (2009) Instantaneous soundness checking of industrial business process models. In: Dayal U, Eder J, Koehler J, Reijers H (eds) Business process management (BPM 2009). Lecture notes in computer science, vol 5701. Springer-Verlag, Berlin, pp 278–293
Finkel A, Schnoebelen Ph (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1–2): 63–92
Georgakopoulos D, Hornick M, Sheth A (1995) An overview of workflow management: from process modeling to workflow automation infrastructure. Distrib Parallel Databases 3(2): 119–153
van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555–600
Hinz S, Schmidt K, Stahl C (2005) Transforming BPEL to Petri nets. In: Aalst WMP, Benatallah B, Casati F, Curbera F (eds) International conference on business process management (BPM 2005). Lecture notes in computer science, vol 3649. Springer-Verlag, Berlin, pp 220–235
van Hee KM, Serebrenik A, Sidorova N, Voorhoeve M (2005) Soundness of resource-constrained workflow nets. In: Ciardo G, Darondeau P (eds) Applications and theory of Petri nets 2005. Lecture notes in computer science, vol 3536. Springer-Verlag, Berlin, pp 250–267
van Hee KM, Sidorova N, Voorhoeve M (2003) Soundness and separability of workflow nets in the stepwise refinement approach. In: Aalst WMP, Best E (eds) Application and theory of Petri nets 2003. Lecture notes in computer science, vol 2679. Springer-Verlag, Berlin, pp 335–354
van Hee KM, Sidorova N, Voorhoeve M (2004) Generalised soundness of workflow nets is decidable. In: Cortadella J, Reisig W (eds) Application and theory of Petri nets 2004. Lecture notes in computer science, vol 3099. Springer-Verlag, Berlin, pp 197–215
Jablonski S, Bussler C (1996) Workflow management: modeling concepts, architecture, and implementation. International Thomson Computer Press, London
Jensen K (1997) Coloured Petri nets. Basic concepts, analysis methods and practical use, vol 1. EATCS monographs on theoretical computer science. Springer-Verlag, Berlin
Juhas G, Kazlov I, Juhasova A (2010) Instance deadlock: a mystery behind frozen programs. In: Lilius J, Penczek W (eds) Applications and theory of Petri nets 2010. Lecture notes in computer science, vol 6128. Springer-Verlag, Berlin, pp 1–17
Kindler E, van der Aalst WMP (1999) Liveness, fairness, and recurrence. Inf Process Lett 70(6): 269–274
Karamanolis C, Giannakopoulou D, Magee J, Wheater SM (2000) Model checking of workflow schemas. In: Proceedings of the fourth international enterprise distributed object computing conference (EDOC’00), Los Alamitos, CA, USA, 2000. IEEE Computer Society, pp 170–181
Kindler E (2006) On the semantics of EPCs: a framework for resolving the vicious circle. Data Knowl Eng 56(1): 23–40
Kindler E, Martens A, Reisig W (2000) Inter-operability of workflow applications: local criteria for global soundness. In: Aalst WMP, Desel J, Oberweis A (eds) Business process management: models, techniques, and empirical studies. Lecture notes in computer science, vol 1806. Springer-Verlag, Berlin, pp 235–253
Keller G, Nüttgens M, Scheer AW (1992) Semantische Processmodellierung auf der Grundlage Ereignisgesteuerter Processketten (EPK). Veröffentlichungen des Instituts für Wirtschaftsinformatik, Heft 89 (in German), University of Saarland, Saarbrücken
Lohmann N, Massuthe P, Stahl C, Weinberg D (2006) Analyzing interacting BPEL processes. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 17–32
Leymann F, Roller D (1999) Production workflow: concepts and techniques. Prentice-Hall PTR, Upper Saddle River, New Jersey
Lohmann N, Weinberg D (2010) Wendy: a tool to synthesize partners for services. In: Lilius J, Penczek W (eds) Applications and theory of Petri nets 2010. Lecture notes in computer science, vol 6128. Springer-Verlag, Berlin, pp 279–307
Lin H, Zhao Z, Li H, Chen Z (2002) A novel graph reduction algorithm to identify structural conflicts. In: Proceedings of the thirty-fourth annual Hawaii international conference on system science (HICSS-35). IEEE Computer Society Press
Martens A (2003) On Compatibility of Web services. Petri Net Newsl 65: 12–20
Martens A (2005) Analyzing Web service based business processes. In: Cerioli M (ed) Proceedings of the 8th international conference on fundamental approaches to software engineering (FASE 2005). Lecture notes in computer science, vol 3442. Springer-Verlag, Berlin, pp 19–33
Martens A (2005) Consistency between executable and abstract processes. In: Proceedings of international IEEE conference on e-Technology, e-Commerce, and e-Services (EEE’05). IEEE Computer Society Press, pp 60–67
Mendling J, Moser M, Neumann G, Verbeek HMW, van Dongen BF, van der Aalst WMP (2006) Faulty EPCs in the SAP reference model. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 451–457
Mendling J, Neumann G, van der Aalst WMP (2007) Understanding the occurrence of errors in process models based on metrics. In: Curbera F, Leymann F, Weske M (eds) Proceedings of the OTM conference on cooperative information systems (CoopIS 2007). Lecture notes in computer science, vol 4803. Springer-Verlag, Berlin, pp 113–130
Massuthe P, Reisig W, Schmidt K (2005) An operating guideline approach to the SOA. In: Proceedings of the 2nd South-East European workshop on formal methods 2005 (SEEFM05), Ohrid, Republic of Macedonia
Massuthe P, Reisig W, Schmidt K (2005) An operating guideline approach to the SOA. Ann Math Comput Teleinformatics 1(3): 35–43
zur Muehlen M (2004) Workflow-based process controlling: foundation, design and application of workflow-driven process information systems. Logos, Berlin
Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4): 541–580
Mendling J, Verbeek HMW, van Dongen BF, van der Aalst WMP, Neumann G (2008) Detection and prediction of errors in EPCs of the SAP reference model. Data Knowl Eng 64(1): 312–329
Ouyang C, Dumas M, van der Aalst WMP, ter Hofstede AHM, Mendling J (2009) From business process models to process-oriented software systems. ACM Trans Softw Eng Methodol 19(1): 1–37
Puhlmann F, Weske M (2006) Interaction soundness for service orchestrations. In: Dan A, Lamersdorf W (eds) Proceedings of service-oriented computing (ICSOC 2006). Lecture notes in computer science, vol 4294. Springer-Verlag, Berlin, pp 302–313
Puhlmann F, Weske M (2006) Investigations on soundness regarding lazy activities. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 145–160
Puhlmann F, Weske M (2009) A look around the corner: the pi-calculus. In: Jensen K, Aalst WMP (eds) Transactions on Petri nets and other models of concurrency II. Lecture notes in computer science, vol 5460. Springer-Verlag, Berlin, pp 64–78
Rozinat A, van der Aalst WMP (2008) Conformance checking of processes based on monitoring real behavior. Inf Syst 33(1): 64–95
Sadiq W, Orlowska ME (1997) On correctness issues in conceptual modeling of workflows. In: Proceedings of the 5th European conference on information systems (ECIS ’97), Cork, Ireland, pp 19–21
Sadiq W, Orlowska ME (2000) Analyzing process models using graph reduction techniques. Inf Syst 25(2): 117–134
Salimifard K, Wright M (2001) Petri net-based modelling of workflow systems: an overview. Eur J Oper Res 134(3): 664–676
Trcka N, van der Aalst WMP, Sidorova N (2009) Data-flow anti-patterns: discovering data-flow errors in workflows. In: Eck P, Gordijn J, Wieringa R (eds) Advanced information systems engineering, proceedings of the 21st international conference on advanced information systems engineering (CAiSE’09). Lecture notes in computer science, vol 5565. Springer-Verlag, Berlin, pp 425–439
van der Toorn R (2004) Component-based software design with Petri nets: an approach based on inheritance of behavior. PhD thesis, Eindhoven University of Technology, Eindhoven, The Netherlands
Verbeek HMW, van der Aalst WMP (2005) Analyzing BPEL processes using Petri nets. In: Marinescu D (ed) Proceedings of the second international workshop on applications of Petri nets to coordination, workflow and business process management. Florida International University, Miami, Florida, pp 59–78
Verbeek HMW, van der Aalst WMP, ter Hofstede AHM (2007) Verifying workflows with cancellation regions and OR-joins: an approach based on relaxed soundness and invariants. Comput J 50(3): 294–314
Verbeek HMW, Basten T, van der Aalst WMP (2001) Diagnosing workflow processes using Woflan. Comput J 44(4): 246–279
Vanhatalo J, Völzer H, Leymann F (2007) Faster and more focused control-flow analysis for business process models through SESE decomposition. In: Krämer B, Lin K, Narasimhan P (eds) Proceedings of service-oriented computing (ICSOC 2007). Lecture notes in computer science, vol 4749. Springer-Verlag, Berlin, pp 43–55
Verbeek HMW, Wynn MT, van der Aalst WMP, ter Hofstede AHM (2010) Reduction rules for reset/inhibitor nets. J Comput Syst Sci 76(2): 125–143
Wynn MT, van der Aalst WMP, ter Hofstede AHM, Edmond D (2006) Verifying workflows with cancellation regions and OR-joins: an approach based on reset nets and reachability analysis. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 389–394
Wynn MT, Edmond D, van der Aalst WMP, ter Hofstede AHM (2005) Achieving a general, formal and decidable approach to the OR-join in workflow using reset nets. In: Ciardo G, Darondeau P (eds) Applications and theory of Petri nets 2005. Lecture notes in computer science, vol 3536. Springer-Verlag, Berlin, pp 423–443
Weske M (2007) Business process management: concepts, languages, architectures. Springer-Verlag, Berlin
Wong PYH, Gibbons J (2007) A process-algebraic approach to workflow specification and refinement. In: Lumpe M, Vanderperren W (eds) Software composition. Lecture notes in computer science, vol 4829. Springer-Verlag, Berlin, pp 51–65
Wong PYH, Gibbons J (2008) A process semantics for BPMN. In: Liu S, Maibaum T, Arki K (eds) International conference on formal engineering methods (ICFEM 2008). Lecture notes in computer science, vol 5256. Springer-Verlag, Berlin, pp 27–31
Wong PYH, Gibbons J (2009) Property specifications for workflow modelling. In: Proceedings of 7th international conference on integrated formal methods. Lecture notes in computer science, vol 5423. Springer-Verlag, Berlin
White SA et al (2009) Business process modeling notation specification (Version 1.2, OMG Final Adopted Specification)
Wolf K (2009) Does my service have partners?. In: Jensen K, Aalst WMP (eds) Transactions on Petri nets and other models of concurrency II. Lecture notes in computer science, vol 5460. Springer-Verlag, Berlin, pp 152–171
Wombacher A (2006) Decentralized consistency checking in cross-organizational workflows. In: Proceedings of international conference on e-Technology, e-Commerce and e-Service (CEC/EEE 2006). IEEE Computer Society, pp 39–46
Wynn MT, Verbeek HMW, van der Aalst WMP, ter Hofstede AHM, Edmond D (2009) Soundness-preserving reduction rules for reset workflow nets. Inf Sci 179(6): 769–790
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Additional information
J. C. P. Woodcock
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
van der Aalst, W.M.P., van Hee, K.M., ter Hofstede, A.H.M. et al. Soundness of workflow nets: classification, decidability, and analysis. Form Asp Comp 23, 333–363 (2011). https://doi.org/10.1007/s00165-010-0161-4
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-010-0161-4