Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

So, I know that testing if a regular language $R$ is a subset of regular language $S$ is decidable, since we can convert them both to DFAs, compute $R \cap \bar{S}$, and then test if this language is empty.

However, since this requires converting to DFAs, it's possible that the DFAs, and thus the testing algorithm, will be exponential in terms of the number of states in the input NFAs.

Is there a known way to do this in polynomial time? Has this problem in general been proved Co-NP complete?

Note that the problem is in Co-NP since a word accepted by $R$ but not by $S$ would be a polynomial certifier that $R \not \subseteq S $.

EDIT: this is incorrect, as there is no guarantee that such a word would be polynomial in the number of states.

share|improve this question
1  
is this a theoretical question, or about in practice? sometimes for a particular "distribution" of inputs encountered in practice, a Pspace complete problem may be "runnable" in P time. –  vzn Feb 21 '13 at 2:00
    
Ideally it's theoretical, but the proofs I'm working on are heavily driven by computer testing, which means that a fast algorithm would definitely be useful. –  jmite Feb 21 '13 at 2:31
    
so yeah, theres a pretty straightfwd algorithm that works by just following the transitions in parallel for each of the two machines and keeping track of the resulting state sets, somewhat like the std determinization algorithm. dont know if its in the literature somewhere, its so simple that presume it is. are you already using some algorithm? it would be helpful if you cite it. also more details on the type of inputs would be helpful. it also sounds like you want to determine if the intersection of two NFAs is empty? do you want the language of the intersection or just Y/N if it is nonempty? –  vzn Feb 21 '13 at 2:40
    
I'm just looking for if it's empty, the idea being I'm looking if $R-S=\{\}$ to test if $R \subseteq S$. The parallel transition algorithm works, I think the hard part is taking the compliment of an NFA, you have to convert to DFA first. The algorithm I've been using right now is just brute-force, since I'm only dealing with finite languages. –  jmite Feb 21 '13 at 3:25
    
believe there may be a way to traverse the two NFAs without converting either to a DFA 1st, even finding the complement of one also. but havent seen it in a ref. –  vzn Feb 21 '13 at 3:57
add comment

3 Answers

up vote 14 down vote accepted

The problem of deciding language containment in NFAs is $PSPACE$-complete. To prove this, it is easy to reduce from the universaility problem for NFAs (testing whether $L(A)=\Sigma^*$) So, in a way, you have to determinize, but you may do so on-the-fly.

Your observation about co-NP is wrong (but nice). Such a witness can indeed be checked in polynomial time in the witness, but the shortest witness itself may be exponential in the length of the input. Since $PSPACE=co-PSPACE$, then deciding non-containment is also $PSPACE$-complete.

To state things more carefully, deciding whether $L(A)\subseteq L(B)$ is $PSPACE$ in the size of $B$ (since only $B$ needs to be complemented), and $NLOGSPACE$ in the size of $A$.

share|improve this answer
    
You're absolutely right. I have been dealing with a specific class of NFAs where what I said holds, but it definitely might not with general infinite NFAs. Thanks! –  jmite Feb 20 '13 at 6:18
    
You wouldn't have a reference to a paper or textbook that proves it PSPACE-complete, would you? –  jmite Feb 20 '13 at 6:21
1  
It's not a very detailed proof, but I think it will do: wisdom.weizmann.ac.il/~vardi/av/notes/lec4.ps –  Shaull Feb 20 '13 at 6:44
add comment

You should have a look at Jean-François Raskin's paper Antichain Algorithms for Finite Automata.

In our experiments, the antichain-based inclusion test performed one or two orders of magnitude better than the "traditionally" approaches.

If I remember correctly, this algorithm is implemented in the libAMoRE++ library.

share|improve this answer
add comment

One of the best, most thorough state-of-the-art and highly optimized, free FSM libraries available online is the AT&T FSM library. It implements "fsmdifference" exactly as you describe, requiring a determinized epsilon-free FSM to do the difference. One idea is to minimize one or both of the FSMs before doing the difference, that may help in some cases. (i.e. determinizing is not the same as minimizing.) This package also has an "approximate" or "greedy" minimization that is designed to be possibly faster than a full minimization.

However, studying similar problems, I believe there is some generalization or construction of FSMs that do not appear in the literature that can help with this problem by avoiding the determinization step, i.e. basically inverting an NFA without creating an additional determinized FSM. The idea is to traverse the NFA edges "in parallel" and keep track of the set of nodes that are part of the current "superstate" (set of states) just like with the standard determinizing algorithm. Then, the NFA complement accepts if and only if the set of current superstate nodes are "all nonaccepting" (in contrast to the determinizing construction which accepts iff "any accepting").

However, I have not seen this written up before and don't see it via a quick online search. There are many references that suggest or imply that the only way to work with the complement of an NFA is to determinize it.

Here are two "nearby" references that might be useful for some ideas. I would be interested to hear of any/others that are "closer". You mention you are working on program verification, which may be a field that has more direct research on the problem.

[1] Construction of Intersection of Nondeterministic Finite Automata using Z Notation Nazir Ahmad Zafar, Nabeel Sabir, and Amir Ali

[2] Complementation Constructions for Nondeterministic Automata on Infinite Words Orna Kupferman and Moshe Vardi

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.