On the Satisfiability of Context-free String Constraints with Subword Order

String constraints impose constraints over variables that take strings as assignments. Given a string constraint C, the satisfiability problem asks if there is an assignment which satisfies every constraint in C. Most classes of string constraints in their full generality although have high expressive power turn out to be undecidable. Hence, a natural direction to recover decidability is to consider meaningful subclasses of string constraints. In this talk, we consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. We call this variant subword-ordering string constraints. The satisfiability problem for the variant turns out to be undecidable (even with regular membership). We consider a fragment in which the subword order constraints do not impose any cyclic dependency between variables. We show that this fragment is NEXPTIME-complete. As an important application of our result, we establish strong connection between the acyclic fragment of the subword-ordering string constraints and acyclic lossy channel systems, an important distributed system model. This allowed us to settle the complexity of control state reachability in acyclic lossy channel pushdown systems. The problem was shown to be decidable by Atig et al. in 2008. However, no elementary upper bound was known. We show that this problem is NEXPTIME-complete. This is a joint work with C. Aiswarya and Prakash Saivasan.

Authors

• Soumodev Mal

Keywords

No keywords are indexed for this paper.