20.2 Deterministic separability of nondeterministic timed languages

• Input: two timed languages \(L\), \(M\) represented as nondeterministic timed automata.
• Question: decide whether there exists a deterministic timed automaton recognising a timed language \(S\) which separates \(L\), \(M\), in the sense that \(L\) is included in \(S\) and \(S\) is disjoint from \(M\).

The version of the problem when we fix in advance the number of clocks of the separating deterministic timed automaton is decidable. The open problem is then when the number of clocks is not fixed (and thus quantified existentially).