A first and fast symbolic approach for data-aware business process compliance checking

State of the art design-time compliance checking techniques are generally limited to verifying control-flow relations. In this paper, we propose an algorithm for verifying design-time compliance of business process models including data. For a faithful resemblance to real-world cases, we include a degree of uncertainty in the outcomes of activities, such that a single execution is not guaranteed to lead to a unique data state. We represent the compliance requirements using conditional obligations. Our proposed approach uses a symbolic representation to compactly represent the possible data states across an execution, and evaluates them as a constraint satisfaction problem to first prune the state space of paths that require no further analysis and finally to evaluate if an execution violates one of the regulatory requirements. The performance of the approach is evaluated against existing algorithms implemented in NuXMV. The results show that our approach significantly outperforms the existing algorithms across the board.