This is a revised and extended version of the paper [CFL15] which has been
presented at the 35th IARCS Annual Conference on Foundation of Software
Technology and Theoretical Computer Science (FSTTCS 2015) in Bangalore, India.
Compared to [CFL15], and in addition to numerous small changes and
improvements, motivation and examples as well as proofs of all results have
been added to the paper.

# An $\boldsymbol{\omega}$-Algebra for Real-Time Energy Problems

David Cachera  Irisa / École normale supérieure, Rennes, France  ,  Uli
Fahrenberg  École Polytechnique, Palaiseau, France  and  Axel Legay  Irisa /
Inria, Rennes, France

###### 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üchi acceptance in real-
time energy automata can be decided in a static way which only involves
manipulations of real-time energy functions.

Most of this work was completed while this author was still employed at Irisa
/ Inria Rennes.

##  1\. Introduction

_Energy_ and _resource management_ problems are important in areas such as
embedded systems or autonomous systems. They are concerned with the following
types of questions:

  * •

Can the system reach a designated state without running out of energy before?

  * •

Can the system reach a designated state within a specified time limit without
running out of energy?

  * •

Can the system repeatedly accomplish certain designated tasks without ever
running out of energy?

Instead of energy, these questions can also be asked using other resources,
for example money or fuel.

Figure 1.  GPS Block II-F satellite (artist’s conception; public domain)

As an example, imagine a satellite like in Fig. 1 which is being sent up into
space. In its initial state when it has arrived at its orbit, its solar panels
are still folded, hence no (electrical) energy is generated. Now it needs to
unfold its solar panels and rotate itself and its panels into a position
orthogonal to the sun’s rays (for maximum energy yield). These operations
require energy which hence must be provided by a battery, and there may be
some operational requirements which state that they have to be completed
within a given time limit. To minimize weight, one will generally be
interested to use a battery which is as little as possible.

closedp $0$halfp $2$open $5$closedp $0$halfp $4$opera-
tionalopen$-20$open$-20$open$-20$open$-20$rotate$-10$rotate$-10$rotate$-10$
Figure 2.  Toy model of the satellite in Fig. 1

Figure 2 shows a simple toy model of such a satellite’s initial operations. We
assume that it opens its solar panels in two steps; after the first step they
are half open and afterwards fully open, and that it can rotate into
orthogonal position at any time. The numbers within the states signify energy
gain per time unit, so that for example in the half-open state, the satellite
gains $2$ energy units per time unit before rotation and $4$ after rotation.
The (negative) numbers at transitions signify the energy cost for taking that
transition, hence it costs $20$ energy units to open the solar panels and $10$
to rotate.

Now if the satellite battery has sufficient energy, then we can follow any
path from the initial to the final state without spending time in intermediate
states. A simple inspection reveals that a battery level of $50$ energy units
is required for this. On the other hand, if battery level is strictly below
$20$, then no path is available to the final state. With initial energy level
between these two values, the device has to regain energy by spending time in
an intermediate state before proceeding to the next one. The optimal path then
depends on the available time and the initial energy. For an initial energy
level of at least $40$, the fastest strategy consists in first opening the
panels and then spending $2$ time units in state (open—$5$) to regain enough
energy to reach the final state. With the smallest possible battery, storing
$20$ energy units, $5$ time units have to be spent in state (half—$2$) before
passing to (half—$4$) and spending another $5$ time units there.

In this paper we will be concerned with models for such systems which, as in
the example, allow to spend time in states to regain energy, some of which has
to be spent when taking transitions between states. (Instead of energy, other
resource types could be modeled, but we will from now think of it as energy.)
We call these models _real-time energy automata_. Their behavior depends,
thus, on both the initial energy and the time available; as we have seen in
the example, this interplay between time and energy means that even simple
models can have rather complicated behaviors. As in the example, we will be
concerned with the _reachability_ problem for such models, but also with
_Büchi acceptance_ : whether there exists an infinite run which visits certain
designated states infinitely often.

Our methodology is strictly algebraic, using the theory of semiring-weighted
automata [DKV09] and extensions developed in [ÉFL15a, ÉFL15b]. We view the
finite behavior of a real-time energy automaton as a function $f(x_{0},t)$
which maps initial energy $x_{0}$ and available time $t$ to a final energy
level, intuitively corresponding to the highest output energy the system can
achieve when run with these parameters. We define a composition operator on
such _real-time energy functions_ which corresponds to concatenation of real-
time energy automata and show that with this composition and maximum as
operators, the set of real-time energy functions forms a _∗ -continuous Kleene
algebra_ [Koz94]. This implies that reachability in real-time energy automata
can be decided in a static way which only involves manipulations of real-time
energy functions.

To be able to decide Büchi acceptance, we extend the algebraic setting to also
encompass real-time energy functions which model infinite behavior. These take
as input an initial energy $x_{0}$ and time $t$, as before, but now the output
is Boolean: true if these parameters permit an infinite run, false if they do
not. We show that both types of real-time energy functions can be organized
into a _∗ -continuous Kleene $\omega$-algebra_ as defined in [ÉFL15a, ÉFL15b].
This entails that also Büchi acceptance for real-time energy automata can be
decided in a static way which only involves manipulations of real-time energy
functions.

The most technically demanding part of the paper is to show that real-time
energy functions form a _locally closed semiring_ [DKV09, ÉK02]; generalizing
some arguments in [ÉK02, ÉFL15b], it then follows that they form a
∗-continuous Kleene $\omega$-algebra. We conjecture that reachability and
Büchi acceptance in real-time energy automata can be decided in exponential
time.

### Related work

Real-time energy problems have been considered in [Qua11, BFL+08, BFLM10,
BLM14, FJLS11]. These are generally defined on _priced timed automata_ [ATP01,
BFH+01], a formalism which is more expressive than ours: it allows for time to
be reset and admits several independent time variables (or _clocks_) which can
be constrained at transitions. All known decidability results apply to priced
timed automata with only _one_ clock; in [BLM14] it is shown that with four
clocks, it is undecidable whether there exists an infinite run.

The work which is closest to ours is [BFLM10]. Their models are priced timed
automata with one clock and energy updates on transitions, hence a
generalization of ours. Using a sequence of complicated ad-hoc reductions,
they show that reachability and existence of infinite runs is decidable for
their models; whether their techniques apply to general Büchi acceptance is
unclear.

Our work is part of a program to make methods from semiring-weighted automata
available for energy problems. Starting with [ÉFLQ13], we have developed a
general theory of ∗-continuous Kleene $\omega$-algebras [ÉFL15a, ÉFL15b] and
shown that it applies to so-called _energy automata_ , which are finite
(untimed) automata which allow for rather general _energy transformations_ as
transition updates. The contribution of this paper is to show that these
algebraic techniques can be applied to a real-time setting.

Note that the application of Kleene algebra to real-time and hybrid systems is
not a new subject, see for example [HM09, DHMS12]. However, the work in these
papers is based on _trajectories_ and _interval predicates_ , respectively,
whereas our work is on real-time energy _automata_ , i.e., at a different
level. A more thorough comparison of our work to [HM09, DHMS12] would be
interesting future work.

### Acknowledgment

We are deeply indebted to our colleague and friend Zoltán Ésik who taught us
all we know about Kleene algebras and ∗-continuity. This work was started
during a visit of Zoltán at Irisa in Rennes; unfortunately, Zoltán did not
live to see it completed.

##  2\. Real-Time Energy Automata

Let $\mathbbm{R}_{\geq 0}=[0,\infty\mathclose{[}$ denote the set of non-
negative real numbers, $[0,\infty]$ the set $\mathbbm{R}_{\geq 0}$ extended
with infinity, and $\mathbbm{R}_{\leq 0}=\mathopen{]}-\infty,0]$ the set of
non-positive real numbers.

A _real-time energy automaton_ (RTEA) $(S,s_{0},F,T,r)$ consists of a finite
set $S$ of _states_ , with _initial state_ $s_{0}\in S$, a subset $F\subseteq
S$ of _accepting_ states, a finite set $T\subseteq S\times\mathbbm{R}_{\leq
0}\times\mathbbm{R}_{\geq 0}\times S$ of _transitions_ , and a mapping
$r:S\to\mathbbm{R}_{\geq 0}$ assigning _rates_ to states. A transition
$(s,p,b,s^{\prime})$ is written
$s\mathrel{\smash{\xrightarrow[\raisebox{2.15277pt}[0.0pt][0.0pt]{\hskip
3.00003pt$\scriptstyle b$\hskip 3.00003pt}]{p}}}s^{\prime}$, $p$ is called its
_price_ and $b$ its _bound_. We assume $b\geq-p$ for all transitions
$s\mathrel{\smash{\xrightarrow[\raisebox{2.15277pt}[0.0pt][0.0pt]{\hskip
3.00003pt$\scriptstyle b$\hskip 3.00003pt}]{p}}}s^{\prime}$.

An RTEA is _computable_ if all its rates, prices and bounds are computable
real numbers.

A _configuration_ of an RTEA $A=(S,s_{0},F,T,r)$ is an element $(s,x,t)\in
C=S\times\mathbbm{R}_{\geq 0}\times\mathbbm{R}_{\geq 0}$. Let
$\mathord{\leadsto}\subseteq C\times C$ be the relation given by
$(s,x,t)\leadsto(s^{\prime},x^{\prime},t^{\prime})$ iff $t^{\prime}\leq t$ and
there is a transition
$s\mathrel{\smash{\xrightarrow[\raisebox{2.15277pt}[0.0pt][0.0pt]{\hskip
3.00003pt$\scriptstyle b$\hskip 3.00003pt}]{p}}}s^{\prime}$ such that
$x+(t-t^{\prime})r(s)\geq b$ and $x^{\prime}=x+(t-t^{\prime})r(s)+p$. Hence
$t-t^{\prime}$ time units are spent in state $s$ and afterwards a transition
$s\mathrel{\smash{\xrightarrow[\raisebox{2.15277pt}[0.0pt][0.0pt]{\hskip
3.00003pt$\scriptstyle b$\hskip 3.00003pt}]{p}}}s^{\prime}$ is taken.

A _run_ in $A$ is a path in the infinite directed graph
$(C,\mathord{\leadsto})$, i.e., a finite or infinite sequence
$(s_{1},x_{1},t_{1})\leadsto(s_{2},x_{2},t_{2})\leadsto\dotsm$. We are ready
to state the decision problems for RTEAs with which we will be concerned. Let
$A=(S,s_{0},F,T,r)$ be a computable RTEA and $x_{0},t,y\in[0,\infty]$
computable numbers.

######  Problem 1 (State reachability).

Does there exist a finite run
$(s_{0},x_{0},t)\leadsto\dotsm\leadsto(s,x,t^{\prime})$ in $A$ with $s\in F$?

######  Problem 2 (Coverability).

Does there exist a finite run
$(s_{0},x_{0},t)\leadsto\dotsm\leadsto(s,x,t^{\prime})$ in $A$ with $s\in F$
and $x\geq y$?

######  Problem 3 (Büchi acceptance).

Does there exist $s\in F$ and an infinite run
$(s_{0},x_{0},t)\leadsto(s_{1},x_{1},t_{1})\leadsto\dotsm$ in $A$ in which
$s_{n}=s$ for infinitely many $n\geq 0$?

Note that the coverability problem only asks for the final energy level $x$ to
be _above_ $y$; as we are interested in _maximizing_ energy, this is natural.
Also, state reachability can be reduced to coverability by setting $y=0$. As
the Büchi acceptance problem asks for infinite runs, there is no notion of
output energy for this problem.

Asking the Büchi acceptance question for a _finite_ available time $t<\infty$
amounts to finding (accepting) _Zeno runs_ in the given RTEA, i.e., runs which
make infinitely many transitions in finite time. Hence one will usually be
interested in Büchi acceptance only for an infinite time horizon.

On the other hand, for $t=\infty$, a positive answer to the state reachability
problem 1 will consist of a finite run
$(s_{0},x_{0},\infty)\leadsto\dotsm\leadsto(s,x,\infty)$. Now as one can delay
indefinitely in the state $s\in F$, this yields an infinite _timed run_ in the
RTEA. Per our definition of $\leadsto$ however, such an infinite run will
_not_ be a positive answer to the Büchi acceptance problem.

##  3\. Weighted Automata over ∗-Continuous Kleene $\omega$-Algebras

We now turn our attention to the algebraic setting of ∗-continuous Kleene
algebras and related structures and review some results on ∗-continuous Kleene
algebras and ∗-continuous Kleene $\omega$-algebras which we will need in the
sequel.

###  3.1. ∗-Continuous Kleene Algebras

An _idempotent semiring_ [Gol99] $S=(S,\vee,\cdot,\bot,1)$ consists of an
idempotent commutative monoid $(S,\vee,\bot)$ and a monoid $(S,\cdot,1)$ such
that the distributive and zero laws

$x(y\vee z)=xy\vee xz\qquad\qquad(y\vee z)x=yx\vee zx\qquad\qquad\bot
x=\bot=x\bot$

hold for all $x,y,z\in S$. It follows that the product operation distributes
over all finite suprema. Each idempotent semiring $S$ is partially ordered by
the relation $x\leq y$ iff $x\vee y=y$, and then sum and product preserve the
partial order and $\bot$ is the least element.

A _Kleene algebra_ [Koz94] is an idempotent semiring $S=(S,\vee,\cdot,\bot,1)$
equipped with an operation ${}^{*}:S\to S$ such that for all $x,y\in S$,
$yx^{*}$ is the least solution of the fixed point equation $z=zx\vee y$ and
$x^{*}y$ is the least solution of the fixed point equation $z=xz\vee y$ with
respect to the order $\leq$.

A _∗ -continuous Kleene algebra_ [Koz94] is a Kleene algebra
$S=(S,\vee,\cdot,^{*},\bot,1)$ in which the infinite suprema
$\bigvee\\{x^{n}\mid n\geq 0\\}$ exist for all $x\in S$,
$x^{*}=\bigvee\\{x^{n}\mid n\geq 0\\}$ for every $x\in S$, and product
preserves such suprema: for all $x,y\in S$,

$y\big{(}\bigvee_{n\geq 0}x^{n}\big{)}=\bigvee_{n\geq
0}yx^{n}\quad\text{and}\quad\big{(}\bigvee_{n\geq
0}x^{n}\big{)}y=\bigvee_{n\geq 0}x^{n}y\,.$

Examples of ∗-continuous Kleene algebras include the set $P(\Sigma^{*})$ of
languages over an alphabet $\Sigma$, with set union as $\vee$ and
concatenation as $\cdot$, and the set $P(A\times A)$ of relations over a set
$A$, with set union as $\vee$ and relation composition as $\cdot$. These are,
in fact, _continuous_ Kleene algebras in the sense that suprema $\bigvee X$ of
arbitrary subsets $X$ exist.

An important example of a ∗-continuous Kleene algebra which is not continuous
is the set $R(\Sigma^{*})$ of _regular_ languages over an alphabet $\Sigma$.
This example is canonical in the sense that $R(\Sigma^{*})$ is the _free_
∗-continuous Kleene algebra over $\Sigma$.

An idempotent semiring $S=(S,\vee,\cdot,\bot,1)$ is said to be _locally
closed_ [ÉK02] if it holds that for every $x\in S$, there exists $N\geq 0$ so
that $\bigvee_{n=0}^{N}x^{n}=\bigvee_{n=0}^{N+1}x^{n}$. In any locally closed
idempotent semiring, we may define a ∗-operation by $x^{*}=\bigvee_{n\geq
0}x^{n}$.

######  Lemma 4.

Any locally closed idempotent semiring is a ∗-continuous Kleene algebra.

######  Proof 3.1.

Let $S=(S,\mathord{\vee},\mathord{\cdot},\bot,1)$ be a locally closed
idempotent semiring. We need to show that for all elements $x,y,z\in S$,

$xy^{*}=\bigvee_{n\geq 0}(xy^{n})\qquad\text{and}\qquad y^{*}z=\bigvee_{n\geq
0}(y^{n}z)\,.$

It is clear that the right-hand sides of the equations are less than or equal
to their left-hand sides, so we are left with proving the other inequalities.
As $S$ is locally closed, there is $N\geq 0$ such that
$y^{*}=\bigvee_{n=0}^{N}y^{n}$, and then by distributivity,
$xy^{*}=x\big{(}\bigvee_{n=0}^{N}y^{n})=\bigvee_{n=0}^{N}(xy^{n})\leq\bigvee_{n\geq
0}(xy^{n})$; similarly, $y^{*}z\leq\bigvee_{n\geq 0}(y^{n}z)$.

###  3.2. ∗-Continuous Kleene $\omega$-Algebras

An _idempotent semiring-semimodule pair_ [ÉK07b, BÉ93] $(S,V)$ consists of an
idempotent semiring $S=(S,\vee,\cdot,\bot,1)$ and a commutative idempotent
monoid $V=(V,\vee,\bot)$ which is equipped with a left $S$-action $S\times
V\to V$, $(s,v)\mapsto sv$, satisfying

$\displaystyle(s\vee s^{\prime})v$ $\displaystyle=sv\vee
s^{\prime}v\qquad\qquad$ $\displaystyle s(v\vee v^{\prime})$
$\displaystyle=sv\vee sv^{\prime}\qquad\qquad$ $\displaystyle\bot s$
$\displaystyle=\bot$ $\displaystyle(ss^{\prime})v$
$\displaystyle=s(s^{\prime}v)$ $\displaystyle s\bot$ $\displaystyle=\bot$
$\displaystyle 1v$ $\displaystyle=v$

for all $s,s^{\prime}\in S$ and $v\in V$. In that case, we also call $V$ a
_(left) $S$-semimodule_.

A _generalized ∗-continuous Kleene algebra_ [ÉFL15a] is an idempotent
semiring-semimodule pair $(S,V)$ where $S=(S,\vee,\cdot,^{*},\bot,1)$ is a
∗-continuous Kleene algebra such that for all $x,y\in S$ and for all $v\in V$,

$xy^{*}v=\bigvee_{n\geq 0}xy^{n}v$

A _∗ -continuous Kleene $\omega$-algebra_ [ÉFL15a] consists of a generalized
∗-continuous Kleene algebra $(S,V)$ together with an infinite product
operation $S^{\omega}\to V$ which maps every infinite sequence
$x_{0},x_{1},\dotsc$ in $S$ to an element $\prod_{n\geq 0}x_{n}$ of $V$. The
infinite product is subject to the following conditions:

  * •

For all $x_{0},x_{1},\dotsc\in S$, $\displaystyle\prod_{n\geq
0}x_{n}=x_{0}\prod_{n\geq 0}x_{n+1}$. $(\textrm{{C}}1)$

  * •

Let $x_{0},x_{1},\dotsc\in S$ and $0=n_{0}\leq n_{1}\leq\dotsm$ a sequence
which increases without a bound. Let $y_{k}=x_{n_{k}}\dotsm x_{n_{k+1}-1}$ for
all $k\geq 0$. Then $\displaystyle\prod_{n\geq 0}x_{n}=\prod_{k\geq 0}y_{k}$.
$(\textrm{{C}}2)$

  * •

For all $x_{0},x_{1},\dotsc,y,z\in S$, $\displaystyle\prod_{n\geq
0}(x_{n}(y\vee
z))=\adjustlimits{\bigvee}_{x_{0}^{\prime},x_{1}^{\prime},\dotsc\in\\{y,z\\}\;}{\prod}_{n\geq
0}x_{n}x_{n}^{\prime}$. $(\textrm{{C}}3)$

  * •

For all $x,y_{0},y_{1},\dotsc\in S$, $\displaystyle\prod_{n\geq
0}x^{*}y_{n}=\adjustlimits{\bigvee}_{k_{0},k_{1},\dotsc\geq 0\;}{\prod}_{n\geq
0}x^{k_{n}}y_{n}$. $(\textrm{{C}}4)$

Hence the infinite product extends the finite product $(\textrm{{C}}1)$; it is
finitely associative $(\textrm{{C}}2)$; it preserves finite suprema
$(\textrm{{C}}3)$; and it preserves the ∗-operation (and hence infinite
suprema of the form $\bigvee_{n\geq 0}x^{n}$) $(\textrm{{C}}4)$.

An example of a ∗-continuous Kleene $\omega$-algebra is the structure
$(P(\Sigma^{*}),P(\Sigma^{\infty}))$ consisting of the set $P(\Sigma^{*})$ of
languages of finite words and of the set $P(\Sigma^{\infty})$ of finite or
infinite words over an alphabet $\Sigma$. This is, in fact, a _continuous_
Kleene $\omega$-algebra [ÉFL15a] in the sense that the infinite product
preserves _all_ suprema.

A ∗-continuous Kleene $\omega$-algebra which is _not_ continuous is
$(R(\Sigma^{*}),R^{\prime}(\Sigma^{\infty}))$, where $R(\Sigma^{*})$ is the
set of regular languages over $\Sigma$, and $R^{\prime}(\Sigma^{\infty})$
contains all subsets of the set $\Sigma^{\infty}$ of finite or infinite words
which are finite unions of _finitary_ infinite products of regular languages,
see [ÉFL15a].

###  3.3. Matrix Semiring-Semimodule Pairs

For any idempotent semiring $S$ and $n\geq 1$, we can form the matrix semiring
$S^{n\times n}$ whose elements are $n\times n$-matrices of elements of $S$ and
whose sum and product are given as the usual matrix sum and product. It is
known [Koz90] that when $S$ is a ∗-continuous Kleene algebra, then $S^{n\times
n}$ is also a ∗-continuous Kleene algebra, with the ∗-operation defined by

$M^{*}_{i,j}=\bigvee_{m\geq
0}\bigvee\big{\\{}M_{k_{1},k_{2}}M_{k_{2},k_{3}}\dotsm
M_{k_{m-1},k_{m}}\mathrel{\big{|}}1\leq k_{1},\dotsc,k_{m}\leq
n,k_{1}=i,k_{m}=j\big{\\}}$ (1)

for all $M\in S^{n\times n}$ and $1\leq i,j\leq n$. Also, if $n\geq 2$ and
$M=\left(\begin{smallmatrix}a&b\\\ c&d\end{smallmatrix}\right)$, where $a$ and
$d$ are square matrices of dimension less than $n$, then

$M^{*}=\begin{pmatrix}(a\vee bd^{*}c)^{*}&(a\vee bd^{*}c)^{*}bd^{*}\\\ (d\vee
ca^{*}b)^{*}ca^{*}&(d\vee ca^{*}b)^{*}\end{pmatrix}$ (2)

For any idempotent semiring-semimodule pair $(S,V)$ and $n\geq 1$, we can form
the matrix semiring-semimodule pair $(S^{n\times n},V^{n})$ whose elements are
$n\times n$-matrices of elements of $S$ and $n$-dimensional (column) vectors
of elements of $V$, with the action of $S^{n\times n}$ on $V^{n}$ given by the
usual matrix-vector product.

When $(S,V)$ is a ∗-continuous Kleene $\omega$-algebra, then $(S^{n\times
n},V^{n})$ is a generalized ∗-continuous Kleene algebra [ÉFL15a]. By [ÉFL15a,
Lemma 17], there is an $\omega$-operation on $S^{n\times n}$ defined by

$M^{\omega}_{i}=\bigvee_{1\leq k_{1},k_{2},\dotsc\leq
n}M_{i,k_{1}}M_{k_{1},k_{2}}\dotsm$

for all $M\in S^{n\times n}$ and $1\leq i\leq n$. Also, if $n\geq 2$ and
$M=\left(\begin{smallmatrix}a&b\\\ c&d\end{smallmatrix}\right)$, where $a$ and
$d$ are square matrices of dimension less than $n$, then

$M^{\omega}=\begin{pmatrix}(a\vee bd^{*}c)^{\omega}\vee(a\vee
bd^{*}c)^{*}bd^{\omega}\\\ (d\vee ca^{*}b)^{\omega}\vee(d\vee
ca^{*}b)^{*}ca^{\omega}\end{pmatrix}$ (3)

It can be shown [ÉK07a] that the number of semiring computations required in
the computation of $M^{*}$ and $M^{\omega}$ in (2) and (3) is $O(n^{3})$ and
$O(n^{4})$, respectively.

###  3.4. Weighted automata

Let $(S,V)$ be a ∗-continuous Kleene $\omega$-algebra and $A\subseteq S$ a
subset. We write $\langle A\rangle$ for the set of all finite suprema
$a_{1}\vee\dotsm\vee a_{m}$ with $a_{i}\in A$ for each $i=1,\dotsc,m$.

A _weighted automaton_ [DKV09] over $A$ of dimension $n\geq 1$ is a tuple
$(\alpha,M,k)$, where $\alpha\in\\{\bot,1\\}^{n}$ is the initial vector,
$M\in\langle A\rangle^{n\times n}$ is the transition matrix, and $k$ is an
integer $0\leq k\leq n$. Combinatorially, this may be represented as a
transition system whose set of states is $\\{1,\dotsc,n\\}$. For any pair of
states $i,j$, the transitions from $i$ to $j$ are determined by the entry
$M_{i,j}$ of the transition matrix: if $M_{i,j}=a_{1}\vee\dotsm\vee a_{m}$,
then there are $m$ transitions from $i$ to $j$, respectively labeled
$a_{1},\dotsc,a_{n}$. The states $i$ with $\alpha_{i}=1$ are _initial_ , and
the states $\\{1,\dotsc,k\\}$ are _accepting_.

The _finite behavior_ of a weighted automaton $A=(\alpha,M,k)$ is defined to
be

$|A|=\alpha M^{*}\kappa\,,$

where $\kappa\in\\{\bot,1\\}^{n}$ is the vector given by $\kappa_{i}=1$ for
$i\leq k$ and $\kappa_{i}=\bot$ for $i>k$. (Note that $\alpha$ has to be used
as a _row_ vector for this multiplication to make sense.) It is clear by (1)
that $|A|$ is the supremum of the products of the transition labels along all
paths in $A$ from any initial to any accepting state.

The _Büchi behavior_ of a weighted automaton $A=(\alpha,M,k)$ is defined to be

$\|A\|=\alpha\begin{pmatrix}(a+bd^{*}c)^{\omega}\\\
d^{*}c(a+bd^{*}c)^{\omega}\end{pmatrix},$

where $a\in\langle A\rangle^{k\times k}$, $b\in\langle
A\rangle^{k\times(n-k)}$, $c\in\langle A\rangle^{(n-k)\times n}$ and
$d\in\langle A\rangle^{(n-k)\times(n-k)}$ are such that
$M=\left(\begin{smallmatrix}a&b\\\ c&d\end{smallmatrix}\right)$. Note that $M$
is split in submatrices $\left(\begin{smallmatrix}a&b\\\
c&d\end{smallmatrix}\right)$ precisely so that $a$ contains transitions
between accepting states and $d$ contains transitions between non-accepting
states. By [ÉFL15a, Thm. 20], $\|A\|$ is the supremum of the products of the
transition labels along all infinite paths in $A$ from any initial state which
infinitely often visit an accepting state.

##  4\. Real-Time Energy Functions

We are now ready to consider the algebra of real-time energy functions. We
will build this up inductively, starting from the functions which correspond
to simple _atomic_ RTEAs. These can be composed to form _linear_ real-time
energy functions, and with additional maximum and star operations, they form a
∗-continuous Kleene algebra. When also taking infinite behaviors into account,
we get a ∗-continuous Kleene $\omega$-algebra of real-time energy functions.

Let $L=[0,\infty]_{\bot}$ denote the set of non-negative real numbers extended
with a bottom element $\bot$ and a top element $\infty$. We use the standard
order on $L$, i.e., the one on $\mathbbm{R}_{\geq 0}$ extended by declaring
$\bot\leq x\leq\infty$ for all $x\in L$. $L$ is a complete lattice, whose
suprema we will denote by $\vee$ for binary and $\bigvee$ for general
supremum. For convenience we also extend the addition on $\mathbbm{R}_{\geq
0}$ to $L$ by declaring that $\bot+x=x+\bot=\bot$ for all $x\in L$ and
$\infty+x=x+\infty=\infty$ for all $x\in L\setminus\\{\bot\\}$. Note that
$\bot+\infty=\infty+\bot=\bot$.

Let $\mathcal{F}$ denote the set of monotonic functions
$f:L\times[0,\infty]\to L$ (with the product order on $L\times[0,\infty]$) for
which $f(\bot,t)=\bot$ for all $t\in L$. We will frequently write such
functions in curried form, using the isomorphism $\langle L\times[0,\infty]\to
L\rangle\approx\langle[0,\infty]\to L\to L\rangle$.

###  4.1. Linear Real-Time Energy Functions

We will be considered with the subset of functions in $\mathcal{F}$ consisting
of _real-time energy functions_ (RTEFs). These correspond to functions
expressed by RTEAs, and we will construct them inductively. We start with
atomic RTEFs:

Let $r,b,p\in\mathbbm{R}$ with $r\geq 0$, $p\leq 0$ and $b\geq-p$. An _atomic
real-time energy function_ is an element $f$ of $\mathcal{F}$ such that
$f(\bot,t)=\bot$, $f(\infty,t)=\infty$, $f(x,\infty)=\infty$, and

$f(x,t)=\begin{cases}x+rt+p&\text{if }x+rt\geq b\,,\\\
\bot&\text{otherwise}\end{cases}$

for all $x,t\in\mathbbm{R}_{\geq 0}$. The numbers $r,b$ and $p$ are
respectively called the _rate_ , _bound_ and _price_ of $f$. We denote by
$\mathcal{A}\subseteq\mathcal{F}$ the set of atomic real-time energy
functions.

These functions arise from RTEAs with one transition:

$r$$p$$b$

Non-negativity of $r$ ensures that atomic RTEFs are monotonic. In our
examples, when the bound is not explicitly mentioned it corresponds to the
lowest possible one: $b=-p$.

Atomic RTEFs are naturally combined along acyclic paths by means of a
composition operator. Intuitively, a composition of two successive atomic
RTEFs determines the optimal output energy one can get after spending some
time in either one or both locations of the corresponding automaton. This
notion of composition is naturally extended to all functions in $\mathcal{F}$,
and formally defined as follows (where $\circ$ denotes standard function
composition).

The _composition_ of $f,g\in\mathcal{F}$ is the element
$f\mathrel{\mathop{\triangleright}}g$ of $\mathcal{F}$ such that

$\forall
t\in[0,\infty]:f\mathrel{\mathop{\triangleright}}g(t)=\bigvee_{t_{1}+t_{2}=t}g(t_{2})\circ
f(t_{1})$ (4)

Note that composition is written in diagrammatic order. Uncurrying the
equation, we see that
$f\mathrel{\mathop{\triangleright}}g(x,t)=\bigvee_{t_{1}+t_{2}=t}g(f(x,t_{1}),t_{2})$.

Let $\mathbf{1},\bot\in\mathcal{F}$ be the functions defined by
$\mathbf{1}(t)(x)=x$ and $\bot(t)(x)=\bot$ for all $x,t$.

######  Lemma 5.

The $\mathrel{\mathop{\triangleright}}$ operator is associative, with
$\mathbf{1}$ as neutral and $\bot$ as absorbing elements.

######  Proof 4.1.

Let $f\in\mathcal{F}$. It is clear that
$f\mathrel{\mathop{\triangleright}}\bot=\bot\mathrel{\mathop{\triangleright}}f=f$.
For $f\mathrel{\mathop{\triangleright}}\mathbf{1}$ and
$\mathbf{1}\mathrel{\mathop{\triangleright}}f$, we have
$f\mathrel{\mathop{\triangleright}}\mathbf{1}(t)(x)=\bigvee_{t_{1}+t_{2}=t}\mathbf{1}(f(x,t_{1}),t_{2})=\bigvee_{t_{1}+t_{2}=t}f(x,t_{1})=f(x,t)$
because of monotonicity of $f$. Similarly,
$\mathbf{1}\mathrel{\mathop{\triangleright}}f(t)(x)=\bigvee_{t_{1}+t_{2}=t}f(\mathbf{1}(x,t_{1}),t_{2})=\bigvee_{t_{1}+t_{2}=t}f(x,t_{2})=f(x,t)$
because of monotonicity of $f$. As to associativity, a routine calculation
shows that for all $f,g,h\in\mathcal{F}$,
$((f\mathrel{\mathop{\triangleright}}g)\mathrel{\mathop{\triangleright}}h)(t)=(f\mathrel{\mathop{\triangleright}}(g\mathrel{\mathop{\triangleright}}h))(t)=\bigvee_{t_{1}+t_{2}+t_{3}=t}h(t_{3})\circ
g(t_{2})\circ f(t_{1})$.

Compositions of atomic RTEFs along paths are called _linear_ RTEFs:

A _linear real-time energy function_ is a finite composition
$f_{1}\mathrel{\mathop{\triangleright}}f_{2}\mathrel{\mathop{\triangleright}}\dots\mathrel{\mathop{\triangleright}}f_{n}$
of atomic RTEFs.

As an example, and also to show that linear RTEFs can have quite complex
behavior, we show the linear RTEF associated to one of the paths in the
satellite example of the introduction. Consider the following (linear) RTEA:

$0$$2$$5$$-20$$20$$-20$$20$$-10$$10$

Its linear RTEF $f$ can be computed as follows:

$f(x,t)=\begin{cases}\bot&\text{if }x<20\text{ or }(20\leq x<40\text{ and
}x+2t<44)\\\ &\phantom{\text{if }x<20}\text{ or }(x\geq 40\text{ and
}x+5t<50)\\\ 2.5x+5t-110&\text{if }20\leq x<40\text{ and }x+2t\geq 44\\\
x+5t-50&\text{if }x\geq 40\text{ and }x+5t\geq 50\end{cases}$

We show a graphical representation of $f$ on Fig. 3. The left part of the
figure shows the boundary between two regions in the $(x,t)$ plane,
corresponding to the minimal value $0$ achieved by the function. Below this
boundary, no path exists through the corresponding RTEA. Above, the function
is linear in $x$ and $t$. The coefficient of $t$ corresponds to the maximal
rate in the RTEA; the coefficient of $x$ depends on the relative position of
$x$ with respect to (partial sums of) the bounds $b_{i}$.

$x$0$20$$40$$50$$t$$2$$12$$f(x,t)=\bot$$f(x,t)\neq\bot$slope $-\infty$slope
$-1/2$slope $-1/5$

$x$$t$$f$0$20$$40$$50$$10$

Figure 3.  Graphical representation of the linear RTEF from Example 4.1.

###  4.2. Normal Form

Next we need to see that all linear RTEFs can be converted to a _normal form_
:

A sequence $f_{1},\dotsc,f_{n}$ of atomic RTEFs, with rates, bounds and prices
$r_{1},\dotsc,r_{n}$, $b_{1},\dotsc,b_{n}$ and $p_{1},\dotsc,p_{n}$,
respectively, is in _normal form_ if

  * •

$r_{1}<\dotsm<r_{n}$,

  * •

$b_{1}\leq\dotsm\leq b_{n}$, and

  * •

$p_{1}=\dotsm=p_{n-1}=0$.

######  Lemma 6.

For any linear RTEF $f$ there exists a sequence $f_{1},\dotsc,f_{n}$ of atomic
RTEFs in normal form such that
$f=f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}$.

A normal form of the RTEF from Example 4.1 is as follows:

$0$$2$$5$$0$$20$$0$$40$$-50$$50$

It is clear that its energy function is the same as the one of Example 4.1:
any run which satisfies the new constraints is equivalent to one which
satisfies the old ones, and vice versa.

######  Proof 4.2.

Let
$f=f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}$,
where $f_{1},\dotsc,f_{n}$ are atomic RTEFs and assume $f_{1},\dots,f_{n}$ is
not in normal form. If there is an index $k\in\\{1,\dotsc,n-1\\}$ with
$r_{k}\geq r_{k+1}$, then we can use the following transformation to remove
the state with rate $r_{k+1}$:

$\leavevmode\hbox to145.72pt{\vbox
to29.8pt{\pgfpicture\makeatletter\hbox{\hskip 27.09583pt\lower-16.22154pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{7.11319pt}{0.0pt}\pgfsys@curveto{7.11319pt}{3.92854pt}{3.92854pt}{7.11319pt}{0.0pt}{7.11319pt}\pgfsys@curveto{-3.92854pt}{7.11319pt}{-7.11319pt}{3.92854pt}{-7.11319pt}{0.0pt}\pgfsys@curveto{-7.11319pt}{-3.92854pt}{-3.92854pt}{-7.11319pt}{0.0pt}{-7.11319pt}\pgfsys@curveto{3.92854pt}{-7.11319pt}{7.11319pt}{-3.92854pt}{7.11319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.9405pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}{}{{}}{}}{{{}}{{}}}{}{{}}{}{{}}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{-20.22981pt}{0.0pt}\pgfsys@lineto{-8.77318pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.77318pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.76282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{62.7686pt}{0.0pt}\pgfsys@curveto{62.7686pt}{5.59343pt}{58.23434pt}{10.12769pt}{52.64091pt}{10.12769pt}\pgfsys@curveto{47.04749pt}{10.12769pt}{42.51323pt}{5.59343pt}{42.51323pt}{0.0pt}\pgfsys@curveto{42.51323pt}{-5.59343pt}{47.04749pt}{-10.12769pt}{52.64091pt}{-10.12769pt}\pgfsys@curveto{58.23434pt}{-10.12769pt}{62.7686pt}{-5.59343pt}{62.7686pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{52.64091pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{45.12262pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{118.42401pt}{0.0pt}\pgfsys@curveto{118.42401pt}{5.59343pt}{113.88976pt}{10.12769pt}{108.29633pt}{10.12769pt}\pgfsys@curveto{102.7029pt}{10.12769pt}{98.16864pt}{5.59343pt}{98.16864pt}{0.0pt}\pgfsys@curveto{98.16864pt}{-5.59343pt}{102.7029pt}{-10.12769pt}{108.29633pt}{-10.12769pt}\pgfsys@curveto{113.88976pt}{-10.12769pt}{118.42401pt}{-5.59343pt}{118.42401pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{108.29633pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{100.77803pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.31319pt}{0.0pt}\pgfsys@lineto{40.85324pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.85324pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.75175pt}{5.47743pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.12155pt}{-10.47745pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{62.9686pt}{0.0pt}\pgfsys@lineto{96.50865pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{96.50865pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{72.82938pt}{5.9441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{73.19917pt}{-10.47743pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\underset{(r_{k}\geq
r_{k+1})}{\longmapsto}\leavevmode\hbox to127.61pt{\vbox
to31.98pt{\pgfpicture\makeatletter\hbox{\hskip
27.09583pt\lower-16.86601pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{7.11319pt}{0.0pt}\pgfsys@curveto{7.11319pt}{3.92854pt}{3.92854pt}{7.11319pt}{0.0pt}{7.11319pt}\pgfsys@curveto{-3.92854pt}{7.11319pt}{-7.11319pt}{3.92854pt}{-7.11319pt}{0.0pt}\pgfsys@curveto{-7.11319pt}{-3.92854pt}{-3.92854pt}{-7.11319pt}{0.0pt}{-7.11319pt}\pgfsys@curveto{3.92854pt}{-7.11319pt}{7.11319pt}{-3.92854pt}{7.11319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.9405pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}{}{{}}{}}{{{}}{{}}}{}{{}}{}{{}}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{-20.22981pt}{0.0pt}\pgfsys@lineto{-8.77318pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.77318pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.76282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{100.31377pt}{0.0pt}\pgfsys@curveto{100.31377pt}{5.59343pt}{95.77951pt}{10.12769pt}{90.18608pt}{10.12769pt}\pgfsys@curveto{84.59265pt}{10.12769pt}{80.0584pt}{5.59343pt}{80.0584pt}{0.0pt}\pgfsys@curveto{80.0584pt}{-5.59343pt}{84.59265pt}{-10.12769pt}{90.18608pt}{-10.12769pt}\pgfsys@curveto{95.77951pt}{-10.12769pt}{100.31377pt}{-5.59343pt}{100.31377pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{90.18608pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{82.66779pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.31319pt}{0.0pt}\pgfsys@lineto{78.3984pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{78.3984pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{26.88512pt}{5.9441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k}+p_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.36879pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\max(b_{k},b_{k+1}-p_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

Informally, any run through the RTEA for
$f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}$
which maximizes output energy will spend no time in the state with rate
$r_{i+1}$, as this time may as well be spent in the state with rate $r_{i}$
without lowering output energy. To make this argument precise, we prove that
this transformation does not change the values of $f$.

Let $f^{\prime}$ denote the function which results from the transformation.
Let $x\in L$ and $t\in[0,\infty]$. We show first that $f(x,t)\leq
f^{\prime}(x,t)$, which is clear if $f(x,t)=\bot$. If $f(x,t)\neq\bot$, then
there is an accepting run through the RTEA corresponding to
$f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}$.
Hence we have $t_{1}+\dotsm+t_{n}=t$ such that
$f(x,t)=x+r_{1}t_{1}+p_{1}+\dotsm+r_{n}t_{n}+p_{n}$ and
$x+\dotsm+r_{j}t_{j}\geq b_{j}$ for all $j=1,\dotsc,n$. Let
$t_{k}^{\prime}=t_{k}+t_{k+1}$, $t_{k+1}^{\prime}=0$, and
$t_{j}^{\prime}=t_{j}$ for all $j\notin\\{k,k+1\\}$. By $r_{k}\geq r_{k+1}$,
we know that $x+\dotsm+r_{k}t_{k}^{\prime}\geq b_{k}$ and
$x+\dotsm+r_{k+1}t_{k+1}^{\prime}\geq b_{k+1}^{\prime}$, hence
$x+\dotsm+r_{j}t_{j}^{\prime}\geq b_{j}$ for all $j=1,\dotsc,n$. Hence this
new run is also accepting, and
$x+r_{1}t_{1}^{\prime}+p_{1}+\dotsm+r_{n}t_{n}^{\prime}+p_{n}\geq f(x,t)$.
Because $t_{k+1}^{\prime}=0$, this also yields an accepting run through the
RTEA for $f^{\prime}$, showing that $f^{\prime}(x,t)\geq f(x,t)$.

The other inequality, $f(x,t)\geq f^{\prime}(x,t)$, is clear if
$f^{\prime}(x,t)=\bot$. Otherwise, there is an accepting run through the RTEA
for $f^{\prime}$. Hence we have $t_{1}+\dotsm+t_{n}=t$, with $t_{k+1}=0$, such
that $f^{\prime}(x,t)=x+r_{1}t_{1}+p_{1}+\dotsm+r_{n}t_{n}+p_{n}$ and
$x+\dotsm+r_{j}t_{j}\geq b_{j}$ for all $j=1,\dotsc,n$. But then this is also
an accepting run through the RTEA for $f$, showing that $f(x,t)\geq
f^{\prime}(x,t)$.

We can hence assume that $r_{1}<\dotsm<r_{n}$. To ensure the last two
conditions of Definition 4.2, we use the following transformation:

$\leavevmode\hbox to145.72pt{\vbox
to29.8pt{\pgfpicture\makeatletter\hbox{\hskip 27.09583pt\lower-16.22154pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{7.11319pt}{0.0pt}\pgfsys@curveto{7.11319pt}{3.92854pt}{3.92854pt}{7.11319pt}{0.0pt}{7.11319pt}\pgfsys@curveto{-3.92854pt}{7.11319pt}{-7.11319pt}{3.92854pt}{-7.11319pt}{0.0pt}\pgfsys@curveto{-7.11319pt}{-3.92854pt}{-3.92854pt}{-7.11319pt}{0.0pt}{-7.11319pt}\pgfsys@curveto{3.92854pt}{-7.11319pt}{7.11319pt}{-3.92854pt}{7.11319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.9405pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}{}{{}}{}}{{{}}{{}}}{}{{}}{}{{}}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{-20.22981pt}{0.0pt}\pgfsys@lineto{-8.77318pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.77318pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.76282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{62.7686pt}{0.0pt}\pgfsys@curveto{62.7686pt}{5.59343pt}{58.23434pt}{10.12769pt}{52.64091pt}{10.12769pt}\pgfsys@curveto{47.04749pt}{10.12769pt}{42.51323pt}{5.59343pt}{42.51323pt}{0.0pt}\pgfsys@curveto{42.51323pt}{-5.59343pt}{47.04749pt}{-10.12769pt}{52.64091pt}{-10.12769pt}\pgfsys@curveto{58.23434pt}{-10.12769pt}{62.7686pt}{-5.59343pt}{62.7686pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{52.64091pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{45.12262pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{118.42401pt}{0.0pt}\pgfsys@curveto{118.42401pt}{5.59343pt}{113.88976pt}{10.12769pt}{108.29633pt}{10.12769pt}\pgfsys@curveto{102.7029pt}{10.12769pt}{98.16864pt}{5.59343pt}{98.16864pt}{0.0pt}\pgfsys@curveto{98.16864pt}{-5.59343pt}{102.7029pt}{-10.12769pt}{108.29633pt}{-10.12769pt}\pgfsys@curveto{113.88976pt}{-10.12769pt}{118.42401pt}{-5.59343pt}{118.42401pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{108.29633pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{100.77803pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.31319pt}{0.0pt}\pgfsys@lineto{40.85324pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.85324pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.75175pt}{5.47743pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.12155pt}{-10.47745pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{62.9686pt}{0.0pt}\pgfsys@lineto{96.50865pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{96.50865pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{72.82938pt}{5.9441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{73.19917pt}{-10.47743pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\longmapsto\leavevmode\hbox
to183.26pt{\vbox to31.98pt{\pgfpicture\makeatletter\hbox{\hskip
27.09583pt\lower-16.86601pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{7.11319pt}{0.0pt}\pgfsys@curveto{7.11319pt}{3.92854pt}{3.92854pt}{7.11319pt}{0.0pt}{7.11319pt}\pgfsys@curveto{-3.92854pt}{7.11319pt}{-7.11319pt}{3.92854pt}{-7.11319pt}{0.0pt}\pgfsys@curveto{-7.11319pt}{-3.92854pt}{-3.92854pt}{-7.11319pt}{0.0pt}{-7.11319pt}\pgfsys@curveto{3.92854pt}{-7.11319pt}{7.11319pt}{-3.92854pt}{7.11319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.9405pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}{}{{}}{}}{{{}}{{}}}{}{{}}{}{{}}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{-20.22981pt}{0.0pt}\pgfsys@lineto{-8.77318pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.77318pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.76282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{62.7686pt}{0.0pt}\pgfsys@curveto{62.7686pt}{5.59343pt}{58.23434pt}{10.12769pt}{52.64091pt}{10.12769pt}\pgfsys@curveto{47.04749pt}{10.12769pt}{42.51323pt}{5.59343pt}{42.51323pt}{0.0pt}\pgfsys@curveto{42.51323pt}{-5.59343pt}{47.04749pt}{-10.12769pt}{52.64091pt}{-10.12769pt}\pgfsys@curveto{58.23434pt}{-10.12769pt}{62.7686pt}{-5.59343pt}{62.7686pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{52.64091pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{45.12262pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{155.96918pt}{0.0pt}\pgfsys@curveto{155.96918pt}{5.59343pt}{151.43492pt}{10.12769pt}{145.84149pt}{10.12769pt}\pgfsys@curveto{140.24806pt}{10.12769pt}{135.7138pt}{5.59343pt}{135.7138pt}{0.0pt}\pgfsys@curveto{135.7138pt}{-5.59343pt}{140.24806pt}{-10.12769pt}{145.84149pt}{-10.12769pt}\pgfsys@curveto{151.43492pt}{-10.12769pt}{155.96918pt}{-5.59343pt}{155.96918pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{145.84149pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{138.3232pt}{-0.94722pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$r_{k+2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.31319pt}{0.0pt}\pgfsys@lineto{40.85324pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{40.85324pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.3132pt}{3.533pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$0$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.12155pt}{-10.47745pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{62.9686pt}{0.0pt}\pgfsys@lineto{134.05382pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{134.05382pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{82.54053pt}{5.9441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{k}+p_{k+1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{66.0242pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\max(b_{k},b_{k+1}-p_{k})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

Informally, any run through the original RTEA can be copied to the other and
vice versa, hence also this transformation does not change the values of $f$.
The precise argument is as follows.

Let $f^{\prime}$ denote the function which results from the transformation.
Let $x\in L$ and $t\in[0,\infty]$. The inequality $f(x,t)\leq f^{\prime}(x,t)$
is again clear if $f(x,t)=\bot$, so assume otherwise. Let
$t_{1}+\dotsm+t_{n}=t$ such that
$f(x,t)=x+r_{1}t_{1}+p_{1}+\dotsm+r_{n}t_{n}+p_{n}$ and
$x+\dotsm+r_{j}t_{j}\geq b_{j}$ for all $j=1,\dotsc,n$. Then this also yields
an accepting run through the RTEA for $f^{\prime}$, hence $f^{\prime}(x,t)\geq
f(x,t)$. The proof that $f(x,t)\geq f^{\prime}(x,t)$ is similar.

Next we define a total order on normal-form sequences of atomic RTEFs. Using
this ordering, we will later be able to show that the semiring of general
real-time energy functions is locally closed.

Let $f_{1},\dotsc,f_{n}$ and $f_{1}^{\prime},\dotsc,f_{n^{\prime}}^{\prime}$
be normal-form sequences of atomic RTEFs with rate sequences
$r_{1}<\dotsm<r_{n}$ and $r_{1}^{\prime}<\dotsm<r_{n^{\prime}}^{\prime}$,
respectively. Then $f_{1},\dotsc,f_{n}$ is _not better than_
$f_{1}^{\prime},\dotsc,f_{n^{\prime}}^{\prime}$, denoted
$(f_{1},\dotsc,f_{n})\preceq(f_{1}^{\prime},\dotsc,f_{n^{\prime}}^{\prime})$,
if $r_{n}\leq r_{n^{\prime}}^{\prime}$.

Note that
$(f_{1},\dotsc,f_{n})\preceq(f_{1}^{\prime},\dotsc,f_{n^{\prime}}^{\prime})$
does not imply
$f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}\leq
f_{1}^{\prime}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n^{\prime}}^{\prime}$
even for very simple functions. For a counterexample, consider the two
following linear RTEFs $f=f_{1}$,
$f^{\prime}=f_{1}^{\prime}\mathrel{\mathop{\triangleright}}f_{2}^{\prime}$
with corresponding RTEAs:

$\displaystyle f:$$4$$0$$0$$1$$5$$0$$1$$0$$2$

We have $(f_{1})\preceq(f_{1}^{\prime},f_{2}^{\prime})$, and for $x\geq 2$,
$f(x,t)=x+4t$ and $f^{\prime}(x,t)=x+5t$, hence $f(x,t)\leq f^{\prime}(x,t)$.
But $f(0,1)=4$, whereas $f^{\prime}(0,1)=\bot$.

######  Lemma 7.

If
$f=f_{1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n}$
and
$f^{\prime}=f_{1}^{\prime}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n^{\prime}}^{\prime}$
are such that
$(f_{1},\dotsc,f_{n})\preceq(f_{1}^{\prime},\dotsc,f_{n^{\prime}}^{\prime})$,
then $f^{\prime}\mathrel{\mathop{\triangleright}}f\leq f^{\prime}$.

######  Proof 4.3.

Let $r_{1}<\dotsm<r_{n}$ and $r_{1}^{\prime}<\dotsm<r_{n^{\prime}}^{\prime}$
be the corresponding rate sequences, then $r_{n}\leq r_{n^{\prime}}^{\prime}$.
The RTEAs for $f^{\prime}\mathrel{\mathop{\triangleright}}f$ and $f^{\prime}$
are as follows, where we have transformed the former to normal form using that
for all indices $i$, $r_{i}\leq r_{n}\leq r_{n^{\prime}}^{\prime}$:

$f^{\prime}\mathrel{\mathop{\triangleright}}f:$$r_{1}^{\prime}$$\cdots$$r_{n^{\prime}}^{\prime}$$b_{1}^{\prime}$$0$$\max(b_{n^{\prime}}^{\prime},b_{n}-p^{\prime})$$p+p^{\prime}$$f^{\prime}:$$r_{1}^{\prime}$$\cdots$$r_{n^{\prime}}^{\prime}$$b_{1}^{\prime}$$0$$b_{n^{\prime}}^{\prime}$$p^{\prime}$

As $p+p^{\prime}\leq p^{\prime}$ (because $p\leq 0$) and
$\max(b_{n^{\prime}}^{\prime},b_{n}-p^{\prime})\geq b_{n^{\prime}}^{\prime}$,
it is clear that $f^{\prime}\mathrel{\mathop{\triangleright}}f(x,t)\leq
f^{\prime}(x,t)$ for all $x\in L$, $t\in[0,\infty]$.

###  4.3. General Real-Time Energy Functions

We now consider all paths that may arise in a real-time energy automaton. When
two locations of an automaton may be joined by two distinct paths, the optimal
output energy is naturally obtained by taking the maximum over both paths.
This gives rise to the following definition.

Let $f,g\in\mathcal{F}$. The function $f\vee g$ is defined as the pointwise
supremum:

$\forall t\in[0,\infty]:(f\vee g)(t)=f(t)\vee g(t)$

######  Lemma 8.

With operations $\vee$ and $\mathrel{\mathop{\triangleright}}$, $\mathcal{F}$
forms a complete lattice and an idempotent semiring, with $\bot$ as unit for
$\vee$ and $\mathbf{1}$ as unit for $\mathrel{\mathop{\triangleright}}$.

######  Proof 4.4.

To show completeness, we note that for $\mathcal{X}\subseteq\mathcal{F}$,
$\bigvee\mathcal{X}$ is the function defined by
$(\bigvee\mathcal{X})(x,t)=\bigvee\\{f(x,t)\mid f\in\mathcal{X}\\}$, which is
monotonic and hence an element of $\mathcal{F}$.

For the semiring axioms, we only miss to show the distributive laws. Let
$f,g,h\in\mathcal{F}$ and $t\in[0,\infty]$, then

$\displaystyle(f\mathrel{\mathop{\triangleright}}(g\vee h))(t)$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}(g\vee h)(t_{2})\circ f(t_{1})$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}(g(t_{2})\vee h(t_{2}))\circ f(t_{1})$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}g(t_{2})\circ f(t_{1})\vee h(t_{2})\circ
f(t_{1})$ $\displaystyle=\bigvee_{t_{1}+t_{2}=t}g(t_{2})\circ
f(t_{1})\vee\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ f(t_{1})$
$\displaystyle=f\mathrel{\mathop{\triangleright}}g(t)\vee
f\mathrel{\mathop{\triangleright}}h(t)=(f\mathrel{\mathop{\triangleright}}g\vee
f\mathrel{\mathop{\triangleright}}h)(t)\,.$

Similarly, and using monotonicity of $h$, we see that

$\displaystyle((f\vee g)\mathrel{\mathop{\triangleright}}h)(t)$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ(f\vee g)(t_{1})$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ(f(t_{1})\vee g(t_{1}))$
$\displaystyle=\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ f(t_{1})\vee h(t_{2})\circ
g(t_{1})$ $\displaystyle=\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ
f(t_{1})\vee\bigvee_{t_{1}+t_{2}=t}h(t_{2})\circ g(t_{1})$
$\displaystyle=f\mathrel{\mathop{\triangleright}}h(t)\vee
g\mathrel{\mathop{\triangleright}}h(t)=(f\mathrel{\mathop{\triangleright}}h\vee
g\mathrel{\mathop{\triangleright}}h)(t)\,.$

The proof is complete.

Finally, a cycle in an RTEA results in a ∗-operation:

Let $f\in\mathcal{F}$. The Kleene star of $f$ is the function
$f^{*}\in\mathcal{F}$ such that

$\forall t\in[0,\infty]:f^{*}(t)=\bigvee_{n\geq 0}f^{n}(t)$

Note that $f^{*}$ is defined for all $f\in\mathcal{F}$ because $\mathcal{F}$
is a complete lattice. We can now define the set of general real-time energy
functions, corresponding to general RTEAs:

The set $\mathcal{E}$ of _real-time energy functions_ is the subsemiring of
$\mathcal{F}$ generated by $\mathcal{A}$, i.e., the subset of $\mathcal{F}$
inductively defined by

  * •

$\mathcal{A}\subseteq\mathcal{E}$,

  * •

if $f,g\in\mathcal{E}$, then
$f\mathrel{\mathop{\triangleright}}g\in\mathcal{E}$ and $f\vee
g\in\mathcal{E}$.

We will show below that $\mathcal{E}$ is locally closed, which entails that
for each $f\in\mathcal{E}$, also $f^{*}\in\mathcal{E}$, hence $\mathcal{E}$
indeed encompasses all RTEFs.

######  Lemma 9.

For every $f\in\mathcal{E}$ there exists $N\geq 0$ so that
$f^{*}=\bigvee_{n=0}^{N}f^{n}$.

######  Proof 4.5.

By distributivity, we can write $f$ as a finite supremum
$f=\bigvee_{k=1}^{m}f_{k}$ of linear energy functions $f_{1},\dotsc,f_{m}$.
For each $k=1,\dotsc,m$, let
$f_{k}=f_{k,1}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{k,n_{k}}$
be a normal-form representation. By re-ordering the $f_{k}$ if necessary, we
can assume that
$(f_{k,1},\dotsc,f_{k,n_{k}})\preceq(f_{k+1,1},\dotsc,f_{k+1,n_{k+1}})$ for
every $k=1,\dotsc,n-1$.

We first show that $f^{*}\leq\bigvee_{0\leq n_{1},\dotsc,n_{m}\leq
1}f_{1}^{n_{1}}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{m}^{n_{m}}$:
The expansion of $f^{*}=(\bigvee_{k=1}^{m}f_{k})^{*}$ is an infinite supremum
of finite compositions
$f_{i_{1}}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{i_{p}}$.
By Lemma 7, any occurrence of
$f_{i_{j}}\mathrel{\mathop{\triangleright}}f_{i_{j+1}}$ in such compositions
with $i_{j}\geq i_{j+1}$ can be replaced by $f_{i_{j+1}}$. The compositions
which are left have $i_{j}<i_{j+1}$ for every $j$, so the claim follows.

Now $\bigvee_{0\leq n_{1},\dotsc,n_{m}\leq
1}f_{1}^{n_{1}}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{m}^{n_{m}}\leq\bigvee_{n=0}^{m}\big{(}\bigvee_{k=1}^{m}f_{k}\big{)}^{n}=\bigvee_{n=0}^{m}f^{n}\leq
f^{*}$, so with $N=m$ the proof is complete.

######  Corollary 10.

$\mathcal{E}$ is locally closed, hence a ∗-continuous Kleene algebra.

######  Proof 4.6.

For every $f\in\mathcal{E}$ there is $N\geq 0$ so that
$f^{*}=\bigvee_{n=0}^{N}f^{n}$ (Lemma 9), hence
$\bigvee_{n=0}^{N}f^{n}=\bigvee_{n=0}^{N+1}f^{n}$. Thus $\mathcal{E}$ is
locally closed, and by Lemma 4, a ∗-continuous Kleene algebra.

To illustrate, we compute the Kleene star of the supremum $f=f_{1}\vee f_{2}$
of two linear RTEFs as below. These are slight modifications of some RTEFs
from the satellite example, modified to make the example more interesting:

$f_{1}$$f_{2}$$0$$4$$1$$5$$0$$30$$-10$$30$$0$$20$$0$$40$$-50$$50$

These functions are in normal form and $f_{1}\preceq f_{2}$. Lemma 9 and its
proof allow us to conclude that $f^{*}=\mathbf{1}\vee f_{1}\vee f_{2}\vee
f_{1}\mathrel{\mathop{\triangleright}}f_{2}$. Figure 4 shows the boundaries of
definition of these functions and the regions in the $(x,t)$ plane where each
of them dominates the supremum.

$x$0$20$$30$$37$$40$$50$$60$$t$$2$$7$$22$$40$$53$$55$$80$$f_{1}(x,t)=4t+x-10$$f_{2}(x,t)=5t+5x-210$$f_{2}(x,t)=5t+x-50$$f_{1}\mathrel{\mathop{\triangleright}}f_{2}(x,t)=5t+1.25x-72.5$$f_{1}\mathrel{\mathop{\triangleright}}f_{2}(x,t)=5t+x-60$$f^{*}=\mathbf{1}$$f^{*}=f_{2}$$f^{*}=f_{1}$$f^{*}=f_{1}\mathrel{\mathop{\triangleright}}f_{2}$
Figure 4.  Computation of $f^{*}$ from Example 4.3.

###  4.4. Infinite Products

Let $\mathbbm{B}=\\{\textup{{ff}},\textup{{t\\!t}}\\}$ denote the Boolean
lattice with standard order $\textup{{ff}}<\textup{{t\\!t}}$. Let
$\mathcal{V}$ denote the set of monotonic functions
$v:L\times[0,\infty]\to\mathbbm{B}$ for which $v(\bot,t)=\bot$ for all $t\in
L$. We define an infinite product operation
$\mathcal{F}^{\omega}\to\mathcal{V}$:

For an infinite sequence of functions $f_{0},f_{1},\dotsc\in\mathcal{F}$,
$\prod_{n\geq 0}f_{n}\in\mathcal{V}$ is the function defined for $x\in L$,
$t\in[0,\infty]$ by $\prod_{n\geq 0}f_{n}(x,t)=\textup{{t\\!t}}$ iff there is
an infinite sequence $t_{0},t_{1},\dotsc\in[0,\infty]$ such that
$\sum_{n=0}^{\infty}t_{n}=t$ and for all $n\geq 0$,
$f_{n}(t_{n})\circ\dotsm\circ f_{0}(t_{0})(x)\neq\bot$.

Hence $\prod_{n\geq 0}f_{n}(x,t)=\textup{{t\\!t}}$ iff in the infinite
composition
$f_{0}\mathrel{\mathop{\triangleright}}f_{1}\mathrel{\mathop{\triangleright}}\dotsm(x,t)$,
all finite prefixes have values $\neq\bot$. There is a (left) action of
$\mathcal{F}$ on $\mathcal{V}$ given by $(f,v)\mapsto
f\mathrel{\mathop{\triangleright}}v$, where the composition
$f\mathrel{\mathop{\triangleright}}v$ is given by the same formula as
composition $\mathrel{\mathop{\triangleright}}$ on $\mathcal{F}$. Let
$\bot\in\mathcal{V}$ denote the function given by $\bot(x,t)=\textup{{ff}}$.

######  Lemma 11.

With the $\mathcal{F}$-action $\mathrel{\mathop{\triangleright}}$, $\vee$ as
addition, and $\bot$ as unit, $\mathcal{V}$ is an idempotent left
$\mathcal{F}$-semimodule.

######  Proof 4.7.

Similar to the proofs of Lemmas 5 and 8.

Let $\mathcal{U}\subseteq\mathcal{V}$ be the $\mathcal{F}$-subsemimodule
generated by $\mathcal{E}\subseteq\mathcal{F}$. Then $\mathcal{U}$ is an
idempotent left $\mathcal{E}$-semimodule.

######  Proposition 12.

$(\mathcal{E},\mathcal{U})$ forms a ∗-continuous Kleene $\omega$-algebra.

######  Proof 4.8.

We first show that $(\mathcal{E},\mathcal{U})$ forms a generalized
∗-continuous Kleene algebra: Let $f,g\in\mathcal{E}$ and $v\in\mathcal{U}$,
then we need to see that
$f\mathrel{\mathop{\triangleright}}g^{*}\mathrel{\mathop{\triangleright}}v=\bigvee_{n\geq
0}f\mathrel{\mathop{\triangleright}}g^{n}\mathrel{\mathop{\triangleright}}v$.
The right-hand side is trivially less than or equal to the left-hand side. For
the other inequality, as $g$ is ∗-closed, we have $N\geq 0$ such that
$g^{*}=\bigvee_{n=0}^{N}g^{n}$, and then

$f\mathrel{\mathop{\triangleright}}g^{*}\mathrel{\mathop{\triangleright}}v=f\mathrel{\mathop{\triangleright}}\big{(}\bigvee_{n=0}^{N}g^{n}\big{)}\mathrel{\mathop{\triangleright}}v=\bigvee_{n=0}^{N}f\mathrel{\mathop{\triangleright}}g^{n}\mathrel{\mathop{\triangleright}}v\leq\bigvee_{n\geq
0}f\mathrel{\mathop{\triangleright}}g^{n}\mathrel{\mathop{\triangleright}}v\,.$

We now need to show that $(\mathcal{E},\mathcal{U})$ satisfies the conditions
$(\textrm{{C}}1)$–$(\textrm{{C}}4)$ in Section 3.2. As to $(\textrm{{C}}1)$,
let $f_{0},f_{1},\dotsc\in\mathcal{E}$, $x\in L$, and $t\in[0,\infty]$. Then

$\displaystyle f_{0}\mathrel{\mathop{\triangleright}}\prod_{n\geq
0}f_{n+1}(x,t)$ $\displaystyle=\bigvee_{t_{0}+t^{\prime}=t}\prod_{n\geq
0}f_{n+1}(t^{\prime})\circ f_{0}(t_{0})(x)$
$\displaystyle=\textup{{t\\!t}}\text{ iff }\exists
t_{0}+t^{\prime}=t:\prod_{n\geq 0}f_{n+1}(t^{\prime})\circ
f_{0}(t_{0})(x)=\textup{{t\\!t}}$ $\displaystyle=\textup{{t\\!t}}\text{ iff
}\exists t_{0}+t^{\prime}=t:\exists t_{1}+t_{2}+\dotsm=t^{\prime}:\forall
n\geq 1:$ $\displaystyle\hskip 150.00023ptf_{n}(t_{n})\circ\dotsm\circ
f_{0}(t_{0})\neq\bot$ $\displaystyle=\prod_{n\geq 0}f_{n}(x,t)\,.$

For $(\textrm{{C}}2)$, let $f_{0},f_{1},\dotsc\in\mathcal{E}$, $x\in L$,
$t\in[0,\infty]$, and $0=n_{0}\leq n_{1}\leq\dotsm$ a sequence which increases
without a bound. Then

$\displaystyle\smash[b]{\prod_{k\geq
0}(f_{n_{k}}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n_{k+1}-1})(x,t)}=\textup{{t\\!t}}$
$\displaystyle\qquad\qquad\text{iff }\exists u_{0}+u_{1}+\dotsm=t:\forall
k\geq 0:$ $\displaystyle\hskip
100.00015pt(f_{n_{k}}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n_{k+1}-1})(u_{k})\circ\dotsm\circ(f_{0}\mathrel{\mathop{\triangleright}}\dotsm\mathrel{\mathop{\triangleright}}f_{n_{1}-1})(u_{0})(x)\neq\bot$
$\displaystyle\qquad\qquad\text{iff }\exists u_{0}+u_{1}+\dotsm=t:\forall
k\geq 0:\exists t^{k}_{0},\dotsc,t^{k}_{n_{k+1}-1}:$ $\displaystyle\hskip
100.00015ptt^{k}_{0}+\dotsm+t^{k}_{n_{1}-1}=u_{0},\dotsc,t^{k}_{n_{k}}+\dotsm+t^{k}_{n_{k+1}-1}=u_{k},$
$\displaystyle\hskip
100.00015ptf_{n_{k+1}-1}(t^{k}_{n_{k+1}-1})\circ\dotsm\circ
f_{0}(t^{k}_{0})\neq\bot\,.$

We can use a diagonal-type argument to finish the proof: For every $k$, we
have $t^{k+1}_{0},\dotsc,t^{k+1}_{n_{k+2}-1}$ such that
$f_{n_{k+2}-1}(t^{k+1}_{n_{k+2}-1})\circ\dotsm\circ
f_{0}(t^{k+1}_{0})\neq\bot$. But then also
$f_{n_{k+1}-1}(t^{k+1}_{n_{k+1}-1})\circ\dotsm\circ
f_{0}(t^{k+1}_{0})\neq\bot$, hence we can update
$t^{k}_{0}:=t^{k+1}_{0},\dotsc,t^{k}_{n_{k+1}-1}:=t^{k+1}_{n_{k+1}-1}$. In the
limit, we have $t_{0},t_{1},\dotsc$ with
$t_{0}+\dotsm+t_{n_{1}-1}=u_{0},\dotsc$, hence $t_{0}+t_{1}+\dotsm=t$, and
$f_{n}(t_{n})\circ\dotsm\circ f_{0}(t_{0})=\bot$.

To show the third condition, we prove that for all
$f_{0},f_{1},\dotsc,g_{0},g_{1},\dotsc\in\mathcal{E}$,

$\prod_{n\geq 0}(f_{n}\vee
g_{n})=\adjustlimits{\bigvee}_{h_{n}\in\\{f_{n},g_{n}\\}\;}{\prod}_{n\geq
0}h_{n}\,,$ (5)

which implies $(\textrm{{C}}3)$. By monotonicity of infinite product, the
right-hand side is less than or equal to the left-hand side. To show the other
inequality, let $x\in L$ and $t\in[0,\infty]$ and suppose that $\prod_{n\geq
0}(f_{n}\vee g_{n})(x,t)=\textup{{t\\!t}}$. We show that there is a choice of
functions $h_{n}\in\\{f_{n},g_{n}\\}$ for all $n\geq 0$ such that
$\prod_{n\geq 0}h_{n}(x,t)=\textup{{t\\!t}}$.

Consider the infinite ordered binary tree where each node at level $n\geq 0$
is the source of an edge labeled $f_{n}$ and an edge labeled $g_{n}$, ordered
as indicated. We can assign to each node $u$ the composition $h_{u}$ of the
functions that occur as the labels of the edges along the unique path from the
root to that node.

Let us mark a node $u$ if $h_{u}(x,t)\neq\bot$. As $\prod_{n\geq 0}(f_{n}\vee
g_{n})(x,t)=\textup{{t\\!t}}$, each level contains a marked node. Moreover,
whenever a node is marked and has a predecessor, its predecessor is also
marked. By König’s lemma [Kön27] there is an infinite path going through
marked nodes. This infinite path gives rise to the sequence
$h_{0},h_{1},\dotsc$ with $\prod_{n\geq 0}h_{n}(x,t)=\textup{{t\\!t}}$.

For $(\textrm{{C}}4)$, we need to see that for all
$f,g_{0},g_{1},\dotsc\in\mathcal{E}$,

$\prod_{n\geq
0}f^{*}\mathrel{\mathop{\triangleright}}g_{n}=\adjustlimits{\bigvee}_{k_{0},k_{1},\dotsc\geq
0\;}{\prod}_{n\geq 0}f^{k_{n}}\mathrel{\mathop{\triangleright}}g_{n}\,.$

Again the right-hand side is less than or equal to the left-hand side because
of monotonicity of infinite product. To show the other inequality, we have
$N\geq 0$ such that $f^{*}=\bigvee_{k=0}^{N}f^{k}$, and then

$\displaystyle\prod_{n\geq 0}f^{*}\mathrel{\mathop{\triangleright}}g_{n}$
$\displaystyle=\prod_{n\geq
0}\big{(}\bigvee_{k=0}^{N}f^{k}\big{)}\mathrel{\mathop{\triangleright}}g_{n}$
$\displaystyle=\prod_{n\geq
0}\big{(}\bigvee_{k=0}^{N}f^{k}\mathrel{\mathop{\triangleright}}g_{n}\big{)}$
$\displaystyle=\adjustlimits{\bigvee}_{0\leq k_{0},k_{1},\dotsc\leq
N\;}{\prod}_{n\geq 0}f^{k_{n}}\mathrel{\mathop{\triangleright}}g_{n}$ (6)
$\displaystyle\leq\adjustlimits{\bigvee}_{k_{0},k_{1},\dotsc\geq
0\;}{\prod}_{n\geq 0}f^{k_{n}}\mathrel{\mathop{\triangleright}}g_{n}\,,$

where (6) holds because of (5).

##  5\. Decidability

We can now apply the results of Section 3.4 to see that our decision problems
as stated at the end of Section 2 are decidable. Let Let $A=(S,s_{0},F,T,r)$
be an RTEA, with matrix representation $(\alpha,M,K)$, and
$x_{0},t,y\in[0,\infty]$.

######  Theorem 13.

There exists a finite run
$(s_{0},x_{0},t)\leadsto\dotsm\leadsto(s,x,t^{\prime})$ in $A$ with $s\in F$
iff $|A|(x_{0},t)>\bot$.

######  Theorem 14.

There exists a finite run
$(s_{0},x_{0},t)\leadsto\dotsm\leadsto(s,x,t^{\prime})$ in $A$ with $s\in F$
and $x\geq y$ iff $|A|(x_{0},t)\geq y$.

######  Theorem 15.

There exists $s\in F$ and an infinite run
$(s_{0},x_{0},t)\leadsto(s_{1},x_{1},t_{1})\leadsto\dotsm$ in $A$ in which
$s_{n}=s$ for infinitely many $n\geq 0$ iff $\|A\|(x_{0},t)=\top$.

######  Theorem 16.

Problems 1, 2 and 3 from Section 2 are decidable.

######  Proof 5.1.

We have seen in the examples that RTEFs are _piecewise linear_ , i.e.,
composed of a finite number of (affine) linear functions which are defined on
polygonal regions in the $(x,t)$-plane. It is clear that this is generally the
case: atomic RTEFs are piecewise linear by definition, and compositions and
maxima of piecewise linear functions are again piecewise linear.

Piecewise linear functions can be represented using the (finitely many) corner
points of their regions of definition together with their values at these
corner points. (In case some regions are not convex or disconnected, they can
be split into finitely many convex regions.)

It is clear that computable atomic RTEFs are computable piecewise linear
(i.e., all numbers in their finite representation are computable), and that
compositions and suprema of computable piecewise linear are again computable
piecewise linear. Using Lemma 9, we see that all functions in $M^{*}$ are
computable piecewise linear.

We miss to show that the ω-operation is computable. Let $f$ be a computable
RTEF. If $f=\bot$, then $f^{\omega}=\bot$, so we can assume $f\neq\bot$. Then
$f$ can be expressed as a finite supremum of linear (computable) RTEFs in
normal form; let $A$ be the corresponding RTEA. Let $x\in L$ and
$t\in[0,\infty]$. If $x=\bot$, then $f^{\omega}(x,t)=\textup{{ff}}$; if
$x=\infty$, then $f^{\omega}(x,t)=\textup{{t\\!t}}$. We can hence assume
$x\in\mathbbm{R}_{\geq 0}$.

We prove the claim for $t\neq\infty$ first. In that case,
$f^{\omega}(x,t)=\textup{{t\\!t}}$ iff there is an infinite sequence
$t_{0},t_{1},\dotsc\in\mathbbm{R}_{\geq 0}$ whose partial sums converge to
$t$: $\sum_{n=0}^{\infty}t_{n}=t$, and such that for all $n\geq 0$,
$f(t_{n})\circ\dotsm\circ f(t_{0})(x)\neq\bot$. By convergence, we have
$\lim_{n\to\infty}t_{n}=0$.

For $y,u\in\mathbbm{R}_{\geq 0}$, $f(y,u)=a(y,u)u+b(y,u)y+p(y,u)$ for
piecewise constant functions $a(y,u)$, $b(y,u)$, $p(y,u)$. Let
$\alpha=\sup\\{p(y,u)\mid y,u\in\mathbbm{R}_{\geq 0}\\}$, then $\alpha\leq 0$,
and $\alpha<0$ iff the prices along all paths through $A$ are non-zero. We
have $\lim_{u\to 0}f(y,u)=b(y,0)y+p(y,0)$. But $b(y,0)=1$ (if no time is
available, we cannot delay in any states), hence $\lim_{u\to
0}f(y,u)=y+p(y,0)$ for all $y\in\mathbbm{R}_{\geq 0}$. By
$\lim_{n\to\infty}t_{n}=0$, this implies that if $\alpha<0$, then there is
$n\geq 0$ such that $f(t_{n})\circ\dotsm\circ f(t_{0})(x)=\bot$. If $\alpha=0$
on the other hand, then we can choose $t_{0}=t$ and $t_{n}=0$ for $n\geq 1$.
We have shown that $f^{\omega}(x,t)=\textup{{t\\!t}}$ iff there is a path
through $A$ with price $0$, which is decidable.

Now we show the claim for $t=\infty$. If there is $t_{0}\in[0,\infty]$ for
which $f(x,t_{0})\geq x$, then we can assume $t_{0}>0$ and put $t_{n}=t_{0}$
for all $n$ to show that $f^{\omega}(x,t)=\textup{{t\\!t}}$.

We now show that if $f(x,t_{0})<x$ for all $t_{0}\in[0,\infty]$, then
$f^{\omega}(x,t)=\textup{{ff}}$. Let $\alpha=\sup\\{f(x,t_{0})-x\mid
t_{0}\in[0,\infty]\\}$, then $\alpha<0$ as $[0,\infty]$ is compact. We have
$f(x,t_{0})\leq x+\alpha$ for all $t_{0}\in[0,\infty]$. Now entering the RTEA
$A$ for $f$ with initial energy lower than $x$ can disable some paths, but
will not enable any new behavior, hence for $x^{\prime}\leq x$ and any
$t_{1}\in[0,\infty]$, $f(x^{\prime},t_{1})\leq f(x,t_{1})+x^{\prime}-x$. Hence
$f(t_{1})\circ f(t_{0})(x)\leq f(x,t_{1})+f(x,t_{0})-x\leq
f(x,t_{1})+\alpha\leq x+2\alpha$ for all $t_{0},t_{1}\in[0,\infty]$. By
induction, we see that for all infinite sequences
$t_{0},t_{1},\dotsc\in[0,\infty]$ and all $n\geq 0$, $f(t_{n})\circ\dotsm\circ
f(t_{0})(x)\leq x+n\alpha$. By $\alpha<0$, $f^{\omega}(x,t)=\textup{{ff}}$. We
have shown that $f^{\omega}(x,t)=\textup{{t\\!t}}$ iff there exists
$t_{0}\in[0,\infty]$ with $f(x,t_{0})\geq x$, which is decidable because $f$
is piecewise linear.

##  6\. Conclusion

We have developed an algebraic methodology for deciding reachability and Büchi
problems on a class of weighted real-time models where the weights represent
energy or similar quantities. The semantics of such systems is modeled by
real-time energy functions which map initial energy of the system and
available time to the maximal final energy level. We have shown that these
real-time energy functions form a ∗-continuous Kleene $\omega$-algebra, which
entails that reachability and Büchi acceptance can be decided in a static way
which only involves manipulations of energy functions.

We have seen that the necessary manipulations of real-time energy functions
are computable, and in fact we conjecture that our method leads to an
exponential-time algorithm for deciding reachability and Büchi acceptance in
real-time energy automata. This is due to the fact that operations on real-
time energy functions can be done in time linear in the size of their
representation, and the representation size of compositions and suprema of
real-time energy functions is a linear function of the representation size of
the operands. In future work, we plan to do a careful complexity analysis
which could confirm this result and to implement our algorithms to see how it
fares in practice.

This paper constitutes the first application of methods from Kleene algebra to
a timed-automata like formalism. In future work, we plan to lift some of the
restrictions of the current model and extend it to allow for time constraints
and resets à la timed automata. We also plan to extend this work with action
labels, which algebraically means passing from the semiring of real-time
energy functions to the one of formal power series over these functions. In
applications, this means that instead of asking for existence of accepting
runs, one is asking for controllability.

## References

  * [ATP01] Rajeev Alur, Salvatore La Torre, and George J. Pappas.  Optimal paths in weighted timed automata.  In Di Benedetto and Sangiovanni-Vincentelli [DBSV01], pages 49–62.
  * [BÉ93] Stephen L. Bloom and Zoltán Ésik.  Iteration Theories: The Equational Logic of Iterative Processes.  EATCS monographs on theoretical computer science. Springer-Verlag, 1993\.
  * [BFH+01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager.  Minimum-cost reachability for priced timed automata.  In Di Benedetto and Sangiovanni-Vincentelli [DBSV01], pages 147–161.
  * [BFL+08] Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba.  Infinite runs in weighted timed automata with energy constraints.  In Franck Cassez and Claude Jard, editors, FORMATS, volume 5215 of Lect. Notes Comput. Sci., pages 33–47. Springer-Verlag, 2008.
  * [BFLM10] Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey.  Timed automata with observers under energy constraints.  In Karl Henrik Johansson and Wang Yi, editors, HSCC, pages 61–70. ACM, 2010.
  * [BLM14] Patricia Bouyer, Kim G. Larsen, and Nicolas Markey.  Lower-bound-constrained runs in weighted timed automata.  Perform. Eval., 73:91–109, 2014.
  * [CFL15] David Cachera, Uli Fahrenberg, and Axel Legay.  An omega-algebra for real-time energy problems.  In Prahladh Harsha and G. Ramalingam, editors, FSTTCS, volume 45 of Leibniz Int. Proc. Inf., pages 394–407. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [DBSV01] Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli, editors.  Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings, volume 2034 of Lect. Notes Comput. Sci. Springer-Verlag, 2001.
  * [DHMS12] Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, and Kim Solin.  Towards an algebra for real-time programs.  In Wolfram Kahl and Timothy G. Griffin, editors, RAMiCS, volume 7560 of Lect. Notes Comput. Sci., pages 50–65. Springer-Verlag, 2012\.
  * [DKV09] Manfred Droste, Werner Kuich, and Heiko Vogler, editors.  Handbook of Weighted Automata.  EATCS Monographs in Theoretical Computer Science. Springer-Verlag, 2009\.
  * [ÉFL15a] Zoltán Ésik, Uli Fahrenberg, and Axel Legay.  Star-continuous Kleene omega-algebras.  In Igor Potapov, editor, DLT, volume 9168 of Lect. Notes Comput. Sci., pages 240–251. Springer-Verlag, 2015.
  * [ÉFL15b] Zoltán Ésik, Uli Fahrenberg, and Axel Legay.  ∗-continuous Kleene $\omega$-algebras for energy problems.  In Ralph Matthes and Matteo Mio, editors, FICS, volume 191 of Electr. Proc. Theor. Comput. Sci., pages 48–59, 2015.
  * [ÉFLQ13] Zoltán Ésik, Uli Fahrenberg, Axel Legay, and Karin Quaas.  Kleene algebras and semimodules for energy problems.  In Dang Van Hung and Mizuhito Ogawa, editors, ATVA, volume 8172 of Lect. Notes Comput. Sci., pages 102–117. Springer-Verlag, 2013.
  * [ÉK02] Zoltán Ésik and Werner Kuich.  Locally closed semirings.  Monatsh. Math., 137(1):21–29, 2002.
  * [ÉK07a] Zoltán Ésik and Werner Kuich.  Modern Automata Theory.  2007\.  http://dmg.tuwien.ac.at/kuich/mat.pdf.
  * [ÉK07b] Zoltán Ésik and Werner Kuich.  On iteration semiring-semimodule pairs.  Semigroup Forum, 75:129–159, 2007.
  * [FJLS11] Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jiří Srba.  Energy games in multiweighted automata.  In Antonio Cerone and Pekka Pihlajasaari, editors, ICTAC, volume 6916 of Lect. Notes Comput. Sci., pages 95–115. Springer-Verlag, 2011.
  * [Gol99] Jonathan S. Golan.  Semirings and their Applications.  Springer-Verlag, 1999.
  * [HM09] Peter Höfner and Bernhard Möller.  An algebra of hybrid systems.  J. Log. Alg. Prog., 78(2):74–97, 2009.
  * [Kön27] Dénes König.  Über eine Schlussweise aus dem Endlichen ins Unendliche.  Acta Sci. Math. (Szeged), 3(2-3):121–130, 1927.
  * [Koz90] Dexter Kozen.  On Kleene algebras and closed semirings.  In Branislav Rovan, editor, MFCS, volume 452 of Lect. Notes Comput. Sci., pages 26–47. Springer-Verlag, 1990.
  * [Koz94] Dexter Kozen.  A completeness theorem for Kleene algebras and the algebra of regular events.  Inf. Comput., 110(2):366–390, 1994.
  * [Qua11] Karin Quaas.  On the interval-bound problem for weighted timed automata.  In Adrian Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, LATA, volume 6638 of Lect. Notes Comput. Sci., pages 452–464. Springer-Verlag, 2011.