Logics for Word Transductions with Synthesis
From MaRDI portal
Publication:5145302
DOI10.1145/3209108.3209181zbMATH Open1452.03080arXiv1701.03670OpenAlexW2798570354WikidataQ130844090 ScholiaQ130844090MaRDI QIDQ5145302FDOQ5145302
Emmanuel Filiot, Luc Dartois, Nathan Lhote
Publication date: 20 January 2021
Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)
Abstract: We introduce a logic, called LT, to express properties of transductions, i.e. binary relations from input to output (finite) words. In LT, the input/output dependencies are modelled via an origin function which associates to any position of the output word, the input position from which it originates. LT is well-suited to express relations (which are not necessarily functional), and can express all regular functional transductions, i.e. transductions definable for instance by deterministic two-way transducers. Despite its high expressive power, LT has decidable satisfiability and equivalence problems, with tight non-elementary and elementary complexities, depending on specific representation of LT-formulas. Our main contribution is a synthesis result: from any transduction R defined in LT , it is possible to synthesise a regular functional transduction f such that for all input words u in the domain of R, f is defined and (u,f(u)) belongs to R. As a consequence, we obtain that any functional transduction is regular iff it is LT-definable. We also investigate the algorithmic and expressiveness properties of several extensions of LT, and explicit a correspondence between transductions and data words. As a side-result, we obtain a new decidable logic for data words.
Full work available at URL: https://arxiv.org/abs/1701.03670
Cited In (4)
This page was built for publication: Logics for Word Transductions with Synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145302)
