Origin-equivalence of two-way word transducers is in PSPACE

TL;DR

This paper proves that the equivalence and containment problems for two-way word transducers under origin semantics are PSPACE-complete, extending decidability results to a broader class of transducers with resynchronizations.

Contribution

It introduces a natural origin semantics for two-way transducers and establishes PSPACE-completeness of their equivalence and containment problems, including variants with resynchronizations.

Findings

Equivalence and containment are PSPACE-complete under origin semantics.

Decidability extends to transducers with resynchronizations.

The paper provides a logical formalism for broad resynchronization classes.

Abstract

We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered by adopting a slightly different, but natural semantics, called origin semantics and introduced by Bojanczyk in 2014. Specifically, we prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose a logical formalism for describing a broad class of resynchronizations, while preserving the decidability of the variant of the containment problem.