Unified explanations clarify cause and effect in reactive systems
Sufficient Reasons and Explanations for Reactive Systems
Formal Languages and Automata Theory
Summary
Understanding why a system does something over time can be tricky. This paper looks at how to explain the behavior of systems that react continuously to inputs, like software controlling machines. The authors combine two ways of explaining decisions, called sufficient reasons and contrastive explanations, and make them work for systems described using time-based rules. They also analyze how hard it is to find and check these explanations and show some examples using their own tool.
What this means in practice
- •For software developers: Provide clearer explanations for why reactive software systems behave as they do using time-based cause analysis.
- •For system test engineers: Detect and verify causes for failures in reactive systems using formal temporal reasoning methods.
Authors
Hadar Frenkel, Nadav Rutman Moshe
Abstract
We address the problem of temporal causality and explainability for reactive systems, and, in this setting, study sufficient reasons and contrastive explanations. These two notions are well-known explainability measures in the context of neural networks. In this work, we unify these notions for reactive systems and formal specifications given in temporal logic, providing dedicated definitions for sufficient reasons and contrastive explanations. We then lift these definitions to \emph{temporal} sufficient reasons and contrastive explanations, providing more general and symbolic representations of explainability. We analyze the complexity of both verifying and finding explanations of the different types, and we demonstrate our approach using a prototype implementation.