Slice closures of indexed languages and word equations with counting constraints

TL;DR

This paper studies the slice closures of indexed languages' Parikh images, providing algorithms to compute semilinear representations, and applies these results to decide properties of word equations with counting constraints.

Contribution

It introduces the computation of the smallest slice containing an indexed language's Parikh image and applies this to decide properties of word equations with counting constraints.

Findings

Computed semilinear representations of slice closures for indexed languages.

Decided affine relations satisfied by Parikh images of indexed languages.

Established decidability of certain word equations with counting and rational constraints.

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$.