Existe-t-il un test efficace pour savoir si un NFA accepte un sous-ensemble d'un autre NFA?

Donc, je sais que tester si un langage régulier $R$ est un sous-ensemble du langage régulier $S$ est décidable, car nous pouvons les convertir tous les deux en DFA, calculer $R \cap \bar{S}$ , puis tester si ce langage est vide.

Cependant, comme cela nécessite une conversion en DFA, il est possible que les DFA, et donc l'algorithme de test, soient exponentiels en termes de nombre d'états dans les NFA en entrée.

Existe-t-il un moyen connu de le faire en temps polynomial? Ce problème a-t-il été prouvé en général que le Co-NP était complet?

$R$$S$$R \not \subseteq S$

EDIT: ceci est incorrect, car il n'y a aucune garantie qu'un tel mot serait polynomial dans le nombre d'états.

Le problème de la décision de confinement de la langue dans les NFA est complet sur . Pour le prouver, il est facile de réduire le problème d'universalité pour les NFA (tester si ) Donc, d'une certaine manière, vous devez déterminer, mais vous pouvez le faire à la volée.$PSPACE$$L(A)=\Sigma^*$

Votre observation sur le co-NP est fausse (mais agréable). Un tel témoin peut en effet être vérifié en temps polynomial dans le témoin , mais le témoin le plus court lui-même peut être exponentiel dans la longueur de l'entrée. Depuis , puis décider non-confinement est également -complete.$PSPACE=co-PSPACE$$PSPACE$

De dire les choses avec plus de soin, de décider si est la taille de (puisque seuls doit être complétée) et la taille de .$L(A)\subseteq L(B)$$PSPACE$$B$$B$$NLOGSPACE$$A$

Vous devriez jeter un œil à l'article de Jean-François Raskin, Antichain Algorithms for Finite Automata .

Dans nos expériences, le test d'inclusion basé sur la chaîne a réalisé un ou deux ordres de grandeur mieux que les approches "traditionnelles".

Si je me souviens bien, cet algorithme est implémenté dans la bibliothèque libAMoRE ++ .

La bibliothèque FSM AT&T est l'une des bibliothèques FSM gratuites les plus avancées, les plus avancées et les plus optimisées disponibles en ligne . Il implémente "fsmdifference" exactement comme vous le décrivez, nécessitant un FSM déterminé sans epsilon pour faire la différence. Une idée est de minimiser un ou les deux FSM avant de faire la différence, ce qui peut aider dans certains cas. (c'est-à-dire que la détermination n'est pas la même chose que la minimisation.) Ce paquet a également une minimisation "approximative" ou "gourmande" qui est conçue pour être éventuellement plus rapide qu'une minimisation complète.

Cependant, en étudiant des problèmes similaires, je pense qu'il y a une généralisation ou une construction de FSM qui n'apparaissent pas dans la littérature qui peut aider à résoudre ce problème en évitant l'étape de détermination, c'est-à-dire en inversant fondamentalement un NFA sans créer un FSM déterminé supplémentaire. L'idée est de traverser les bords NFA "en parallèle" et de suivre l'ensemble des nœuds qui font partie du "superstate" (ensemble d'états) actuel, tout comme avec l'algorithme de détermination standard. Ensuite, le complément NFA accepte si et seulement si l'ensemble des nœuds superstates actuels sont "tous non acceptants" (contrairement à la construction déterminante qui accepte ssi "toute acceptation").

Cependant, je n'ai jamais vu cela écrit auparavant et je ne le vois pas via une recherche en ligne rapide. De nombreuses références suggèrent ou impliquent que la seule façon de travailler avec le complément d'un NFA est de le déterminer.

Voici deux références "à proximité" qui pourraient être utiles pour certaines idées. Je serais intéressé d'entendre parler de ceux qui sont "plus proches". Vous mentionnez que vous travaillez sur la vérification de programme, qui peut être un domaine qui a des recherches plus directes sur le problème.

[1] Construction d'une intersection d'automates finis non déterministes à l'aide de la notation Z Nazir Ahmad Zafar, Nabeel Sabir et Amir Ali

[2] Constructions de complémentation pour les automates non déterministes sur des mots infinis Orna Kupferman et Moshe Vardi