Parikh's Theorem Made Symbolic
Matthew Hague, Artur Jeż, Anthony W. Lin
TL;DR
Parikh's Theorem provides a bridge between language theory and arithmetic, but direct application to large alphabets is impractical. The authors develop a polynomial-time method to compute existential formulas that capture predicate-counting Parikh images for symbolic grammars and pushdown automata, and extend this to parametric variants, enabling reasoning over infinite alphabets. They implement the approach and demonstrate its usefulness for solving difficult string constraints, offering a practical, scalable unsat-filter that complements existing solvers. The work advances both theory and practice by enabling Parikh-style analysis in symbolic and parametric settings with real-world string-processing implications.
Abstract
Parikh's Theorem is a fundamental result in automata theory with numerous applications in computer science: software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases). Parikh's Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Presburger Arithmetic. Unfortunately, real-world applications typically require large alphabets - which are well-known to be not amenable to explicit treatment of the alphabets. Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh's Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh's Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. We provide a new construction for Parikh's Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm extends to the model of parametric symbolic grammars, which are one of the most expressive models of languages over infinite alphabets. We have implemented our algorithm and show it can be used to solve string constraints that are difficult to solve by existing solvers.