# Verifying Compliance in Process Choreographies: Foundations, Algorithms, and Implementation

arXiv: https://arxiv.org/abs/2110.09399 · HTML: https://mlsanity.com/paper/2110.09399/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Oct 2021.

## Built on by (most cited first, 4 of 4)

- [Predictive Compliance Monitoring in Process-Aware Information Systems: State of the Art, Functionalities, Research Directions](https://mlsanity.com/paper/2205.05446/) (2022)
- [A Case Study for Compliance as Code with Graphs and Language Models: Public release of the Regulatory Knowledge Graph](https://mlsanity.com/paper/2302.01842/) (2023)
- [Preventing Object-centric Discovery of Unsound Process Models for Object Interactions with Loops in Collaborative Systems: Extended Version](https://mlsanity.com/paper/2303.16680/) (2023)
- [INEXA: Interactive and Explainable Process Model Abstraction Through Object-Centric Process Mining](https://mlsanity.com/paper/2403.18659/) (2024)

## Abstract (arXiv)

The current push towards interoperability drives companies to collaborate through process choreographies. At the same time, they face a jungle of continuously changing regulations, e.g., due to the pandemic and developments such as the BREXIT, which strongly affect cross-organizational collaborations. Think of, for example, supply chains spanning several countries with different and maybe even conflicting COVID19 traveling restrictions. Hence, providing automatic compliance verification in process choreographies is crucial for any cross-organizational business process. A particular challenge concerns the restricted visibility of the partner processes at the presence of global compliance rules (GCR), i.e., rules that span across the process of several partners. This work deals with the question how to verify global compliance if affected tasks are not fully visible. Our idea is to decompose GCRs into so called assertions that can be checked by each affected partner whereby the decomposition is both correct and lossless. The algorithm exploits transitivity properties of the underlying rule specification, and its correctness and complexity are proven, considering advanced aspects such as loops. The algorithm is implemented in a proof-of-concept prototype, including a model checker for verifying compliance. The applicability of the approach is further demonstrated on a real-world manufacturing use case.