We are happy to present Soumodev Mal’s talk titled “On the Satisfiability of Context-free String Constraints with Subword Ordering”.

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 such 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 a 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. Accepted at LICS’22.

Bio

Soumodev Mal is a second year PhD student at Chennai Mathematical Institute, India working under the supervision of Prof. C. Aiswarya, CMI and Prof. Prakash Saivasan, IMSc. His research interests broadly lies in Formal verification. He is currently working on verification of String Constraints.