License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.43
URN: urn:nbn:de:0030-drops-128554
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12855/
Dave, Vrunda ;
Filiot, Emmanuel ;
Krishna, Shankara Narayanan ;
Lhote, Nathan
Synthesis of Computable Regular Functions of Infinite Words
Abstract
Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming ω-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. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function f (equivalently specified by one of the aforementioned transducer model), is f computable and if it is, synthesize a Turing machine computing it.
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 and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.
BibTeX - Entry
@InProceedings{dave_et_al:LIPIcs:2020:12855,
author = {Vrunda Dave and Emmanuel Filiot and Shankara Narayanan Krishna and Nathan Lhote},
title = {{Synthesis of Computable Regular Functions of Infinite Words}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {43:1--43:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Igor Konnov and Laura Kov{\'a}cs},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12855},
URN = {urn:nbn:de:0030-drops-128554},
doi = {10.4230/LIPIcs.CONCUR.2020.43},
annote = {Keywords: transducers, infinite words, computability, continuity, synthesis}
}
|
Keywords: |
|
transducers, infinite words, computability, continuity, synthesis |
|
Collection: |
|
31st International Conference on Concurrency Theory (CONCUR 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
26.08.2020 |
