Logics for word transductions with synthesis

DOI10.1145/3209108.3209181MaRDI QIDQ5145302zbMATH OpenOpenAlexWikidataFDO

Authors Luc Dartois, Emmanuel Filiot, 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)

Full work available at URL https://arxiv.org/abs/1701.03670

zbMATH Keywords

originsynthesislogicdata wordstransductions

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70)

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.

Recommendations

• Synthesis of data word transducers
• A uniformization theorem for nested word to word transductions
• Synthesis of deterministic top-down tree transducers from automatic tree relations
• Logical and algebraic characterizations of rational transductions

Cited in

(6)

• scientific article; zbMATH DE number 7566055 (Why is no real title available?)
• Synthesis of data word transducers
• Minimal synthesis of string to string functions from examples
• A tour of recent results on word transducers
• Synthesis of Data Word Transducers
• Origin-equivalence of two-way word transducers is in PSPACE

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)