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.