Mostowski Index via extended register games

TL;DR

This paper introduces parity transduction games, a new game-based approach to determine the Mostowski index of tree automata, simplifying previous proofs and connecting automaton recognition to game outcomes.

Contribution

It presents parity transduction games as an extended game framework to analyze the Mostowski index, offering a simplified proof and new insights into automaton recognition.

Findings

Parity transduction games characterize automaton recognition by index J.

The approach simplifies the proof of the Mostowski index problem.

It connects automaton acceptance to game-theoretic conditions.

Abstract

The parity index problem of tree automata asks, given a regular tree language L, what is the least number of priorities of a nondeterministic parity tree automaton that recognises L. This is a long-standing open problem, also known as the Mostowski or Rabin-Mostowski index problem, of which only a few sub-cases and variations are known to be decidable. In a significant step, Colcombet and L\"oding reduced the problem to the uniform universality of distance-parity automata. In this brief note, we present a similar result, with a simplified proof, based on on the games in Lehtinen's quasipolynomial algorithm for parity games. We define an extended version of these games, which we call parity transduction games, which take as parameters a parity index J and an integer bound N. We show that the language of a guidable automaton A is recognised by a nondeterministic automaton of index J if and only if there is a bound N such that the parity transduction game with parameters J and N captures membership of the language, that is, for all trees t, Eve wins the parity transduction game on the acceptance parity game of t in A if and only in t is in L(A).