A Deterministic One-Counter Automaton (DOCA) is a DPDA with single letter stack alphabet. They can be used to define (context-free, word) languages by reaching an accepting state and counter 0.
Let's call a language $L\subseteq\Sigma^*$, given as the language of some DOCA $A$ decomposable if there exist languages $L_0,L_1,\ldots,L_k$ such that
- $L \subseteq L_i$ for every $i\le k$,
- every $L_i$ is "smaller"
- $L = \bigcap_{i=0}^k L_i$
Here, "smaller" means it is represented by a DOCA with strictly fewer states than $A$. A language that is not decomposable is prime.
The question is if it is decidable to check if a given a language (DOCA) is it prime. Notice that one can guess a decomposition into "smaller" automata, but not directly verify such a guess, because checking emptiness of intersections is undecidable for DOCA.
Examples
An example for a prime language is $a^nb^n$. It is recognized by a two-state DOCA (accepting with the second state and counter zero). Yet, any language $L_i\supseteq a^nb^n$, recognized by a single-state DOCA, must include the word $w=abab$. On the other hand, $a^nb^nb^mc^m$ can be shown to be DOCA but not prime.
Reference
The question is really if the work of Kupfermann & Mosheiff, MFCS'13 can be sensibly extended to infinite Automata. They consider regular languages defined by DFA, minimal wrt. their index (number of states). They show decidability by brute force, which works in this way only for finite automata: A language $A$ is prime iff there is a word $w\not\in A$ but in every $B\supseteq A$ that satisfies condition 2. There are finitely many such $B$ so one can take the big product and derive a bound on the length of the shortest such prime witness $w$ (This uses the finite-index!).