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

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.

Original language | English |
---|---|

Title of host publication | Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science |

Publisher | Association for Computing Machinery |

ISBN (Print) | 9798400706608 |

DOIs | |

Publication status | Published - 8 Jul 2024 |

Event | 39th Annual ACM/IEEE Symposium on Logic in Computer Science 2024 - Tallinn, Estonia Duration: 8 Jul 2024 → 11 Jul 2024 |

### Conference

Conference | 39th Annual ACM/IEEE Symposium on Logic in Computer Science 2024 |
---|---|

Abbreviated title | LICS 2024 |

Country/Territory | Estonia |

City | Tallinn |

Period | 8/07/24 → 11/07/24 |

## Keywords

- indexed language
- higher-order
- slice
- semilinear
- effective
- word equation
- counting constraints
- length equations
- decidability
- computability