Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reactive Synthesis for Expected Impacts

Emanuele Chini, Pietro Sala, Andrea Simonetti, Omid Zare

TL;DR

A formal extension of the Business Process Model and Notation that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI is introduced, motivated by the growing emphasis on precise control within business process management.

Abstract

As business processes become increasingly complex, effectively modeling decision points, their likelihood, and resource consumption is crucial for optimizing operations. To address this challenge, this paper introduces a formal extension of the Business Process Model and Notation (BPMN) that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI. This extension is motivated by the growing emphasis on precise control within business process management, where carefully selecting decision pathways in repeated instances is crucial for conforming to certain standards of multiple resource consumption and environmental impacts. In this context we deal with the problem of synthesizing a strategy (if any) that guarantees that the expected impacts on repeated execution of the input process are below a given threshold. We show that this problem belongs to PSPACE complexity class; moreover we provide an effective procedure for computing a strategy (if present).

Reactive Synthesis for Expected Impacts

TL;DR

A formal extension of the Business Process Model and Notation that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI is introduced, motivated by the growing emphasis on precise control within business process management.

Abstract

As business processes become increasingly complex, effectively modeling decision points, their likelihood, and resource consumption is crucial for optimizing operations. To address this challenge, this paper introduces a formal extension of the Business Process Model and Notation (BPMN) that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI. This extension is motivated by the growing emphasis on precise control within business process management, where carefully selecting decision pathways in repeated instances is crucial for conforming to certain standards of multiple resource consumption and environmental impacts. In this context we deal with the problem of synthesizing a strategy (if any) that guarantees that the expected impacts on repeated execution of the input process are below a given threshold. We show that this problem belongs to PSPACE complexity class; moreover we provide an effective procedure for computing a strategy (if present).

Paper Structure

This paper contains 13 sections, 4 theorems, 3 equations, 8 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related work
  3. BPMN+CPI: Processes with Choices, Probabilities, and Impacts
  4. Motivating Example
  5. Problem Formulation
  6. Dealing with Loops
  7. Computational Complexity
  8. Synthesizing Strategies
  9. A $k$-cost Reachability Game
  10. From BPMN+CPI to $k$-cost Reachability Game
  11. Implementation
  12. Conclusion
  13. Acknowledgments

Key Result

Theorem 1

Problem prob:winningStrategyExistence is NP-HARD and belongs to the complexity class PSPACE.

Figures (8)

  • Figure 1: An example of BPMN+CPI diagram for an industrial process.
  • Figure 2: A BPMN+CPI utilizing all the components considered in this work (a) and its $\mathsf{SPIN}$ translation (b).
  • Figure 3: A $\mathsf{SPIN}$ for illustrating $\hbox{$\textit{MNCE}$}$ and probabilistic variants.
  • Figure 4: An example of a $2$-unraveling of a loop region.
  • Figure 5: Reduction from Partition to k-cost game Problem.
  • ...and 3 more figures

Theorems & Definitions (19)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 9 more