Alladi Ramakrishnan Hall

Satisfiability of String Constraints with Sub-word Ordering and Transducers

Prakash Saivasan

IMSc

In this talk, we will consider constraints over the domain of finite strings. Constraint system typically involve relational constraints and membership constraints. In our setting, we consider sub-word relation for relating the variables. We will study the satisfiability problem for such constraint systems. While the problem in full generality is undecidable, we will consider an acyclic fragment of it and show decidability. When no transducers are involved, we show that the problem is uniformly NExptime-complete when regular or context free languages are involved in the membership constraints. We will further establish a close connection between this problem and reachability in certain kinds of lossy channel systems. This connection in fact resolves a long standing complexity gap there. We will next investigate what happens when transducers are involved in the relational constraints. We will show that in this case, the problem remains NExptime-complete when only regular languages are involved in the membership constraints. Interestingly, the problem becomes 2Nexptime-complete in the presence of context free languages.