Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generating Counterfactual Explanations Under Temporal Constraints

Andrei Buliga, Chiara Di Francescomarino, Chiara Ghidini, Marco Montali, Massimiliano Ronzani

TL;DR

This paper tackles the challenge of generating counterfactual explanations for temporal process traces by enforcing background temporal knowledge expressed in $LTL_p$ within a genetic algorithm. It introduces temporal knowledge-aware crossover and mutation operators that, guided by a precomputed DFA $A_oldsymbol{ m \varphi}$, guarantee that generated counterfactual traces satisfy the temporal constraints by design. The fitness function combines standard counterfactual objectives (validity, proximity, sparsity, plausibility, diversity) with a new compliance term, enabling simultaneous optimization for outcome flip and background-consistency. Empirical results on real-world and synthetic process mining datasets show that the proposed approach yields temporally meaningful, compliant, and high-quality counterfactuals with favorable runtime characteristics, outperforming baseline GA and a mutate-and-retry strategy at higher coverage levels. This work enables reliable, interpretable explanations for temporal processes, with potential impact on predictive process monitoring and decision-support in domains where temporal feasibility is essential.

Abstract

Counterfactual explanations are one of the prominent eXplainable Artificial Intelligence (XAI) techniques, and suggest changes to input data that could alter predictions, leading to more favourable outcomes. Existing counterfactual methods do not readily apply to temporal domains, such as that of process mining, where data take the form of traces of activities that must obey to temporal background knowledge expressing which dynamics are possible and which not. Specifically, counterfactuals generated off-the-shelf may violate the background knowledge, leading to inconsistent explanations. This work tackles this challenge by introducing a novel approach for generating temporally constrained counterfactuals, guaranteed to comply by design with background knowledge expressed in Linear Temporal Logic on process traces (LTLp). We do so by infusing automata-theoretic techniques for LTLp inside a genetic algorithm for counterfactual generation. The empirical evaluation shows that the generated counterfactuals are temporally meaningful and more interpretable for applications involving temporal dependencies.

Generating Counterfactual Explanations Under Temporal Constraints

TL;DR

This paper tackles the challenge of generating counterfactual explanations for temporal process traces by enforcing background temporal knowledge expressed in within a genetic algorithm. It introduces temporal knowledge-aware crossover and mutation operators that, guided by a precomputed DFA , guarantee that generated counterfactual traces satisfy the temporal constraints by design. The fitness function combines standard counterfactual objectives (validity, proximity, sparsity, plausibility, diversity) with a new compliance term, enabling simultaneous optimization for outcome flip and background-consistency. Empirical results on real-world and synthetic process mining datasets show that the proposed approach yields temporally meaningful, compliant, and high-quality counterfactuals with favorable runtime characteristics, outperforming baseline GA and a mutate-and-retry strategy at higher coverage levels. This work enables reliable, interpretable explanations for temporal processes, with potential impact on predictive process monitoring and decision-support in domains where temporal feasibility is essential.

Abstract

Counterfactual explanations are one of the prominent eXplainable Artificial Intelligence (XAI) techniques, and suggest changes to input data that could alter predictions, leading to more favourable outcomes. Existing counterfactual methods do not readily apply to temporal domains, such as that of process mining, where data take the form of traces of activities that must obey to temporal background knowledge expressing which dynamics are possible and which not. Specifically, counterfactuals generated off-the-shelf may violate the background knowledge, leading to inconsistent explanations. This work tackles this challenge by introducing a novel approach for generating temporally constrained counterfactuals, guaranteed to comply by design with background knowledge expressed in Linear Temporal Logic on process traces (LTLp). We do so by infusing automata-theoretic techniques for LTLp inside a genetic algorithm for counterfactual generation. The empirical evaluation shows that the generated counterfactuals are temporally meaningful and more interpretable for applications involving temporal dependencies.

Paper Structure

This paper contains 22 sections, 2 theorems, 9 equations, 1 figure, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Running Example
  3. Background
  4. Linear Temporal Logic on Process Traces
  5. Counterfactual Explanations
  6. Genetic Algorithms
  7. Approach
  8. Optimisation Problem Formulations
  9. Temporal Knowledge-Aware Operators
  10. Temporal Knowledge-aware Crossover
  11. Temporal Knowledge-aware Mutation
  12. Correctness of the approach.
  13. Evaluation
  14. Baselines, Datasets and Evaluation metrics
  15. Experimental procedure
  16. ...and 7 more sections

Key Result

Theorem 1

Let $\varphi$ be a ltl$_p$ formula, and $\tau\xspace_{p_1}$, $\tau\xspace_{p_2}$, and $\tau\xspace$ be process traces over $\Sigma\xspace$, with $\tau\xspace \models \varphi$. Let $p_\text{c}\in\mathbb{R}_{[0,1]}$. Assume that Algorithm alg:crossoveroperator is invoked by passing $\tau\xspace_{p_1}

Figures (1)

  • Figure 1: Graphical representation of the dfa for the ltl$_p$ formula $\varphi_{\mathit{chk}} = (\neg \textnormal{man-chk}\xspace) \mathbin{\mathsf{U}} \textnormal{aut-chk}\xspace$. Each transition labelled $\overline{\Sigma\xspace_{\varphi_{\mathit{chk}}}\xspace}$ is a placeholder for the set of transitions connecting the same pair of states, one per activity in the set $\overline{\Sigma\xspace_{\varphi_{\mathit{chk}}}\xspace}$ (i.e., different from $\textnormal{man-chk}\xspace$ and $\textnormal{aut-chk}\xspace$).

Theorems & Definitions (4)

  • Theorem 1
  • proof
  • Theorem 2
  • proof