Consider a deterministic transition structure having states in set $X$ and transition function $\rightarrow$, and an initial state $x \in X$. This structure is intended to be part of an automaton accepting streams, such as a Buchi or Muller automaton.
Given a regular language of non-empty finite words $L$, and a word $v \in L$, define $I(v)$ to be the inf-set of $v^\omega$, that is, the set of states that is traversed infinitely often by the unique run of $v^\omega$ starting from $x$.
One can define the following notion:
$(X,\rightarrow)$ is separated by $L$ if and only if the sets $\{ I(v) | v \in L \}$ and $\{ I(v) | v \notin L\}$ have empty intersection. In words, the set of inf-sets of words in $L$ and of words not in $L$ are disjoint.
A counterexample is the single-state deterministic structure against the regular language $a^+ \cup b^+$; we have $I(ab) = I(a)$ with $a \in L$ and $ab \notin L$.
The question is: is this notion known? In particular, I would like to prove that all non-empty regular languages separate some finite deterministic structure. I wonder if that is known already.
Note: one can assume that $L$ is invariant under the equivalence $u = v \iff u^\omega = v^\omega$, making it a "looping" language.
