Satisfiability of Context-free String Constraints with Subword-ordering and Transducers

TL;DR

The paper analyzes satisfiability of string constraints that combine subword-ordering with transductions under two membership regimes: context-free (CFL) and regular. It proves a sharp complexity dichotomy: 2NEXPTIME-completeness for CFL membership and NEXPTIME-completeness for regular membership within acyclic formulations. A key technical contribution is a lemma showing that the shortest word in the intersection of a pushdown automaton of size $O(n)$ with $n$ DFAs of size $O(n)$ can be double-exponential in $n$, enabling a powerful lower-bound construction via a double-exponentially bounded PCP. The results illuminate how transductions interact with subword constraints and contrast the CFL versus regular cases, with implications for regular abstractions, DFA-size blowups, and the (un)decidability landscape when concatenation substitutes for shuffle.

Abstract

We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size $O(n)$) and $n$ finite-state automata (each of size $O(n)$) can be double exponential in $n$.

Figures (5)

• Figure 1: A transducer. Here the label $x/y$ on a transition $t$ indicates that $\textsf{label}(t) = x$ and $\textsf{out}(t) = y$. It nondeterministically chooses to duplicates $a$s leaving $b$s as such, or duplicates $b$s leaving $a$s as such.
• Figure 2: A PDA with $3n+2$ states that accepts $(\Gamma_2)^{2^n}$.
• Figure 3: A PDA with $3n+3$ states that accepts $(\Gamma_2)^{2^{n+1}}$.
• Figure 4: The automaton $B_i$. The transitions on $\{{\color{blue} 0}, {\color{blue} 1}\}$ are depicted in blue. The transitions on $\Gamma_2$ (resp. $\textsf{inc}$, $\textsf{dec}$) are depicted in brown (resp. green, red).
• Figure 5: The PDA $A$. This PDA and the $\ell$ DFAs together faithfully encode the accepting runs of the PDA in Figure \ref{['fig:exp-pda-1']} with $n = 2^\ell-1$. Thus they accept words with exactly $2^{2^\ell}$ occurrences of $\Gamma_2$.

Theorems & Definitions (22)

• Definition 1
• Definition 2
• Example 3
• Definition 4
• Theorem 5
• Theorem 6
• Remark 7
• Remark 8
• Remark 9
• Definition 10