State propagation in abstracted business processes

Business process models are abstractions of concrete operational procedures that occur in the daily business of organizations. Typically one model is insufficient to describe one business process. For instance, a detailed technical model may enable automated process execution, while a more abstract model supports decision making and process monitoring by business users. Thereafter, multiple models capturing one process at various levels of abstraction often coexist. While the relations between such models are studied, little is known about the relations between process instances and abstract models. In this paper we show how the state of an abstract activity can be calculated from the states of related, detailed process activities as they happen. The approach uses activity state propagation. With state uniqueness and state transition correctness we introduce formal properties that improve the understanding of state propagation. Algorithms to check these properties are devised. Finally, we use behavioral profiles to identify and classify behavioral inconsistencies in abstract process models that might occur, once activity state propagation is used.