Towards Diagnostic Explainability in Workflow Verification via Shapley Attribution

Counts differ because each database indexes a different set of publications. We treat OpenAlex as the canonical count; Google Scholar is not shown (no API, and crawling it violates its ToS).

Workflow mining produces hierarchical workflow models from event logs, yet it is often unclear why such models satisfy or violate logical properties, or how individual model elements influence these outcomes. This work explores diagnostic explainability in workflow verification through the lens of attribution. We outline an approach that translates mined workflow models into logical specifications, checks properties, such as satisfiability, liveness and safety using automated theorem provers and interprets verification outcomes via Shapley values from the cooperative game theory. This attribution-based perspective provides a diagnostic view of how different parts of a workflow model contribute to property satisfaction or violation, highlighting elements that are critical, redundant or potentially harmful with respect to formal properties. Preliminary results suggest that Shapley-based attribution may support an interpretable workflow analysis while revealing limitations and trade-offs relevant to future research in explainable verification.

Last synced 2026-10-16 02:31 UTC