An Algebraic Approach to Energy Problems I — *-Continuous Kleene ω-Algebras

Ésik, Zoltán;Fahrenberg, Uli;Legay, Axel;Quaas, Karin
(2017) University of Szeged. Acta Cybernetica — Vol. 23, n° 1, p. 203-228 (2017)

Files

3923-Article-2175-1-10-20180614.pdf
  • Open Access
  • Adobe PDF
  • 446.98 KB

Details

Authors
  • Ésik, Zoltán
    Author
  • Fahrenberg, Uli
    Author
  • Legay, AxelUCLouvain
    Author
  • Quaas, Karin
    Author
Abstract
Energy problems are important in the formal analysis of embedded or autonomous systems. With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce energy automata. These are finite automata whose edges are labeled with energy functions that define how energy levels evolve during transitions. Motivated by this application and in order to compute with energy functions, we introduce a new algebraic structure of *-continuous Kleene ω-algebras. These involve a *-continuous Kleene algebra with a *-continuous action on a semimodule and an infinite product operation that is also *-continuous. We define both a finitary and a non-finitary version of *-continuous Kleene ω-algebras. We then establish some of their properties, including a characterization of the free finitary *-continuous Kleene ω-algebras. We also show that every *-continuous Kleene ω-algebra gives rise to an iteration semiring-semimodule pair.
Affiliations

Citations

Ésik, Z., Fahrenberg, U., Legay, A., & Quaas, K. (2017). An Algebraic Approach to Energy Problems I — *-Continuous Kleene ω-Algebras. University of Szeged. Acta Cybernetica, 23(1), 203-228. https://doi.org/10.14232/actacyb.23.1.2017.13 (Original work published 2017)