Est-il possible de décider si la longueur de sortie d'un transducteur est limitée par la longueur d'entrée?

Les transducteurs considérés ici sont ceux que Wikipedia appelle les transducteurs à états finis . Le comportement d'un transducteur , qui est la relation qu'il calcule, est écrit : un mot est une sortie pour ssi .[ T ] y x x [ T ] $T$$[T]$$y$$x$$x[T]y$

Question: Le problème suivant est-il décidable:

Étant donné: Un transducteur et un langage régulier Décide: Tient-il que , un mot, implique que?L ∀ x ∈ $T$$L$
$\forall x \in L$x [ T ] y | y | ≤ | x $\forall y$$x[T]y$$|y| \leq |x|$

Je recherche une analyse non triviale / des sous-cas résolubles, une réduction des problèmes connus et / ou des références associées. (en ce moment même pas sûr que c'est décidable en général ...?)

Motivation: ce problème a été inspiré par une analyse / recherche d' un théorème automatisé prouvant des problèmes de théorie des nombres en général et une étude très étudiée, la conjecture de Collatz , en particulier.

L'autre contributeur a supprimé sa réponse, peut-être pour me permettre d'étendre mon commentaire ci-dessus, alors le voici.

Soit un transducteur éventuellement non déterministe, et L un langage régulier. Modifiez T en un transducteur T ' qui vérifie que son entrée est dans L (par exemple en changeant l'ensemble d'état en produit cartésien des ensembles d'états de T et L , et en modifiant la fonction de transition de sorte que la partie L des états est correctement mis à jour, tout en conservant le comportement de T. )$T$$L$$T$$T'$$L$$T$$L$$L$$T$

Une branche de est une séquence ρ 1 C 1 ρ 2 C 2 ⋯ ρ n C n ρ n + 1 telle que ρ 1 ρ 2 ⋯ ρ n + 1 est un chemin simple accepteur dans T ′ , et chaque C i est une composante fortement connectée de T ′ dont les états incluent la destination de ρ i (et l'origine de ρ $T'$$\rho_1 C_1\rho_2 C_2 \cdots \rho_n C_n \rho_{n+1}$$\rho_1\rho_2 \cdots \rho_{n+1}$$T'$$C_i$$T'$$\rho_i$ ). La branche estapprivoiséesi:$\rho_{i+1}$

1. La longueur d'entrée du chemin est supérieure ou égale à sa longueur de sortie;$\rho_1\rho_2\cdots\rho_{n+1}$

2. Pour tout , tout cycle simple en C i , la longueur d'entrée du cycle est supérieure ou égale à sa longueur de sortie.$i$$C_i$

Fait: Pour tout x , y , x [ T ′ ] y implique | y | ≤ | x | ] ssi toutes les branches sont apprivoisées.$\big[$$x, y$$x[T']y$$|y| \leq |x|$ $\big]$

La preuve est assez immédiate. Cette dernière propriété étant décidable (comme le nombre de branches est borné, et le nombre de cycles simples aussi), cela montre que le problème de la question est décidable.