Tags:Context-free languages, Lossy channel systems, Satisfiability, String constraints and Subword order
Abstract:
We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. The satisfiability problem for this variant turns out to be undecidable. 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 application of our result, we settle the complexity of control state reachability in acyclic lossy channel pushdown systems, an important distributed system model. 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.
On the Satisfiability of Context-Free String Constraints with Subword Ordering