Satisfiability of Context-free String Constraints with Subword-ordering and Transducers
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 ) and finite-state automata (each of size ) can be double exponential in .
Keywords
Cite
@article{arxiv.2401.07996,
title = {Satisfiability of Context-free String Constraints with Subword-ordering and Transducers},
author = {C Aiswarya and Soumodev Mal and Prakash Saivasan},
journal= {arXiv preprint arXiv:2401.07996},
year = {2024}
}