Formalization and Verification of EPCs with OR-Joins Based on State and Context

The semantics of the OR-join in business process modeling languages like EPCs or YAWL have been discussed for a while. Still, the existing solutions suffer from at least one of two major problems. First, several formalizations depend upon restrictions of the EPC to a subset. Second, several approaches contradict the modeling intuition since the structuredness of the process does not guarantee soundness. In this paper, we present a novel semantical definition of EPCs that addresses these aspects yielding a formalization that is applicable for all EPCs and for which structuredness is a sufficient condition for soundness. Furthermore, we introduce a set of reduction rules for the verification of an EPC-specific soundness criterion and present a respective implementation.

• Type: Conference
• Year: 2007
• Where: CAISE
• Authors: Jan Mendling, Wil M. P. van der Aalst
• Keywords: CAISE 2007, EPC-specific Soundness Criterion, Information Management, Modeling Intuition, Process Modeling Languages