Hypercube Graph Decomposition for Boolean Simplification: An Optimization of Business Process Verification

This paper deals with the optimization of busi-ness processes (BP) verification by simplifying their equivalent algebraic expressions. Actual approaches of business processes verification use formal methods such as automated theorem proving and model checking to verify the accuracy of the business process design. Those processes are abstracted to mathematical models in order to make the verification task possible. However, the structure of those mathematical models is usually a Boolean expression of the business process variables and gateways. Thus leading to a combinatorial explosion when the number of literals is above a certain threshold. This work aims at optimizing the verification task by managing the problem size. A novel algorithm of Boolean simplification is proposed. It uses hypercube graph decomposition to find the minimal equivalent formula of a business process model given in its disjunctive normal form (DNF). Moreover, the optimization method is totally automated and can be applied to any business process having the same formula due to the independence of the Boolean simplification rules from the studied processes. This new approach has been numerically validated by comparing its performance against the state of the art method Quine-McCluskey (QM) through the optimization of several processes with various types of branching.

@article{NAOUM2019,
  title     = {Hypercube Graph Decomposition for Boolean Simplification: An Optimization of Business Process Verification},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {10},
  number    = {2},
  year      = {2019},
  publisher = {The Science and Information Organization},
  author    = {Mohamed NAOUM and Outman EL HICHAMI and Mohammed AL ACHHAB and Badr eddine EL MOHAJIR},
  doi       = {10.14569/IJACSA.2019.0100261},
  url       = {https://doi.org/10.14569/IJACSA.2019.0100261}
}