pith. sign in

arxiv: 1906.08688 · v2 · pith:DIETDF27new · submitted 2019-06-20 · 💻 cs.FL

On Synthesis of Resynchronizers for Transducers

Sougata Bose , Shankara Narayanan Krishna , Anca Muscholl , Vincent Penelle , Gabriele Puppis This is my paper

Pith reviewed 2026-05-25 18:56 UTC · model grok-4.3

classification 💻 cs.FL
keywords resynchronizerstransducerssynthesisdecidabilityorigin semanticsone-way transducerstwo-way transducersrational relations
0
0 comments X

The pith

Synthesis of rational resynchronizers is decidable for functional and finite-valued one-way transducers but undecidable for relational ones.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines ways to compare two transducers by synthesizing a resynchronizer that makes the outputs of one contained in the other when runs are matched by origin. It proves that the existence of a rational resynchronizer can be decided when the transducers are one-way and either functional or finite-valued. The same synthesis problem becomes undecidable once the transducers are allowed to be relational. For two-way transducers the paper shifts to regular resynchronizers and shows decidability when the transducers are unambiguous.

Core claim

Rational resynchronizers are captured by regular ones. Synthesis of rational resynchronizers is decidable for functional and finite-valued one-way transducers, undecidable for relational one-way transducers. Synthesis of regular resynchronizers is decidable for unambiguous two-way transducers.

What carries the argument

Rational and regular resynchronizers under origin semantics, where a resynchronizer supplies a relation between origins that turns one transducer's behavior into a contained version of the other's.

If this is right

  • Existence of a rational resynchronizer between two functional one-way transducers can be decided algorithmically.
  • The same decision procedure works when the transducers are finite-valued rather than functional.
  • No algorithm exists that decides existence for arbitrary relational one-way transducers.
  • Existence of a regular resynchronizer between two unambiguous two-way transducers can be decided algorithmically.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results separate classes of transducers for which automated comparison under origin semantics is feasible from those where it is not.
  • Because rational resynchronizers are captured by regular ones, any positive decidability result for rational resynchronizers immediately transfers to the regular case.
  • The open status for general two-way transducers indicates a natural next target for extending the decision procedures.

Load-bearing premise

Origin semantics together with the definitions of rational and regular resynchronizers correctly express the intended containment relation between transducer computations.

What would settle it

An algorithm that outputs a rational resynchronizer for a given pair of finite-valued one-way transducers, yet direct inspection of the two transducers shows that no such resynchronizer can exist.

Figures

Figures reproduced from arXiv: 1906.08688 by Anca Muscholl, Gabriele Puppis, Shankara Narayanan Krishna, Sougata Bose, Vincent Penelle.

Figure 1
Figure 1. Figure 1: Two functional 1NFT T1, T2, their origin graphs, and a rational resynchronizer R. have the same projections over the input and output alphabets, then the relation represents a resynchronization. We also recall that rational relations are captured by one-way transducers, so, by analogy, we call rational resynchronizer any one-way transducer over Σ⊎Γ that preserves the input and output projections. It is rou… view at source ↗
Figure 2
Figure 2. Figure 2: Factorization of an output block. ρ may have arbitrarily long factors on outputs blocks. Another difficulty is that we cannot uniquely identify the positions in an output block using offsets ranging over a fixed finite set. We will see that a solution to both problems comes from covering most of the output by factors in which the positions behave similarly in terms of the source-to-target origin transforma… view at source ↗
read the original abstract

We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T1, T2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T1 is contained in R(T2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper studies rational and regular resynchronizers for comparing transducers under origin semantics, proving that every rational resynchronizer is captured by a regular one. It then addresses the synthesis problem of constructing a rational (resp. regular) resynchronizer R such that T1 is contained in R(T2) under origin semantics. The main results are: synthesis of rational resynchronizers is decidable for functional and finite-valued one-way transducers but undecidable for relational one-way transducers; synthesis of regular resynchronizers is decidable for unambiguous two-way transducers (with the status open for larger two-way classes).

Significance. If the results hold, the paper contributes precise decidability boundaries for the synthesis of resynchronizers in transducer theory, extending origin semantics to comparison and synthesis problems. The reduction of rational to regular resynchronizers and the decidability/undecidability dichotomy for one-way cases provide useful technical tools; the decidability for unambiguous two-way transducers is a positive result in a setting where two-way models are expressive.

minor comments (3)
  1. [Introduction] The abstract and introduction would benefit from a brief, self-contained example (e.g., two simple transducers and a resynchronizer) to illustrate the containment relation under origin semantics before the formal definitions.
  2. [§2] Notation for origin semantics and the containment T1 ⊆ R(T2) should be introduced with a small diagram or table in §2 to aid readers unfamiliar with the origin-tracking convention.
  3. [Conclusion] The open decidability question for general two-way transducers is stated clearly but could be accompanied by a short discussion of why the unambiguous case is tractable while the general case resists the same techniques.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation of minor revision. No specific major comments appear in the report, so we have no points requiring detailed rebuttal or technical clarification at this stage. We will incorporate any minor suggestions during the revision process.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper establishes decidability and undecidability of synthesis problems for rational and regular resynchronizers via reductions to established automata problems (e.g., emptiness, inclusion for transducers). No fitted quantities, self-definitional equations, or load-bearing self-citations appear; the results are proven from standard automata constructions without reducing the central claims to their own inputs by construction. The modeling choice of origin semantics is external to the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The results rest on standard definitions and closure properties of transducers and automata; no new entities or fitted parameters are introduced in the abstract.

axioms (1)
  • domain assumption Standard closure and decidability properties of one-way and two-way transducers under origin semantics hold.
    Invoked implicitly when reducing synthesis to emptiness or inclusion problems.

pith-pipeline@v0.9.0 · 5671 in / 1151 out tokens · 17411 ms · 2026-05-25T18:56:51.480992+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    Expressiveness of streaming string transducer

    Rajeev Alur and Pavel Cern \'y . Expressiveness of streaming string transducer. In Proc. of FSTTCS'10 , volume 8 of LIPIcs , pages 1--12. Schloss Dagstuhl - Leibniz-Zentrum f \"u r Informatik, 2010

    work page 2010

  2. [2]

    Squaring transducers: an efficient procedure for deciding functionality and sequentiality

    Marie-Pierre B \'e al, Olivier Carton, Christophe Prieur, and Jacques Sakarovitch. Squaring transducers: an efficient procedure for deciding functionality and sequentiality. Theor. Comput. Sci. , 292:45--63, 2003

    work page 2003

  3. [3]

    Which classes of origin graphs are generated by transducers? In ICALP'17 , volume 80 of LIPIcs , pages 114:1--114:13, 2017

    Mikolaj Boja \'n czyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle. Which classes of origin graphs are generated by transducers? In ICALP'17 , volume 80 of LIPIcs , pages 114:1--114:13, 2017

    work page 2017

  4. [4]

    Single-valued a-transducers

    Meera Blattner and Tom Head. Single-valued a-transducers. J. Comput. and System Sci. , 15:310--327, 1977

    work page 1977

  5. [5]

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

    Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis. Origin-equivalence of two-way word transducers is in PSPACE . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18) , volume 122 of LIPIcs , pages 1--18. Schloss Dagstuhl - Leibniz-Zentrum f \"u r Informatik, 2018

    work page 2018

  6. [6]

    Transducers with origin information

    Mikolaj Boja \'n czyk. Transducers with origin information. In International Colloquium on Automata, Languages and Programming (ICALP'14) , number 8572 in LNCS, pages 26--37. Springer, 2014

    work page 2014

  7. [7]

    Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach , volume 138 of Encyclopedia of mathematics and its applications

    Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach , volume 138 of Encyclopedia of mathematics and its applications . Cambridge University Press, 2012

    work page 2012

  8. [8]

    Unambiguous constrained automata

    Micha \" e l Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. Int. J. Found. Comput. Sci. , 24(7):1099--1116, 2013

    work page 2013

  9. [9]

    Elgot and Jorge E

    Calvin C. Elgot and Jorge E. Mezei. On relations defined by generalized finite automata. IBM Journal of Research and Development , 9(1):47--68, 1965

    work page 1965

  10. [10]

    e l Jecker, Christof L \

    Emmanuel Filiot, Isma \" e l Jecker, Christof L \" o ding, and Sarah Winter. On equivalence and uniformisation problems for finite transducers. In ICALP'16 , volume 55 of LIPIcs , pages 125:1--125:14, 2016

    work page 2016

  11. [11]

    Fischer and Arnold L

    Patrick C. Fischer and Arnold L. Rosenberg. Multi-tape one-way nonwriting automata. J. Comput. and System Sci. , 2:88--101, 1968

    work page 1968

  12. [12]

    T. V. Griffiths. The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines. J. ACM , 15(3):409--413, 1968

    work page 1968

  13. [13]

    personal communication

    Piotr Hofman. personal communication

    work page

  14. [14]

    Oscar H. Ibarra. The unsolvability of the equivalence problem for e-free NGSM 's with unary input (output) alphabet and applications. SIAM J. of Comput. , 7(4):524--532, 1978

    work page 1978

  15. [15]

    The many facets of string transducers (invited talk)

    Anca Muscholl and Gabriele Puppis. The many facets of string transducers (invited talk). In 36th International Symposium on Theoretical Aspects of Computer Science (STACS) , volume 126 of LIPIcs , pages 2:1--2:21. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019

    work page 2019

  16. [16]

    Shepherdson

    J.C. Shepherdson. The reduction of two-way automata to one-way automata. IBM J. Res. Dev. , 3(2):198--200, 1959

    work page 1959

  17. [17]

    Decomposing a k -valued transducer into k unambiguous ones

    Andreas Weber. Decomposing a k -valued transducer into k unambiguous ones. ITA , 30(5):379--413, 1996

    work page 1996