Explainability Requirements as Hyperproperties

TL;DR

This work formalizes explainability as a hyperproperty for multi-agent systems by integrating Lewis-style counterfactuals, temporal logic, and knowledge into a unified framework. The authors introduce ICE, WCE, and GCE to capture internal, weak, and external facets of explainability, and demonstrate how these notions can be embedded into a hyperlogic whose model checking is decidable via translation to $FO[<,E]$ and HyperQPTL. A concrete hiring-system example illustrates how the framework distinguishes explainable from unexplainable behaviors and how observation and similarity relations drive agent-specific explanations. The paper establishes a rigorous taxonomy of explainability, proves decidability for finite-state models, and outlines a path toward practical verification tools, with future work on minimality constraints and probabilistic extensions. Overall, it provides a foundational formal theory and a viable verification route for explainability requirements in autonomous multi-agent systems.

Abstract

Explainability is emerging as a key requirement for autonomous systems. While many works have focused on what constitutes a valid explanation, few have considered formalizing explainability as a system property. In this work, we approach this problem from the perspective of hyperproperties. We start with a combination of three prominent flavors of modal logic and show how they can be used for specifying and verifying counterfactual explainability in multi-agent systems: With Lewis' counterfactuals, linear-time temporal logic, and a knowledge modality, we can reason about whether agents know why a specific observation occurs, i.e., whether that observation is explainable to them. We use this logic to formalize multiple notions of explainability on the system level. We then show how this logic can be embedded into a hyperlogic. Notably, from this analysis we conclude that the model-checking problem of our logic is decidable, which paves the way for the automated verification of explainability requirements.

Figures (3)

• Figure 1: Illustrating the semantics of the statements $\mathtt{K}_a \, \varphi$ and $\varphi \mathop{\mathrm{\operatorname{ }\space\rightarrow}}\nolimits_a \psi$ on a set of traces. The statements are evaluated at the second position of the trace $\pi$, which is framed by the black square. The epistemic operator $\mathtt{K}_a$ (cf. Subfigure \ref{['subfig:sem1']}) requires $\varphi$ to hold at the same position on all traces $\pi'$ with an observation equivalent prefix, i.e., where $\pi =_{\Omega(a)} \pi'$ is satisfied. These positions are covered by the area with diagonal lines (colored red). In contrast, the counterfactual $\mathop{\mathrm{\operatorname{ }\space\rightarrow}}\nolimits_a$ (cf. Subfigure \ref{['subfig:sem2']}) requires that the trace closest to $\rho$ that satisfies $\varphi$, which is in this case $\rho_1$, also satisfies $\psi$ at the same position. This is marked by the area with crossed lines (colored red and blue). $<_{\Sigma_a^\rho}$ is used in the illustration to denote, e.g., $(\rho_n,\rho_k) \in \Sigma_a^\rho \land (\rho_k,\rho_n) \notin \Sigma_a^\rho$, which means that $\rho_n$ is strictly more similar to $\rho$ than $\rho_k$.
• Figure 2: Lewis' original semantics for the counterfactuals $\mathop{\mathrm{\operatorname{ }\!\!\rightarrow}}\nolimits_a$ and $\mathop{\mathrm{\operatorname{ }\space\rightarrow}}\nolimits_a$ are illustrated in Subfigures \ref{['subfig:cf1a']} and \ref{['subfig:cf1a']}, respectively. Arrows and point depict traces that are ordered in ascending similarity to $\pi$ and $\rho$, respectively, according to the similarity relation $\geq_{\Sigma_a}$. Subfigure \ref{['subfig:cf2']} highlights problems when evaluating the counterfactual $\varphi$$\,\mathop{\mathrm{\operatorname{ }\!\!\rightarrow}}\nolimits_a$$\,\psi$ in a non-total similarity relation. Here, circles represent full traces such as $\phi$ or $\gamma$, while arrows indicate that two traces are ordered by the similarity relation $\leq_{\Sigma_a^\pi}$. In all subfigures, areas with diagonal lines (colored red) indicate that the covered traces satisfy $\varphi$, while crossed lines (colored red and blue) indicate that the traces satisfy $\psi$.
• Figure 3: KLTL's exact place in the hierarchy of hyperlogics. The result of Theorem \ref{['thm:exp']} is highlighted in bold.

Theorems & Definitions (11)

• Proposition 1
• Proposition 2
• Example 1
• Example 2
• Example 3
• Lemma 1
• proof
• Theorem 1: YLTL Model Checking
• proof
• Theorem 2