The complexity of downward closures of indexed languages

Authors:
Preprint
Publisher website
Google Scholar
Abstract
Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precisely the languages accepted by order-2 pushdown automata. The downward closure of an indexed language -- the set of all (scattered) subwords of its members -- is well-known to be a regular over-approximation. It was shown by Zetzsche (ICALP 2015) that the downward closure of a given indexed language is effectively computable. However, the algorithm comes with no complexity bounds, and it has remained open whether a primitive-recursive construction exists. We settle this question and provide a triply (resp.\ quadruply) exponential construction of a non-deterministic (resp.\ deterministic) automaton. We also prove (asymptotically) matching lower bounds. For the upper bounds, we rely on recent advances in semigroup theory, which let us compute bounded-size summaries of words with respect to a finite semigroup. By replacing stacks with their summaries, we are able to transform an indexed grammar into a context-free one with the same downward closure, and then apply existing bounds for context-free grammars.
All Related Versions

This publication has 44 references indexed in Scilit: