# Publications 2009

• W. M. P. van der Aalst, B. F. van Dongen, C. W. GÃ¼nther, A. Rozinat, H. M. W. Verbeek, and A. J. M. M. Weijters, “Prom: the process mining toolkit,” , 2009.
[Bibtex]
@Electronic{Aalst09a,
Title = {ProM: The Process Mining Toolkit},
Author = {Aalst, W. M. P. van der and Dongen, B. F. van and G\"{u}nther, C. W. and Rozinat, A. and Verbeek, H. M. W. and Weijters, A. J. M. M.},
Month = {September},
Organization = {CEUR-WS},
Url = {http://ceur-ws.org/Vol-489/paper3.pdf},
Year = {2009},
Abstract = {Nowadays, all kinds of information systems store detailed information in logs. Process mining has emerged as a way to analyze these systems based on these detailed logs. Unlike classical data mining, the focus of process mining is on processes. First, process mining allows us to extract a process model from an event log. Second, it allows us to detect discrepancies between a modeled process (as it was envisioned to be) and an event log (as it actually is). Third, it can enrich an existing model with knowledge derived from an event log. This paper presents our tool ProM, which is the world-leading tool in the area of process mining.},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Aalst09a.pdf:URL},
Owner = {hverbeek},
Timestamp = {2009.09.15}
}
• W. M. P. van der Aalst, K. M. van Hee, A. H. M. ter Hofstede, N. Sidorova, H. M. W. Verbeek, M. Voorhoeve, and M. T. Wynn, “Soundness of workflow nets with reset arcs,” Lncs transactions on petri nets and other models of concurrency (topnoc), vol. 5800, pp. 50-70, 2009.
[Bibtex]
@Article{Aalst09,
Title = {Soundness of Workflow Nets with Reset Arcs},
Author = {Aalst, W. M. P. van der and Hee, K. M. van and Hofstede, A. H. M. ter and Sidorova, N. and Verbeek, H. M. W. and Voorhoeve, M. and Wynn, M. T.},
Journal = {LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)},
Year = {2009},
Pages = {50--70},
Volume = {5800},
Abstract = {Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a mapping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.},
Doi = {10.1007/978-3-642-04856-2_3},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Aalst09.pdf:URL},
Owner = {hverbeek},
Timestamp = {2009.06.05},
Url = {http://www.springerlink.com/content/f15t41545m061682/fulltext.pdf}
}
• K. M. van Hee, H. M. W. Verbeek, C. Stahl, and N. Sidorova, “A framework for linking and pricing no-cure-no-pay services,” Lncs transactions on petri nets and other models of concurrency (topnoc) ii, vol. 5460, pp. 192-207, 2009.
[Bibtex]
@Article{Hee09,
Title = {A Framework for Linking and Pricing No-Cure-No-Pay Services},
Author = {Hee, K. M. van and Verbeek, H. M. W. and Stahl, C. and Sidorova, N.},
Journal = {LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) II},
Year = {2009},
Pages = {192--207},
Volume = {5460},
Abstract = {In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the \emph{risk} a web service takes, we consider the variance of costs.},
Doi = {10.1007/978-3-642-00899-3_11},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Hee09.pdf:PDF;ToPNoC:http\://www.springer.com/computer/lncs?SGWID=0-164-6-417809-0:URL},
Owner = {hverbeek},
Timestamp = {2008.11.03},
Url = {http://www.springerlink.com/content/j4q58mukx6643674/fulltext.pdf}
}
• N. Lohmann, H. M. W. Verbeek, and R. M. Dijkman, “Petri net transformations for business processes a survey,” Lncs transactions on petri nets and other models of concurrency (topnoc) ii, vol. 5460, pp. 46-63, 2009.
[Bibtex]
@Article{Lohmann09,
Title = {Petri Net Transformations for Business Processes – A Survey},
Author = {Lohmann, N. and Verbeek, H. M. W. and Dijkman, R. M.},
Journal = {LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) II},
Year = {2009},
Pages = {46--63},
Volume = {5460},
Abstract = {In Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding \emph{academic} models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.},
Doi = {10.1007/978-3-642-00899-3_3},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Lohmann09.pdf:PDF;ToPNoC:http\://www.springer.com/computer/lncs?SGWID=0-164-6-417809-0:URL},
Owner = {hverbeek},
Timestamp = {2008.11.03},
Url = {http://www.springerlink.com/content/n7464131r6751453/fulltext.pdf}
}
• N. Lohmann, H. M. W. Verbeek, C. Ouyang, and C. Stahl, “Comparing and evaluating petri net semantics for bpel,” International journal of business process integration and management (ijbpim), vol. 4, iss. 1, pp. 60-73, 2009.
[Bibtex]
@Article{Lohmann09a,
Title = {Comparing and Evaluating Petri Net Semantics for BPEL},
Author = {Lohmann, N. and Verbeek, H. M. W. and Ouyang, C. and Stahl, C.},
Journal = {International Journal of Business Process Integration and Management (IJBPIM)},
Year = {2009},
Number = {1},
Pages = {60--73},
Volume = {4},
Abstract = {We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.},
Doi = {10.1504/IJBPIM.2009.026986},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Lohmann09a.pdf:PDF;IJBPIM:https\://www.inderscience.com/browse/index.php?journalID=115:URL},
Keywords = {business process modelling; business process execution language; Petri nets; semantics; formal methods; verification; BPEL; web services; WS-BPEL.},
Owner = {hverbeek},
Timestamp = {2008.11.03}
}
• M. T. Wynn, H. M. W. Verbeek, W. M. P. van der Aalst, A. H. M. ter Hofstede, and D. Edmond, “Soundness-preserving reduction rules for reset workflow nets,” Information sciences, vol. 179, iss. 6, pp. 769-790, 2009.
[Bibtex]
@Article{Wynn09,
Title = {Soundness-preserving Reduction Rules for Reset Workflow Nets},
Author = {Wynn, M. T. and Verbeek, H. M. W. and Aalst, W. M. P. van der and Hofstede, A. H. M. ter and Edmond, D.},
Journal = {Information Sciences},
Year = {2009},
Number = {6},
Pages = {769--790},
Volume = {179},
Abstract = {The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net's essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on Reset Workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.},
Doi = {10.1016/j.ins.2008.10.033},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Wynn09.pdf:URL;Information Sciences:http\://www.elsevier.com/locate/ins:URL},
Owner = {hverbeek},
Timestamp = {2008.11.03}
}
• M. T. Wynn, H. M. W. Verbeek, W. M. P. van der Aalst, A. H. M. ter Hofstede, and D. Edmond, “Reduction rules for yawl workflows with cancellation regions and or-joins,” Information and software technology (infsof), vol. 51, pp. 1010-1020, 2009.
[Bibtex]
@Article{Wynn09b,
Title = {Reduction rules for YAWL workflows with cancellation regions and OR-joins},
Author = {Wynn, M. T. and Verbeek, H. M. W. and Aalst, W. M. P. van der and Hofstede, A. H. M. ter and Edmond, D.},
Journal = {Information and Software Technology (InfSof)},
Year = {2009},
Pages = {1010--1020},
Volume = {51},
Abstract = {As the need for concepts such as cancellation and OR-joins occurs naturally in business scenarios, comprehensive support in a workflow language is desirable. However, there is a clear trade-off between the expressive power of a language (i.e., introducing complex constructs such as cancellation and OR-joins) and ease of verification. When a workflow contains a large number of tasks and involves complex control flow dependencies, verification can take too much time or it may even be impossible. There are a number of different approaches to deal with this complexity. Reducing the size of the workflow, while preserving its essential properties with respect to a particular analysis problem, is one such approach. In this paper, we present a set of reduction rules for workflows with cancellation regions and OR-joins and demonstrate how they can be used to improve the efficiency of verification. Our results are presented in the context of the YAWL workflow language.},
Doi = {10.1016/j.infsof.2008.12.002},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Wynn09b.pdf:PDF},
Owner = {hverbeek},
Timestamp = {2009.02.06}
}
• M. T. Wynn, H. M. W. Verbeek, W. M. P. van der Aalst, A. H. M. ter Hofstede, and D. Edmond, “Business process verification -finally a reality!,” Business process management journal, vol. 15, iss. 1, pp. 74-92, 2009.
[Bibtex]
@Article{Wynn09a,
Title = {Business Process Verification -Finally a Reality!},
Author = {Wynn, M. T. and Verbeek, H. M. W. and Aalst, W. M. P. van der and Hofstede, A.H.M. ter and Edmond, D.},
Journal = {Business Process Management Journal},
Year = {2009},
Number = {1},
Pages = {74--92},
Volume = {15},
Abstract = {The goal of this paper is to demonstrate that process verification has matured to a level where it can be used in practice. Earlier techniques assumed simplified process models without the more advanced constructs available in today’s modelling languages (e.g., cancellation and OR-joins). This paper reports on new verification techniques that can be used to assess the correctness of real-life models.},
Doi = {10.1108/14637150910931479},
File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Wynn09a.pdf:PDF;BPMJ:http\://info.emeraldinsight.com/products/journals/journals.htm?id=BPMJ:URL},
Owner = {hverbeek},
Timestamp = {2008.11.03}
}