An $\omega$-Algebra for Real-Time Energy Problems

TL;DR

This paper introduces a mathematical framework using $^*$-continuous Kleene $ extomega$-algebras to model and analyze real-time energy systems, enabling static decision procedures for reachability and acceptance.

Contribution

It develops a novel algebraic structure for real-time energy functions and automata, facilitating static analysis of energy-related properties in real-time systems.

Findings

Decidability of reachability in real-time energy automata.

Decidability of Büchi acceptance in real-time energy automata.

Framework supports modeling energy consumption and recovery over time.

Abstract

We develop a $^*$-continuous Kleene $\omega$-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on $^*$-continuous Kleene $\omega$-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and B\"uchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.