A logic for transductions and its decision through data words

*this talk does not correspond to an accepted or published paper* In the model of graph transductions from Courcelle, an output structure is obtained from several copies of the input structure and the predicates are defined by MSO formulas interpreted over the input structure. This formalism is asymmetric in the sense that one cannot speak of the output structure independently from the input one. In contrast we introduce a logical description of word to word transductions which allows one to both speak about the input and output structures independently, but also to express dependencies between the two structures through an origin predicate. Both the input and output words are seen as a single compound graph structure, with an origin predicate that relate output positions to input positions. When considering the full power of MSO over these compound structures, the satisfiability problem is, unsurprisingly, undecidable. To overcome this we consider the logical fragment of first-order logic with two variables, enriched with arbitrary binary MSO-definable predicates with quantification restricted to the input positions. We show that this logic is decidable yet expressive enough to encompass MSO transductions à la Courcelle. The decidability is obtained through a reduction to data word logic. Intuitively the datum of a position corresponds to its origin position in the input word. Following [Schwentick & Zeume 2012] we see a data word as a structure with one linear order and one total pre-order, and extending their result we show the decidability (over data words) of first-order logic with two variables enriched with arbitrary binary MSO-definable relations that use only the pre-order predicate (and unary predicates).

Authors

• Joint with Luc Dartois
• Emmanuel Filiot

Keywords

No keywords are indexed for this paper.