Abstract

Data in business processes is becoming more and more important. Current standards for process-modeling languages like BPMN 2.0 which include the data flow reflect this. Ensuring the correctness of the data flow in processes is challenging. Model checking, i. e., verifying properties of process models, is a well-known technique to this end. An important part of model checking is the construction of the state space of the model. State-space explosion however typically is in the way of an effective verification. We study how to overcome this problem in our context by means of reduction. More specifically, we propose a reduction on the level of the process model. To our knowledge, this is new for the data-flow analysis of processes. To accomplish this, we specify regions relevant for the verification of properties describing the data flow. Our evaluation shows that our approach works well on real process models.