Deconstructing Subset Construction

Reducing While Determinizing

April 16, 2026 @ TACAS

John Nicol1 Markus Frohme2
1 Unaffiliated, United States
2 TU Dortmund University, Germany

NFA Canonization

NFA

DFA

DFA'

Honorable Mentions

NFA analysis

  • NFA universality testing (De Wulf et al., 2006)
  • NFA language inclusion testing (Abdulla et al., 2010)
  • NFA equivalence testing (Bonchi & Pous, 2013)

NFA canonization

  • 2-phase reversal of NFAs (Brzozowski, 1962)
  • External simulation information (Glabbeek & Ploeger, 2008)

On-The-Fly Minimization

NFA

DFA

DFA'

Subset Construction

A nondeterministic finite automaton (NFA) is a tuple $A = (S, \Sigma, \delta, S_0, F)$ such that

  • $S$ denotes a finite non-empty set of states,
  • $\Sigma$ denotes a finite non-empty set of input symbols,
  • $\delta \subseteq S \times \Sigma \times S$ denotes the transition relation,
  • $S_0 \subseteq S$ denotes the set of initial states, and
  • $F \subseteq S$ denotes the set of final (or accepting) states.

A deterministic finite automaton (DFA) is an NFA $A' = (S', \Sigma, \delta', S_0', F')$ such that $\vert S'_0 \vert = 1$ and $\delta'$ is functional.

                            
                            def determinize(nfa):

                                dfa = DFA()
                                dfa.S_0 = State(nfa.isAccepting(nfa.S_0))

                                mapping = {nfa.S_0: dfa.S_0}
                                queue = [nfa.S_0]

                                while len(queue) > 0:

                                    curr_nfa = queue.pop()
                                    curr_dfa = mapping[curr_nfa]

                                    for i in nfa.sigma:

                                        succ_nfa = nfa.delta[curr_nfa][i]
                                        succ_dfa = mapping[succ_nfa]

                                        if succ_dfa is None:
                                            succ_dfa = State(nfa.isAccepting(succ_nfa))
                                            mapping[succ_nfa] = succ_dfa
                                            queue.append(succ_nfa)

                                        dfa.delta[curr_dfa][i] = succ_dfa

                                return dfa
                            
                        
                            
                            def determinize(nfa, reg):

                                dfa = DFA()
                                dfa.S_0 = State(nfa.isAccepting(nfa.S_0))

                                reg.put(nfa.S_0, dfa.S_0)
                                queue = [nfa.S_0]

                                while len(queue) > 0:

                                    curr_nfa = queue.pop()
                                    curr_dfa = reg.get(curr_nfa)

                                    for i in nfa.sigma:

                                        succ_nfa = nfa.delta[curr_nfa][i]
                                        succ_dfa = reg.get(succ_nfa)

                                        if succ_dfa is None:
                                            succ_dfa = State(nfa.isAccepting(succ_nfa))
                                            reg.put(succ_nfa, succ_dfa)
                                            queue.append(succ_nfa)

                                        dfa.delta[curr_dfa][i] = succ_dfa

                                return dfa
                            
                        
                            
                            def determinize(nfa, reg, threshold):

                                dfa = DFA()
                                dfa.S_0 = State(nfa.isAccepting(nfa.S_0))

                                reg.put(nfa.S_0, dfa.S_0)
                                queue = [nfa.S_0]

                                while len(queue) > 0:

                                    curr_nfa = queue.pop()
                                    curr_dfa = reg.get(curr_nfa)

                                    for i in nfa.sigma:

                                        succ_nfa = nfa.delta[curr_nfa][i]
                                        succ_dfa = reg.get(succ_nfa)

                                        if succ_dfa is None:
                                            succ_dfa = State(nfa.isAccepting(succ_nfa))
                                            reg.put(succ_nfa, succ_dfa)
                                            queue.append(succ_nfa)

                                        dfa.delta[curr_dfa][i] = succ_dfa

                                    if threshold(dfa):
                                        equiv = minimize(dfa)
                                        for (s,t) in equiv:
                                            reg.unify(s,t)

                                return dfa

Equivalence Registries

A datastructure that supports the following operations:

  • PUT($Q, q'$) links the language of metastate $Q$ to state $q'$.
  • GET($Q$) returns a state $q' \in S'$ such that $L(Q) = L(q')$.
  • UNIFY($q'_1, q'_2$) informs the registry about the equivalence of states $q'_1$ and $q'_2$.

Convexity Closure Lattice (CCL)

Central observation by Bonchi & Pous: Let $A, B \subseteq S$, then we have

$$L(A \cup B) = L(A) \cup L(B)$$

In case of $L(A) = L(B)$, we have

$$L(A \cup B) = L(A) \cup L(B) = L(A) = L(B)$$

Generalized to any $X$ with $A \subseteq X \subseteq A \cup B$, we have

$$L(A \cup B) = L(X) = L(A)$$

Convexity Closure Lattice (CCL)

CCL with simulation (CCLS)

Let $a, b \in S$. If $b$ simulates $a$, i.e., $a \preceq b$, then

$$L(\{a\}) \subseteq L(\{b\})$$

Applied to our previous setting, this means

$$L(\{a,b\}) = L(\{a\}) \cup L(\{b\}) = L(\{b\})$$

Idea:

Prune (e.g., $\{a,b\} \mapsto \{b\}$) and saturate (e.g., $\{b\} \mapsto \{a,b\}$) $Q$ when invoking PUT($Q, q'$).

CCL with simulation (CCLS)

Benchmarks (Walnut)

Takeaways

  • NFA canonization via on-the-fly minimization
  • Parameterizable via equivalence registries and threshold predicates
  • Open-source implementation available at

https://github.com/jn1z/OTF

Bonus: Benchmarks (Walnut)

Bonus: Benchmarks (Ranmod)