Slice closures of indexed languages and word equations with counting constraints

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 𝒖, 𝒖 +𝒗, 𝒖 +𝒘 implies membership of 𝒖 + 𝒗 + 𝒘. Our main result is that given an indexed language 𝐿, one can compute a semilinear representation of the smallest slice containing 𝐿'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 𝑎's as 𝑏'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 𝑎 differs between variables 𝑋 and 𝑌 .