Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Radoslaw Klimek, Jakub Blazowski

TL;DR

This paper tackles explainability in mined hierarchical workflows by translating process trees into logical specifications and evaluating properties with automated theorem provers. It then augments this analysis with Shapley-value attribution to quantify each element's contribution to satisfiability, liveness, and safety. The authors introduce a pattern-based encoding of workflow operators into propositional temporal logic and two scalable Shapley-approximation methods, validating the approach on benchmark datasets to diagnose critical, redundant, and harmful nodes. The results demonstrate interpretable diagnostics that aid model simplification, compliance checks, and more informative process mining tools, bridging formal verification and explainable AI for software analytics and governance.

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.

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

TL;DR

This paper tackles explainability in mined hierarchical workflows by translating process trees into logical specifications and evaluating properties with automated theorem provers. It then augments this analysis with Shapley-value attribution to quantify each element's contribution to satisfiability, liveness, and safety. The authors introduce a pattern-based encoding of workflow operators into propositional temporal logic and two scalable Shapley-approximation methods, validating the approach on benchmark datasets to diagnose critical, redundant, and harmful nodes. The results demonstrate interpretable diagnostics that aid model simplification, compliance checks, and more informative process mining tools, bridging formal verification and explainable AI for software analytics and governance.

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.

Paper Structure

This paper contains 14 sections, 1 equation, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Logical Verification and Shapley Attribution
  3. Workflows as Logical Specifications
  4. Players, Coalitions and Shapley Values
  5. Approximation Strategies
  6. Preliminary Results
  7. Datasets and Setup
  8. Findings
  9. Interpretation of Results
  10. Model Diagnostics
  11. Limitations
  12. Potential Applications
  13. Future Work
  14. Conclusion

Figures (3)

  • Figure 1: Workflow tree mined from the BPI dataset at noise level 0.5, with nodes colored by Shapley values indicating their relative contribution to logical properties. Red nodes are critical, blue nodes redundant or harmful.
  • Figure 2: Effect of noise on positive vs. negative Shapley values.
  • Figure 3: Impact of noise on Shapley values across datasets. Left: correlation between noise and average $|\phi|$. Middle: average Shapley values vs. noise. Right: correlation strength by dataset and property.