Constraint-based reasoning on declarative process execution with the logics workbench

An integral part of declarative process modelling is to guarantee that the execution of a declarative workflow is compliant with the respective business rules. The purpose of this paper is to establish a formal framework for representing business rules and determining whether any business rules are violated during the executions of declarative process models.

In the approach, a business rule is phrased in terms of restricted English that is related to a constraint template. Linear temporal logic (LTL) is employed as a formalism for defining the set of constraint templates. By exploiting the theorem-proving feature of the Logics Workbench (LWB), business rule violations are then detected in an automatic manner.

This study explored the viability of encoding: first, process executions by means of LTL and second, business rules in terms of restricted English that built upon pattern-oriented templates and LTL. The LWB was used for carrying out temporal reasoning through automated techniques. The applicability of the formal verification approach was exemplified by a case study concerning supply chain management. The findings showed that practical reasoning could be achieved by combining declarative process modelling, restricted English, pattern-oriented templates, LTL and LWB.

First, new business rule templates are proposed; second, business rules are expressed in restricted English instead of graphical constructs; third, both finite execution trace and business rules are grounded in LTL. There is no need to deal with the semantic differences between different formalisms; and finally, the theorem prover LWB is used for the conformance checking of a finite execution trace against business rules.