¿Cómo verifico que un DFA es equivalente a un NFA?

Estoy aprendiendo cómo convertir NFA a DFA y quiero asegurarme de que lo estoy haciendo bien. Obviamente, retroceder en la otra dirección no es una cosa. ¿Alguien sabe de un algoritmo para verificar que un DFA es equivalente a un NFA?

Esta es una pregunta problemática. Hay una manera de verificar la equivalencia de autómatas, que ahora explicaré, pero me temo que no te ayudará, como verás al final.

Recuerde que dos conjuntos y son iguales si y (esta es la definición de igualdad de conjunto). Por lo tanto, es suficiente que verifique que y , donde y son sus DFA y NFA, respectivamente.$A$$B$$A\subseteq B$$B\subseteq A$$L(D)\subseteq L(N)$$L(N)\subseteq L(D)$$D$$N$

Pero, ¿cómo verifica la contención de idiomas? Bueno, ahora observe que iff (donde es el complemento de ).$A\subseteq B$$A\cap \overline{B}=\emptyset$$\overline{B}$$B$

Consideremos primero verificar si . Para hacer esto, debe complementar (muy fácil: intercambie los estados de aceptación y rechazo), luego construya el autómata de intersección (por ejemplo, con la construcción del producto) con , y verifique el vacío, encontrando una ruta a un estado de aceptación.$L(N)\subseteq L(D)$$D$$N$

Sin embargo, la dirección inversa mostrará por qué esto no te ayuda. Con el fin de comprobar si , es necesario complementar . Pero para complementar un NFA, primero debe convertirlo en un DFA, lo que hace que la idea no tenga sentido.$L(D)\subseteq L(N)$$N$

Esencialmente, el problema con su pregunta es mucho más profundo: desea verificar que usted (un modelo computacional indefinido) ejecutó un algoritmo bien definido correctamente. Así que esto no es realmente un problema de informática.

Diré esto: siguiendo las construcciones que sugerí, no es difícil concluir que si hay una palabra de longitud como máximo ( es el número de estados de ) que es aceptado por uno y no por el otro. Para que pueda probar todas las palabras hasta esta longitud.2 2 n n $L(D)\neq L(N)$$2^{2n}$$n$$N$

Una forma de proceder es convertir el NFA en un DFA y luego verificar la equivalencia de los dos DFA, para lo cual existe un algoritmo lineal [1].

El siguiente documento trata el caso más general de la equivalencia de dos NFA (que por supuesto también se aplica a su caso).

Filippo Bonchi, Damien Pous, Comprobando la equivalencia de NFA con bisimulaciones hasta congruencia Principio de lenguajes de programación (POPL), enero de 2013, Roma, Italia. ACM, pp.457-468, 2013.

Abstracta . Introducimos la bisimulación hasta la congruencia como una técnica para probar la equivalencia del lenguaje de autómatas finitos no deterministas. Explotando esta técnica, ideamos una optimización del algoritmo clásico por Hopcroft y Karp [1]. Comparamos nuestro enfoque con los algoritmos antichain recientemente introducidos, analizando y relacionando los dos métodos de prueba coinductivos subyacentes. Damos ejemplos concretos donde mejoramos exponencialmente sobre antichains; Los resultados experimentales muestran además mejoras no despreciables.

[1] JE Hopcroft y RM Karp. Un algoritmo lineal para probar la equivalencia de autómatas finitos. TR 114, Cornell Univ., Diciembre de 1971.

Consulte también el apéndice web de este documento , que contiene scripts de prueba de Coq de los resultados, un enlace a una implementación y un applet interactivo.

Esta pregunta trata más sobre las pruebas de software aplicado y la verificación de la corrección en la práctica en lugar de una pregunta teórica.

• si tiene otro código para calcular las intersecciones y los complementos (y los idiomas vacíos de DFA), puede usar la idea de que y están vacíos donde está el complemento. D 2 ∩ ¯ D 1 ˉ $D_1 \cap \bar{D_2}$$D_2 \cap \bar{D_1}$$\bar{D}$

• puede confiar en el software probado previamente que se ha probado para validar sus resultados. por ejemplo, la biblioteca AT&T FSM

• Otra idea: pruebas aleatorias. elija cadenas aleatorias dentro de su idioma. determinar si las cadenas son aceptadas o no por el DFA / NFA. si los dos no son iguales, con alta probabilidad encontrará cadenas que no coinciden.

• Otra idea: puede escribir código para atravesar todas las ramas de DFA y NFA a una profundidad particular y buscar desajustes. Esto es equivalente a enumerar todas las posibles cadenas aceptadas de longitudes dadas.