Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Formal Framework for the Explanation of Finite Automata Decisions

Jaime Cuartas Granada, Alexey Ignatiev, Peter J. Stuckey

TL;DR

This work investigates how to explain the behaviour of an FA on an input word in terms of the word's characters, and proposes an efficient method to determine all minimal explanations for the behaviour of an FA on a particular word.

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.

A Formal Framework for the Explanation of Finite Automata Decisions

TL;DR

This work investigates how to explain the behaviour of an FA on an input word in terms of the word's characters, and proposes an efficient method to determine all minimal explanations for the behaviour of an FA on a particular word.

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.
Paper Structure (23 sections, 16 theorems, 5 equations, 10 figures, 3 tables, 3 algorithms)

This paper contains 23 sections, 16 theorems, 5 equations, 10 figures, 3 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Finite Automata and Regular Expressions
  4. Classification Problems and Formal Explanations
  5. Explainable Finite Automata
  6. Why Formal Explanations?
  7. Computing One Formal Explanation
  8. Enumerating All Explanations
  9. Extra Heuristics.
  10. Experiments
  11. Deep Packet Inspection.
  12. Generated corpus of FA.
  13. DNA Sequence.
  14. Maze.
  15. Summary.
  16. ...and 8 more sections

Key Result

Proposition 1

(Proofs for this and all other propositions are provided in the Appendix) Given $w\in L(\mathcal{A})$, assume that the sets of all AXps and CXps are denoted as $\mathbb{A}=\{X\subseteq\{1,\ldots,|w|\} \mid \mathsf{AXp}_l^u(X, w)\in\mathbb{W}\}$ and $\mathbb{C}=\{Y\subseteq\{1,\ldots,|w|\} \mid \math

Figures (10)

  • Figure 1: Input bbbbb is accepted by this automata. Opaque states indicate transitions that are not traversed for the input bbbbb. Two valid explanations are bbbbb and (a shorter one) bbbbb.
  • Figure 2: DFA recognising the language (abcd+)|(ab[c-z]e+)|(bc+da)|(bc+).
  • Figure 3: Duality between AXps and CXps in $\mathbb{W}_1^1$. AXps fix the characters at given indices; CXps free them.
  • Figure 4: FFA for maze using language $\mathbb{W}_1^1$.
  • Figure 5: Deep Packet Inspection performance.
  • ...and 5 more figures

Theorems & Definitions (34)

  • Example 1
  • Definition 1: Abductive Explanation - AXp
  • Definition 2: Contrastive Explanation - CXp
  • Example 2: AXp and CXp
  • Example 3
  • Proposition 1
  • Proposition 2
  • Example 4
  • Proposition 3
  • Proposition 4
  • ...and 24 more