On the verification of EPCs using T-invariants

To verify a (business) process model, for example expressed in terms of an Event-driven Process Chain (EPC), most of the approaches described in literature require the construction of its state space. Unfortunately, for complex business processes the state space can be extremely large (if at all finite) and, as a result, constructing the state space may require excessive time. Moreover, semi-formal modeling languages such as the EPC language require a rather lenient interpretation of their semantics. To circumvent both the state-explosion problem and the semantics-related problems of EPCs, we propose an alternative approach based on transition invariants (T-invariants). T-invariants are well-known in the Petri-net community. They do not require the construction of the state space and can be computed efficiently. Moreover, we will show that our interpretation of T-invariants in this context can be used to deal effectively with the semantics-related problems of EPCs. To demonstrate our approach we will use two case studies: one is based on the reference model of SAP R/3 while the other one is based on a trade execution process within a large Dutch bank. We will also argue that the approach can be applied to other (informal or formal) modeling techniques.