We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables, or their transductions. 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 decidable. 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.
Based on joint works with Soumodev Mal and Prakash Saivasan (LICS'22, STACS'24)
Short Bio: C. Aiswarya is an Associate Professor in Computer Science at Chennai Mathematical Institute, India. She has held Invited Professor position at ENS Paris-Saclay, France and has a Visiting Faculty position at IIT Bombay India. Prior to joining CMI, she was a post-doctoral researcher in Uppsala University, Sweden. She received her PhD from ENS Cachan, France. Her primary research interests are in automata theory, concurrency theory and logic. She is also interested in developing theoretical tools for the verification of infinite state systems.