The Complexity of Mean-Payoff Automaton Expression

TL;DR

This paper establishes that decision problems for mean-payoff automaton expressions are PSPACE-complete, improving the previous upper bound from 4EXPTIME and providing a simpler algorithm for these problems.

Contribution

It proves the optimal PSPACE-complete complexity for decision problems in mean-payoff automaton expressions, refining prior bounds and simplifying solution methods.

Findings

Decision problems are PSPACE-complete.

Improved from 4EXPTIME upper bound.

Provided a simple algorithm for solving these problems.

Abstract

"Quantitative languages are extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. The class of \emph{mean-payoff automaton expressions}, introduced in [1], is a class of quantitative languages, which is robust: it is closed under the four pointwise operations of max, min, sum and numerical complement."[1] In this paper we improve the computational complexity for solving the classical decision problems for mean-payoff automaton expressions: while the previously best known upper bound was 4EXPTIME, and no lower bound was known, we give an optimal PSPACE complete bound. As a consequence we also obtain a conceptually simple algorithm to solve the classical decision problems for mean-payoff automaton expressions.