One of the most debatable features of Event driven Process Chains (EPCs) is their non-local semantics, which
results in some difficulties when formalising their semantics. Recently, we have overcome these problems by using techniques from fixed-point theory for defining the semantics of an EPC, which consists of a pair of related
transition relations. This fixed-point characterisation of the semantics of EPCs provides a mathematical
characterisation of the semantics of EPCs only. For simulating an EPC based on this semantics, we need an
efficient way for calculating the corresponding pair of transition relations. A naive implementation of the
underlying fixed-point iteration for calculating the transition relations results in a practically useless algorithm.
In this paper, we show how to calculate the semantics of an EPC in a more efficient way by employing different
techniques and optimisations from symbolic model checking. We also analysed all kinds of simplifications of EPCs
to make the calculation of the semantics more efficient, but it turned out that most of these techniques are
ineffective. Still, our algorithms are fast enough for simulating practical size EPCs.
In order to demonstrate the efficiency of our algorithms and data structures, we have started an open source
project called EPC Tools, which could be a good starting point for an open source tool for the EPC community.
]