*-Continuous Kleene $\omega$-Algebras for Energy Problems

TL;DR

This paper introduces algebraic methods based on continuous Kleene omega-algebras to solve energy problems in embedded systems by manipulating transition matrices of energy automata.

Contribution

It extends the theory of Kleene omega-algebras to continuous cases and applies it to energy automata for the first time.

Findings

Energy problems can be solved algebraically using transition matrices.

Finitely additive functions on complete lattices are key to the approach.

The approach generalizes previous algebraic methods for energy analysis.

Abstract

Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on star-continuous Kleene omega-algebras, we show here that energy problems can be solved by algebraic manipulations on the transition matrix of energy automata. To this end, we prove general results about certain classes of finitely additive functions on complete lattices which should be of a more general interest.