Então, eu sei que testar se uma linguagem regular é um subconjunto de linguagem regular é decidível, já que pode converter-los tanto para DFAs, compute , e em seguida, teste se esta linguagem é vazia.
No entanto, como isso requer conversão em DFAs, é possível que os DFAs e, portanto, o algoritmo de teste sejam exponenciais em termos do número de estados nos NFAs de entrada.
Existe uma maneira conhecida de fazer isso em tempo polinomial? Este problema em geral foi provado Co-NP completo?
EDIT: está incorreto, pois não há garantia de que essa palavra seja polinomial no número de estados.
Respostas:
O problema de decidir a contenção de idiomas nos AFNs é incompleto. Para provar isso, é fácil reduzir o problema de universalidade para as AFNs (testando se L ( A ) = Σ ∗ ) Então, de certa forma, você precisa determinar, mas pode fazê-lo rapidamente.PSPACE L(A)=Σ∗
Sua observação sobre o co-NP está errada (mas agradável). Essa testemunha pode realmente ser verificada em tempo polinomial na testemunha , mas a testemunha mais curta em si pode ser exponencial no comprimento da entrada. Desde , em seguida, decidir não contenção é também P S P A C E -completo.PSPACE=co−PSPACE PSPACE
Para declarar as coisas com mais cuidado, decidindo se é P S P A C E no tamanho de B (já que apenas B precisa ser complementado) e N L O G S P A C E em o tamanho de um .L(A)⊆L(B) PSPACE B B NLOGSPACE A
fonte
Você deve dar uma olhada no artigo de Jean-François Raskin, Algoritmos Antichain para autômatos finitos .
Em nossos experimentos, o teste de inclusão baseado em antichain teve uma ou duas ordens de magnitude melhor do que as abordagens "tradicionalmente".
Se bem me lembro, esse algoritmo é implementado na biblioteca libAMoRE ++ .
fonte
Uma das melhores, mais completas e modernas bibliotecas FSM gratuitas, de ponta e altamente otimizadas, disponíveis on-line é a biblioteca AT&T FSM . Ele implementa "fsmdifference" exatamente como você descreve, exigindo um FSM sem epsilon determinado para fazer a diferença. Uma idéia é minimizar um ou ambos os FSMs antes de fazer a diferença, o que pode ajudar em alguns casos. (isto é, determinar não é o mesmo que minimizar.) Este pacote também possui uma minimização "aproximada" ou "gananciosa" projetada para ser possivelmente mais rápida que uma minimização completa.
No entanto, estudando problemas semelhantes, acredito que exista alguma generalização ou construção de FSMs que não apareçam na literatura que possam ajudar com esse problema, evitando a etapa de determinação, ou seja, basicamente invertendo um NFA sem criar um FSM determinado adicional. A idéia é atravessar as bordas do NFA "em paralelo" e acompanhar o conjunto de nós que fazem parte do "superestado" atual (conjunto de estados), exatamente como no algoritmo de determinação padrão. Então, o complemento NFA aceita se, e somente se, o conjunto de nós atuais do superestado for "não aceitável" (em contraste com a construção determinante que aceita se "aceitável").
No entanto, eu nunca vi isso escrito antes e não o vejo através de uma rápida pesquisa on-line. Existem muitas referências que sugerem ou implicam que a única maneira de trabalhar com o complemento de uma NFA é determiná-lo.
Aqui estão duas referências "próximas" que podem ser úteis para algumas idéias. Eu estaria interessado em ouvir qualquer um / outros que estão "mais próximos". Você mencionou que está trabalhando na verificação do programa, que pode ser um campo que possui pesquisas mais diretas sobre o problema.
[1] Construção da interseção de autômatos finitos não determinísticos usando a notação Z Nazir Ahmad Zafar, Nabeel Sabir e Amir Ali
[2] Construções de complementação para autômatos não determinísticos em palavras infinitas Orna Kupferman e Moshe Vardi
fonte