Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Decomposition Identification of Deterministic Finite Automata from Examples

Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang

TL;DR

A novel framework that bridges DFA decomposition with recent advancements in automata representation is proposed, which replaces APTA with 3-valued DFA (3DFA) derived directly from labeled examples, thus drastically reducing variables in the improved SAT encoding.

Abstract

The identification of deterministic finite automata (DFAs) from labeled examples is a cornerstone of automata learning, yet traditional methods focus on learning monolithic DFAs, which often yield a large DFA lacking simplicity and interoperability. Recent work addresses these limitations by exploring DFA decomposition identification problems (DFA-DIPs), which model system behavior as intersections of multiple DFAs, offering modularity for complex tasks. However, existing DFA-DIP approaches depend on SAT encodings derived from Augmented Prefix Tree Acceptors (APTAs), incurring scalability limitations due to their inherent redundancy. In this work, we advance DFA-DIP research through studying two variants: the traditional Pareto-optimal DIP and the novel states-optimal DIP, which prioritizes a minimal number of states. We propose a novel framework that bridges DFA decomposition with recent advancements in automata representation. One of our key innovations replaces APTA with 3-valued DFA (3DFA) derived directly from labeled examples. This compact representation eliminates redundancies of APTA, thus drastically reducing variables in the improved SAT encoding. Experimental results demonstrate that our 3DFA-based approach achieves significant efficiency gains for the Pareto-optimal DIP while enabling a scalable solution for the states-optimal DIP.

Efficient Decomposition Identification of Deterministic Finite Automata from Examples

TL;DR

A novel framework that bridges DFA decomposition with recent advancements in automata representation is proposed, which replaces APTA with 3-valued DFA (3DFA) derived directly from labeled examples, thus drastically reducing variables in the improved SAT encoding.

Abstract

The identification of deterministic finite automata (DFAs) from labeled examples is a cornerstone of automata learning, yet traditional methods focus on learning monolithic DFAs, which often yield a large DFA lacking simplicity and interoperability. Recent work addresses these limitations by exploring DFA decomposition identification problems (DFA-DIPs), which model system behavior as intersections of multiple DFAs, offering modularity for complex tasks. However, existing DFA-DIP approaches depend on SAT encodings derived from Augmented Prefix Tree Acceptors (APTAs), incurring scalability limitations due to their inherent redundancy. In this work, we advance DFA-DIP research through studying two variants: the traditional Pareto-optimal DIP and the novel states-optimal DIP, which prioritizes a minimal number of states. We propose a novel framework that bridges DFA decomposition with recent advancements in automata representation. One of our key innovations replaces APTA with 3-valued DFA (3DFA) derived directly from labeled examples. This compact representation eliminates redundancies of APTA, thus drastically reducing variables in the improved SAT encoding. Experimental results demonstrate that our 3DFA-based approach achieves significant efficiency gains for the Pareto-optimal DIP while enabling a scalable solution for the states-optimal DIP.

Paper Structure

This paper contains 20 sections, 8 theorems, 2 equations, 13 figures, 6 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Problem Formalization
  4. An Improved SAT Encoding of DFA-DIP via 3DFAs
  5. Existing encoding via APTAs
  6. Our improved encoding via 3DFAs
  7. Why not use minimal 3DFAs
  8. Identification Algorithms for DFA Decomposition
  9. Experimental Evaluation
  10. Comparison between ParetoAPTA and Pareto3DFA on solving Pareto-optimal DIP
  11. The scalability for our method on solving states-optimal DIP
  12. Conclusion and Future Work
  13. Acknowledgments.
  14. Proofs of Theorems and Lemmas
  15. SAT Encoding of DFA-DIP and Algorithm for Solving Pareto-optimal DIP in LaufferYVSS22
  16. ...and 5 more sections

Key Result

theorem thmcountertheorem

Given a set of examples $S = (S^{+}, S^{-})$, the 3DFA construction produces a 3DFA consistent with $S$.

Figures (13)

  • Figure 1: (a) The generated APTA, where an accepting node is represented by a double circle and a rejecting node is represented by a square. (b) and (c) show the two DFAs in a corresponding $(2,2)$-DFA decomposition $(\mathcal{A}_{1},\mathcal{A}_2)$ consistent with $S = (S^{+},S^{-})$.
  • Figure 2: The 3DFA $\mathcal{A} = (\mathcal{T}, A, R)$ constructed from the APTA in Fig.\ref{['subfig:example_apta']}, where $A=\{3,5\}$ and $R=\{6,7\}.$
  • Figure 3: Running time comparison between ParetoAPTA and Pareto3DFA
  • Figure 4: Box plots for the StatesOptimalDIP experiments
  • Figure 5: Running time comparison between ParetoAPTA and Pareto3DFA using two DFAs
  • ...and 8 more figures

Theorems & Definitions (16)

  • definition thmcounterdefinition: Deterministic finite automata
  • definition thmcounterdefinition: 3-valued DFAs DellErbaLS24
  • definition thmcounterdefinition: DFA decomposition LaufferYVSS22
  • definition thmcounterdefinition: Entropy of DFA decomposition
  • theorem thmcountertheorem
  • lemma thmcounterlemma
  • theorem thmcountertheorem
  • theorem thmcountertheorem: Termination and Correctness
  • theorem thmcountertheorem
  • proof
  • ...and 6 more