pith. sign in

arxiv: 2602.13351 · v2 · submitted 2026-02-12 · 💻 cs.AI · cs.FL· cs.LO

A Formal Framework for the Explanation of Finite Automata Decisions

Jaime Cuartas Granada , Alexey Ignatiev , Peter J. Stuckey This is my paper

Pith reviewed 2026-05-16 01:48 UTC · model grok-4.3

classification 💻 cs.AI cs.FLcs.LO
keywords finite automataminimal explanationsdecision explanationinput featuresformal methodsinterpretabilityautomaton verification
0
0 comments X

The pith

Finite automata decisions can be explained by identifying all minimal sets of input characters responsible for the outcome.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an efficient procedure to compute every minimal explanation for a finite automaton's result on a given word, where a minimal explanation is the smallest collection of characters from that word sufficient to determine whether the automaton accepts, rejects, or produces its result. This matters because automata often grow too large for direct inspection, yet their decisions appear in pattern matching, control systems, and verification tasks across multiple fields. The same procedure also yields the smallest changes to the input word that would flip the automaton's result. By returning every such minimal set rather than a single one, the method avoids favoring any particular character or position.

Core claim

The central claim is that all minimal explanations for an FA's behaviour on a particular word can be found efficiently by determining the minimal sets of input characters that suffice to produce the observed result, together with the minimal modifications that would change the result.

What carries the argument

Enumeration of minimal sets of input characters whose presence forces the automaton through the transitions that lead to its final result.

If this is right

  • Any finite automaton decision on any word admits a complete set of minimal character-based explanations.
  • The fewest changes to an input word that reverse the automaton's result can be identified directly from the same computation.
  • Explanations remain unbiased because every minimal set is reported rather than a selected subset of characters.
  • The technique applies to automata arising in linguistics, biology, electrical engineering, and verification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same minimal-set approach could be applied after converting other decision models, such as certain neural networks, into equivalent automata.
  • Highlighting critical input positions might help designers simplify or debug automata by revealing unnecessary dependencies.
  • The framework could be extended to weighted or probabilistic automata to explain expected outcomes with minimal sets of characters.

Load-bearing premise

Minimal collections of input characters are enough to explain and alter the automaton's decision without reference to the full transition sequence or non-minimal dependencies.

What would settle it

An automaton and input word for which the enumerated minimal character sets fail to determine the observed result or for which the enumeration procedure does not finish in reasonable time.

Figures

Figures reproduced from arXiv: 2602.13351 by Alexey Ignatiev, Jaime Cuartas Granada, Peter J. Stuckey.

Figure 1
Figure 1. 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. Interestingly, while the latter question can be related to the well-known problem of (and algorithms for) computing the minimum edit distance [29], no similar mechanisms exist for answering the former ‘why’ question. Moreover, a… view at source ↗
Figure 2
Figure 2. Figure 2: DFA recognising the language (abcd+)|(ab[c-z]e+)|(bc+da)|(bc+). We first define explanations abstractly, then consider concrete instantiations. An explanation is a regular language L from a set L(w, A) of candidate explanations, defined over the alphabet Σ and depending on both w and A. We refer to L(w, A) as the language of explanations. 3 Definition 1 (Abductive Explanation - AXp). A weak AXp for w ∈ L(A… view at source ↗
Figure 3
Figure 3. Figure 3: Duality between AXps and CXps in W1 1 . AXps fix the characters at given indices; CXps free them. Example 5 [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: FFA for maze using language W1 1 . the language W1 1 , which fixes the word length, making the symbol “up” a bad decision when there are only two remaining symbols. 6.1 Extra Heuristics. In practice, changing a single symbol in w ∈ L(A) often yields a counterexample, i.e. many CXps are singletons. We can determine all singleton CXps for w ∈ L(A) in Wu l by checking for each i ∈ {1, . . . , |w|} whether CXp… view at source ↗
Figure 5
Figure 5. Figure 5: Deep Packet Inspection performance. 0 100 200 300 400 500 600 instances 0 100 200 300 400 500 600 CPU time (s) 520 540 560 0 50 100 XpEnum(false) XpEnum(true)-Warm XpEnum(true) [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Generated FA corpus, with accepted words. We use a dataset of 98 File Transfer Protocol (FTP) signatures from [31].5 The task is to check whether a given word matches any of these reg￾ular expressions. We created an FA with the union of the 98 regular expressions, resulting in an (non-deterministic) FA with 30,590 states and 2,752,238 transitions.6 This large FA is used to test scalability of Al￾gorithm 2.… view at source ↗
Figure 7
Figure 7. Figure 7: Motifs in DNA sequences. DNA Sequence. DNA is a molecule con￾formed by two complementary chains of nu￾cleotides. These nucleotides contain four types: adenine (A), thymine (T), cytosine (C), and gua￾nine (G). DNA sequences contain motifs, which are recurring patterns that are deemed to have a biological function [8]. We used a benchmark of 25 datasets of real DNA sequences with a known mo￾tif [27].7 Each d… view at source ↗
Figure 8
Figure 8. Figure 8: Rejected paths in mazes. Maze. This benchmark set is based on the Ex￾ample 7, we generate 861 mazes with dimensions ranging from 10×10 to 50×50. For each height h ∈ {10, . . . , 50}, we produce mazes of size h × w for all w ∈ {h, . . . , 50}. This results in a total of P5 h=10 0(51 − h) = 861 distinct maze sizes. Walls were randomly placed with a 1/3 proba￾bility per cell. To generate a rejected path, we r… view at source ↗
Figure 9
Figure 9. Figure 9: Maze with a rejected path and its minimal cardinality CXps using [PITH_FULL_IMAGE:figures/full_fig_p016_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Maze with a rejected path and its minimal cardinality CXps using [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Generated corpus with rejected words Many patterns in this corpus are easy to match with long words. For example, with l = 5, m = 1, d = 2 a possible pattern is (a|b)∗abbba(a|b)∗ . A long word that does not match this pattern may have a large num￾ber of didsjoint CXps, as many positions can be modified to match the pattern. Impliying that the number of AXps is exponential in the number of CXps (Propositio… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper proposes a formal framework for explaining finite automata (FA) decisions on a given input word by identifying all minimal sets of input characters responsible for the outcome (accept/reject or other results). It introduces an efficient algorithm to enumerate these minimal explanations, enabling unbiased attribution of input features, and reports experimental results showing good scalability even on challenging instances.

Significance. If the central algorithmic claim holds, the work provides a principled, model-agnostic way to interpret FA behavior in terms of minimal input features. This could be useful for debugging, verification, and explainability in domains where automata are deployed (e.g., protocol checking, pattern matching). The emphasis on enumerating all minimal explanations rather than a single one is a strength, as is the focus on both explanatory and counterfactual (minimal-change) aspects.

major comments (3)
  1. [Abstract, §3] Abstract and §3 (algorithm description): The claim of an 'efficient method' to determine all minimal explanations is not supported by any complexity statement. For nondeterministic automata the number of minimal hitting sets over accepting paths can be exponential in the input length; without an output-polynomial bound or reduction showing that enumeration avoids this blow-up, the efficiency assertion remains unsubstantiated.
  2. [§4] §4 (experiments): The scaling results are reported without reference to the number of minimal explanations produced or to worst-case instances (e.g., highly nondeterministic automata with exponentially many minimal sets). It is therefore impossible to assess whether the observed runtimes are consistent with output-sensitive efficiency or simply reflect instances with few explanations.
  3. [§2] §2 (formal definitions): The notion of 'minimal explanation' is defined via minimal sets of positions whose characters determine acceptance, but the paper does not prove that every minimal set is a minimal hitting set of the accepting paths, nor does it address whether the enumeration procedure returns exactly those sets without duplication or omission when the automaton is nondeterministic.
minor comments (2)
  1. [§2] Notation for the set of minimal explanations is introduced without a running example that illustrates both the input word and the enumerated sets; adding such an example early would improve readability.
  2. [§4] The experimental section should report the number of minimal explanations found per instance alongside runtime, to allow readers to judge output sensitivity.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for their thorough review and constructive feedback on our manuscript. We address each of the major comments below, indicating the changes we will make to strengthen the paper.

read point-by-point responses

  1. Referee: [Abstract, §3] Abstract and §3 (algorithm description): The claim of an 'efficient method' to determine all minimal explanations is not supported by any complexity statement. For nondeterministic automata the number of minimal hitting sets over accepting paths can be exponential in the input length; without an output-polynomial bound or reduction showing that enumeration avoids this blow-up, the efficiency assertion remains unsubstantiated.

    Authors: We agree that an explicit complexity analysis is necessary to substantiate the efficiency claim. In the revised manuscript, we will add a detailed complexity analysis in §3, proving that our enumeration algorithm runs in time polynomial in the input size and the number of minimal explanations (i.e., output-polynomial time). This addresses the potential exponential blow-up by showing that the procedure only generates minimal sets and does so efficiently relative to the output size. revision: yes

  2. Referee: [§4] §4 (experiments): The scaling results are reported without reference to the number of minimal explanations produced or to worst-case instances (e.g., highly nondeterministic automata with exponentially many minimal sets). It is therefore impossible to assess whether the observed runtimes are consistent with output-sensitive efficiency or simply reflect instances with few explanations.

    Authors: We acknowledge the need for more detailed reporting in the experiments. We will revise §4 to include the number of minimal explanations for each benchmark instance and add experiments on worst-case nondeterministic automata to demonstrate the output-sensitive behavior of the algorithm. revision: yes

  3. Referee: [§2] §2 (formal definitions): The notion of 'minimal explanation' is defined via minimal sets of positions whose characters determine acceptance, but the paper does not prove that every minimal set is a minimal hitting set of the accepting paths, nor does it address whether the enumeration procedure returns exactly those sets without duplication or omission when the automaton is nondeterministic.

    Authors: We will strengthen the formal section by adding a proof that the minimal explanations are precisely the minimal hitting sets of the accepting paths. Additionally, we will prove that the enumeration procedure is complete, sound, and duplication-free for both deterministic and nondeterministic automata. revision: yes

Circularity Check

0 steps flagged

No circularity: new enumeration method for minimal FA explanations is self-contained

full rationale

The paper proposes a direct algorithmic framework for enumerating all minimal sets of input characters that explain an FA's accept/reject decision on a given word. No equations or steps reduce by construction to fitted parameters, self-definitions, or prior self-citations that would make the result tautological. The method is introduced as a fresh formalization independent of any load-bearing external result from the same authors; experiments are presented as empirical validation rather than a hidden fit. The derivation chain remains non-circular because the core claim (efficient enumeration of minimal explanations) does not presuppose its own output or rely on uniqueness theorems imported from overlapping prior work.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper builds on standard finite automata theory without introducing new free parameters or entities; the novelty is in the explanation method.

axioms (1)
  • standard math Finite automata accept or reject words based on their transition rules
    Core definition from automata theory invoked implicitly.

pith-pipeline@v0.9.0 · 5527 in / 1089 out tokens · 219117 ms · 2026-05-16T01:48:07.656956+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    Aho, Ravi Sethi, and Jeffrey D

    Alfred V . Aho, Ravi Sethi, and Jeffrey D. Ullman.Compilers: Principles, Techniques, and Tools. Addison- Wesley series in computer science / World student series edition. Addison-Wesley, 1986

    work page 1986

  2. [2]

    Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI.Inf

    Alejandro Barredo Arrieta, Natalia Díaz Rodríguez, Javier Del Ser, Adrien Bennetot, Siham Tabik, Alberto Barbado, Salvador García, Sergio Gil-Lopez, Daniel Molina, Richard Benjamins, Raja Chatila, and Francisco Herrera. Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI.Inf. Fusion, 58:82–115, 2020

    work page 2020

  3. [3]

    Carroll and Darrell D

    John L. Carroll and Darrell D. E. Long.Theory of finite automata with an introduction to formal languages. Prentice Hall, 1989. 10

    work page 1989

  4. [4]

    Mata: A fast and simple finite automata library

    David Chocholatý, Tomás Fiedor, V ojtech Havlena, Lukás Holík, Martin Hruska, Ondrej Lengál, and Juraj Síc. Mata: A fast and simple finite automata library. InTACAS (2), volume 14571 ofLecture Notes in Computer Science, pages 130–151. Springer, 2024

    work page 2024

  5. [5]

    Danesh, Anurag Koul, Alan Fern, and Saeed Khorram

    Mohamad H. Danesh, Anurag Koul, Alan Fern, and Saeed Khorram. Re-understanding finite-state represen- tations of recurrent policy networks. InICML, volume 139 ofProceedings of Machine Learning Research, pages 2388–2397. PMLR, 2021

    work page 2021

  6. [6]

    Logic for explainable AI

    Adnan Darwiche. Logic for explainable AI. InLICS, pages 1–11. IEEE, 2023

    work page 2023

  7. [7]

    On the (complete) reasons behind decisions.J

    Adnan Darwiche and Auguste Hirth. On the (complete) reasons behind decisions.J. Log. Lang. Inf., 32(1):63–88, 2023

    work page 2023

  8. [8]

    What are dna sequence motifs?Nature Biotechnology, 24(4):423–425, 2006

    Patrik D’haeseleer. What are dna sequence motifs?Nature Biotechnology, 24(4):423–425, 2006

    work page 2006

  9. [9]

    Graeme Gange, Pierre Ganty, and Peter J. Stuckey. Fixing the state budget: Approximation of regular languages with small dfas. InATVA, volume 10482 ofLecture Notes in Computer Science, pages 67–83. Springer, 2017

    work page 2017

  10. [10]

    Solving optimization problems with DLL

    Enrico Giunchiglia and Marco Maratea. Solving optimization problems with DLL. InECAI, pages 377–381, 2006

    work page 2006

  11. [11]

    Gurobi optimizer reference manual, 2024

    LLC Gurobi Optimization. Gurobi optimizer reference manual, 2024. URL:http://www.gurobi.com

    work page 2024

  12. [12]

    Deepsynth: Automata synthesis for automatic task segmentation in deep reinforcement learning

    Mohammadhosein Hasanbeig, Natasha Yogananda Jeppu, Alessandro Abate, Tom Melham, and Daniel Kroening. Deepsynth: Automata synthesis for automatic task segmentation in deep reinforcement learning. InAAAI, pages 7647–7656. AAAI Press, 2021

    work page 2021

  13. [13]

    III Hunt

    Harry B. III Hunt. On the time and tape complexity of languages. InProceedings of the 5th Annual ACM Symposium on Theory of Computing, pages 10–19. ACM Press, 1973.doi:10.1145/800125.804030

    work page doi:10.1145/800125.804030 1973

  14. [14]

    PySAT: A Python toolkit for prototyping with SAT oracles

    Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. InSAT, pages 428–437, 2018.doi:10.1007/978-3-319-94144-8_26

    work page doi:10.1007/978-3-319-94144-8_26 2018

  15. [15]

    RC2: an efficient maxsat solver.J

    Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver.J. Satisf. Boolean Model. Comput., 11(1):53–64, 2019

    work page 2019

  16. [16]

    From contrastive to abductive explanations and back again

    Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and João Marques-Silva. From contrastive to abductive explanations and back again. InAI*IA, volume 12414 ofLecture Notes in Computer Science, pages 335–355. Springer, 2020

    work page 2020

  17. [17]

    Towards universally accessible SAT technology

    Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In SAT, pages 4:1–4:11, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.16, doi:10.4230/ LIPICS.SAT.2024.16

    work page doi:10.4230/lipics.sat.2024.16 2024

  18. [18]

    Liffiton and Ammar Malik

    Mark H. Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple muses quickly. InCPAIOR, volume 7874 ofLecture Notes in Computer Science, pages 160–175. Springer, 2013

    work page 2013

  19. [19]

    Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva

    Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva. Fast, flexible MUS enumera- tion.Constraints An Int. J., 21(2):223–250, 2016

    work page 2016

  20. [20]

    Delivering trustworthy AI through formal XAI

    João Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. InAAAI, pages 12342–12350. AAAI Press, 2022

    work page 2022

  21. [21]

    No silver bullet: interpretable ML models must be ex- plained.Frontiers Artif

    Joao Marques-Silva and Alexey Ignatiev. No silver bullet: interpretable ML models must be ex- plained.Frontiers Artif. Intell., 6, 2023. URL: https://doi.org/10.3389/frai.2023.1128212, doi:10.3389/FRAI.2023.1128212

    work page doi:10.3389/frai.2023.1128212 2023

  22. [22]

    Explainable reinforcement learning: A survey and comparative review.ACM Comput

    Stephanie Milani, Nicholay Topin, Manuela Veloso, and Fei Fang. Explainable reinforcement learning: A survey and comparative review.ACM Comput. Surv., 56(7):168:1–168:36, 2024

    work page 2024

  23. [23]

    Explanation in artificial intelligence: Insights from the social sciences.Artif

    Tim Miller. Explanation in artificial intelligence: Insights from the social sciences.Artif. Intell., 267:1–38, 2019. 11

    work page 2019

  24. [24]

    Finite automata

    Dominique Perrin. Finite automata. InHandbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 1–57. Elsevier and MIT Press, 1990

    work page 1990

  25. [25]

    Partial MUS enumeration

    Alessandro Previti and João Marques-Silva. Partial MUS enumeration. In Marie desJardins and Michael L. Littman, editors,AAAI, pages 818–825, 2013

    work page 2013

  26. [26]

    Rabin and Dana S

    Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems.IBM J. Res. Dev., 3(2):114–125, 1959

    work page 1959

  27. [27]

    Improved benchmarks for computa- tional motif discovery.BMC Bioinform., 8, 2007

    Geir Kjetil Sandve, Osman Abul, Vegard Walseng, and Finn Drabløs. Improved benchmarks for computa- tional motif discovery.BMC Bioinform., 8, 2007

    work page 2007

  28. [28]

    PWS Publishing Company, 1997

    Michael Sipser.Introduction to the theory of computation. PWS Publishing Company, 1997

    work page 1997

  29. [29]

    Robert A. Wagner. Order-ncorrection for regular languages.Commun. ACM, 17(5):265–268, 1974

    work page 1974

  30. [30]

    A survey on regular expression matching for deep packet inspection: Applications, algorithms, and hardware platforms.IEEE Commun

    Chengcheng Xu, Shuhui Chen, Jinshu Su, Siu-Ming Yiu, and Lucas Chi Kwong Hui. A survey on regular expression matching for deep packet inspection: Applications, algorithms, and hardware platforms.IEEE Commun. Surv. Tutorials, 18(4):2991–3029, 2016

    work page 2016

  31. [31]

    Improving nfa-based signature matching using ordered binary decision diagrams

    Liu Yang, Rezwana Karim, Vinod Ganapathy, and Randy Smith. Improving nfa-based signature matching using ordered binary decision diagrams. InRAID, volume 6307 ofLecture Notes in Computer Science, pages 58–78. Springer, 2010

    work page 2010

  32. [32]

    Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime approximate formal feature attribution. InSAT, pages 30:1–30:23, 2024

    work page 2024

  33. [33]

    accept” s.t. κ is the DFA applied to w. Similarly CXpu l (S, w) is a CXp iff S is a CXp of the classification problem κ(w) =“accept

    Jinqiang Yu, Alexey Ignatiev, and Peter J. Stuckey. On formal feature attribution and its approximation. CoRR, abs/2307.03380, 2023. 12 A Supplementary Material A.1 Propositions and proofs This section provides the complete set of formal propositions and their corresponding proofs. Proposition 1.Given w∈L(A) , assume that the sets of all AXps and CXps are...

    work page arXiv 2023

  34. [34]

    replacing aw[i]-transition inA w with aΣ-transition, inO(1)time

    work page

  35. [35]

    replacing a Σ-transition in Aw with a w[i]-transition, in O(1) time (if the check determines that position imust be kept)

    work page

  36. [36]

    checking whether AXpu l (X\ {i}, w)≜L(A w)⊆L(A) , in O(|Σ|mn) time because |A|=m and |Aw|=n+ 1(the above operationsdo not addnew states inA w). Hence, the overall complexity of the algorithm isO(|Σ|mn 2)for the languageW 1 1.8 Proposition 7.Computing a single AXp using W∞ 0 for w∈L(R) given a regular expression R is PSPACE-hard. Proof. Note that ∅ defines...

    work page 2000

  37. [37]

    , d}for l∈ {5,10,15,20} , m∈ {1,3,5,10} , 16 Table 3: Average number of explanations computed if reaching the timeout

    For the generated corpus, we generated m random words M with length l over the alphabet{1, . . . , d}for l∈ {5,10,15,20} , m∈ {1,3,5,10} , 16 Table 3: Average number of explanations computed if reaching the timeout. Corpus (rejected) AXp CXp XPENUM(f alse) 254.0 1.0 XPENUM(true) 51976.7 540.2 XPENUM(true)-WARM52964.1 543.0 d∈ {2,3,5,10} . Figure 11 shows ...

    work page