Suppose I have regular languages $B \subseteq A$, with corresponding (known) minimal deterministic finite automata $M_A, M_B$.

I would like to find another regular language $C$ such that $B = A \cap C$ that minimizes the size of $M_C$ (the minimal DFA corresponding to $C$).

In general $M_C$ can be much smaller than $M_B$. e.g. if we let $B$ the set of strings in $A$ that have even length, $M_C$ can be a two-state machine, while $M_B$ may be about as complex (or more) as $M_A$.

This feels like it should be an easy application of existing automaton minimization algorithms, but I'm not seeing it if so.

It's at least in NP: The corresponding decision problem is in NP, because such an automaton has size at most $|M_B|$, and we can determine whether a given automaton is a solution by testing its equivalence with the intersection automaton with states $M_A \times M_B$, and testing equivalence is in $P$. There's almost certainly some nice transformation into SAT or ILP that I haven't worked through yet because I'm hoping for a better solution.

What looked liked the obvious thing to try to do is to to try and distinguish strings using an analogue of the Myhill-Nerode theorem, with the distinguishing relationship being that $x, y$ are distinct if there is some $s$ such that $xs, ys \in A$ but $xs \in B \neq ys \in B$, but the problem is that the corresponding indistinguishability relation is no longer transitive (I think) - Given $a$ indistinguishable from $b$ indistinguishable from $c$, there might be $s$ such that $as, cs \in A$ with $as \in B \neq cs \in B$, but $bs \not\in A$, so (s) cannot be used to distinguish $a$ from $c$.

I think this arises from some genuine ambiguity in the problem - unlike normal DFA minimization, there's no reason to expect $M_C$ to be unique - two non-equivalent machines could represent languages $C \neq C'$ such that $A \cap C = A \cap C'$.

Is this some well studied problem? Or can it be reduced to one?

Suppose I have regular languages $B \subseteq A$, with corresponding (known) minimal deterministic finite automata $M_A, M_B$.

I would like to find another regular language $C$ such that $B = A \cap C$ that minimizes the size of $M_C$ (the minimal DFA corresponding to $C$).

In general $M_C$ can be much smaller than $M_B$. e.g. if we let $B$ the set of strings in $A$ that have even length, $M_C$ can be a two-state machine, while $M_B$ may be about as complex (or more) as $M_A$.

This feels like it should be an easy application of existing automaton minimization algorithms, but I'm not seeing it if so.

What looked liked the obvious thing to try to do is to to try and distinguish strings using an analogue of the Myhill-Nerode theorem, with the distinguishing relationship being that $x, y$ are distinct if there is some $s$ such that $xs, ys \in A$ but $xs \in B \neq ys \in B$, but the problem is that the corresponding indistinguishability relation is no longer transitive (I think) - Given $a$ indistinguishable from $b$ indistinguishable from $c$, there might be $s$ such that $as, cs \in A$ with $as \in B \neq cs \in B$, but $bs \not\in A$, so $s$ cannot be used to distinguish $a$ from $c$.

I think this arises from some genuine ambiguity in the problem - unlike normal DFA minimization, there's no reason to expect $M_C$ to be unique - two non-equivalent machines could represent languages $C \neq C'$ such that $A \cap C = A \cap C'$. It might be that those ambiguities don't matter and you can just resolve them arbitrarily, but I haven't been able to convince myself of that.

The problem is at least "reasonably tractable", as the corresponding decision problem is in NP, because such an automaton has size at most $|M_B|$, and we can determine whether a given automaton is a solution by testing its equivalence with the intersection automaton with states $M_A \times M_B$, and testing equivalence is in $P$. There's almost certainly some nice transformation into SAT or ILP that I haven't worked through yet because I'm hoping for a better solution.

Is this some well studied problem? Or can it be reduced to one?