Understanding Behavior of Business Process Models

Introduction Business processes have intrinsic parallelism given by the relative independence of some activities. Parallelizing a process might "dramatically reduce cycle times and the resultant costs" [5], but it might lead to anomalous behavior, like deadlock or useless activities. There are three main approaches to avoid behaviorally incorrect models, a notion that is not even well defined: 1) Build a model and then verify its properties (e.g., building the space state, or finding net invariants [2]). 2) Build a model that is correct by construction (e.g., using activity annotations [1] akin to parbegin parend pairs). 3) Use only small models by abstracting models and submodels. The first approach does not explain why or where a particular model has behavioral problems. The second approach constrains the forms of parallelism: it is impossible to model a PERT chart. The third approach is just a rule of thumb that may lead to oversimplified models. This work intends to: defi