Entonces, sé que probar si un lenguaje regular es un subconjunto del lenguaje regular S es decidible, ya que podemos convertirlos a ambos en DFA, calcular R ∩ ˉ S y luego probar si este idioma está vacío.
Sin embargo, dado que esto requiere la conversión a DFA, es posible que los DFA, y por lo tanto el algoritmo de prueba, sean exponenciales en términos del número de estados en los NFA de entrada.
¿Hay alguna forma conocida de hacer esto en tiempo polinómico? ¿Se ha demostrado en general que este problema Co-NP está completo?
EDITAR: esto es incorrecto, ya que no hay garantía de que tal palabra sea polinómica en el número de estados.
Respuestas:
El problema de decidir la contención del lenguaje en los NFA es completo para . Para probar esto, es fácil reducir el problema de universalidad para los NFA (probar si ) Entonces, de alguna manera, tienes que determinar, pero puedes hacerlo sobre la marcha.PSPACE L(A)=Σ∗
Su observación sobre co-NP es incorrecta (pero agradable). Tal testigo se puede verificar en tiempo polinómico en el testigo , pero el testigo más corto en sí mismo puede ser exponencial en la longitud de la entrada. Como , entonces decidir no contención también es completo para .PSPACE=co−PSPACE PSPACE
Decir las cosas con más cuidado, decidir si es en el tamaño de (ya que sólo debe complementarse), y en el tamaño de .L(A)⊆L(B) PSPACE B B NLOGSPACE A
fuente
Deberías echar un vistazo al artículo Antichain Algorithms for Finite Automata de Jean-François Raskin .
En nuestros experimentos, la prueba de inclusión basada en antichain realizó uno o dos órdenes de magnitud mejor que los enfoques "tradicionalmente".
Si no recuerdo mal , este algoritmo se implementa en la biblioteca libAMoRE ++ .
fuente
Una de las mejores bibliotecas FSM gratuitas, avanzadas y altamente optimizadas, disponibles en línea es la biblioteca AT&T FSM . Implementa "fsmdifference" exactamente como usted describe, requiriendo un FSM libre de epsilon determinado para hacer la diferencia. Una idea es minimizar uno o ambos FSM antes de hacer la diferencia, lo que puede ayudar en algunos casos. (es decir, determinar no es lo mismo que minimizar). Este paquete también tiene una minimización "aproximada" o "codiciosa" que está diseñada para ser posiblemente más rápida que una minimización completa.
Sin embargo, al estudiar problemas similares, creo que hay una generalización o construcción de FSM que no aparecen en la literatura que pueden ayudar con este problema evitando el paso de determinación, es decir, básicamente invirtiendo un NFA sin crear un FSM determinado adicional. La idea es atravesar los bordes de NFA "en paralelo" y realizar un seguimiento del conjunto de nodos que forman parte del "superestado" actual (conjunto de estados) al igual que con el algoritmo de determinación estándar. Entonces, el complemento NFA acepta si y solo si el conjunto de nodos superestados actuales son "no aceptables" (en contraste con la construcción determinante que acepta iff "cualquier aceptación").
Sin embargo, no he visto esto escrito antes y no lo veo a través de una búsqueda rápida en línea. Hay muchas referencias que sugieren o implican que la única forma de trabajar con el complemento de un NFA es determinarlo.
Aquí hay dos referencias "cercanas" que pueden ser útiles para algunas ideas. Me interesaría saber de cualquiera / otros que estén "más cerca". Usted menciona que está trabajando en la verificación del programa, que puede ser un campo que tiene una investigación más directa sobre el problema.
[1] Construcción de la intersección de autómatas finitos no deterministas utilizando la notación Z Nazir Ahmad Zafar, Nabeel Sabir y Amir Ali
[2] Construcciones de complementación para autómatas no deterministas en palabras infinitas Orna Kupferman y Moshe Vardi
fuente