A Formal Framework for the Explanation of Finite Automata Decisions

TL;DR

This paper introduces an efficient method to identify minimal explanations for the decisions of finite automata on specific inputs, aiding interpretability of automata behavior.

Contribution

The work presents a novel, scalable approach to determine all minimal explanations for FA decisions, enhancing understanding of automata behavior.

Findings

Method efficiently finds all minimal explanations for FA decisions.

Approach scales well to complex automata and input words.

Provides unbiased insights into input features responsible for outcomes.

Abstract

Finite automata (FA) are a fundamental computational abstraction that is widely used in practice for various tasks in computer science, linguistics, biology, electrical engineering, and artificial intelligence. Given an input word, an FA maps the word to a result, in the simple case "accept" or "reject", but in general to one of a finite set of results. A question that then arises is: why? Another question is: how can we modify the input word so that it is no longer accepted? One may think that the automaton itself is an adequate explanation of its behaviour, but automata can be very complex and difficult to make sense of directly. In this work, we investigate how to explain the behaviour of an FA on an input word in terms of the word's characters. In particular, we are interested in minimal explanations: what is the minimal set of input characters that explains the result, and what are the minimal changes needed to alter the result? In this paper, we propose an efficient method to determine all minimal explanations for the behaviour of an FA on a particular word. This allows us to give unbiased explanations about which input features are responsible for the result. Experiments show that our approach scales well, even when the underlying problem is challenging.