×

zbMATH — the first resource for mathematics

Soundness of workflow nets: classification, decidability, and analysis. (English) Zbl 1225.68129
The workflow verification is an object of investigation since a few years. The WorkFlow Nets (WFNs) were introduced by the first author, W. M. P. van der Aalst, in 1997 as a particular case of Petri nets. In the following research of the same author it was shown that WFNs can be used as a tool for modelling and analysis of workflows. In the present research, important properties of WFNs, related to decidability and undecidability problems, are studied.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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
[2] van der Aalst WMP (1998) The application of Petri nets to workflow management. J Circ Syst Comput 8(1): 21–66 · doi:10.1142/S0218126698000043
[3] 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
[4] van der Aalst WMP, van Hee KM (2004) Workflow management: models, methods, and systems. MIT press, Cambridge
[5] van der Aalst WMP, ter Hofstede AHM (2005) YAWL: yet another workflow language. Inf Syst 30(4): 245–275 · Zbl 02238482 · doi:10.1016/j.is.2004.02.002
[6] 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
[7] 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 · Zbl 1266.68140
[8] van der Aalst WMP, ter Hofstede AHM, Kiepuszewski B, Barros AP (2003) Workflow patterns. Distrib Parallel Databases 14(1): 5–51 · Zbl 01904961 · doi:10.1023/A:1022883727209
[9] 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 · Zbl 1046.68975
[10] 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
[11] 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
[12] Basu A, Blanning RW (2000) A formal approach to workflow analysis. Inf Syst Res 11(1): 17–36 · doi:10.1287/isre.11.1.17.11787
[13] 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
[14] Basu A, Kumar A (2002) Research commentary: workflow management issues in e-business. Inf Syst Res 13(1): 1–14 · doi:10.1287/isre.13.1.1.94
[15] 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
[16] Bi HH, Zhao JL (2004) Applying propositional logic to workflow verification. Inf Technol Manag 5(3–4): 293–318 · Zbl 02242386 · doi:10.1023/B:ITEM.0000031583.16306.0f
[17] 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 · Zbl 0935.68074
[18] 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 · Zbl 02179418 · doi:10.1142/S0218843004000973
[19] 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
[20] 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
[21] 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
[22] Desel J, Esparza J (1995) Free choice Petri nets. In: Cambridge tracts in theoretical computer science, vol 40. Cambridge University Press, Cambridge · Zbl 0836.68074
[23] 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 · Zbl 0909.68124
[24] 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 · Zbl 0943.68122
[25] 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 · Zbl 0980.68816
[26] Esparza J, Nielsen M (1994) Decidability issues for Petri nets: a survey. J Inf Process Cybern 30: 143–160 · Zbl 0838.68082
[27] 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 · Zbl 0926.68087
[28] Esparza J (1998) Reachability in live and safe free-choice Petri nets is NP-complete. Theor Comput Sci 198(1–2): 211–224 · Zbl 0902.68136 · doi:10.1016/S0304-3975(97)00235-1
[29] 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
[30] 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
[31] 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
[32] Finkel A, Schnoebelen Ph (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1–2): 63–92 · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[33] 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 · doi:10.1007/BF01277643
[34] van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555–600 · Zbl 0882.68085 · doi:10.1145/233551.233556
[35] 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
[36] 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 · Zbl 1128.68391
[37] 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 · Zbl 1274.68263
[38] 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 · Zbl 1094.68070
[39] Jablonski S, Bussler C (1996) Workflow management: modeling concepts, architecture, and implementation. International Thomson Computer Press, London
[40] Jensen K (1997) Coloured Petri nets. Basic concepts, analysis methods and practical use, vol 1. EATCS monographs on theoretical computer science. Springer-Verlag, Berlin · Zbl 0883.68098
[41] 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
[42] Kindler E, van der Aalst WMP (1999) Liveness, fairness, and recurrence. Inf Process Lett 70(6): 269–274 · Zbl 0953.68575 · doi:10.1016/S0020-0190(99)00074-5
[43] 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
[44] Kindler E (2006) On the semantics of EPCs: a framework for resolving the vicious circle. Data Knowl Eng 56(1): 23–40 · doi:10.1016/j.datak.2005.02.005
[45] 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
[46] 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
[47] 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
[48] Leymann F, Roller D (1999) Production workflow: concepts and techniques. Prentice-Hall PTR, Upper Saddle River, New Jersey · Zbl 0945.68539
[49] 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
[50] 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
[51] Martens A (2003) On Compatibility of Web services. Petri Net Newsl 65: 12–20
[52] 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 · Zbl 1119.68305
[53] 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
[54] 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
[55] 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
[56] 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
[57] Massuthe P, Reisig W, Schmidt K (2005) An operating guideline approach to the SOA. Ann Math Comput Teleinformatics 1(3): 35–43
[58] zur Muehlen M (2004) Workflow-based process controlling: foundation, design and application of workflow-driven process information systems. Logos, Berlin
[59] Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4): 541–580 · doi:10.1109/5.24143
[60] 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 · doi:10.1016/j.datak.2007.06.019
[61] 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 · doi:10.1145/1555392.1555395
[62] 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
[63] 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
[64] 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 · Zbl 1235.68110
[65] Rozinat A, van der Aalst WMP (2008) Conformance checking of processes based on monitoring real behavior. Inf Syst 33(1): 64–95 · Zbl 05353610 · doi:10.1016/j.is.2007.07.001
[66] 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
[67] Sadiq W, Orlowska ME (2000) Analyzing process models using graph reduction techniques. Inf Syst 25(2): 117–134 · Zbl 02177947 · doi:10.1016/S0306-4379(00)00012-0
[68] Salimifard K, Wright M (2001) Petri net-based modelling of workflow systems: an overview. Eur J Oper Res 134(3): 664–676 · Zbl 0984.90005 · doi:10.1016/S0377-2217(00)00292-7
[69] 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
[70] 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
[71] 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
[72] 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 · Zbl 05534169 · doi:10.1093/comjnl/bxl074
[73] Verbeek HMW, Basten T, van der Aalst WMP (2001) Diagnosing workflow processes using Woflan. Comput J 44(4): 246–279 · Zbl 0993.68141 · doi:10.1093/comjnl/44.4.246
[74] 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
[75] 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 · Zbl 1187.68330 · doi:10.1016/j.jcss.2009.06.003
[76] 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
[77] 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 · Zbl 1128.68389
[78] Weske M (2007) Business process management: concepts, languages, architectures. Springer-Verlag, Berlin
[79] 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
[80] 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
[81] 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 · Zbl 1211.68258
[82] White SA et al (2009) Business process modeling notation specification (Version 1.2, OMG Final Adopted Specification)
[83] 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
[84] 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
[85] 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 · Zbl 1162.68488 · doi:10.1016/j.ins.2008.10.033
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.