String constraints with subword ordering: complexity of satisfiability

Speaker: C. Aiswarya, CMI

Monday, 17 April 2023, 15:00, Salle 1Z14 and Zoom

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, which was shown to be decidable in Atig-Bouajjani-Touilli-08. We show that this problem is \nexptime-complete.

This is a joint work with Prakash Saivasan and Soumodev Mal, which appeared in LICS 22.

Aiswarya will be at LMF from 2 April to 2 June 2023 as a Visiting Professor of ENS Paris-Saclay.