# Separation of the states of a deterministic omega-automaton by looping words taken from a regular language of non-empty words

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.

• If $u^\omega = v^\omega$ then $I(u) = I(v)$, so your condition is necessary. In other words, you have to assume it if you want the language to separate some DFA. Jul 20 '13 at 21:37
• I would be curious to know the origin of your problem. Actually the fact that you consider the behavior of periodic infinite words (of the form $v^\omega$) rather than ultimately periodic ones (of the form $uv^\omega$) makes your problem somewhat odd to me. Aug 26 '13 at 18:26
• Well, I have some lemma about finding an automaton that is compatible with a "lasso language", by first constructing several automata that are compatible with the looping parts of it. The purpose is to find a simple constructive procedure for getting a deterministic Muller automaton out of a two-sorted structure as defined in "Ciancia-Venema - Stream automata are coalgebras". See the paper below (and the acks section too! :) ). coalg.org/cmcs12/papers/00010090.pdf Sep 2 '13 at 7:40