Slice closures of indexed languages and word equations with counting constraints
Laura Ciobanu, Georg Zetzsche
TL;DR
The paper introduces slice closures of Parikh images as an effective semilinear overapproximation for indexed languages, enabling preservation of counting properties and enabling new decidability results. It develops a fixpoint framework with a derivation operator $\mathcal{D}$ and a saturation-based procedure to compute the smallest slice containing $\Psi(L)$, expressed semilinearly via $\mathcal{S}^\omega$. It then applies this machinery to (i) decide affine relations satisfied by $\Psi(L)$, including whether all words in $L$ have $|w|_a=|w|_b$, and (ii) establish decidability of word equations with rational constraints together with counting inequations. This introduces a novel, first step toward non-regular counting properties for indexed languages and paves the way for applications in higher-order model checking and related verification tasks.
Abstract
Indexed languages are a classical notion in formal language theory. As the language equivalent of second-order pushdown automata, they have received considerable attention in higher-order model checking. Unfortunately, counting properties are notoriously difficult to decide for indexed languages: So far, all results about non-regular counting properties show undecidability. In this paper, we initiate the study of slice closures of (Parikh images of) indexed languages. A slice is a set of vectors of natural numbers such that membership of $u,u+v,u+w$ implies membership of $u+v+w$. Our main result is that given an indexed language $L$, one can compute a semilinear representation of the smallest slice containing $L$'s Parikh image. We present two applications. First, one can compute the set of all affine relations satisfied by the Parikh image of an indexed language. In particular, this answers affirmatively a question by Kobayashi: Is it decidable whether in a given indexed language, every word has the same number of $a$'s as $b$'s. As a second application, we show decidability of (systems of) word equations with rational constraints and a class of counting constraints: These allow us to look for solutions where a counting function (defined by an automaton) is not zero. For example, one can decide whether a word equation with rational constraints has a solution where the number of occurrences of $a$ differs between variables $X$ and $Y$.