FSM transducer sequential composition decidability

Question

this is a followup/ sequel to this recent question which was answered, this one presumably significantly harder. consider a deterministic FSM transducer $F$ and its mapping $F(x)$ of an input word $x$. define a sequence/ composition of such mappings $x_n = F(\ldots F(x_1))$ where $F^n(x)$ is $n$ sequential mappings of $x$. the sequence terminates if/ "at the point" that $F(x_n)$ is unaccepted (by the FSM transducer).

now consider/ define a property of such sequences "descending". a FSM sequence $x_i$ is "descending" iff $|x_i| \geq |x_{i + 1}|$ where $|x|$ denotes word length, and for all $i,j$, $x_i \neq x_j$. (by defn all such sequences must be finite/ terminating.)

question: given an input regular language $L$ and a FSM transducer $F$. is it decidable if all sequences $x_n = F^n(x) = F(\ldots F(x))$ for all $x \in L$ are descending?

a complete answer would be ideal but prefer partial answer(s) to none at all. looking for nontrivial analysis, reduction(s) to known problems, refs to related literature etc.

motivation/ background: a long story, but inspired/ related to investigation of a highly studied open number theory problem. the basic idea is to look for/ formulate a generalized loop invariant function applicable to automated theorem proving.

Answer 1

The problem seems undecidable: consider a transducer $F$ that parses and "executes" a single step of a Turing machine $M$ with the head $H$ on symbol $a$, in state $S$ and with tape content $x[a]by$ where $a,b \in \Sigma; x,y \in \Sigma^*$:

$$\# x \, a \, H\, S \, b \, y \, \# \, w $$

where $w \in \{0,1\}^+$ and it outputs

$$\# x \, H \, S' \, a'\, b \, y \, \# \, w' $$

if the head moves left, i.e. $\sigma(a,S)\to (a',S',L)$ or it outputs

$$\# x \, a' \, b \, H \, S' \, y \, \# \, w' $$

if the head moves right, i.e. $\sigma(a,S)\to (a',S',R)$.

$w'$ is simply $w +1$ (binary addition with the LSB on the left) and its "role" is to make $x_{i+1} \neq x_j \forall j \leq i$ as required.

If $M$ halts (when $S'$ is a final state), then $F$ adds an extra $\#$ at the end (i.e. it makes the output ascending) and rejects to stop the sequence; otherwise it accepts and the length is unaltered.

If there is not enough space for a right move of the head then $F$ rejects to stop the sequence.

If there is not enough space for writing $w+1$ (carry overflow on the right), it simply replaces the last digit with $\#$ (to make $x_{i+1} \neq x_i$) and rejects to stop the sequence.

Note that:

1. $F$ needs only a limited look-ahead buffer (4 symbols) to make the rewrite and also to perform the $w+1$ operation;
2. the internal states of $F$ embeds the internal states of $M$ so it can simulate the transition function $\sigma$;

Now, consider $M$ on an empty tape; we can use an (infinite) regular language:

$L = \{ \# \, H \, S_0\, \, 0^+ \# \, 0^+ \}$

$M$ halts if and only if $F^n(x)$ is not descending for all $n$, for all $x \in L$

Indeed the only length increase occurs when $F$ runs on $\# \, H \, S_0\, 0^s \, \# \, 0^t$ and $s,t$ are such that $M$ halts in less than $2^t$ steps using at most $s$ space.

Answer 2

This is an extended comment rather than an answer, but it may be helpful to find a decidable subcase.

Assume that the transduction $F$ is definable in some logic $\mathcal{L}$, i.e. there exists some formula $\alpha_F(x,y)$ of $\mathcal{L}$, with free SO variables encoding words $x$ and $y$, which is true only when $y = F(x)$. Given a word $x$, the property "$(F^n(x))$ is descending" is definable in SO with transitive closure (see 1 for a definition): $(\forall y . TC(\alpha_F)(x,y))(\forall z . \exists z' . \alpha_F(y,z') \wedge TC(\alpha_F)(z',z)) (|z| \leq |y| \wedge z \neq y)$

The transitive closure operator works as expected. If $\phi$ is a formula with two free variables, it describes a binary relation $R$ over the domain of the variables. $TC(\phi)$ then describes the transitive closure $R^*$ of this relation. Intuitively, the transitive closure allows (in a controlled way) an arbitrary number of quantifications: when $x R^* y$, then $x R^i y$ for some $i$, but expressing $R^i$ would require $i$ existential quantifiers.

Thus, the language $L_d = \{ x \in L ~|~ (F^n(x)) \text{ is descending} \}$ is definable in $\mathcal{L}$ + SO + TC. Thus, if in the latter logic $\mathcal{L}$ + SO + TC, the universality is decidable, then your problem is decidable as well.

Unfortunately, little is known about the appropriate logic needed to define the above $\alpha_F$ in the general case.