Uniformisations of Regular Relations Over Bi-Infinite Words

We consider the problem of deciding whether a given mso-definable relation over bi-infinite words contains an mso-definable function with the same domain. We prove that this problem is decidable. There are two obstacles to the existence of such uniformisations: the first is related to the existence of non-trivial automorphisms of bi-infinite words, whereas the second, more subtle obstacle, is related to the existence of finite, discrete dynamical systems, where no trajectory can be selected by an mso formula.