# An Information-Flow Perspective on Explainability Requirements: Specification and Verification

arXiv: https://arxiv.org/abs/2509.01479 · HTML: https://mlsanity.com/paper/2509.01479/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 56 references that are in the map.
- First posted on arXiv 1 Sep 2025.

## Builds on (most cited first, 16 of 16)

- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- ["Why Should I Trust You?": Explaining the Predictions of Any Classifier](https://mlsanity.com/paper/1602.04938/) (2016)
- [Explanation in Artificial Intelligence: Insights from the Social Sciences](https://mlsanity.com/paper/1706.07269/) (2017)
- [Counterfactual Explanations without Opening the Black Box: Automated Decisions and the GDPR](https://mlsanity.com/paper/1711.00399/) (2017)
- [Deep Learning for Case-Based Reasoning through Prototypes: A Neural Network that Explains Its Predictions](https://mlsanity.com/paper/1710.04806/) (2017)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [What Do We Want From Explainable Artificial Intelligence (XAI)? -- A Stakeholder Perspective on XAI and a Conceptual Model Guiding Interdisciplinary XAI Research](https://mlsanity.com/paper/2102.07817/) (2021)
- [Temporal Logics for Hyperproperties](https://mlsanity.com/paper/1401.4492/) (2014)
- [A unified logical framework for explanations in classifier systems](https://mlsanity.com/paper/2105.14452/) (2021)
- [Counterfactual Explanations for Misclassified Images: How Human and Machine Explanations Differ](https://mlsanity.com/paper/2212.08733/) (2022)
- [Expectation-Aware Planning: A Unifying Framework for Synthesizing and Executing Self-Explaining Plans for Human-Aware Planning](https://mlsanity.com/paper/1903.07269/) (2019)
- [AutoHyper: Explicit-State Model Checking for HyperLTL](https://mlsanity.com/paper/2301.11229/) (2023)
- [A Uniform Language to Explain Decision Trees](https://mlsanity.com/paper/2310.11636/) (2023)
- [The Hierarchy of Hyperlogics](https://mlsanity.com/paper/2005.05934/) (2020)
- [Visual Analysis of Hyperproperties for Understanding Model Checking Results](https://mlsanity.com/paper/2108.03698/) (2021)
- [Closure and Complexity of Temporal Causality](https://mlsanity.com/paper/2505.10186/) (2025)

## Abstract (arXiv)

Explainable systems expose information about why certain observed effects are happening to the agents interacting with them. We argue that this constitutes a positive flow of information that needs to be specified, verified, and balanced against negative information flow that may, e.g., violate privacy guarantees. Since both explainability and privacy require reasoning about knowledge, we tackle these tasks with epistemic temporal logic extended with quantification over counterfactual causes. This allows us to specify that a multi-agent system exposes enough information such that agents acquire knowledge on why some effect occurred. We show how this principle can be used to specify explainability as a system-level requirement and provide an algorithm for checking finite-state models against such specifications. We present a prototype implementation of the algorithm and evaluate it on several benchmarks, illustrating how our approach distinguishes between explainable and unexplainable systems, and how it allows to pose additional privacy requirements.