Kleene Algebras and Semimodules for Energy Problems

TL;DR

This paper introduces generalized energy automata with energy functions on transitions, unifies various energy problem approaches, and proves their decidability and complexity results for key cases.

Contribution

It presents a unified framework for energy problems using semiring-weighted automata and establishes their decidability and complexity.

Findings

Energy problems are decidable within the generalized automata framework.

Complexity results are provided for specific energy problem cases.

A close connection between energy problems and automata reachability is demonstrated.

Abstract

With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce generalized energy automata. These are finite automata whose edges are labeled with energy functions that define how energy levels evolve during transitions. Uncovering a close connection between energy problems and reachability and B\"uchi acceptance for semiring-weighted automata, we show that these generalized energy problems are decidable. We also provide complexity results for important special cases.