¿Es decidible si la longitud de salida de un transductor está limitada por la longitud de entrada?

Los transductores considerados aquí son aquellos que Wikipedia llama transductores de estado finito . El comportamiento de un transductor , es decir, la relación que calcula, se escribe : una palabra es una salida para iff .$T$$[T]$$y$$x$$x[T]y$

Pregunta: ¿Se puede resolver el siguiente problema:

Dado: Un transductor y un lenguaje regular Decidir: ¿Sostiene que , una palabra, implica que?L ∀ x ∈ L ∀ y x [ T ] y | y | ≤ | x $T$$L$
$\forall x \in L$$\forall y$$x[T]y$$|y| \leq |x|$

Estoy buscando análisis no triviales / subcajas solucionables, reducción a problemas conocidos y / o referencias relacionadas. (en este momento ni siquiera estoy seguro de que sea decidible en general ...?)

Motivación: este problema se inspiró en el análisis / investigación sobre la demostración automatizada de teoremas de problemas teóricos de números en general y uno altamente estudiado, la conjetura de Collatz , en particular.

El otro contribuyente eliminó su respuesta, tal vez para permitirme extender mi comentario anterior, así que aquí está.

Sea un transductor posiblemente no determinista, y L sea ​​un lenguaje regular. Modifique T en un transductor T ' que verifique que su entrada esté en L (por ejemplo, cambiando el conjunto de estados en el producto cartesiano de los conjuntos de estados de T y L , y modificando la función de transición para que la parte L de los estados se actualiza correctamente, conservando el comportamiento de T ).$T$$L$$T$$T'$$L$$T$$L$$L$$T$

Una rama de es una secuencia ρ 1 C 1 ρ 2 C 2 ⋯ ρ n C n ρ n + 1 tal que ρ 1 ρ 2 ⋯ ρ n + 1 es una ruta simple de aceptación en T ′ , y cada C i es un componente fuertemente conectado de T ′ cuyos estados incluyen el destino de ρ i (y el origen 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 rama esmansasi:$\rho_{i+1}$

1. La longitud de entrada de la ruta es mayor o igual que su longitud de salida;$\rho_1\rho_2\cdots\rho_{n+1}$

2. Para cualquier , cualquier ciclo simple en C i , la longitud de entrada del ciclo es mayor o igual que su longitud de salida.$i$$C_i$

Hecho: Para cualquier x , y , x [ T ′ ] y implica | y | ≤ | x | ] si todas las ramas son mansas.$\big[$$x, y$$x[T']y$$|y| \leq |x|$ $\big]$

La prueba es bastante inmediata. La última propiedad es decidible (ya que el número de ramas está limitado y el número de ciclos simples también), esto muestra que el problema de la pregunta es decidible.