Ricerc@Sapienza

Modern companies execute business processes to deliver products and services, whose enactment requires to adhere to laws and regulations. Compliance checking is the task of identifying potential violations of such requirements prior to process execution. Traditional approaches to compliance checking employ formal verification techniques (e.g., model checking) to identify which process paths in a process model may lead to violations. However, this diagnostics is, in most of the cases, not rich enough for the user to understand how the process model should be changed to solve the violations.

Declarative approaches to business process modeling allow to represent loosely-structured
(declarative) processes in flexible scenarios as a set of constraints on the allowed flow of
activities. However, current graphical notations for declarative processes are difficult to
interpret. As a consequence, this has affected widespread usage of such notations, by
increasing the dependency on experts to understand their semantics. In this paper, we
tackle this issue by introducing a novel visual declarative notation targeted to a more

Nowadays, business processes are increasingly supported by IT services that produce massive amounts of event data during the execution of a process. These event data can be used to analyze the process using process mining techniques to discover the real process, measure conformance to a given process model, or to enhance existing models with performance information. Mapping the produced events to activities of a given process model is essential for conformance checking, annotation and understanding of process mining results.