# How do I verify that a DFA is equivalent to a NFA?

I'm learning how to convert NFAs to DFAs and I want to make sure I'm doing it right. Obviously, going back in the other direction isn't a thing. Does anyone know of an algorithm to check that a DFA is equivalent to a NFA?

• One candidate interpretation: is there a "result checker" (in the sense of Wasserman and Blum) for the problem of converting a NFA to a DFA? In other words, is there an algorithm that is asymptotically faster than doing the conversion itself, that given an alleged (input,output) pair for the conversion-algorithm, checks whether the output is correct? – D.W. Dec 9 '15 at 7:38

This is a problematic question. There is a way to check equivalence of automata, which I'll now explain, but I'm afraid it won't help you, as you will see at the end.

Recall that two sets $A$ and $B$ are equal iff $A\subseteq B$ and $B\subseteq A$ (this is the definition of set equality). Thus, it is enough for you to verify that $L(D)\subseteq L(N)$ and $L(N)\subseteq L(D)$, where $D$ and $N$ are your DFA and NFA, respectively.

But how do you check containment of languages, you might ask. Well, now observe that $A\subseteq B$ iff $A\cap \overline{B}=\emptyset$ (where $\overline{B}$ is the complement of $B$).

Let's consider first checking whether $L(N)\subseteq L(D)$. To do this, you need to complement $D$ (very easy - swap the accepting an rejecting states), then construct the intersection automaton (e.g. with the product construction) with $N$, and check for emptiness, by finding a path to an accepting state.

The converse direction, however, will show why this doesn't help you. In order to check whether $L(D)\subseteq L(N)$, you need to complement $N$. But in order to complement an NFA, you first need to convert it to a DFA, rendering the whole idea pointless.

Essentially, the problem with your question is much deeper: you want to verify that you (an undefined computational model) executed a well-defined algorithm properly. So this is not really a computer-science problem.

I will say this: following the constructions I suggested, it is not hard to conclude that $L(D)\neq L(N)$ iff there is a word of length at most $2^{2n}$ ($n$ being the number of states of $N$) that is accepted by one and not by the other. So you can try all words up to this length.

• Thank you for the well-thought out reply. I learned something new today. It sounds like my best bet is to just compare my work against JFLAP. – IAmOnStackExchange Dec 9 '15 at 6:43
• Unless your NFA is big (e.g. with more than 7-8 states), your best option is probably to just check yourself carefully. Typically, after removing non-reachable states, you get a small DFA, and checking manually is not too hard. – Shaull Dec 9 '15 at 6:49
• Can't you determinize and minimize both machines and check if the two machines are isomorphic ? – saadtaame Dec 9 '15 at 13:01

One way to proceed is to convert the NFA to a DFA and then check the equivalence of the two DFAs, for which there is a linear algorithm [1].

The following paper treats the more general case of the equivalence of two NFAs (which of course also applies to your case).

Filippo Bonchi, Damien Pous, Checking NFA equivalence with bisimulations up to congruence Principle of Programming Languages (POPL), Jan 2013, Roma, Italy. ACM, pp.457-468, 2013.

Abstract. We introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp [1]. We compare our approach to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements.

[1] J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata. TR 114, Cornell Univ., December 1971.

See also the web appendix to this paper, which contains Coq proof scripts of the results, a link to an implementation and an interactive applet.

• One way to proceed is to convert the NFA to a DFA, the goal of the poster is to verify the result of that algorithm. Applying twice is indeed one way but not immune to misunderstanding of the algorithm. That's probably why a checking method was asked. – AProgrammer Dec 9 '15 at 12:34
• @aprogrammer The main part of my answer is a reference to an algorithm for which a Coq proof script is available, which is certainly the safest checking method I can think of. – J.-E. Pin Dec 9 '15 at 12:46
• I'm not sure what someone unsure about his understanding of a simple algorithm like the NFA to DFA one will do with a Coq proof script. This looks like using algebra to solve the math problem of a third grader. – AProgrammer Dec 9 '15 at 12:56

this question is more about applied software testing and verifying correctness in practice rather than a theoretical question.

• if you have other code to compute intersections and complements (and empty DFA languages), you can use the idea that $D_1 \cap \bar{D_2}$ and $D_2 \cap \bar{D_1}$ are both empty where $\bar{D}$ is the complement.

• you can rely on prior tested software that has been tested to validate your results. eg AT&T FSM library

• another idea: randomized testing. pick random strings within your language. determine if the strings are accepted or unaccepted by the DFA/ NFA. if the two are not equal, with high probability you will find strings that mismatch.

• another idea: you can write code to traverse all branches of the DFA and NFA to some particular depth and look for mismatches. this is equivalent to enumerating all potential accepted strings of given lengths.