Intersecting Dense Automata
This work provides a more efficient algorithm for NFA intersection emptiness, a fundamental problem in automata theory and formal verification, with optimality conditional on a long-standing combinatorial conjecture.
The paper addresses the inefficiency of the classical Cartesian product construction for intersecting nondeterministic finite automata (NFA), which can produce Θ(m²) transitions. It presents alternative constructions with O(m n) transitions for two NFA and O(m n^{k-1}) for k NFA, leading to a faster algorithm for NFA intersection emptiness that is optimal unless a breakthrough in clique detection occurs.
We observe that the classical Cartesian product construction for the intersection of (languages of) nondeterministic finite automata (NFA) is non-optimal in the worst case, if the automata have many transitions. For a fixed alphabet, the product of two NFA may have $Θ(m^2)$ transitions if these NFA have at most $n$ states and $m$ transitions each. We describe alternative constructions with $O(m n)$ transitions: or $O(m n^{k-1})$ for the intersection of $k$ NFA (for fixed $k \ge 2$ and alphabet $Σ$). This gives a faster algorithm for deciding NFA intersection emptiness. The new algorithm is optimal, unless there exists a breakthrough combinatorial algorithm for detecting $(k+1)$-cliques in undirected graphs. This also leads to a more efficient certification scheme for NFA intersection emptiness.