Decision problems for origin-close top-down tree transducers (full version)

TL;DR

This paper introduces a similarity measure for origin-close non-deterministic top-down tree transducers, enabling decidability of inclusion, equivalence, and synthesis problems that are otherwise undecidable.

Contribution

It extends the concept of origin semantics by defining a similarity measure, allowing for decidable analysis of transducers that are close in behavior.

Findings

Decidability of inclusion, equivalence, and synthesis for origin-close transducers.

Introduction of a similarity measure for origin semantics.

Extension of decidability results to a broader class of transducers.

Abstract

Tree transductions are binary relations of finite trees. For tree transductions defined by non-deterministic top-down tree transducers, inclusion, equivalence and synthesis problems are known to be undecidable. Adding origin semantics to tree transductions, i.e., tagging each output node with the input node it originates from, is a known way to recover decidability for inclusion and equivalence. The origin semantics is rather rigid, in this work, we introduce a similarity measure for transducers with origin semantics and show that we can decide inclusion, equivalence and synthesis problems for origin-close non-deterministic top-down tree transducers.