Petri net based certification of event-driven process chains

Abstract

One of the widespread methods for modeling business processes is the method of event-driven process chains (EPCs) (Ereignisgesteuerte Prozesskette [EPK]). The paper shows that EPCs can be translated into a simple class of colored Petri nets, which have a single color of type Boole and formulas from propositional logic as guards. The structure of the resulting Boolean net is a tree of bipolar synchronization (bp) graphs. This property simplifies considerably the behavioral analysis of EPCs, because Genrich and Thiagarajan proved, that well-formedness of bp schemes can be tested by a reduction algorithm. If the Boolean net resulting from the translation of an EPC is well-formed, it can be eventually translated into a free-choice net showing the same behavior. Therefore the translation of EPCs into Boolean Petri nets fixes the semantics of EPCs and allows a formal analysis of the EPC-method. In the domain of business process engineering only those EPCs, which have been certified as well-formed, can be recommended for further steps like simulation, activity based cost analysis or workflow. Topics. System design and verification using nets, analysis and synthesis, structure and behavior of nets.