Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DFAMiner: Mining minimal separating DFAs from labelled samples

Daniele Dell'Erba, Yong Li, Sven Schewe

TL;DR

The paper addresses Min-DFA inference for separating labelled samples by introducing DFAMiner, which combines incremental construction of a minimal $3DFA$ with SAT-based minimisation to a Min-$DFA$. It further explores a double-$3DFA$ (or $dDFA$) workflow and a direct APTA approach, achieving substantial empirical gains over prior tools and enabling parity-game solving insights. The results show smaller intermediate automata and faster minimisation, with promising applications to parity conditions, though sample generation remains a scalability bottleneck. Overall, the approach advances practical Min-DFA inference and offers a pathway to deeper understanding of separating automata in complex domains.

Abstract

We propose DFAMiner, a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don't-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to solving SAT problems. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that DFAMiner can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.

DFAMiner: Mining minimal separating DFAs from labelled samples

TL;DR

The paper addresses Min-DFA inference for separating labelled samples by introducing DFAMiner, which combines incremental construction of a minimal with SAT-based minimisation to a Min-. It further explores a double- (or ) workflow and a direct APTA approach, achieving substantial empirical gains over prior tools and enabling parity-game solving insights. The results show smaller intermediate automata and faster minimisation, with promising applications to parity conditions, though sample generation remains a scalability bottleneck. Overall, the approach advances practical Min-DFA inference and offers a pathway to deeper understanding of separating automata in complex domains.

Abstract

We propose DFAMiner, a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don't-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to solving SAT problems. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that DFAMiner can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.
Paper Structure (16 sections, 5 theorems, 1 equation, 10 figures, 6 tables, 1 algorithm)

This paper contains 16 sections, 5 theorems, 1 equation, 10 figures, 6 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Automata.
  4. Overview of DFAMiner
  5. The construction of 3DFAs
  6. Our proposal
  7. Evaluation
  8. Application in parity game solving
  9. Discussion and Future Work
  10. Minimal APTA construction
  11. SAT Encoding
  12. SAT-based encoding of minimisation
  13. SAT encoding of the representative DFA
  14. More experimental results
  15. Size growth of APTA, dDFA and 3DFA in parity game solving
  16. ...and 1 more sections

Key Result

theorem 1

The incremental construction produces the minimal 3DFA recognising exactly the sample set $S$.

Figures (10)

  • Figure 1: Workflow of DFAMiner with 3DFAs
  • Figure 2: Workflow of DFAMiner with dDFAs
  • Figure 3: figure
  • Figure 4: figure
  • Figure 5: Minimisation time of DFAMiner with double DFA and DFA inductor on 1,300 DFAs.
  • ...and 5 more figures

Theorems & Definitions (6)

  • theorem 1
  • theorem 2
  • theorem 3
  • proof
  • theorem 4
  • theorem 5