\section{Introduction}

\emph{Energy} and \emph{resource management} problems are important in
areas such as embedded systems or autonomous systems.  They are
concerned with the question whether a given system admits infinite
schedules during which (1) certain tasks can be repeatedly accomplished
and (2) the system never runs out of energy (or other specified
resources).  Starting with~\cite{DBLP:conf/formats/BouyerFLMS08}, formal
modeling and analysis of such problems has recently attracted some
attention~\cite{conf/ictac/FahrenbergJLS11, DBLP:conf/lata/Quaas11,
  DBLP:conf/icalp/ChatterjeeD10, DBLP:conf/hybrid/BouyerFLM10,
  DBLP:conf/qest/BouyerLM12, DBLP:conf/csl/DegorreDGRT10}.

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.0cm,initial text=,scale=.9]
    \tikzstyle{every node}=[font=\small]
    \tikzstyle{every state}=[inner sep=.5mm,minimum size=2.2mm,outer
    sep=.8mm]
    \begin{scope}[xscale=.9]
      \node[state with output,initial,accepting] (W) at (0,0) {$W$
        \nodepart{lower} $\!-10$};
      \node[state with output] (R1) at (6,1) {$R_1$ \nodepart{lower}
        $\!+20$};
      \node[state with output] (R2) at (6,-1) {$R_2$ \nodepart{lower}
        $\!+10$};
      \path (W) edge [bend left] node [below] {$-4$} node
      [above,pos=.2] {$c\ge 1\,\,\,\,\,\,\,\,$} node [above,pos=.8]
      {$c\leftarrow 0$} (R1);
      \path (R1) edge node [below,pos=.4] {$-4$} node
      [above,pos=.3] {$c\le 1$} node [above,pos=.7] {$c\leftarrow 0$}
      (W);
      \path (W) edge [bend right] node [above] {$-2$} node
      [below,pos=.2] {$c\ge 1\,\,\,\,\,\,\,\,$} node [below,pos=.8]
      {$c\leftarrow 0$} (R2);
      \path (R2) edge node [above,pos=.4] {$-2$} node
      [below,pos=.3] {$c\le 1$} node [below,pos=.7] {$c\leftarrow 0$}
      (W);
      \path (R2) edge [bend left] node [left] {$-2$} (R1);
      \path (R1) edge [bend left] node [right] {$-2$} (R2);
    \end{scope}
    \begin{scope}[xshift=8.3cm,scale=.9]
      \node[state,initial,accepting] (W) at (0,0) {$W$};
      \node[state] (R) at (3,0) {$R$};
      \path (W) edge [bend left] node [below] {$f_\textit{WR}$} (R);
      \path (R) edge [bend left] node [above] {$f_\textit{RW}$} (W);
      \path (R) edge [out=-20,in=20,loop] node [below,pos=.3] {$x\mapsto
        \infty$} (R);
      \node at (1.5,1.5) {%
        $f_\textit{WR}( x) =
        \begin{cases}
          \text{undef.} & ( x< 12) \\
          x- 12 & ( x\ge 12)
        \end{cases}$};
      \node at (1.5,-1.5) {%
        $f_\textit{RW}( x) =
        \begin{cases}
          2 x+ 12 & ( x< 2) \\
          x+ 14 & ( x\ge 2)
        \end{cases}$};
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:example}
    Simple model of an electric car as a weighted timed automaton (left);
    the corresponding energy automaton (right)}
\end{figure}

As an example, the left part of Fig.~\ref{fi:example} shows a simple
model of an electric car, modeled as a weighted timed
automaton~\cite{DBLP:conf/hybrid/AlurTP01,
  DBLP:conf/hybrid/BehrmannFHLPRV01}.  In the \emph{working} state $W$,
energy is consumed at a rate of $10$ energy units per time unit; in the
two \emph{recharging} states $R_1$, $R_2$, the battery is charged at a
rate of $20$, respectively $10$, energy units per time unit.  As the
clock $c$ is reset ($c\leftarrow 0$) when entering state $W$ and has
guard $c\ge 1$ on outgoing transitions, we ensure that the car always
has to be in state $W$ for at least one time unit.  Similarly, the
system can only transition back from states $R_1$, $R_2$ to $W$ if it
has spent at most one time unit in these states.

Passing between states $W$ and $R_1$ requires $4$ energy units, while
transitioning between $W$ and $R_2$, and between $R_2$ to $R_1$,
requires $2$ energy units.  Altogether, this is intended to model the
fact that there are two recharge stations available, one close to work
but less powerful, and a more powerful one further away.  Now assume
that the initial state $W$ is entered with a given \emph{initial energy}
$x_0$, then the energy problem of this model is as follows: Does there
exist an infinite trace which (1) visits $W$ infinitely often and (2)
never has an energy level below $0$?

This type of energy problems for weighted timed automata is treated
in~\cite{DBLP:conf/hybrid/BouyerFLM10}, and using a reduction like
in~\cite{DBLP:conf/hybrid/BouyerFLM10}, our model can be transformed to
the \emph{energy automaton} in the right part of Fig.~\ref{fi:example}.
(The reduction is quite complicated and only works for one-clock timed
automata; see~\cite{DBLP:conf/hybrid/BouyerFLM10} for details.)  It can
be shown that the energy problem for the original automaton is
equivalent to the following problem in the energy automaton: Given an
initial energy $x_0$, and updating the energy according to the
transition label whenever taking a transition, does there exist an
infinite run which visits $W$ infinitely often?  Remark that the energy
update on the transition from $R$ to $W$ is rather complex (in the
general case of $n$ recharge stations, the definition of $f_\textit{RW}$
can have up to $n$ branches), and that we need to impose a B{\"u}chi
condition to enforce visiting $W$ infinitely often.

In this paper we propose a generalization of the energy automata
of~\cite{DBLP:conf/hybrid/BouyerFLM10} which also encompasses most other
approaches to energy problems.  Abstracting the properties of the
transition update functions in our example, we define a general notion
of \emph{energy functions} which specify how weights change from one
system state to another.  Noticing that our functional energy automata
are semiring-weighted automata in the sense of~\cite{book/DrosteKV09},
we uncover a close connection between energy problems and reachability
and B{\"u}chi problems for weighted automata.  More precisely, we show
that one-dimensional energy problems can be naturally solved using
matrix operations in semirings and
semimodules~\cite{book/DrosteKV09,BEbook,EK2,DBLP:conf/mfcs/EsikK04}.

For reachability, we use only standard results~\cite{book/DrosteKV09},
but for B{\"u}chi acceptance we have to extend previous
work~\cite{EK2,DBLP:conf/mfcs/EsikK04} as our semiring is not complete.
We thus show that reachability and B{\"u}chi acceptance are decidable
for energy automata.  For the class of \emph{piecewise affine} energy
functions, which generalize the functions of Fig.~\ref{fi:example} and
are important in applications, they are decidable in exponential time.

\smallskip\noindent\textit{Structure of the Paper.}\quad %
We introduce our general model of energy automata in
Section~\ref{se:energyaut}.  In Section~\ref{se:esemiring} we show that
the set of energy functions forms a star-continuous Kleene algebra, a
fact which allows us to give an elegant characterization of reachability
in energy automata.  We also expose a structure of Conway
semiring-semimodule pair over energy functions which permits to
characterize B{\"u}chi acceptance.  In Section~\ref{se:reach} we use
these characterizations to prove that reachability and B{\"u}chi
acceptance are decidable for energy automata.  We also show that this
result is applicable to most of the above-mentioned examples and give
complexity bounds.  To put our results in perspective, we generalize
energy automata along several axes in Section~\ref{se:multi} and analyze
these generalized reachability and B{\"u}chi acceptance problems.

\smallskip\noindent\textit{Related Work.}\quad %
A simple class of energy automata is the one of \emph{integer-weighted
  automata}, where all energy functions are updates of the form
$x\mapsto x+ k$ for some (positive or negative) integer $k$.  Energy
problems on these automata, and their extensions to multiple weights
(also called \emph{vector addition systems with states} (VASS)) and
games, have been considered \eg~in~\cite{conf/ictac/FahrenbergJLS11,
  DBLP:conf/fsttcs/ChatterjeeDHR10, DBLP:conf/icalp/ChatterjeeD10,
  DBLP:conf/icalp/BrazdilJK10, DBLP:conf/rp/Chaloupka10,
  DBLP:journals/ipl/Chan88, DBLP:conf/formats/BouyerFLMS08}.  Our energy
automata may hence be considered as a generalization of one-dimensional
VASS to arbitrary updates; in the final section of this paper we will
also be concerned with multi-dimensional energy automata and games.

Energy problems on \emph{timed
  automata}~\cite{DBLP:journals/tcs/AlurD94} have been considered
in~\cite{DBLP:conf/lata/Quaas11, DBLP:conf/formats/BouyerFLMS08,
  DBLP:conf/hybrid/BouyerFLM10, DBLP:conf/qest/BouyerLM12}.  Here timed
automata are enriched with integer weights in locations and on
transitions (the \emph{weighted timed automata}
of~\cite{DBLP:conf/hybrid/AlurTP01, DBLP:conf/hybrid/BehrmannFHLPRV01},
\cf~Fig.~\ref{fi:example}), with the semantics that the weight of a
delay in a location is computed by multiplying the length of the delay
by the location weight.  In~\cite{DBLP:conf/formats/BouyerFLMS08} it is
shown that energy problems for one-clock weighted timed automata without
updates on transitions (hence only with weights in locations) can be
reduced to energy problems on integer-weighted automata with additive
updates.

For one-clock weighted timed automata \emph{with} transition updates,
energy problems are shown decidable
in~\cite{DBLP:conf/hybrid/BouyerFLM10}, using a reduction to energy
automata as we use them here.  More precisely, each path in the timed
automaton in which the clock is not reset is converted to an edge in an
energy automaton, labeled with a \emph{piecewise affine} energy function
(\cf~Definition~\ref{de:fpwint}).  Decidability of the energy problem is
then shown using ad-hoc arguments, but can easily be inferred from our
general results in the present paper.

Also another class of energy problems on weighted timed automata is
considered in~\cite{DBLP:conf/hybrid/BouyerFLM10}, in which weights
during delays are increasing \emph{exponentially} rather than linearly.
These are shown decidable using a reduction to energy automata with
\emph{piecewise polynomial} energy functions; again our present
framework applies.

We also remark that semigroups acting on a set, or more generally,
semiring-semimodule pairs, have been used to describe the infinitary
behavior of automata for a long time, see~\cite{book/PerrinP04,
  DBLP:conf/icalp/Wilke91, BEbook}. In this framework, the infinitary
product or omega operation is defined on the semiring and takes its
values in the semimodule. Another approach is studied
\eg~in~\cite{DBLP:conf/RelMiCS/MathieuD05}, where the omega operation
maps the semiring into itself.  It seems to the authors that there is no
reasonable definition of an infinitary product or omega operation on
energy functions that would again result in an energy function, hence we
chose to use the framework of semiring-semimodule pairs.

\section{Energy Automata}
\label{se:energyaut}

The transition labels on the energy automata which we consider in the
paper, will be functions which model transformations of energy levels
between system states.  Such transformations have the (natural)
properties that below a certain energy level, the transition might be
disabled (not enough energy is available to perform the transition), and
an increase in input energy always yields at least the same increase in
output energy.  Thus the following definition.

\begin{definition}
  An \emph{energy function} is a partial function $f: \Realnn\to
  \Realnn$ which is defined on a closed interval $[ l_f,
  \infty\mathclose[$ or on an open interval $\mathopen] l_f,
  \infty\mathclose[$, for some lower bound $l_f\ge 0$, and such that for
  all $x_1\le x_2$ for which $f$ is defined,
  \begin{equation}
    \label{eq:deriv1}\tag{$\ast$}
    f( x_2)\ge f( x_1)+ x_2- x_1\,.
  \end{equation}
  The class of all energy functions is denoted by $\mathcal F$.
\end{definition}

Thus energy functions are strictly increasing, and in points where they
are differentiable, the derivative is at least $1$.\footnote{Remark
  that, in relation to the example in the introduction, the derivative
  is taken with respect to \emph{energy input}, not \emph{time}.  Hence
  the mapping from input to output energy in state $W$ is indeed an
  energy function in our sense.}  The inverse functions to energy
functions exist, but are generally not energy functions.  Energy
functions can be \emph{composed}, where it is understood that for a
composition $g\circ f$ (to be read from right to left), the interval of
definition is $\{ x\in \Realnn\mid f( x)\text{ and } g( f( x))\text{
  defined}\}$.  We will generally omit the symbol $\circ$ and write
composition simply as $gf$.

\begin{definition}
  An \emph{energy automaton} $( S, T)$ consists of finite sets $S$ of
  states and $T\subseteq S\times \mathcal F\times S$ of transitions
  labeled with energy functions.
\end{definition}

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.0cm,initial text=,scale=.8,transform shape]
    \tikzstyle{every node}=[font=\small]
    \tikzstyle{every state}=[fill=white,shape=circle,inner
    sep=.5mm,minimum size=2.2mm,outer sep=.8mm]
    \node[state,initial] (1) at (0,0) {};
    \node[state] (2) at (4,0) {};
    \node[state] (3) at (8,0) {};
    \path (1) edge[out=10,in=170] node[above] {$x\mapsto x+ 2; x\ge 2$}
    (2);
    \path (1) edge[out=-10,in=-170] node[below] {$x\mapsto x+ 3; x> 1$}
    (2);
    \path (2) edge[out=120,in=60,loop] node[above] {$x\mapsto 2x- 2; x\ge
      1$} (2);
    \path (2) edge[out=10,in=170] node[above] {$x\mapsto x- 1; x> 1$}
    (3);
    \path (3) edge[out=190,in=-10] node[below] {$x\mapsto x+ 1;
      x\ge 0$}
    (2);
  \end{tikzpicture}
  \caption{%
    \label{fi:eauto}
    A simple energy automaton.}
\end{figure}

We show an example of a simple energy automaton in Fig.~\ref{fi:eauto}.
Here we use inequalities to give the definition intervals of energy
functions.

A finite \emph{path} in an energy automaton is a finite sequence of
transitions $\pi= (s_0,f_1,s_1), (s_1,f_2,s_2),\dots,
(s_{n-1},f_n,s_n)$.  We use $f_\pi$ to denote the combined energy
function $f_n\cdots f_2 f_1$ of such a finite path.  We will also use
infinite paths, but note that these generally do not allow for combined
energy functions.

A \emph{global state} of an energy automaton is a pair $q=( s, x)$ with
$s\in S$ and $x\in \Realnn$.  A transition between global states is of
the form $((s,x), f, (s',x'))$ such that $(s,f,s')\in T$ and $x'=f(x)$.
A (finite or infinite) \emph{run} of $( S, T)$ is a path in the graph of
global states and transitions.

We are ready to state the decision problems with which our main concern
will lie.  As the input to a decision problem must be in some way
finitely representable, we will state them for subclasses $\mathcal
F'\subseteq \mathcal F$ of \emph{computable} energy functions; an
$\mathcal F'$-automaton is an energy automaton $( S, T)$ with
$T\subseteq S\times \mathcal F'\times S$.

\begin{problem}[Reachability]
  \label{pb:reach}
  Given a subset $\mathcal F'$ of computable functions, an $\mathcal
  F'$-automaton $( S, T)$, an initial state $s_0\in S$, a set of
  accepting states $F\subseteq S$, and a computable initial energy $x_0\in
  \Realnn$: does there exist a finite run of $( S, T)$ from $(s_0,x_0)$
  which ends in a state in $F$?
\end{problem}

\begin{problem}[B{\"u}chi acceptance]
  \label{pb:buchi}
  Given a subset $\mathcal F'$ of computable functions, an $\mathcal
  F'$-automaton $( S, T)$, an initial state $s_0\in S$, a set of
  accepting states $F\subseteq S$, and a computable initial energy
  $x_0\in \Realnn$: does there exist an infinite run of $( S, T)$ from
  $(s_0,x_0)$ which visits $F$ infinitely often?
\end{problem}

As customary, a run such as in the statements above is said to be
accepting.  We let $\preach_{ \mathcal F'}$ denote the function which
maps an $\mathcal F'$-automaton together with an initial state, a set of
final states, and an initial energy to the Boolean values $\FALSE$ or
$\TRUE$ depending on whether the answer to the concrete reachability
problem is negative or positive.  $\pbuchi_{ \mathcal F'}$ denotes the
similar mapping for B{\"u}chi problems.

The special case of Problem~\ref{pb:buchi} with $F= S$ is the question
whether there \emph{exists an infinite run} in the given energy
automaton.  This is what is usually referred to as \emph{energy
  problems} in the literature; our extension to general B{\"u}chi
conditions has not been treated before.

\section{The Algebra of Energy Functions}
\label{se:esemiring}

In this section we develop an algebraic framework of
\emph{star-continuous Kleene algebra} around energy functions which will
allow us to solve reachability and B{\"u}chi acceptance problems in a
generic way.  Let $[ 0, \infty]_\bot=\{ \bot\}\cup[ 0, \infty]$ denote
the non-negative real numbers together with extra elements $\bot$,
$\infty$, with the standard order on $\Realnn$ extended by $\bot< x<
\infty$ for all $x\in \Realnn$.  Also, $\bot+ x= \bot- x= \bot$ for all
$x\in \Realnn\cup\{ \infty\}$ and $\infty+ x= \infty- x$ for all $x\in
\Realnn$.

\begin{definition}
  An \emph{extended energy function} is a mapping $f:[ 0,
  \infty]_\bot\to[][ 0, \infty]_\bot$, for which $f( \bot)= \bot$ and
  $f( x_2)\ge f( x_1)+ x_2- x_1$ for all $x_1\le x_2$, as
  in~\eqref{eq:deriv1}.  Moreover, $f( \infty)= \infty$, unless $f( x)=
  \bot$ for all $x\in[ 0, \infty]_\bot$.  The class of all extended
  energy functions is denoted $\E$.
\end{definition}

This means, in particular, that $f( x)= \bot$ implies $f( x')= \bot$ for
all $x'\le x$, and $f( x)= \infty$ implies $f( x')= \infty$ for all
$x'\ge x$.  Hence, except for the extension to $\infty$, these functions
are indeed the same as our energy functions from the previous section.
Composition of extended energy functions is defined as before, but needs
no more special consideration about its definition interval.

We also define an ordering on $\E$, by $f\le g$ iff $f( x)\le g( x)$ for
all $x\in[ 0, \infty]_\bot$.  We will need three special energy
functions, $\bbot$, $\id$ and $\ttop$; these are given by $\bbot( x)=
\bot$, $\id( x)= x$ for $x\in[ 0, \infty]_\bot$, and $\ttop( \bot)=
\bot$, $\ttop( x)= \infty$ for $x\in[ 0, \infty]$.

\begin{lemma}
  \label{le:distr}
  With the ordering $\le$, $\E$ is a complete lattice with bottom
  element $\bbot$ and top element $\ttop$.  The supremum on $\E$ is
  pointwise, \ie~$( \sup_{ i\in I} f_i)( x)= \sup_{ i\in I} f_i( x)$ for
  any set $I$, all $f_i\in \E$ and $x\in[ 0, \infty]_\bot$.  Also,
  $(\sup_{i \in I}f_i)h = \sup_{i \in I}( f_i h)$ for all $h\in \E$.
\end{lemma}

We denote binary suprema using the symbol $\vee$; hence $f\vee g$, for
$f, g\in \E$, is the function $( f\vee g)( x)= \max( f( x), g( x))$.

\begin{lemma}
  \label{le:idmsring}
  $( \E, \vee, \circ, \bbot, \id)$ is an idempotent semiring with natural
  order $\le$.
\end{lemma}

Recall~\cite{book/DrosteKV09} that $\le$ being natural refers to the
fact that $f\le g$ iff $f\vee g= g$.

For iterating energy functions, we define a unary star operation on $\E$
by
\begin{equation*}
  f^*( x)= \left\{
  \begin{array}{cl}
    x &\quad\text{if } f( x)\le x\,, \\
    \infty &\quad\text{if } f( x)> x\,.
  \end{array} \right.
\end{equation*}

\begin{lemma}
  \label{le:prop-star}
  For any $f\in \E$, we have $f^*\in \E$.  Also, for any
  $g\in \E$, there exists $f\in \E$ such that $g= f^*$
  if, and only if, there is $k\in[ 0, \infty]_\bot$ such that $g( x)= x$
  for all $x< k$, $g( x)= \infty$ for all $x> k$, and $g( k)= k$ or $g(
  k)= \infty$.
\end{lemma}

By Lemma~\ref{le:distr}, composition right-distributes over arbitrary
suprema in $\E$.  The following example shows that a similar left
distributivity does \emph{not} hold in general, hence $\E$ is \emph{not}
a complete semiring the sense of~\cite{book/DrosteKV09}.  Let $f_n,
g\in \E$ be defined by $f_n( x)= x+ 1- \frac1n$ for $x\ge 0$, $n\in
\Natp$ and $g( x)= x$ for $x\ge 1$.  Then $g( \sup_n f_n)( 0)= g( \sup_n
f_n( 0))= g( 1)= 1$, whereas $( \sup_n g f_n)( 0)= \sup_n g( f_n( 0))=
\sup_n g( 1- \frac1n)= \bot$.

The next lemma shows a restricted form of left distributivity which
holds only for function powers $f^n$.  Note that it implies that $f^*=
\sup_n f^n$ for all $f\in \E$, which justifies the definition of $f^*$
above.

\begin{lemma}
  \label{le:distl}
  For any $f, g\in \E$, $g f^*= \sup_{ n\in \Nat}( g f^n)$.
\end{lemma}

\begin{proposition}
  \label{pr:EcontKA}
  For any $f, g, h\in \E$, $g f^* h= \sup_{ n\in \Nat}( g f^n h)$.
  Hence $\E$ is a star-continuous Kleene
  algebra~\cite{DBLP:conf/mfcs/Kozen90}.
\end{proposition}

We call a subsemiring $\E'\subseteq \E$ a \emph{subalgebra} if $f^*\in
\E'$ for all $f\in \E'$.

It is known~\cite{book/DrosteKV09, book/Conway71, BEbook,
  DBLP:journals/iandc/Kozen94} that when $S$ is a star-continuous Kleene
algebra, then so is any matrix semiring $S^{n \times n}$, for all $n\ge
1$, with the usual sum and product operations. The natural order on
$S^{n \times n}$ is pointwise, so that for all $n\times n$ matrices
$A,B$ over $S$, $A\le B$ iff $A_{i,j}\le B_{i,j}$ for all $i,j$.  Now a
star-continuous Kleene algebra is also a Conway semiring, hence the
Conway identities
\begin{equation}
  \label{eq:conway1}
  (g \vee f)^*= (g^*f)^*g^* \quad\text{and}\quad (gf)^*= g(fg)^*f\vee \id
\end{equation}
are satisfied for all $f, g\in \E$.  Also, this implies that the matrix
semiring $\E^{ n\times n}$ is again a Conway semiring, for any $n\ge 1$,
with the star operation defined inductively for a matrix
\begin{equation}
  \label{eq:matrix}
  M=
  \begin{bmatrix}
    a & b\\
    c & d
  \end{bmatrix}
  \in \E^{n \times n}\,,
\end{equation}
where $a$ is $k \times k $ and $d$ is $m \times m$ with $k + m  = n$, by
\begin{equation}
  \label{eq:starM}
  M^*= 
  \begin{bmatrix}
    ( a\vee b d^* c)^* \;\;&\;\; ( a\vee b d^* c)^* b d^* \\
    ( d\vee c a^* b)^* c a^* \;\;&\;\; ( d\vee c a^* b)^*
  \end{bmatrix}
  \in \E^{n \times n}\,.
\end{equation}
The definition of $M^*$ does not depend on how $M$ is split into parts,
and star-continuity implies that for all matrices $M, N, O$,
\begin{equation}
  \label{eq:starcontM}
  N M^* O= \sup_{ n\in \Nat}( N M^n O)\,.
\end{equation}

Note again that this implies that $M^*= \sup_n M^n$ for all matrices
$M$.  In a sense, this gives another, inductive definition of the star
operation on the matrix semiring; the important property of
star-continuous Kleene algebras is, then, that this inductive definition
and the one in~\eqref{eq:starM} give rise to the same operation.

We introduce a semimodule $\V$ over $\E$.  Let $\B=\{ \FALSE, \TRUE\}$
be the Boolean algebra, with order $\FALSE< \TRUE$, and $\V=\{ u:[ 0,
\infty]_\bot\to \B\mid u( \bot)= \FALSE, x_1\le x_2\IMPL u( x_1)\le u(
x_2)\}$.  Identifying $\FALSE$ with $\bot$ and $\TRUE$ with $\infty$, we
have an embedding of $\V$ into $\E$; note that $\bbot, \ttop\in \V$.

\begin{lemma}
  \label{le:semimod}
  With action $( u, f)\mapsto u f: \V\times \E\to \V$, $\V$ is a right
  $\E$-semimodule~\cite{EK2}.  Moreover, $( \sup_{ i\in I} u_i) f=
  \sup_{ i\in I}( u_i f)$ for any set $I$, all $u_i\in \V$ and $f\in
  \E$, and $u f^*= \sup_{ n\in \Nat} u f^n$ for all $u\in \V$.
\end{lemma}

So like the situation for $\E$ (\cf~Lemmas~\ref{le:distr}
and~\ref{le:distl}), the action of $\E$ on $\V$ right-distributes over
arbitrary suprema and left-distributes over function powers.

We define an infinitary product operation $\E^\omega\to \V$.  Let $f_0,
f_1,\dotsc$ be an infinite sequence of energy functions and $x_0\in[ 0,
\infty]_\bot$, and put $x_{ n+ 1}= f_n( x_n)$ for $n\in \Nat$.  Then we
define
\begin{equation*}
  \big( \prod_{ i= 0}^\infty f_i)( x_0)=
  \begin{cases}
    \FALSE &\text{if } \exists n\in \Nat: x_n= \bot\,, \\
    \TRUE &\text{if } \forall n\in \Nat: x_n\ne \bot\,.
  \end{cases}
\end{equation*}
Note that this product is order-preserving.  By the next lemma, it is a
conservative extension of the finite product.  As $\E$ is not a complete
semiring, it follows that $( \E, \V)$ is not a complete
semiring-semimodule pair in the sense of~\cite{EK2}.

\begin{lemma}
  \label{le:prod_is_prod}
  For all $f_0, f_1,\dotsc\in \E$, $( \prod_{ i= 1}^\infty f_i) f_0=
  \prod_{ i= 0}^\infty f_i$.  For all indices $0= n_0\le n_1\le\dotsc$,
  $\prod_{ i= 0}^\infty f_i= \prod_{ i= 0}^\infty( f_{ n_{ i+ 1}-
    1}\dotsm f_{ n_i})$.
\end{lemma}

To deal with infinite iterations of energy functions, we define a unary
omega operation $\E\to \V$ by
\begin{equation*}
  f^\omega( x)= \left\{
  \begin{array}{cl}
    \FALSE &\quad\text{if } x= \bot\text{ or } f( x)< x\,, \\
    \TRUE &\quad\text{if } x\ne \bot\text{ and } f( x)\ge x\,.
  \end{array} \right.
\end{equation*}

Note that $f^\omega= \prod_{ i= 0}^\infty f$ for all $f\in \E$.

\begin{proposition}
  \label{pr:smodpair}
  $( \E, \V)$ is a Conway semiring-semimodule pair.
\end{proposition}

Recall~\cite{BEbook} that this means that additionally to the
identities~\eqref{eq:conway1},
\begin{equation*}
  ( g f)^\omega=( fg)^\omega f \quad\text{and}\quad ( f\vee g)^\omega=
  f^\omega( g f^*)^*\vee( g f^*)^\omega
\end{equation*}
for all $f, g\in \E$.  Like for Conway semirings, it implies that the
pair $( \E^{ n\times n}, \V^n)$ is again a Conway semiring-semimodule
pair, for any $n\ge 1$, with the action of $\E^{ n\times n}$ on $\V^n$
similar to matrix-vector multiplication using the action of $\E$ on
$\V$, and the omega operation $\E^{ n\times n}\to \V^n$ given
inductively as follows: for $M\in \E^{ n\times n}$ with blocks as
in~\eqref{eq:matrix}, define
\begin{gather}
  \label{eq:omegaM}
  M^\omega =
  \begin{bmatrix}
    ( a\vee b d^* c)^\omega\vee d^\omega c( a\vee b d^* c)^* \;\;&\;\; (
    d\vee c a^* b)^\omega\vee a^\omega b( d\vee c a^* b)^*
  \end{bmatrix}, \\
  M^{ \omega_k} =
  \begin{bmatrix}
    ( a\vee b d^* c)^\omega \;\;&\;\; ( a\vee b d^* c)^\omega b d^*
  \end{bmatrix}. \notag
\end{gather}
The definition of $M^\omega$ does not depend on how $M$ is split into
parts, but the one of $M^{ \omega_k}$ does (recall that $a$ is a
$k\times k$ matrix).  It can be shown~\cite{BEbook}
that~\eqref{eq:omegaM}, and also~\eqref{eq:starM}, follow directly from
certain general properties of fixed point operations.

\section{Decidability}
\label{se:reach}

We are now ready to apply the Kleene algebra framework to reachability
and B{\"u}chi acceptance for energy automata.  We first show that it is
sufficient to consider energy automata $( S, T)$ with precisely one
transition $( s, f, s')\in T$ for each pair of states $s, s'\in S$.
This will allow us to consider $T$ as a matrix $S\times S\to \E$ (as is
standard in weighted-automata theory~\cite{book/DrosteKV09}).

\begin{lemma}
  \label{le:onetransition}
  Let $\E'\subseteq \E$ be a subalgebra and $( S, T)$ an
  $\E'$-automaton.  There exists an $\E'$-automaton $( S, T')$ for which
  $\preach_{ \E'}( S, T)= \preach_{ \E'}( S, T')$ and $\pbuchi_{ \E'}(
  S, T)= \pbuchi_{ \E'}( S, T')$, and in which there is precisely one
  transition $( s, f, s')\in T'$ for all $s, s'\in S$.
\end{lemma}

Hence we may, without loss of generality, view the transitions $T$ of an
energy automaton as a matrix $T: S\times S\to \E$.  We can also let
$S=\{ 1,\dots, n\}$ and assume that the set of accepting states is $F=\{
1,\dots, k\}$ for $k\le n$.  Further, we can represent an initial state
$s_0\in S$ by the $s_0$th unit (column) vector $I^{ s_0}\in\{ \bbot,
\id\}^n$, defined by $I^{ s_0}_i= \id$ iff $i= s_0$, and $F$ by the
(column) vector $F^{ \le k}\in\{ \bbot, \id\}^n$ given by $F^{ \le k}_i=
\id$ iff $i\le k$.  Note that $T\in \E^{ n\times n}$ is an $n\times
n$-matrix of energy functions; as composition of energy functions is
written right-to-left, $T_{ ij}\in \E$ is the function on the transition
from $s_j$ to $s_i$.

\begin{theorem}
  \label{th:reach}
  Let $\E'\subseteq \E$ be a subalgebra.  For any $\E'$-automaton $(S,
  T)$ with $S=\{ 1,\dots, n\}$, $F=\{ 1,\dots, k\}$, $k\le n$, $s_0\le
  n$, and $x_0\in \Realnn$, we have $\preach_{ \E'}( S, T)( F, s_0,
  x_0)= \TRUE$ if, and only if, $\transpose F^{ \le k} T^* I^{ s_0}(
  x_0)\ne \bot$.
\end{theorem}

\begin{proof}
  Here $\transpose F^{ \le k}$ denotes the transpose of $F^{ \le k}$.
  By~\eqref{eq:starcontM}, we have $\transpose F^{ \le k} T^* I^{ s_0}=
  \sup_n( \transpose F^{ \le k} T^n I^{ s_0})$, so that $\transpose F^{
    \le k} T^* I^{ s_0}( x_0)\ne \bot$ iff $\transpose F^{ \le k} T^n
  I^{ s_0}( x_0)\ne \bot$ for some $n\in \Nat$, \ie~iff there is a
  finite run from $( s_0, x_0)$ which ends in a state in $F$. \qed
\end{proof}

Referring back to the example automaton $( S, T)$ from
Fig.~\ref{fi:eauto}, we display in Fig.~\ref{fi:eautoclos} the automaton
with transition matrix $T^*$.

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.0cm,initial text=,scale=.8,transform shape]
    \tikzstyle{every node}=[font=\small]
    \tikzstyle{every state}=[fill=white,shape=circle,inner
    sep=.5mm,minimum size=2.2mm,outer sep=.8mm]
    \node[state,initial] (1) at (0,0) {};
    \node[state] (2) at (3,0) {};
    \node[state] (3) at (6,0) {};
    \path (1) edge[out=120,in=60,loop] node[above] {$f_{ 11}$} (1);
    \path (1) edge node[below] {$f_{ 12}$} (2);
    \path (1) edge[out=-20,in=200] node[below left] {$f_{ 13}$} (3);
    \path (2) edge[out=120,in=60,loop] node[above] {$f_{ 22}$} (2);
    \path (2) edge[out=20,in=160] node[above] {$f_{ 23}$} (3);
    \path (3) edge node[below] {$f_{ 32}$} (2);
    \path (3) edge[out=120,in=60,loop] node[above] {$f_{ 33}$} (3);
  \end{tikzpicture}

  \vspace{-1ex}
  {\small
    \begin{minipage}{.3\linewidth}
      \begin{align*}
        f_{ 11}( x) &= \hspace*{.9em} x; \hspace*{1.4em} x\ge 0 \\
        f_{ 12}( x) &= \hspace*{.9em} \infty; \hspace*{1.0em} x> 1 \\
        f_{ 22}( x) &= \left\{
          \begin{aligned}
            &x;\hspace*{.4em} && x\le 2 \\
            &\infty; && x> 2
          \end{aligned}
        \right.
      \end{align*}
    \end{minipage}
    \hfill
    \begin{minipage}{.3\linewidth}
      \begin{align*}
        f_{ 23}( x) &= \left\{
          \begin{aligned}
            &x- 1; && 1< x\le 2 \\
            &\infty; && x> 2
          \end{aligned}
        \right. \\
        f_{ 32}( x) &= \left\{
          \begin{aligned}
            &x+ 1; && x\le 1 \\
            &\infty; && x> 1
          \end{aligned}
        \right.
      \end{align*}
    \end{minipage}
    \hfill
    \begin{minipage}{.3\linewidth}
      \begin{align*}
        f_{ 33}( x) &= \left\{
          \begin{aligned}
            &x;\hspace*{.4em} && x\le 1 \\
            &\infty; && x> 1
          \end{aligned}
        \right. \\
        f_{ 13}( x) &= \hspace*{.9em} \infty; \hspace*{1.0em} x> 1
      \end{align*}
    \end{minipage}}
  \caption{%
    \label{fi:eautoclos}
    The closure of the automaton from Fig.~\ref{fi:eauto}.}
\end{figure}

\begin{theorem}
  \label{th:buchi2}
  Let $\E'\subseteq \E$ be a subalgebra.  For any $\E'$-automaton $(S,
  T)$ with $S=\{ 1,\dots, n\}$, $F=\{ 1,\dots, k\}$, $k\le n$, $s_0\le
  n$, and $x_0\in \Realnn$, we have $\pbuchi_{ \E'}( S, T)( F, s_0,
  x_0)= T^{ \omega_k} I^{ s_0}( x_0)$.
\end{theorem}

\begin{proof
  This is a standard result for \emph{complete} semiring-semimodule
  pairs, \cf~\cite{EK2}.  Now $( \E, \V)$ is not complete, but the
  properties developed in the previous section allow us to show the
  result nevertheless.  We need to see that for all $M \in \E^{n \times
    n}$ and $1 \leq i \leq n$,
  \begin{equation*} 
    (M^\omega)_{i}=  \sup\{\cdots M_{k_3,k_2}M_{k_2,k_1}M_{k_1,i} : 1
    \leq k_1,k_2,\ldots \leq n \}\,,
  \end{equation*}
  which we shall deduce inductively from~\eqref{eq:omegaM}.

  Let $a\in \E^{ \ell\times \ell}$, $d\in \E^{ m\times m}$, for $\ell+
  m= n$, and let $i\in\{ 1,\dots, \ell\}$.  Then the $i$th component of
  $M^\omega$ is the $i$th component of $(a \vee bd^*c)^\omega \vee
  d^\omega c (a \vee bd^*c)^*$.  By induction hypothesis, the $i$th
  component of $(a \vee bd^*c)^\omega$ is the supremum of all infinite
  products $(\cdots M_{k_2,k_1}M_{k_1,i})$ such that $1 \leq k_j \leq m$
  for an infinite number of indices $j$, and similarly, the $i$th
  component of $d^\omega c (a \vee bd^*c)^*$ is the supremum of all
  infinite products $(\cdots M_{k_2,k_1}M_{k_1,i})$ such that $1 \leq
  k_j \leq m$ for a finite number of indices $j$.  Thus, the $i$th
  component of $(a \vee bd^*c)^\omega \vee d^\omega c (a \vee bd^*c)^*$
  is the supremum of all infinite products $(\cdots
  M_{k_2,k_1}M_{k_1,i})$.  \qed
\end{proof}

We remark that our decision algorithms are \emph{static} in the sense
that the matrix expressions can be pre-computed and then re-used to
decide reachability and B{\"u}chi acceptance for different values $x_0$
of initial energies.

Using elementary reasoning on infinite paths, we can provide an
alternative characterization of B{\"u}chi acceptance which does not use
the omega operations:

\begin{theorem}
  \label{th:buchi}
  Let $\E'\subseteq \E$ be a subalgebra.  For any $\E'$-automaton $(S,
  T)$ with $S=\{ 1,\dots, n\}$, $F=\{ 1,\dots, k\}$, $k\le n$, $s_0\le
  n$, and $x_0\in \Realnn$, we have $\pbuchi_{ \E'}( S, T)( F, s_0,
  x_0)= \TRUE$ if, and only if, there exists $j\le k$ for which
  \begin{equation*}
    \transpose I^j T T^* I^j \, \transpose I^j T^* I^{ s_0}( x_0)\ge
    \transpose I^j T^* I^{ s_0}( x_0)\ne \bot.
  \end{equation*}
\end{theorem}

\begin{corollary}
  \label{co:decidereach}
  \label{co:decidebuchi}
  For subalgebras $\E'\subseteq \E$ of computable functions in which it
  is decidable for each $f\in \E'$ whether $f( x)\le x$,
  Problems~\ref{pb:reach} and~\ref{pb:buchi} are decidable.  For an
  energy automaton with $n$ states and $m$ transitions, the decision
  procedures use $O( m+ n^3)$, respectively $O( m+ n^4)$, algebra
  operations.
\end{corollary}

\begin{proof}
  Maxima and compositions of computable functions are again computable,
  and if it is decidable for each $f\in \E'$ whether $f( x)\le x$, then
  also $f^*$ is computable for each $f\in \E'$.  Hence all matrix
  operations used in Lemma~\ref{le:onetransition} and
  Theorems~\ref{th:reach} and~\ref{th:buchi} are computable.  The number
  of operations necessary in the construction in the proof of
  Lemma~\ref{le:onetransition} is $O( m)$, and, using \eg~the
  Floyd-Warshall algorithm to compute $T^*$, $O( n^3)$ operations are
  necessary to compute $\transpose I^{ \le k} T^* I^{ s_0}$.  \qed
\end{proof}

We proceed to identify two important subclasses of computable energy
functions, which cover most of the related work mentioned in the
introduction, and to give complexity results on their reachability and
B{\"u}chi acceptance problems.

The \emph{integer update functions} in $\E$ are the functions $f_k$,
for $k\in \Int$, given by
\begin{equation*}
  f_k( x)= \left\{
  \begin{array}{cl}
    x+ k &\quad\text{if } x\ge \max( 0, -k)\,, \\
    \bot &\quad\text{otherwise}\,,
  \end{array} \right.
\end{equation*}
together with $f_\infty:= \ttop$.  These are the update functions
usually considered in integer-weighted automata and
VASS~\cite{conf/ictac/FahrenbergJLS11, DBLP:conf/fsttcs/ChatterjeeDHR10,
  DBLP:conf/icalp/ChatterjeeD10, DBLP:conf/icalp/BrazdilJK10,
  DBLP:conf/rp/Chaloupka10, DBLP:journals/ipl/Chan88,
  DBLP:conf/formats/BouyerFLMS08}.  We have $f_\ell f_k= f_{ k+ \ell}$
and $f_k\vee f_\ell= f_{ \max( k, \ell)}$, and $f_k^*= f_0$ for $k\le 0$
and $f_k^*= f_\infty$ for $k> 0$, whence the class $\Eint$ of integer
update functions forms a subalgebra of $\E$.  A function $f_k\in \Eint$
can be represented by the integer $k$, and algebra operations can then
be performed in constant time.  Hence Corollary~\ref{co:decidereach}
implies the following result.

\begin{theorem}
  For $\Eint$-automata, Problems~\ref{pb:reach} and~\ref{pb:buchi} are
  decidable in PTIME.
\end{theorem}

Next we turn our attention to piecewise affine functions as used
in~Fig.~\ref{fi:example}.

\begin{definition}
  \label{de:fpwint}
  A function $f\in \E$ is said to be \emph{(rational) piecewise affine}
  if there exist $x_0< x_1<\dots< x_k\in \Rat$ such that $f( x)\ne \bot$
  iff $x\ge x_0$ or $x> x_0$, $f( x_j)\in \Rat\cup\{ \bot\}$ for all
  $j$, and all restrictions $f\rest{ \mathopen] x_j, x_{ j+
      1}\mathclose[}$ and $f\rest{ \mathopen] x_k, \infty\mathclose[}$
  are affine functions $x\mapsto a_jx+ b_j$ with $a_j, b_j\in \Rat$,
  $a_j\ge 1$.
\end{definition}

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[radius=2pt]
    \path (-.5,0) edge[black!30] (5,0);
    \path (0,-.5) edge[black!30] (0,5);
    \foreach \x in {1,2,3,4,5} \node at (\x,-.4) {\small \color{gray} $\x$};
    \foreach \y in {1,2,3,4,5} \node at (-.4,\y) {\small \color{gray} $\y$};
    \fill (2,.5) circle;
    \draw (2,.5) -- (3,2) circle;
    \fill (3,2.3) circle;
    \draw (3,2.7) circle -- (4.5,4.2) circle;
    \fill (4.5,4.5) circle;
    \draw (4.5,4.5) -- (4.75,5);
    \draw (4.75,5) edge[dotted] (5,5.5);
    \node at (8,2.5) {$%
      f( x)=
      \begin{cases}
        .5 &( x= 2) \\
        1.5\, x- 2.5 &( 2< x< 3) \\
        2.3 &( x= 3) \\
        x- .3 &( 3< x< 4.5) \\
        4.5 &( x= 4.5) \\
        2\, x- 4.5 &( x> 4.5)
      \end{cases}
      $};
  \end{tikzpicture}
  \caption{%
    \label{fi:example-pw}
    A piecewise affine energy function}
\end{figure}

Note that the definition does not make any assertion about continuity at
the $x_j$, but~\eqref{eq:deriv1} implies that $\lim_{ x\nearrow x_j} f(
x)\le f( x_j)\le \lim_{ x\searrow x_j} f( x)$.  A piecewise affine
function as above can be represented by its break points $x_0,\dotsc,
x_k$, the values $f( x_0),\dotsc, f( x_k)$, and the numbers $a_0,
b_0,\dotsc, a_k, b_k$.  These functions arise in the reduction used
in~\cite{DBLP:conf/hybrid/BouyerFLM10} to show decidability of energy
problems for one-clock timed automata with transition updates.  The
notion of \emph{integer piecewise affine} functions is defined
similarly, with all occurrences of $\Rat$ above replaced by $\Int$.
Fig.~\ref{fi:example-pw} shows an example of a piecewise affine
function.

The class $\Epw$ of piecewise affine energy functions forms a subsemiring
of $\E$: if $f, g\in \Epw$ with break points $x_0,\dots, x_k$,
$y_0,\dots, y_\ell$, respectively, then $f\vee g$ is piecewise affine
with break points a subset of $\{ x_0,\dots, x_k, y_0,\dots, y_\ell\}$,
and $gf$ is piecewise affine with break points a subset of $\{
x_0,\dots, x_k,$ $f^{ -1}( y_0),\dots, f^{ -1}( y_\ell)\}$.

Let, for any $k\in \Rat$, $g_k^-, g_k^+:[ 0, \infty]_\bot\to[][ 0,
\infty]_\bot$ be the functions defined by
\begin{equation*}
  g_k^-( x)= \left\{
  \begin{array}{cl}
    x &\quad\text{for } x< k\,, \\
    \infty &\quad\text{for } x\ge k\,,
  \end{array} \right.
  \qquad
  g_k^+( x)= \left\{
  \begin{array}{cl}
    x &\quad\text{for } x\le k\,, \\
    \infty &\quad\text{for } x> k\,.
  \end{array} \right.
\end{equation*}
By Lemma~\ref{le:prop-star} (and noticing that for all $f\in \Epw$,
$\sup\{ x\mid f( x)\le x\}$ is rational), $\Epw$ completed with the
functions $g_k^-$, $g_k^+$ forms a subalgebra of $\E$.

Remark that, unlike $\Epw$, the class $\Epwi$ of integer piecewise affine
functions does \emph{not} form a subsemiring of $\E$, as composites of
$\Epwi$-functions are not necessarily integer piecewise affine.
As an example, for the functions $f, g\in \Epwi$ given by
\begin{equation*}
  f( x)= 2x\,, \qquad g( x)=
  \begin{cases}
    x+ 1; & x< 3\,, \\
    x+ 2; & x\ge 3\,,
  \end{cases}
\end{equation*}
we have
\begin{equation*}
  g( f( x))=
  \begin{cases}
    2x+ 1; & x< 1.5\,, \\
    2x+ 2; & x\ge 1.5\,.
  \end{cases}
\end{equation*}
which is not integer piecewise affine.  Similarly, the class of rational
\emph{affine} functions $x\mapsto ax+ b$ (without break points) is not
closed under maximum, and $\Epw$ is the semiring generated by rational
affine functions.

\begin{theorem}
  \label{th:exptime}
  For $\Epw$-automata, Problems~\ref{pb:reach} and~\ref{pb:buchi} are
  decidable in EXPTIME.
\end{theorem}

\begin{proof
  We need to show that it is decidable for each $f\in \Epw$ whether $f(
  x)\le x$.  Let thus $f$ be a piecewise affine function, with
  representation $( x_0,\dots, x_k, f( x_0),$ $\ldots, f( x_k),
  a_0,\dots, a_k, b_0,\dots, b_k)$.  If $x< x_0$, then $f( x)= \bot\le
  x$.  If $x= x_j$ for some $j$, we can simply compare $x_j$ with $f(
  x_j)$.

  Assume now that $x\in \mathopen] x_j, x_{ j+ 1}\mathclose[$ for some
  $j$.  If $a_j x_j+ b_j\le x_j$ and $a_j x_{ j+ 1}+ b_j\le x_{ j+ 1}$,
  then also $f( x)\le x$ by~\eqref{eq:deriv1}.  Likewise, if $a_j x_j+
  b_j> x_j$ and $a_j x_{ j+ 1}+ b_j> x_{ j+ 1}$, then also $f( x)> x$.
  The case $a_j x_j+ b_j> x_j$, $a_j x_{ j+ 1}+ b_j\le x_{ j+ 1}$ cannot
  occur because of~\eqref{eq:deriv1}, and if $a_j x_j+ b_j\le x_j$ and
  $a_j x_{ j+ 1}+ b_j> x_{ j+ 1}$, then $a_j> 1$, and $f( x)\le x$ iff
  $x\le \frac{ b_j}{ 1- a_j}$.

  For the case $x\in \mathopen] x_k, \infty\mathclose[$, the arguments
  are similar: if $a_k x_k+ b_k> x_k$, then also $f( x)> x$; if $a_k
  x_k+ b_k\le x_k$ and $a_k= 1$, then also $f( x)\le x$, and if $a_k> 1$
  in this case, then $f( x)\le x$ iff $x\le \frac{ b_k}{ 1- a_k}$.

  Using Corollary~\ref{co:decidereach}, we have hence shown
  decidability.  For the complexity claim, we note that all algebra
  operations in $\Epw$ can be performed in time linear in the size of
  the representations of the involved functions.  However, the maximum
  and composition operations may double the size of the representations,
  hence our procedure may take time $O( 2^{ m+ n^3} p)$ for
  reachability, and $O( 2^{ m+ n^4} p)$ for B{\"u}chi acceptance, for an
  $\Epw$-automaton with $n$ states, $m$ transitions, and energy
  functions of representation length at most $p$.  \qed
\end{proof}

In the setting of $\Epw$-automata and their application to one-clock
weighted timed automata with transition updates, our
Theorem~\ref{th:buchi} is a generalization of~\cite[Lemmas~24,
25]{DBLP:conf/hybrid/BouyerFLM10}.  Complexity of the decision procedure
was left open in~\cite{DBLP:conf/hybrid/BouyerFLM10}; as the conversion
of a one-clock weighted timed automaton to an $\Epw$-automaton incurs an
exponential blowup, we now see that their procedure is
doubly-exponential.

Considerations similar to the above show that also the setting of
\emph{piecewise polynomial} energy functions allows an application of
Theorem~\ref{th:buchi} to show energy problems on the exponentially
weighted timed automata from~\cite{DBLP:conf/hybrid/BouyerFLM10}
decidable.



\section{Multi-dimensional Energy Automata and Games}
\label{se:multi}
\label{se:reachgamemulti}

Next we turn our attention to several variants of energy automata. 
We will generally stick to the set $\Epwi$ of integer piecewise affine
energy functions; the fact that $\Epwi$ is not a subsemiring of $\E$
will not bother us here.

An \emph{$n$-dimensional integer piecewise affine energy automaton}, or
\emph{$\Epwi^n$-auto\-maton} for short, $( S, T)$, for $n\in \Natp$,
consists of finite sets $S$ of states and $T\subseteq S\times
\Epwi^n\times S$ of transitions.  A \emph{global state} in such an
automaton is a pair $(s,\vec{x})\in S\times \Nat^n$, and
\emph{transitions} are of the form
$(s,\vec{x})\to[ \vec{f}](s',\vec{x}')$
such that $(s,\vec{f},s')\in T$ and $\vec{x}'( i)=\vec{f}( i)(\vec{x}(
i))$ for each $i\in\{1,\dots,n\}$.

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.0cm,initial text=,scale=.8,transform shape]
    \tikzstyle{every node}=[font=\small]
    \tikzstyle{every state}=[fill=white,shape=circle,inner
    sep=.5mm,minimum size=2.2mm,outer sep=.8mm]
    \node[state,initial] (1) at (0,0) {};
    \node[state,accepting] (2) at (3,0) {};
    \path (1) edge[out=60,in=120,loop] node[right,pos=.3] {$( -1, 1)$} (1);
    \path (1) edge node[below] {$( 0, -2)$} (2);
  \end{tikzpicture}
  \caption{%
    \label{fi:2dim-nokleene}
    A simple two-dimensional VASS}
\end{figure}

For reachability in $\Epwi^n$-automata (with $n\ge 2$), our algebraic
results do not apply.  To see this, we refer to the reachability problem
in Fig.~\ref{fi:2dim-nokleene}: with initial energy $( 1, 1)$, the loop
needs to be taken precisely once, but with initial energy $( 2, 0)$, one
needs to loop twice.  Hence there is no static algorithm which can
decide reachability for this VASS.

However, we remark that $\Epwi^n$-automata are \emph{well-structured
  transition systems}~\cite{DBLP:journals/tcs/FinkelS01}, with ordering
on global states defined by $(s,\vec{x})\preceq (s',\vec{x}')$ iff
$s=s'$ and $\vec{x}(i)\leq\vec{x}'(i)$ for each $i= 1,\dots, n$ (here we
also have to assume $x_0\in \Nat$).  Also, the reachability problem for
energy automata is a \emph{control state reachability problem} in the
sense of~\cite{DBLP:journals/iandc/AbdullaCJT00}.  Decidability of the
reachability problem for $\Epwi^n$-automata thus follows from the
decidability of the control state reachability problem for
well-structured transition
systems~\cite{DBLP:journals/iandc/AbdullaCJT00}.  Note that B{\"u}chi
acceptance is not generally decidable for well-structured transition
systems (it is undecidable for lossy counter
machines~\cite{DBLP:conf/rp/Schnoebelen10}), so our reduction proof does
not imply a similar result for B{\"u}chi acceptance.

\begin{theorem}
  \label{thm_multiple_var_reach}
  The reachability problem for $\Epwi^n$-automata with $x_0\in \Nat$ is
  decidable.
\end{theorem}

Next we show that if the requirement~\eqref{eq:deriv1} on energy
functions, that $f( x_2)\ge f( x_1)+ x_2- x_1$ for each $x_1\le x_2$, is
lifted, then reachability becomes undecidable from dimension $4$.  We
call such functions \emph{flat} energy functions; remark that we still
require them to be strictly increasing, but the derivative, where it
exists, may be less than $1$.  The class of all flat energy functions is
denoted $\Eflat$ and its restrictions by $\Eflatpw$, $\Eflatpwi$.

\begin{theorem}
  \label{th:undec4dim}
  The reachability problem for $\Eflatpw^4$-automata is undecidable.
\end{theorem}

Next we extend our energy automata formalism to (turn based)
\emph{reachability games}.  Let $(S,T)$ be an $n$-dimensional energy
automaton such that $S= S_A\cup S_B$ forms a partition of $S$ and
$T\subseteq (S_A\times\Epwi^n\times S_B)\cup (S_B\times\Epwi^n\times
S_A)$.  Then $(S,S_A,S_B,T)$ induces an $n$-dimensional \emph{energy
  game} $G$.  The intuition of the reachability game is that the two
players $A$ and $B$ take turns to move along the game graph $( S, T)$,
updating energy values at each turn.  The goal of player~$A$ is to reach
a state in $F$, the goal of player~$B$ is to prevent this from
happening.

The reachability game is a \emph{coverability game} in the sense
of~\cite{DBLP:journals/entcs/RaskinSB05}.  In general, the reachability
game on well-structured transition systems is
undecidable~\cite{DBLP:journals/logcom/AbdullaBd08}.  Indeed, the games
on VASS considered in~\cite{DBLP:conf/icalp/BrazdilJK10} are a special
case of reachability games on energy automata with integer update
functions; their undecidability is shown
in~\cite{DBLP:journals/logcom/AbdullaBd08,
  DBLP:conf/icalp/BrazdilJK10}. It is hence clear that it is undecidable
whether player~$A$ wins the reachability game in $2$-dimensional
$\Eint$-automata.  As a corollary, we can show that for \emph{flat}
energy functions, already one-dimensional reachability games are
undecidable.

\begin{theorem}
  \label{th:undec2game}
  Whether player~$A$ wins the reachability game in $\Eint^2$-automata is
  undecidable.
\end{theorem}

\begin{theorem}
  \label{th:flatgame}
  It is undecidable for $\Eflatpw$-automata whether player~$A$ wins the
  reachability game.
\end{theorem}

\begin{proof}[sketch]
  The proof is by reduction from reachability games on $2$-dimen\-sional
  $\Eint$-automata to reachability games on $1$-dimensional
  $\Eflatpwi$-automata.  The intuition is that the new energy variable
  $x$ encodes the two old ones as $x= 2^{ x_1} 3^{ x_2}$, and then
  transitions in the $2$-dimensional game are encoded using gadgets in
  which the other player may interrupt to demand proof that the required
  inequalities for $x_1$ \emph{and} $x_2$ were satisfied.  The energy
  functions in the so-constructed $1$-dimensional automaton are
  piecewise affine because the original ones were integer updates.  The
  details of the proof are in appendix. \qed
\end{proof}

\section{Conclusion}

We have in this paper introduced a functional framework for modeling and
analyzing energy problems.  We have seen that our framework encompasses
most existing formal approaches to energy problems, and that it allows
an application of the theory of automata over semirings and semimodules
to solve reachability and B{\"u}chi acceptance problems in a generic
way.  For the important class of piecewise affine energy functions, we
have shown that reachability and B{\"u}chi acceptance are PSPACE-hard
and decidable in EXPTIME.  As our algorithm is static, computations do
not have to be repeated in case the initial energy changes.  Also,
decidability of B{\"u}chi acceptance implies that LTL model checking is
decidable for energy automata.

In the last part of this paper, we have seen that one quickly comes into
trouble with undecidability if the class of energy functions is extended
or if two-player games are considered.  This can be remedied by
considering \emph{approximate} solutions instead, using notions of
distances for energy automata akin to the ones
in~\cite{DBLP:conf/fsttcs/FahrenbergLT11} to provide quantitative
measures for similar energy behavior.
 
Another issue that remains to be investigated is reachability and
B{\"u}chi problems for one-dimensional energy automata with flat energy
functions; we plan to do this in future work.

