We investigate properties of strings which are expressible by canonical types of string constraints. Specifically, we consider a landscape of 20 logical theories, whose syntax is built around combinations of four common elements of string constraints: language membership (e.g. for regular languages), concatenation, equality between string terms, and equality between string-lengths. For a variable x and formula f from a given theory, we consider the set of values for which x may be substituted as part of a satisfying assignment, or in other words, the property f expresses through x. Since we consider string-based logics, this set is a formal language. We firstly consider the relative expressive power of different combinations of string constraints by comparing the classes of languages expressible in the corresponding theories, and are able to establish a mostly complete picture in this regard. Secondly, we consider the question of deciding whether the language or property expressed by a variable/formula in one theory can be expressed in another theory. We establish several negative results which are relevant to preprocessing and normalisation of string constraints in practice. Some of our results have strong connections to important open problems regarding word equations and the theory of string solving.
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:45 | |||
13:30 25mTalk | Witnessability of Undecidable Problems POPL DOI | ||
13:55 25mTalk | On the Expressive Power of String Constraints POPL Joel D. Day Loughborough University, Vijay Ganesh Georgia Tech, Nathan Grewal University of Waterloo, Florin Manea University of Göttingen DOI | ||
14:20 25mTalk | A Robust Theory of Series Parallel Graphs POPL Rajeev Alur University of Pennsylvania, Caleb Stanford University of California, San Diego; University of California, Davis, Chris Watson University of Pennsylvania DOI |