Verification of EPCs Based on the Finite State Automata and State-space

Event-driven Process Chains (EPCs) have become a widespread process modeling technique because of their agility and simple. But they also have serious drawback, such as the informal semantics of EPCs that resulted in the process reengineering based on EPC can't be implemented automatically. This paper aims at the automatic reengineering of process, adopts the FSA (Finite State Automata) theory, and indicates an arithmetic based on state-space, for the purpose of implement automatic verification of EPCs, then the Operational staff can do the process reengineeiring by themselves. Process reengineering is based on EPC. Aims at the EPC which has been gained, first, it is reduced using universally accepted reduction rules. Second, the reduced EPC is analyzed using a mixture of state-space analysis, automata theory, and human judgment; then the arithmetic is implemented.