\section{INTRODUCTION}

  The complex quark-gluon and meson cloud dynamics of hadrons
  give rise to non-spherical components in their wavefunction which in a
  classical limit and at large wavelengths will correspond to a "deformation".
  The spectroscopic quadrupole moment provides the most reliable and interpretable
  measurement of these components. For the proton, the only stable hadron, it
  vanishes identically because of its spin 1/2 nature. Instead, the signature
  of the non-spherical components of the proton is sought in the presence of
  resonant quadrupole amplitudes $(E^{3/2}_{1+}, S^{3/2}_{1+})$ in the
  predominantly magnetic dipole ($M^{3/2}_{1+}$)  $\gamma^* N\rightarrow \Delta$
  transition. Nonvanishing resonant quadrupole amplitudes will signify that
  either the proton or the $\Delta^{+}(1232)$ or more likely both are deformed.
  The ratios CMR $= Re(S^{3/2}_{1+}/M^{3/2}_{1+})$  and EMR $= Re(E^{3/2}_{1+}/M^{3/2}_{1+})$
  are routinely used to present the relative magnitude of the amplitudes of interest.

  In the quark model, the non-spherical amplitudes in the nucleon and $\Delta$ are caused by
  the non-central, tensor interaction between quarks \cite{glashow}. However, the magnitudes
  of this effect for the predicted E2 and C2 amplitudes \cite{capstick} are at least an
  order of magnitude too small to explain the experimental results and even the dominant M1 matrix element is
  $\simeq$ 30\% low. A likely cause of these dynamical shortcomings
  is that the quark model does not respect chiral symmetry, whose spontaneous breaking leads
  to strong emission of virtual pions (Nambu-Goldstone Bosons)\cite{amb}. These couple to
  nucleons as $\vec{\sigma}\cdot \vec{p}$ where  $\vec{\sigma}$ is the nucleon spin, and
  $\vec{p}$ is the pion momentum. The coupling is strong in the p wave and mixes in non-zero
  angular momentum components. Based on this, it is physically reasonable to expect that
  the pionic contributions increase the M1 and dominate the E2 and C2 transition matrix
  elements in the low $Q^2$ (large distance) domain. This was first indicated by adding
  pionic effects to quark models\cite{quarkpion1,quarkpion2,quarkpion3}, subsequently
  in pion cloud model calculations\cite{sato_lee,dmt}, and recently demonstrated in
  effective field theory (chiral) calculations \cite{pasc}.

\section{EXPERIMENTAL AND THEORETICAL LANDSCAPE}

 In recent years an extensive experimental and theoretical effort has been focused on
 identifying and understanding the origin of possible non-spherical components in the
 nucleon wavefunction \cite{review} through the study of the $\gamma^* N\rightarrow \Delta$
 transition. The exploration of the two pion excitation channels has allowed the measurement
 of the E2 and C2 amplitudes up to $Q^2 \approx7~(GeV/c)^2$ \cite{joo,frol,pos01,spaprl,elsner,ungaro,spaplb,aznauryan,villano}
 with JLab dominating the intermediate
 and high momentum transfer region and with MAMI and Bates focusing at the low momentum transfers,
 a region where the pionic contributions are expected to dominate. Both quadrupole amplitudes
 have been precisely measured to be non zero, with EMR exhibiting a relatively constant behavior
 as a function of the momentum transfer while CMR is following a fall off as a function of $Q^2$.

 With the existence of non-spherical components in the nucleon wavefunction well established, recent
  investigations have focused on understanding the various mechanisms that could
  generate it.
  The experimental results \cite{joo,frol,pos01,spaprl,elsner,ungaro,spaplb,aznauryan,villano} are in reasonable agreement
  with predictions of models invoking the presence of non-spherical amplitudes and in
  strong disagreement with all nucleon models that assume sphericity for the proton and
  the $\Delta$. A wide range of theoretical approaches has
  been developed to interpret the experimental data such as the phenomenological model MAID~2007 \cite{mai00,kama},
  the dynamical calculations of Sato-Lee \cite{sato_lee} and of DMT
\cite{dmt} and the ChEFT calculation of Pascalutsa and Vanderhaegen
\cite{pasc}. The MAID model  which offers a flexible phenomenology
provides an overall consistent agreement with the experimental
results. The DMT and Sato-Lee are dynamical reaction models which
include pion cloud effects and both calculate the resonant channels
from dynamical equations. DMT uses the background amplitudes of MAID
with some small modifications while Sato-Lee calculate all
amplitudes consistently within the same framework with only three
free parameters. DMT exhibits a reasonable agreement with the data
while the Sato-Lee model on the other hand exhibits a clear
disagreement with the $\pi^+$ data which is a bit surprising if we
consider the reasonable agreement of the Sato-Lee calculation with
the $\pi^\circ$ channel experimental results \cite{spaprl}. The
chiral effective field theory (ChEFT) calculation of Pascalutsa and
Vanderhaegen is a systematic expansion based on QCD\cite{pasc}. The
results of this expansion up to next to leading order exhibit an
overestimation of the $\pi^+$ channel results which indicates that
the next order calculation is required. It is worth pointing out
that this calculation is in reasonable agreement with the
experimental results for the $\pi^\circ$ channel
\cite{stave,spaplb}.

\section{FUTURE PROSPECTS}

Although the Electric quadrupole amplitude has been sufficiently
mapped as a function of momentum transfer the Coulomb quadrupole
still needs to be further explored at the low $Q^2$ regime.
Jefferson Lab Hall A experiment E08-010 \cite{halla} will extend the
Coulomb quadrupole measurements lower in momentum transfer down to
$Q^2=0.04~(GeV/c)^2$ and it will map the low $Q^2$ region with
measurements of unprecedented precision. Data taking of the E08-010
experiment was completed in 2011 and the results are expected in
early 2013.

Another valuable prospect will be offered by the exploration of the
VCS excitation channel at the $\Delta$ region. A MAMI experiment
\cite{mami} will offer the first precise exploration of the weak
H$(e,e^\prime p)\gamma$ channel at the $\Delta$ at
$Q^2=0.20~(GeV/c)^2$. The experiment will offer the first results
for the quadrupole amplitudes through the photon channel; the
different nature of this reaction channel, being purely
electromagnetic, and the fact that it will be measured
simultaneously with the dominant $\pi^\circ$ channel \cite{stave},
will allow important tests of the reaction framework and of the
systematic uncertainties of the extracted resonant amplitudes. The
experiment will also offer a simultaneous measurement of the protons
electric generalized polarizability exploring further its non
trivial behavior at low momentum transfers. The experiment will
acquire data at the end of 2012.

The upcoming results from JLab and MAMI along with the expected
progress on the theoretical front will provide a definitive
measurement of the non-spherical components in the nucleon wave
function, the identification of the dynamics that give rise to it,
and will have a profound impact on our understanding of hadrons and
QCD in the confinement regime.

\bibliographystyle{aipproc}


\section*{Abstract}
We perform the analysis of scientific collaboration at the level of universities. The scope of this study is to answer two fundamental questions: (i) can one indicate a category (i.e., a scientific discipline) that has the greatest impact on the rank of the university and (ii) do the best universities collaborate with the best ones only? Using two university ranking lists (ARWU and QS) as well as data from the Science Citation Index we show how the number of publications in certain categories correlates with the university rank. Moreover, using complex networks analysis, we give hints that the scientific collaboration is highly embedded in the physical space and the number of common papers decays with the distance between them. We also show the strength of the ties between universities is proportional to product of their total number of publications.

\section*{Introduction}
The 20th century is well known for its critical works of Kuhn, Popper, Lakatos and Feyerabend that tried to build models of how the science should work or to show how it does in fact work. In the same, owing to the entrance into era of overwhelming information it was possible to tackle this problem quantitatively \cite{merton,king}, pointing out specific phenomena observed in science. Several studies are bound to answer such questions like "How to measure who the best scientist is?" \cite{hirsh,rad1,rad2,petersen,rad3,mz,fronczak} or try to simulate the process of paradigms shifts \cite{bornholdt,kondratiuk}. In this study, we make use of complex networks tools \cite{ba,chmiel} to show how this issue is resolved at the level of scientific institutions (i.e., universities), to be more specific (i) what is the correlation between university rank and the number of papers in a specific discipline and (ii) what are the components of the scientific collaborations.

\section*{Results}

In order to estimate the correlations between university rankings and scientific productivity we had to identify two different sources of data: (i) first devoted to the university ranking with at least 10 years activity , (ii) second connected to actual bibliographic information, in particular complying with the following rules: (1) allowing to view categories of publications,(2) allowing to view address of the publication, (3) allowing to view year of publication. The lists of top hundred universities were downloaded from two services: Academic Ranking of World Universities\footnote{http://www.arwu.org} - later referred to as ARWU and QS World University Ranking\footnote{http://www.topuniversities.com} - later referred to as QS. The rationale behind choosing two rankings that follow different rules was to check the robustness of the performed analysis. After preliminary analysis, we have chosen the service Web of Science as a data source for obtaining the information on citations. For one institution the average number of publications ranges between few to dozens of thousands of publications. As a result each university has two tables containing the following fields: (i) published (date of publication),(ii) ID (reference to the second table),(iii) subject category (category of publications),(iv) language. The key information used in this report is the subject category of the published paper (we will refer to it later as to simply {\it category})

We start the analysis with the estimation of correlation reflecting the dependence of the number of papers a university has published on its rank in the list. To be more precise, for each of 180 categories we build a 100 by 2 matrix, where the first row gives ranks $r_i$ of all universities in this category and the second one gathers the number of papers $n_i$ published in this category by the given university. As one of the variables is already given in the form of rank we decided to use Spearman's rank correlation coefficient $\rho$ as the measure of dependence between $r$ and $n$. The results are gathered in Table \ref{tab:all} together with the total number of papers in the given category and the statistical significance of the test.

It is of use to examine the relation between the size of the category, measured by the number of papers $N$ belonging to it and the above mentioned correlation coefficient $\rho$. Those results are shown in Fig. \ref{fig:rho} giving the evidence that lower correlation (i.e., larger number of papers following higher rank) is in general characteristic for categories with large total number of papers. Moreover, the correlation for such categories are statistically significant.

\subsection*{Categorical separation}
Here, we would like to check the hypothesis of categorical separation of Science. It is our belief, that certain categories ten to "glue together" the scientists working in them. In other words, the possibility of interdisciplinary research is not that high as one would expect it to be. In order to test this assumption we we performed the Principal Component Analysis (PCA) for 10 most prominent categories (in sense of the total number of papers). As can be seen in Fig. \ref{fig:pca}a, the first three principal components explain 90\% of variability in the data, so the analysis can be restricted just to them. Further, by plotting 2nd component vs 1st (Fig. \ref{fig:pca}b) and 3rd component vs. 2nd (Fig. \ref{fig:pca}c) we can identify the main directions of the dataset. In Fig. \ref{fig:pca}b we have biochemistry, biology, neuroscience, medicine and psychology in the positive part of x-axis while chemistry, physics, materials science, engineering and computer science are in negative part of this axis. In can thus mean that the 1st component divides the categories into technical sciences (negative values) and medicine-related ones (positive values). The 2nd component is much harder to be identified --- a rough estimate could link positive axis with {\it fundamental sciences} as we have physics, chemistry and biology. Finally there is a clear interpretation as to the 3rd component --- the only significant positive value is connected to physics.

\subsection*{Network analysis}
Apart from the categorical point of view we can also consider university quality by analyzing the direct connections between universities $i$ and $j$ on the basis of the collaboration matrix $\mathbf{C_{ij}}$ where the element $\mathbf{C_{ij}}$ gives the number of common publications of institutions $i$ and $j$. The principal concept of the network analysis is depicted in Fig. \ref{fig:sch1}.

Using 100 highest ranked universities, for each of them ($u_1,u_2,...,u_{100}$) we search for its publications $p_1,p_2,...,p_{M(u1)}$. Then, if among the co-authors of $p_1$ there is any that comes from either of the universities $u_2,...,u_{100}$ a link of weight $w=1$ between those universities (e.g, $u_1$ and $u_2$) is established. The weight is increased by one each time $u_2$ is found among the following publications of $u_1$. Finally the weight of the link between nodes $u_1$ and $u_2$ is just the number of their common publications (as seen in the database).

\paragraph{Weights probability distribution} The first, fundamental quantity to be computed is the probability distribution of weights $p(w)$ giving the idea about the diversity of number of publications between universities. Figure \ref{fig:pw} presents $p(w)$ for raw data (black circles) as well as for the logarithmically binned ones (with the base $b=2$, red-filled circles). The plot suggests that the majority of weights can be found for w between 1 and 10 - there a plateau can be clearly seen. However, there is still a clear pattern for the remaining part even for weights as large as $w=10000$ that could be presumably fitted by a power-law function. However it is possible to fit a full-range log-normal function (red curve)
\begin{equation}\label{eq:pw}
p(w) = \frac{1}{w \sigma \sqrt{2 \pi}} \mathrm{e}^{-\frac{ \left( \ln w - \mu \right)^2}{2 \sigma^2}}
\end{equation}
with the parameters $\mu=3.44 \pm 0.02$ and $\sigma=1.63 \pm 0.01$ (values obtained by a maximum-likelihood fitting). However, the Kolmogorov-Smirnov goodness-of-fit test accepts the hypothesis that the data points come from the distribution described by (\ref{eq:pw}) for relatively low level of significance ($\alpha=0.01$). The result is similar to this obtained in

Performing this search for consecutive universities from the ranking we obtain a fully connected network of all 100 universities with links denoting the number of common publications.

\paragraph{Dependence of edge width on node strength} An interesting point of the further analysis is to test if the strength of the university, measured as the total number of its publications with other universities from the ranking influence the affinity of one university to link to another one. More precisely, we shall test what is dependence of the weight $w_{AB}$ between universities $u_A$ and $u_B$ on the product of their strengths $s_A s_B$. A log-log scatter-plot of this relation for all pairs of universities is shown in Fig. \ref{fig:wsasb}a with black circles. It brings clear evidence that the larger is the product of universities' strengths the higher is the number of common publications between them. By performing a logarithmic binning (red-filled circles) it is possible to analyze the specific form of the relation. The outcome is presented in Fig. \ref{fig:wsasb}b, where two fits are shown: a linear one (blue line, slope $a = 6.54 \times 10^{-7} \pm 0.15 \times 10^{-7}$ and negligible intercept) and power-law one (red dotted line, exponent $0.97 \pm 0.01$). The linear fitting has the $R^2$ value of 0.99 while the power-law one 0.94. Taking into account those value as well as close to 1 exponent of the power-law fitting it is reasonable to assume that the average weight between universities characterized by strengths (number of publications) $s_A$ and $s_B$ is given by the relation
\begin{equation}\label{eq:wab}
\langle w_{AB} \rangle \propto s_A s_B.
\end{equation}
Equation (\ref{eq:wab}) can serve as a kind of predictor for estimating a possible level of cooperation between two universities. Also, observed deviations from this law could indicate either a presence of outliers in a given dataset or invalid data, thus Eq. (\ref{eq:wab}) might be useful as a first-step verification procedure of the examined data.

\paragraph{Weight threshold} Following analysis will use the concept of weight threshold \cite{chmiel} depicted in Fig. \ref{fig:sch2}. Let us take the original network of 5 fully connected universities from Fig. \ref{fig:sch2}a. Let us assume now that we are interested in constructing an unweighted network that would take into account only the connections with weight higher than a certain threshold weight $w_T$ ($w > w_T$). A possible outcome of this procedure is presented in Fig. \ref{fig:sch2}b - all the links with $w < w_T$ are omitted and as a result we obtain a network where links indicate only connections between nodes (i.e., they do not bear any value).

Using weight threshold as a parameter it is possible to obtain several unweighted networks - for each value of $w_T$ in the range $\langle w_{min}; w_{max} \rangle$ we get a different network $NT(w_T)$ whose structure is determined only by $w_T$. Then, for each of these networks it is possible to compute standard network quantities: (i) number of nodes $N$ that have a at least one link (i.e., nodes with degree $k_i=0$ are not taken into account), (ii) Number of edges (links) $E$ between the nodes,(iii) clustering coefficient $C$,  (iv) assortativity coefficient $r$ (v) entropy $S$ of node degree probability distribution and (vi) the average shortest path $\langle l \rangle$ (see Materials and Methods for details).

\paragraph{Network observables as function of weight threshold} Figure \ref{fig:allw} gathers the plots of the above described network parameters as a function of $w_T$. First, as can be seen in Fig. \ref{fig:allw}a, the number of nodes $N$ is a linearly decreasing function of the weight threshold $w_T$. The number edges $E$ decreases even faster - for $w > 200$ it follows an exponential function (Fig. \ref{fig:allw}b). Similarly to $N(w_T)$ the clustering coefficient also drops down linearly with the weight threshold (Fig. \ref{fig:allw}c), although several small jumps over the trend can be seen. The most interesting is the behaviour of $r(w_T)$ shown in Figure 5d: the coefficient starts with $r<0$, while for larger thresholds it crosses $r=0$ and for $w_T$ in range $[200;400]$ it takes its maximal value. Then it once again drops down below zero reaching $r=-0.4$ for $w_T$ around 1000. Finally it increases toward zero for large $w_T$. A non-monotonic behaviour is also observed in the case of the normalized entropy $S/S_{max}$ (Fig. \ref{fig:allw}e) - here a rapid growth occurs at the very beginning (for small $w_T$), then a linear decrease happens. For large $w_T$ the normalized entropy $S/S_{max}$ again increases. The average shortest path (Fig. \ref{fig:allw}f) resembles the shape of $r$ except for the lack of growth at the end.

\paragraph{Network visualisation} The above described non-trivial behaviour of quantities $r$, $S/S_{max}$ and $\langle l \rangle$ cannot be the sole cause of the relations presented by Eqs (\ref{eq:pw}) and (\ref{eq:wab}). It seems that there has to be another phenomenon leading to such an effect.

Using Pajek\footnote{http://www.pajek.org} program as well as a tool for community detection\footnote{http://sites.google.com/site/findcommunities} it is possible to visualize connections between universities and community structure (denoted by color) for different values of $w_T$. The results for $w_T=250,600,800$ and 1200 are shown in Figs \ref{fig:w250}-\ref{fig:w1200}, providing an input for further analysis. Up to $w_T=250$ the network is percolated (it is possible to reach any node from another one); over that value a separation occurs - Chinese, Australian and Singapore, Danish and Swedish as well as Swiss universities all form separate clusters. The giant cluster is built out of American, Canadian, English, Dutch, Swiss, German and Japan universities (Fig. \ref{fig:w250}). For $w_T=600$ Dutch, Swiss, German and Japan universities are separated from the giant cluster (Fig. \ref{fig:w600}) and for $w_T=800$ also the English ones (Fig. \ref{fig:w800}). The final separation touches also American universities ($w_T=1200$, Fig. \ref{fig:w1200}).

It seems that the key aspect governing this kind of phenomenon is the geographical distance between the universities. In fact, Figure \ref{fig:dw} confirms this supposition: the number of publications between universities A and B is a decreasing power-law function of the geographical distance between them. The gap around $d_{AB}$=5000 is most probably caused by the presence of continents. Similar results regarding the role of geographical distance in science were obtained in \cite{rybski,pan}.

\section*{Discussion}
Our preliminary results show that even such fundamental and straightforward analysis as calculation of correlation coefficient between position of the university in the ranking and the number of papers published by its employees may reveal some non-trivial relationships. In particular, one may use it as indicator of the interest a certain scientific area gains over the years. Thus it can be possible to spot an emergence of certain trends in science and, in effect, react for example establishing a new direction of research in the university.

Our final results show that the scientific collaboration is highly embedded in the physical  space - it seems that the key aspect that governs the number of common publications is the geographical vicinity of the universities. It is relevant even in the case of links between continents (link between Australia and Singapore). On the other hand the strength of the ties between universities is proportional to product of their total number of publications. These two relations could be used as a starting point for modeling of university collaboration.

\section*{Materials and Methods}
\par {\bf Data verification}

{\it Abbreviations}. The seemingly straightforward procedure of querying for a specific university name encounters some problems that could have a strong impact on the further results. Web of Science has a set of abbreviations commonly used for searching such as {\it Univ} for "University" or {\it Coll} for "College". Moreover it is essential to notice that one has to form a very specific query in order to get rid of severe mistakes. Table \ref{tab:univ} shows an exemplary list of the search universities together with the exact search phrase that had to be used.

{\it Ambiguity of queries}. The 'Search' field is a search key that we use to associate with the authors of the publications and it can consist of one of the operators: {\it +} which stands for {\it AND} operator in Boolean logic and {\it $|$} which stands for {\it NOT} operator in Boolean logic. These operators are used to clearly assess the origin of the publication. Table 2 shows that using just the names of universities from the list (first column) would lead in the case of number 98 to obtaining publications of both {\it Technical University in Munich} and {\it University of Munich}, instead of just the latter. To omit this problem one has to insert a query {\it Univ Munich $|$ Tech Univ Munich} that ensures achieving proper results. On the other hand for the case shown as number 78, it was not sufficient to enter {it Washington Univ}, as there are many universities with such an abbreviation; it was necessary to add {\it St. Louis} in the query text.

\par {\bf Network analysis}
{\it Clustering coefficient} $C_i$ for node $i$ is defined as the number of existing links among its nearest neighbors $e_i$ (i.e, nodes to which it has links) divided by the total number of possible links among them $k_i(k_i-1)/2$
\begin{equation}
C_i = \frac{2 e_i}{k_i(k_i - 1)}
\end{equation}
The total clustering coefficient for the whole network is calculated as the average over all $C_i$.\\
{\it Assortativity coefficient} $r$ defined by
\begin{equation}
r = \frac{ \frac{1}{E} \sum_i j_i k_i  - \left[ \frac{1}{2E} \sum_i \left(j_i + k_i \right) \right]^2}{ \frac{1}{2E} \left( \sum_i j_i^2 +  k_i^2  \right)- \left[ \frac{1}{2E} \sum_i \left(j_i + k_i \right) \right]^2}
\end{equation}
where i goes over all edges in the network. The coefficient is in the range $[-1;1]$, $r=1$ means that the highly connected nodes have the affinity to connect to other nodes with high $k_i$ while $r=-1$ happens when highly connected nodes tend to link to nodes with very low $k_i$.\\
{\it Entropy} of node degree probability distribution. It is calculated by first obtaining the degree probability distribution $p(k)$ (i.e., the probability that a randomly chosen node has exactly $k$ edges) and then evaluating the expression:
\begin{equation}
S = - \sum_{k = k_{min}}^{k = k_{max}} p(k) \ln p(k),
\end{equation}
where $k_{min}$ and $k_{max}$ are, respectively, the smallest and the largest degree in the network. For the sake of comparison we divide the obtained value of entropy by its maximal value, i.e., $S_{max}=\ln \left( k_{max}-k_{min} \right)$.
{\it Average shortest path} $\langle l \rangle$. It is calculated as the average value of shortest distance (measured in the number of steps) between all pairs of nodes $i$, $j$ in the network.

\section*{Acknowledgments}
We acknowledge support by FP7 FET Open project Dynamically Changing Complex Networks-DynaNets EU Grant Agreement Number 233847. This work has been supported by the European Union in the framework of European Social Fund through the Warsaw University of Technology Development Programme, realized by Center for Advanced Studies.


\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.