I have been thinking about this problem for weeks and I'm still not sure if the problem is decidable or not. Basically it asks there are NFA's with states that can be substituted to DFA's. Given two such NFA's, determine whether they are equivalent in any possible DFA substitutions. Of course these two NFA's have states that are labelled with letters from a same variable set, and same variables will be substituted into same DFA's.
Below is an example of such substitutions.
Note the equivalence must hold with any possible plugins. For example, NFA A1 and A2 both has same variables X and Y, A1 and A2 are equivalent iff L(A1) = L(A2) for any two DFA's plugged into A1 and A2. Of course same DFA will be plugged into same variable in both NFA's.
I have tried to prove the problem is decidable. However, I run into the trouble that although I can easily show two NFA's are equivalence before plugin the DFA's, this equivalence is only related to the strings they generate, not the sequences of states. It is still possible same variable symbol holds different states (by different, I mean different place along the sequence of states) in these two NFA's therefore the they generated different strings after plugging in DFA's.
On the other hand, if this problem is undecidable, I can't find a reduction from any undecidable problems.
Any thoughts on this problem will be really appreciated!