A problem instance is a finite list of 4-tuples $(\alpha_1, u_1, v_1, \beta_1), ..., (\alpha_N, u_N, v_N, \beta_N)$, where $\alpha_i, \beta_i \in X$ come from a finite set, and each $u_i,v_i \in A^*$ are words over a finite alphabet $A$.
A solution to the problem is a sequence of indices $i_1, i_2, ..., i_K$ such that
- For all $1 \leq k \leq K-1$, we have $\alpha_{i_k} = \beta_{i_{k+1}}$.
- The words $u' = u_{i_1} u_{i_2} \cdots u_{i_K}$ and $v' = v_{i_1} v_{i_2} \cdots v_{i_K}$ are not prefixes of each other
That is, an instance is like an instance of PCP, but with restrictions on how "dominoes" can be composed, and instead of finding strings that are equal, we need strings that differ by at least one symbol.
It is not immediately obvious to me how to decide this problem, and I have not been able to find an example of it in the literature.
Update: Origin of the problem
Given a finite state transducer over input/output alphabets $\Sigma, \Gamma$ and with initial state $p^{-}$, two states $q_1, q_2$ are said to be twinned iff for all $u,v \in \Sigma^*$ and $y_1,y_2,z_1,z_2 \in \Gamma^*$ if
$$ p^{-} \stackrel{u/y_1}{\to} q_1 \stackrel{v/z_1}{\to} q_1 \text{ and } p^{-} \stackrel{u/y_2}{\to} q_2 \stackrel{v/z_2}{\to} q_2$$
then either $z_1=z_2=\varepsilon$ or $|z_1|=|z_2| \neq 0$ and one of $y_1, y_2$ is a prefix of the other. [Weber & Klemm, Economy of description for single-valued transducers, 1995]. This is equivalent to the "algebraic" definition given in [Berstel, Transductions and Context-free languages, 1979].
There are effective procedures for deciding whether all states are twinned or not. I am interested in computing all pairs of states that are not twinned. Applying the method of squaring transducers [Beal, Carton, Prieur, Sakarovitch, 2000], this reduces to deciding the problem in my question for all pairs of states.