Optimisation of BPMN Business Models via Model Checking

We present a framework for the optimisation of business processes modelled in the business process modelling language BPMN, which builds upon earlier work, where we developed a model checking based method for the analysis of BPMN models. We define a structure for expressing optimisation goals for synthesized BPMN components, based on probabilistic computation tree logic and real-valued reward structures of the BPMN model, allowing for the specification of complex quantitative goals. We here present a simple algorithm, inspired by concepts from evolutionary algorithms, which iteratively generates candidate improved processes based on the fittest of the previous generation. The evaluation of the fitness of each candidate in a generation is performed via model checking, detailed in previous work. At each iteration, this allows the determination of the precise numerical evaluation of the performance of a candidate in terms of the specified goals. A discussion of this method’s application, and the degree of optimization which is possible, is illustrated using an example drawn from the healthcare industry.