fastNFA: Practical Approximate Counting for Non-Deterministic Finite Automata

Counting the number of words of a fixed length accepted by a non-deterministic finite automaton (NFA) is a fundamental problem in data management and formal verification, with applications in query answer counting, probabilistic model checking, and symbolic analysis. Recent theoretical advances have established fully polynomial-time randomized approximation schemes (FPRAS) for this SpanL-complete problem, culminating in an O(m³n² log(mn) ε⁻²) algorithm. However, the state-of-the-art algorithm remains orders of magnitude slower than brute-force enumeration on typical instances, rendering the theoretical breakthrough of limited utility in practice. We present the first practical FPRAS implementation for NFA counting, called fastNFA, through three algorithmic refinements: tightening probabilistic analysis via exact binomial computations, optimizing the algorithmic parameters for multi-core architectures, and efficiently processing deterministic substructures of the NFA. Our evaluation on 7,240 instances shows order-of-magnitude improvements: we solve 4,056 instances within 300 seconds compared to 149 for direct implementation of prior work, and obtain significantly lower PAR2 scores while maintaining rigorous (ε,δ)-approximation guarantees.