Wed 18 Jan 2023 13:55 - 14:20 at Grand Ballroom A - Logic & Decidability I Chair(s): Zachary Kincaid

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
Logic & Decidability IPOPL at Grand Ballroom A
Chair(s): Zachary Kincaid Princeton University
13:30
25m
Talk
Witnessability of Undecidable Problems
POPL
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI
13:55
25m
Talk
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
25m
Talk
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