A Complexity Bound for Determinisation of Min-Plus Weighted Automata

TL;DR

This paper establishes the first complexity bound for the determinisation of min-plus weighted automata, providing a constructive analysis framework that simplifies previous proofs and advances understanding of the problem's computational complexity.

Contribution

It introduces a complexity bound within the Fast-growing hierarchy and develops a versatile, constructive framework for analyzing weighted automata runs.

Findings

Placed the determinisation problem in the Fast-growing hierarchy.

Provided a constructive framework simplifying previous non-constructive proofs.

Achieved a tighter analysis of the automata determinisation process.

Abstract

The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, placing it in the Fast-growing hierarchy. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.