Explainable Verification of Hierarchical Workflows Mined from Event Logs with Shapley Values

TL;DR

This paper introduces a method to explain hierarchical workflows mined from event logs by translating them into logical specifications and using Shapley values to attribute contributions of individual elements, aiding in compliance and optimization.

Contribution

It presents a novel approach combining logical analysis and Shapley values to explain workflow models and identify critical elements, redundancies, and harmful structures.

Findings

Identifies critical nodes in workflows

Reveals redundancies and harmful structures

Supports compliance and process optimization

Abstract

Workflow mining discovers hierarchical process trees from event logs, but it remains unclear why such models satisfy or violate logical properties, or how individual elements contribute to overall behavior. We propose to translate mined workflows into logical specifications and analyze properties such as satisfiability, liveness, and safety with automated theorem provers. On this basis, we adapt Shapley values from cooperative game theory to attribute outcomes to workflow elements and quantify their contributions. Experiments on benchmark datasets show that this combination identifies critical nodes, reveals redundancies, and exposes harmful structures. This outlines a novel direction for explainable workflow analysis with direct relevance to software engineering practice, supporting compliance checks, process optimization, redundancy reduction, and the design of next-generation process mining tools.