Declarative algorithm for checking wrong indirect relationships of process model containing non-free choice

In the presence of a large number of activities that occur in the company, recording activities are needed to obtain reports on the results of the process. The set of recorded activities is an event log and can be modeled by process discovery to make analysis easier. Out of all existing relationships, Non-Free Choice is a challenging relationship for process discovery algorithms, because Non-Free Choice contains indirect relationships. However, the obtained Non-Free Choice by existing algorithms is a graphical model, so it cannot be used to detect processes containing wrong indirect relationships. A wrong indirect relationship is an indirect relationship that is not fit with the obtained Non-Free Choice. This study proposes a method, namely declarative algorithm for checking indirect relationships, to detect wrong indirect relationships in processes by creating rules of a process model in the form of Linear Temporal Logic (LTL). Experiments prove that this declarative algorithm can detect wrong indirect relationships automatically by using proposed LTL rules deriving from a process model containing Non-Free Choice. The evaluation verifies that the accuracy of obtained wrong indirect relationships is 100%.