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.

  • $\begingroup$ 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. $\endgroup$ Jul 20, 2013 at 21:37
  • $\begingroup$ 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. $\endgroup$
    – J.-E. Pin
    Aug 26, 2013 at 18:26
  • $\begingroup$ 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 $\endgroup$
    – vincenzoml
    Sep 2, 2013 at 7:40


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.