Supervisory control of business processes with resources, parallel and mutually exclusive branches, loops, and uncertainty

A recent direction in Business Process Management studied methodologies to control the execution of Business Processes under several sources of uncertainty in order to always get to the end by satisfying all constraints. Current approaches encode business processes into temporal constraint networks or timed game automata in order to exploit their related strategy synthesis algorithms. However, the proposed encodings can only synthesize single-strategies and fail to handle loops. To overcome these limits we propose an approach based on supervisory control. We consider structured business processes with resources, parallel and mutually exclusive branches, loops, and uncertainty. We provide an encoding into finite state automata and prove that their concurrent behavior models exactly all possible executions of the process. After that, we introduce tentative commitment constraints as a new class of constraints restricting the executions of a process. We define a tree decomposition of the process that plays a central role in modular supervisory control, and we prove that this modular approach is equivalent to the monolithic one. We provide an algorithm to compute the finest tree decomposition to reduce the computational effort of synthesizing supervisors.