Langage régulier qui fait la distinction entre deux CFG déterministes

Supposons que l'on vous donne deux automates déterministes push down qui reconnaissent les langages et B et souhaitent déterminer s'il existe un langage régulier R tel que A ⊆ R et R ∩ B = ∅ . Fondamentalement, le défi consiste à déterminer s'il existe un DFA qui peut reconnaître de quelle langue provient une chaîne donnée, étant donné qu'elle provient de l'une de ces langues.$A$$B$$R$$A \subseteq R$$R \cap B = \emptyset$

Est-ce décidable? Si oui, quelle est la complexité? Le DFA peut-il être construit explicitement?

Eryk Kopczyński [1] a montré en 2015 que la séparabilité (c'est le nom de votre problème) des langues visiblement refoulées par les langues régulières est indécidable. La classe des langages visiblement pushdown est un sous-ensemble strict de CFL déterministe.

[1]: Eryk Kopczyński, Invisible Pushdown Languages, LICS'16, disponible sur https://arxiv.org/abs/1511.00289