Deciding the Computability of Regular Functions over Infinite Words

V. Dave, E. Filiot, S. Krishna, N. Lhote

The class of regular functions from infinite words to infinite words is characterised by MSO-transducers, streaming $\omega$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. This paper proposes a decision procedure for the fundamental question : given a regular function $f$, is $f$ computable (by a Turing machine with infinite input)? For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational functions in \textsc{NLogSpace} (it was already known to be in \textsc{PTime} by Prieur), and of regular functions.

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment