On Computability of Data Word Functions Defined by Transducers (FoSSaCS 2020)

Abstract

In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data $\omega$‑words). The notion of computability is defined through Turing machines with infinite inputs which can produce the corresponding infinite outputs in the limit. We use non-deterministic transducers equipped with registers, an extension of register automata with outputs, to specify functions. Such transducers may not define functions but more generally relations of data $\omega$‑words, and we show that it is PSpace-complete to test whether a given transducer defines a function. Then, given a function defined by some register transducer, we show that it is decidable (and again, PSpace-complete) whether such function is computable. As for the known finite alphabet case, we show that computability and continuity coincide for functions defined by register transducers, and show how to decide continuity. We also define a subclass for which those problems are PTime.

Publication
Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings

The work of Vrunda Dave, Emmanuel Filiot, Krishna S and Nathan Lhote, which settles the finite alphabet case and inspired us this research direction, was accepted at CONCUR 2020 as Synthesis of Computable Regular Functions of Infinite Words. For the present paper, we refer to the preprint arXiv version 1, as it was the one available when we wrote the paper. We have been invited to write an extended version for the LMCS special issue dedicated to FoSSaCS 2020, that has been accepted with minor revisions (more details here). The contributions of both papers are detailed in the second part of my manuscript.

Due to the worldwide outbreak of CoViD-19, ETAPS 2020 was postponed; so was my presentation of this work, but I could present it a year later at ETAPS 2021. I also got the opportunity to give a longer talk about it at MOVEP 2020 and a short one at HIGHLIGHTS 2020.

Related