<figure><img src="image_1.png" /></figure>

HAL
open science

# Energy Transfer in timed cyclic networks

Luca Paparazzo, Loïc Hélouët, Nicolas Markey

► To cite this version:

Luca Paparazzo, Loïc Hélouët, Nicolas Markey. Energy Transfer in timed cyclic networks. 2024. [hal-05006900](https://hal-inriaHal)[https://inria.hal.science/hal-05006900v1](https://inria.hal.science/hal-05006900v1)

HAL Id: hal-05006900

[https://inria.hal.science/hal-05006900v1](https://inria.hal.science/hal-05006900v1)

Preprint submitted on 26 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Energy Transfer in timed cyclic networks

Luca Paparazzo[0009-0007-1134-000X], Loïc Hélouët[0000-0001-7056-2672], and Nicolas Markey[0000-0003-1977-7525]

University of Rennes, Inria, CNRS, IRISA, France,
luca.paparazzo@inria.fr, loic.helouet@inria.fr, nicolas.markey@irisa.fr

**Abstract.** This paper considers a timed model tailored to study energy savings in transport networks. It focuses on regenerative braking, a situation where the kinetic energy of a vehicle is transformed in electrical energy and sent back in the electrical network. We first describe transport networks, and formalize their semantics as timed runs of an equivalent network of timed automata (NTA). We then consider three problems. The transfer existence problem checks whether a network has the ability to save energy. The ratio maximization problem aims at computing the maximal ratio of energy saved by time unit in the long run, and the threshold problem consists in verifying the existence of a strategy allowing the saving of more energy than a fixed minima. We show that the transfer problem is a reachability question in the region automaton of the NTA, which can be solved in PSPACE. The ratio problem can be solved using Karp's algorithm on a corner point abstraction for the NTA, yielding an EXPTIME complexity. Finally, the threshold problem requires to address properties of elementary cycles and finite paths of the corner-point automaton, yielding a PSPACE complexity.

**Keywords:** Transport networks · Timed automata · Energy

## 1 Introduction

Energy is an actual concern in urban transports, and considering the sizes, weights, and power used by equipments such as metros, the smallest improvement can save huge amounts of energy. Regenerative braking is a way to save energy: the kinetic energy of a braking vehicle is transformed in electrical energy that is either stored or transferred in the power network where it can be used to feed motors of other vehicles. Of course, these transformations induce losses at each conversion and transfer. However, considering the mass of a metro and the power needed to move such a mass, regenerative braking results in huge savings. The easiest way to transfer energy from a braking vehicle to a moving one is to synchronize brakings and departures of close trains (the Joule effect prevents energy transfer on long distances). This means that to save as much energy as possible, one may have to slightly delay departures of trains to benefit from the additional power sent back to the power network. However, saving energy is not the primary concern of a metro: trains have to be operated to meet an expected quality of service (QoS), measured for instance as the number of kilometers ran
per hour by passengers in the network, the number of trains leaving a station per hour, etc. Hence, the most appropriate strategy is not necessarily to syn- chronize pairs of trains to favor regenerative braking: such solution may bring situations where the first train in a pair is crowded, while the second is almost empty. Energy saving strategies are hence non-trivial. Due to the cost of metro operation, one cannot make too many real-life tests. Hence, a sound approach is to build formal models of metro networks, synthesize strategies and test them in silico before considering an implementation in situ.

Metro networks have rather simple topologies that can be safely represented as cyclic graphs. We propose a model called *cyclic transport networks*, where energy transfer is measured as a function of time and distances between trains. In this architecture, metro positions at a given instant can be captured by a position on arcs of this graph. Metros move according to a predetermined speed profile, that specify the duration of the acceleration phase when a train leaves a station, of the cruise phase where a train maintains a constant speed, and of a braking phase when approaching the next station. The dwell durations of trains in station can be chosen in a predetermined range by an operator. QoS constraints are set station by station, and indicate the maximal time allowed between train stops at the considered station. We show that the semantics of this model can be captured by a network of priced timed automata.

We then consider three problems on these models. The first one is called the *transfer problem*: starting from a given configuration of the network, how to reach a situation in which energy transfer via regenerative braking is feasible? The answer to the transfer problem is not always positive: to use regenerative braking, one has to reduce distances between two consecutive trains. This can be enforced by choosing dwell times, but may induce behaviors that violate QoS constraints. The second problem is called the *ratio problem*, and aims at determining the maximal amount of energy that can be saved per time unit in average. The third problem is called the *threshold problem*, and consists in deciding if some run saves more energy than a given threshold $\lambda$.

We show that the transfer problem can be solved by finding a path of positive cost in the region automaton, and is in PSPACE. The ratio problem is more involved. Regions completely abstract time, so the cost of cyclic behaviors cannot be computed on a region automaton. We hence use a richer abstraction of priced timed automata, namely a corner point automaton. Then, the ratio problem can be solved by finding the cycles with optimal ratio in this corner point automaton. This is achieved by first translating the corner point automaton into a weighted automaton, and then using an adaptation of Karp's algorithm [10] to find optimal ratios. Last the threshold problem amounts to showing that either a cycle with strictly positive ratio exists, or that for some finite run, the saved energy exceeds the given threshold.

Several works have considered energy or ratios in a timed setting. [9] considers multiweighted energy games on graphs with lower/upper level constraints and their extension to timed automata. Unsurprisingly, many questions on this model are undecidable. [7] considers one-clock priced timed automata where prices can
grow linearly or exponentially. Existence of controllers to avoid negative rewards is shown in EXPTIME. [6] considers ratio questions for double priced automata: one price represents time, the other one a reward. The objective is to find cycles with minimal ratios, where a ratio is the time needed to get one unit of reward. [6] shows how to use a corner point abstraction to compute ratios. Though the ratio we want to maximize is a quantity of energy saved per time unit, the results of [6] can be adapted to our setting.

## 2 Preliminaries

In the rest of the paper, we will denote by $\mathbb{R}, \mathbb{Q}, \mathbb{N}$ the sets of reals, rationals, and non-negative integers. To simplify notations, for a pair of integers $a, b$ chosen from a set $\{0, \dots, n\}$ we will write $a \oplus b$ instead of $a + b \bmod n$ when $n$ is clear from the context. We will mainly use real valued variables. For a given real or rational $a$, we will denote by $\lfloor a \rfloor$ its integral part, and by $\text{frac}(a)$ its fractional part. We hence have $a = \lfloor a \rfloor + \text{frac}(a)$. Let $X = \{x_1, \dots, x_k\}$ be a set of real valued variables. A valuation for $X$ is a map $\nu : X \to \mathbb{R}$ that associates a real value to every variable in $X$. The valuation $\nu + d$ assigns value $\nu(x) + d$ to every variable $x \in X$. Similarly, for $Y \subseteq X$, $\nu_{[Y:=0]}$ is the valuation that assigns $\nu(x)$ to each variable $x \in X \setminus Y$, and 0 to variables in $Y$. A linear constraint over $X$ is an inequality of the form $a_1 x_1 + a_2 x_2 + \dots + a_n x_n \le b$, where $b$ is a rational value and $a_1, \dots, a_n$ are rational coefficients (which can have value 0). In the rest of the paper, we will only need simple constraints of the form $x_i - x_j \equiv b_{i,j}$, where $\equiv \in \{<, >, \le, \ge\}$. A guard is a conjunction of simple constraints, and we will denote by $\Psi_X$ the set of guards on $X$. We will assume that constants $b_{i,j}$ are integers. However, assuming rational values does not change the results of this paper. We will say that a valuation $\nu$ satisfies a guard $g \in \Psi_X$, denoted $\nu \models g$, iff replacing every variable $x_i$ in $g$ by value $\nu(x_i)$ yields a tautology.

**Definition 1.** A timed automaton is a tuple $\mathcal{A} = (S, s_0, \text{Act}, X, T, I)$ where $S$ is a set of states, $s_0 \in S$ is the initial state, \text{Act} is an alphabet of actions, $X$ is a set of real valued variables called clocks, $T \subseteq S \times \text{Act} \times \Psi_X \times 2^X \times S$ is a set of transitions, and $I : S \to \Psi_X$ associates a guard called invariant to states of $S$.

Let $\mathcal{A} = (S, s_0, \text{Act}, X, T, I)$ be a timed automaton. We will write $s \xrightarrow{a,g,R} s'$ when $(s, a, g, R, s') \in T$. A configuration of $\mathcal{A}$ is a pair $(s, \nu)$, where $s \in S$ and $\nu$ is a valuation for $X$. The semantics of timed automata is defined in terms of timed and discrete moves. A timed move of duration $\delta$ from a configuration $C = (s, \nu)$ is allowed if elapsing $\delta$ time units in configuration $C$ does not violate the time invariant of state $s$, i.e. if $\nu + \delta \models I(s)$. Timed moves are denoted $C = (s, \nu) \xrightarrow{\delta} C' = (s, \nu + \delta)$. A discrete move from a configuration $C = (s, \nu)$ with a transition $t = (s, a, g, R, s')$ is allowed if $\nu \models g$, and $\nu_{[R:=0]} \models I(s')$. This discrete move transforms configuration $C$ into a new configuration $C' = (s', \nu_{[R:=0]})$. A discrete move is denoted $C = (s, \nu) \xrightarrow{a} C' = (s', \nu_{[R:=0]})$. A run of a timed automaton is a sequence $\rho = C_0 \xrightarrow{e_1} C_1 \xrightarrow{e_2} C_2 \dots$ where each $e_i$
is either a timed or discrete move. We denote by Runs($\mathcal{A}$) the set of runs of a timed automaton $\mathcal{A}$. We will sometimes distinguish between finite runs (denoted Runs*($\mathcal{A}$)) and infinite ones (denoted Runs$^\infty(\mathcal{A})$).

An automaton $\mathcal{A}$ is strongly non-Zeno iff there exists $K \in \mathbb{N}$ such that for every run $\rho = C_0 \xrightarrow{e_1} C_1 \xrightarrow{e_2} C_2 \dots$ of length $k$, $k \ge K$ implies $\sum_{e_i \in \mathbb{R}} \delta_i \ge 1$. Non-Zenoness is a standard assumption when considering timed models, and Zeno specifications are considered as ill-formed [5].

As one can see from the semantics, the space of configurations is infinite. A frequent approach to reason on timed automata is to build an abstraction for its state space, called the region abstraction [2,3]. We will define regions more precisely in Section 4.

**Definition 2.** Let $\mathcal{A}_1 = (S_1, s_0^1, \text{Act}_1, X_1, T_1, I_1)$ and $\mathcal{A}_2 = (S_2, s_0^2, \text{Act}_2, X_2, T_2, I_2)$ be two timed automata. The synchronous product of $\mathcal{A}_1$ and $\mathcal{A}_2$ is a timed automaton $\mathcal{A}_1 \otimes \mathcal{A}_2 = (S_1 \times S_2, (s_0^1, s_0^2), \text{Act}_1 \cup \text{Act}_2, X_{1,2}T_{1,2}, I_{1,2})$ where:

$$ - (s_1, s_2) \xrightarrow{a,g,R} (s'_1, s_2) \text{ iff } (s_1, a, g, R, s'_1) \in T_1 \text{ and } a \in \text{Act}_1 \setminus \text{Act}_2 $$

$$ - (s_1, s_2) \xrightarrow{a,g,R} (s_1, s'_2) \text{ iff } (s_2, a, g, R, s'_2) \in T_2 \text{ and } a \in \text{Act}_2 \setminus \text{Act}_1 $$

$$ - (s_1, s_2) \xrightarrow{a,g,R} (s'_1, s'_2) \text{ iff } \exists (s_1, a, g_1, R_1, s'_1) \in T_1, (s_2, a, g_2, R_2, s'_2) \in T_2 \text{ and } g = g_1 \wedge g_2, R = R_1 \cup R_2 $$

$$ - X_{1,2} = X_1 \cup X_2 \text{ and } I_{1,2}(s_1, s_2) = I(s_1) \wedge I(s_2) $$

The synchronous product of two timed automata is a timed automaton. The notion of synchronous product extends to an arbitrary number of automata in the obvious way: automata that share a common action $a$ have to take jointly transitions labeled by $a$ that meet all their respective guards, while other components do not move. In the rest of the paper, we will define products where at most two components are concerned by discrete moves.

**Definition 3.** A priced timed automaton is a pair $(\mathcal{A}, \text{Cost})$ where $\mathcal{A}$ is a timed automaton and Cost: $S \cup T \to \mathbb{Q}$ assign a cost to every transition and a growth rate to every state of $\mathcal{A}$.

Let $\rho = C_0 \xrightarrow{e_1} C_1 \dots$ be a run of $\mathcal{A}$. The cost of a timed move $(s, \nu) \xrightarrow{\delta} (s, \nu + \delta)$ is Cost$(s) \times \delta$. The cost of a discrete move $(s, \nu) \xrightarrow{a} (s', \nu')$ using a transition $t = (s, a, g, R, s')$ is Cost$(t)$. Slightly abusing our notation, we will write Cost$(C \xrightarrow{e} C')$ to denote the cost of a timed or discrete move. The cost of a run $\rho$ is the value Cost$(\rho) = \sum_{i \in 1..|\rho|-1} \text{Cost}(C_i \xrightarrow{e_i} C_{i+1})$. Products of priced timed automata are built similarly to products of timed automata, with a particular cost function: the cost of a composite state $(s_1, s_2, \dots, s_k)$ of $k$ components $(A_i, \text{Cost}_i)$ is Cost$(s_1, \dots, s_k) = \text{Cost}_1(s_1) + \text{Cost}_2(s_2) + \dots + \text{Cost}_k(s_k)$. In a product automaton, the cost of a transition $t = (S, a, g, R, S')$ involving a pair of transitions $t_i, t_j$ from two components $A_i, A_j$ is Cost$(t) = \text{Cost}_i(t_i) + \text{Cost}_j(t_j)$.
**Definition 4.** A weighted graph is a tuple $\mathcal{G} = (S, A, w)$ where $S$ is a set of states, $A \subseteq S \times S$ is a set of arcs, and $w: A \to \mathbb{Q}$ is a weight function assigning a rational value to each arc.

A path in a weighted graph is a sequence of states $\rho = s_1.s_2...s_k$ such that $(s_i, s_{i+1}) \in A$. Path $\rho$ is a cycle iff $s_1 = s_k$. We denote by $\text{Paths}(\mathcal{G})$ the set of paths of a weighted graph $\mathcal{G}$ and by $\text{Cycles}(\mathcal{G})$ the set of cycles of a weighted graph $\mathcal{G}$. We will write $s \rightsquigarrow \rho$ $s'$ when $\rho$ is a path from $s$ to $s'$ and $s \rightsquigarrow s'$ when a path from $s$ to $s'$ exists in $\mathcal{G}$. The cost of a path $\rho = s_1.s_2...s_k$ is the sum $w(\rho) = \sum_{i=1..k-1} w(s_i, s_{i+1})$. The length of $\rho$ is denoted $|\rho|$ and is the number of arcs in $\rho$. The ratio of a cycle $\rho_c \in \text{Cycles}(\mathcal{G})$ is the value $\text{rat}(\rho_c) = \frac{w(\rho_c)}{|\rho_c|}$ and represents the average weight of a transition in cycle $\rho_c$. The minimal ratio of $\mathcal{G}$ is the value $\text{rat}_{\mathcal{G}}^{\min} = \min_{\rho_c \in \text{Cycles}(\mathcal{G})} \text{rat}(\rho_c)$ and the maximal ratio $\text{rat}_{\mathcal{G}}^{\max} = \max_{\rho_c \in \text{Cycles}(\mathcal{G})} \text{rat}(\rho_c)$.

The problem of the minimal ratio (i.e., the question of finding the minimal ratio in a weighted graph) has been studied by Karp [10]. The method proposed by Karp is to evaluate the minimal mean cycle value by iteratively computing, for a given state $s$, the minimal weight at fixed distance. In the rest of the paper, we will compute optimal energy saving strategies, and we are hence interested in maximal ratios. However, we show below that Karp's algorithm can be easily adapted to compute maximal ratios. We first assume, for simplicity, that all the graphs considered are strongly connected. We will then generalize the approach to all graphs, by focusing on their strongly connected components.

**Definition 5 (maximal weight at fixed distance).** Let $\mathcal{G} = (S, A, w)$ be a weighted graph, $k \in \mathbb{N}$, and $v \in S$. We define by $P_{\max}^{\mathcal{G}}(k, v)$ the maximal weight at distance $k$ from $v$ as: $P_{\max}^{\mathcal{G}}(k, v) = \max\{w(\rho) \mid s \rightsquigarrow \rho \ v \wedge |\rho| = k\}$.

By convention, if there is no path of size $k$ from $s$ to $v$, then we set $P_{\max}^{\mathcal{G}}(k, v) = -\infty$. As $\mathcal{G}$ is strongly connected, then there exists an integer $k$ such that $P_{\max}^{\mathcal{G}}(k, v) > -\infty$. To simplify notations, we will simply write $P_{\max}(k, v)$ instead of $P_{\max}^{\mathcal{G}}(k, v)$ when $\mathcal{G}$ is clear from the context.

**Theorem 1.** Let $\mathcal{G} = (S, A, w)$ be a strongly connected weighted graph with $|S| = g$, and $\mu_{\mathcal{G}}^*$ be the maximal ratio for cycles of $\mathcal{G}$. Then,

$$ \mu_{\mathcal{G}}^* = \max_{v \in S} \min_{k \in [0, g-1]} \frac{P_{\max}(g, v) - P_{\max}(k, v)}{g-k} \quad (1) $$

A complete proof for this theorem is given in Appendix A.1. Following Theorem 1, we can compute $\mu_{\mathcal{G}}^*(s)$ for a strongly connected graph $\mathcal{G}$ by computing $P_{\max}(k, v)$ for every $k \in [0, g-1]$ and every $v \in S$. We then get $\text{rat}_{\mathcal{G}}^{\max} = \mu_{\mathcal{G}}^*$. The computation of $\text{rat}_{\mathcal{G}}^{\max}$ easily extends to graphs that are not strongly connected. Let $\text{SCC}_{\mathcal{G}}$ denote the set of strongly connected components of $\mathcal{G}$, and for a chosen component $C \in \text{SCC}_{\mathcal{G}}$, let $\mathcal{G}_C$ be the restriction of $\mathcal{G}$ to vertices of $C$. Then, we have that $\text{rat}_{\mathcal{G}}^{\max} = \max_{\rho_c \in \text{Cycles}(\mathcal{G})} \text{rat}(\rho_c) = \max_{C \in \text{SCC}_{\mathcal{G}}} \max_{\rho_c \in \text{Cycles}(\mathcal{G}_C)} \text{rat}(\rho_c) = \max_{C \in \text{SCC}_{\mathcal{G}}} \text{rat}_{\mathcal{G}_C}^{\max}$.
Now, the complexity to find connected components of $\mathcal{G}$ is linear w.r.t the number of edges in $\mathcal{G}$ [11], and for a given vertex $s \in S$ computing $\mu_{\mathcal{G}}^*(s)$ can be done by iteratively computing $P_{\max}^{\mathcal{G}}(k, v)$ for each $v$ from the values of $P_{\max}^{\mathcal{G}}(k-1, v')$ for each $v' \in S$ computed at previous step $k-1$. This step can be done in $O(|S|^2)$ and is repeated at most $g$ times. As in [10], we can then compute $\text{rat}_{\mathcal{G}}^{\max}$ in $O(g \cdot |A|)$.

### 3 Cyclic Transport Networks

A metro network can be seen as a ring connecting stations, with trains moving on this ring. The speed of trains is predetermined: trains are stopped in a station for a duration fixed by metro operators. Then they accelerate, maintain their cruise speed for a while, and brake to stop at the next station. Figure 1 represents a network, the speed variation for a train moving from a station $St_i$ to a station $St_{i+1}$ and its position between $St_i$ and $St_{i+1}$.

<figure><img src="image_3.png" /><figcaption>**Fig. 1.** A cyclic transport Network with 8 stations and 4 vehicles (left) and the four phases of a trip from a station $St_i$ to a station $St_{i+1}$ (right)</figcaption></figure>

**Definition 6.** A Cyclic transport network (CTN for short) is a tuple $\mathcal{N} = (ST, P, E, freq)$, where $ST = \{St_1, \dots, St_n\}$ is a set of stations, $P \subseteq (\mathbb{Q}^+)^3$ is a set of speed profiles, and $E: ST \times ST \to P$ is a partial map associating a speed profile to every pair of consecutive stations. We furthermore require that the support of $E$ is a cycle. The map $freq: ST \to \mathbb{Q}$ is a partial map that adds a frequency constraint to a set $ST_C \subseteq ST$.

Intuitively, a CTN models a cyclic physical network where vehicles move from one station to the next one, following the speed profile for this area of the
network. A profile is a triple of positive values (a, c, b) ∈ (Q+)³ describing an acceleration duration a, a duration c for a part of the trip where the vehicle is at cruise speed, and a braking duration b. freq(Stᵢ) = dᵢ indicates that a vehicle has to stop in station Stᵢ at least every dᵢ time units to meet the network's service level. We do not make speeds nor distances explicit, as in the simple energy model that we propose later, the quantity that matters is the duration of overlapping braking and acceleration phases of vehicles around stations.

A configuration of a CTN with n stations and p vehicles is a triple $C_{CTN} = (pos, phase, trip)$, where $pos: 1..p \rightarrow ST$ indicates the last station visited by a vehicle, $phase: 1..p \rightarrow \{Stp, Ac, Cr, Br\}$ indicates the status of each vehicle's trip (stopped, accelerating, in cruise speed, braking) and $trip: 1..p \rightarrow \mathbb{R}^{\ge 0}$ indicates the time elapsed since a vehicle started a new phase of its trip. The semantics of a CTN is given in terms of timed and discrete moves. We define three types of possible events: a vehicle stops in a station, leaves a station, enters a cruise speed period or starts braking. To allow passenger transfers, the system ensures that a vehicle cannot leave less than $\delta_{min} > 0$ time units after its arrival in station. We also impose that the time spent in station is upper bounded by a value $\delta_{max}$. Choosing an appropriate dwell duration in [$\delta_{min}, \delta_{max}$] is a way to perform traffic management, for instance to recover from an unexpected delay, or in our case to favor energy transfer and meet frequency constraints. We can now define discrete and timed moves in a CTN.

- $(pos, phase, trip) \xrightarrow{leave St_i} (pos, phase', trip')$ iff
  $\exists k, (pos(k) = St_i \land phase(k) = St \land trip(k) \in [\delta_{min}, \delta_{max}].$
  Then $phase'(k) = Ac, trip'(k) = 0$.

- $(pos, phase, trip) \xrightarrow{cruise St_i} (pos, phase', trip')$ iff
  $\exists k, (pos(k) = St_i \land phase(k) = Ac \land trip(k) = a.$
  Then $phase'(k) = Cr, trip'(k) = 0$.

- $(pos, phase, trip) \xrightarrow{brake St_i} (pos, phase', trip')$ iff
  $\exists k, (pos(k) = St_i \land phase(k) = Cr \land trip(k) = c.$
  Then $phase'(k) = Br, trip'(k) = 0$.

- $(pos, phase, trip) \xrightarrow{stop St_{i \oplus 1}} (pos', phase', trip')$ iff
  $\exists k, (pos(k) = St_i \land phase(k) = Br \land trip(k) = b.$
  Then $pos'(k) = St_{i \oplus 1}, phase'(k) = Stp, trip'(k) = 0$.

- A duration $\delta \in \mathbb{R}$ can elapse in configuration $C_{CTN}$ if, letting this duration elapse does not violate the upper bound for the maximal duration of a trip phase for some vehicle. Formally, $\delta$ time units can elapse if:
  $\forall k, phase(k) = St \Rightarrow trip(k) + \delta \le \delta_{max} \land phase(k) = Ac \Rightarrow trip(k) + \delta \le a$
  $\land phase(k) = Cr \Rightarrow trip(k) + \delta \le c \land phase(k) = Br \Rightarrow trip(k) + \delta \le a.$
  Elapsing $\delta$ time units in $C_{CTN}$ then results in a configuration where each trip of a vehicle has progressed, leading to a new configuration:

$$C_{CTN} + \delta = (pos, phase, trip + \delta), \text{ where } [trip + \delta](k) = trip(k) + \delta.$$

Timed move are denoted by $C_{CTN} \xrightarrow{\delta} C_{CTN} + \delta$.

A run of a CTN from a configuration $C_0$ is a (possibly infinite) sequence of moves $C_0 \xrightarrow{e_1} C_1 \xrightarrow{e_2} \dots$ where each $e_i$ is either a discrete event of a duration.
Given a run $\rho$, we denote by $\rho_{[i,j]}$ its restriction to steps from configuration $C_i$ to configuration $C_j$. The duration of a finite run $\rho$ is the value $\mathcal{T}(\rho) = \sum_{i \in 1..|\rho|, e_i=\delta_i \in \mathbb{R}} \delta_i$. A run $\rho$ of a $\mathcal{N}$ meets its frequency constraints if, for every $St_i \in ST_C$, for every pair of consecutive stop events at station $St_i$ at respective indexes $i, j$ we have $\mathcal{T}(\rho_{[i,j]}) \le freq(St_i)$. We denote by $Runs(\mathcal{N})$ the set of runs of a transport network $\mathcal{N}$.

We adopt a simple energy model. Instead of measuring the total energy consumption along runs and trying to minimize this power demand, we assume that energy is saved mainly when trains can transfer energy via regenerative braking. We assume that energy is transferred from a braking train to an accelerating one around each station, but we do not measure how much energy is passed from one train to the next one. More realistic models should handle properties of the power network, trains characteristics and distances between trains. Instead, we take a simplified energy model and we say that there is an energy transfer at station $St_k$ in a configuration $C = (\text{pos}, \text{phase}, \text{trip})$ iff there exists a pair of vehicles $i, j$ such that $\text{pos}(j) = \text{pos}(i) \oplus 1 = St_k$ and $\text{phase}(i) = \text{Br}, \text{phase}(j) = \text{Ac}$. For the whole time spent in configuration $C$ there is an energy transfer between the train braking to stop in $St_k$ and the train leaving $St_k$. In a configuration $C$, we define by $\mathcal{E}_C$ the number of stations where an energy exchange occurs. Formally, $\mathcal{E}_C = |\{St_i | \exists k', k' \in 1..p, \text{pos}(k) = i \wedge \text{pos}(k') = i \oplus 1 \wedge \text{phase}(k) = \text{Br} \wedge \text{phase}(k') = \text{Ac}\}|$ With this definition in mind, the energy transferred in a run $\rho$ is $\mathcal{E}(\rho) = \sum_{C_i \xrightarrow{\delta_i} C_i + \delta_i \in \rho} \delta_i \mathcal{E}_{C_i}$.

We are now ready to define problems addressing energy management in cyclic transport networks. Let $\mathcal{N} = (ST, P, E, freq)$ and $C_0$ be its initial configuration:

- **Transfer**: Is there a run $\rho$ starting from $C_0$ such that $\rho$ satisfies constraints in freq and $\mathcal{E}(\rho) > 0$?

- **Ratio**: Given a CTN, what is the optimal ratio $r = \lim_{n \to \infty} \frac{\mathcal{E}(\rho_{[0,n]})}{\mathcal{T}(\rho_{[0,n]})}$ for an infinite run $\rho$ starting from $C_0$ that satisfies constraints in freq?

- **Threshold**: Given a value $\lambda \in \mathbb{Q}$, is there a finite run $\rho$ starting from $C_0$ such that $\rho$ satisfies constraints in freq and $\mathcal{E}(\rho) > \lambda$?

We will show in the next sections that these three problems can be answered on an equivalent timed automaton, computed as a product of automata depicting the behaviors of trains and the status of stations, and that generates the same timed runs as the original CTN.

# 4 The transfer problem

**Lemma 1.** Let $\mathcal{N} = (ST, P, E, freq)$ be a cyclic transport network with $n$ stations and $p$ vehicles. Then, there exists a timed automaton $A_{\mathcal{N}}$ of size $O((4.n)^p \cdot 4^n)$ such that $Runs(\mathcal{N})$ and $Runs(A_{\mathcal{N}})$ are isomorphic.

*Proof (sketch).* For every vehicle in the system, we build a timed automaton $\overline{M}_i$ that describes the position and status of the vehicle with $4.n$ states and one
clock $x_i$ to measure the time elapsed in each phase. For this automaton, discrete
transitions use the same alphabet as the CTN, and are triggered in obvious way
when $x_i = a$, $x_i = c$, $x_i = b$ to initiate beginning of cruising, or braking, or stop,
or when $\delta_{min} \le x_i \le \delta_{max}$ to trigger a departure after an allowed dwell time.
States memorize the *pos* and *phase* maps of the CTN. For each station $St_i$, we
build an automaton $\overline{T}_i$ with 4 states that memorizes whether a train is leaving
$St_i$, on its cruise from $St_i$ to $St_{i \oplus 1}$, stopped in station, or braking to stopping in
station $St_i$. Transitions are set the obvious way to memorize respective status
of 0, 1 or 2 trains. In addition to these states, when $St_i \in ST_C$ automaton $\overline{T}_i$
has a clock $y_i$ that measures the time elapsed between two stops and can be
used to enforce the frequency constraint $freq(St_i)$. For each station automaton,
we distinguish a particular state $T_i$, reached when a train is braking before the
station and another one is leaving the station. As in CTNs, these are states where
energy transfer can occur. Then, the overall automaton is obtained as a product
$\overline{M}_1 \otimes \cdots \otimes \overline{M}_p \otimes \overline{T}_1 \otimes \cdots \otimes \overline{T}_n$. The size of this automaton is in $O((4.n)^p \cdot 4^n)$.
It is easy to see that the timed transition systems underlying the two models are
isomorphic. Appendix A.2 shows the general shape of these timed automata. $\square$

The shape of states in $\mathcal{A}_N$ is of the form $S = (s_{\overline{M}_1}, \dots, s_{\overline{M}_p}, s_{\overline{T}_1}, \dots, s_{\overline{T}_n})$,
where each $s_{\overline{T}_i} \in \{N_i, A_i, B_i, T_i\}$ depicts the vehicles around station $ST_i$. $N_i$
means that no vehicle is around the station, $A_i$ that a single vehicle has left the
station and is currently accelerating, $B_i$ that a single vehicle is currently braking
and will stop at the station, and $T_i$ that there is both an accelerating and a brak-
ing vehicle around the station, i.e., a transfer. We can hence assign a cost function
to $\mathcal{A}_N$ as follows: for each composite state $S = (s_{\overline{M}_1}, \dots, s_{\overline{M}_p}, s_{\overline{T}_1}, \dots, s_{\overline{T}_n})$, we
set $\text{Cost}(S) = |\{i \in 1..n \mid s_{\overline{T}_i} = T_i\}|$.

Translating a CTN into a timed automaton is not sufficient to get an algo-
rithm that decides whether an energy transfer can occur or not. CTNs and their
timed automata translations have an infinite set of configurations. Fortunately,
we show below that we can rely on the standard region construction to build a
finite abstraction and get a decision procedure.

**Definition 7 (Regions [3]).** Let $\mathcal{A}$ be a timed automaton, and let $C_{\max}$ be the largest value that appears in guards and invariants of $\mathcal{A}$. Then, we can define an equivalence relation $\equiv$ on clock valuations as follows:
$\forall \nu, \nu' \in \mathbb{R}^X, \nu \equiv \nu'$ iff

- $\forall x \in X$, either $\lfloor \nu(x) \rfloor = \lfloor \nu'(x) \rfloor$, or $\lfloor \nu(x) \rfloor > C_{\max}$ and $\lfloor \nu'(x) \rfloor > C_{\max}$: both valuations agree on the integral parts of their clocks.

- $\forall x, y \in X$, such that $\nu(x) \le C_{\max}$ and $\nu(y) \le C_{\max}$ we have $\text{frac}(\nu(x)) \le \text{frac}(\nu(y))$ if and only if $\text{frac}(\nu'(x)) \le \text{frac}(\nu'(y))$: both valuations agree on the ordering of fractional parts of their clocks.

- $\forall x \in X$, such that $\nu(x) \le C_{\max}$, $\text{frac}(\nu(x)) = 0$ if and only if $\text{frac}(\nu'(x)) = 0$

The regions of a timed automaton $\mathcal{A}$ are the equivalence classes of $\equiv$, and
we will denote by $\mathcal{R}$ the set of regions. For a given valuation $\nu$ we will denote
by $[\nu]$ the region that contains $\nu$. Regions can have several forms. Consider a
clock $x \in X$. As clocks take a positive value, we can split the domain of $x$ into a subset of atomic constraints $C_x = \{\nu(x) = k \mid k \in 0..C_{max}\} \cup \{k-1 < \nu(x) < k \mid k \in 1..C_{max}\} \cup \{\nu(x) > C_{max}\}$. A region can be represented by choosing for each $x \in X$ an atomic constraint in $C_x$, and for each pair of clocks $x, y$ such that $k-1 < \nu(x) < k$ and $k' - 1 < \nu(y) < k'$, choose whether $\text{frac}(\nu(x)) = \text{frac}(\nu(y))$, $\text{frac}(\nu(x)) < \text{frac}(\nu(y))$ or $\text{frac}(\nu(x)) > \text{frac}(\nu(y))$. This means that regions can be represented by selecting an atomic constraint in $C_x$ for each clock $x \in X$ and an ordering on fractional parts of clocks valuations. The ordering on fractional parts can be described by a partition $X_0 \cdot X_1 \dots X_q$ on $X$, such that $x, y \in X_i$ iff $\text{frac}(\nu(x)) = \text{frac}(\nu(y))$, and $x \in X_i, y \in X_j$ with $i < j$ iff $\text{frac}(\nu(x)) < \text{frac}(\nu(y))$. It is well known that the truth value of a guard is invariant in a region, and we will write $r \models g$ iff $\nu \models g$ for every valuation $\nu \in [\nu]$.

We can define a successor relation on regions, by saying that $r'$ is a successor of $r$ if and only if there exists $\nu \in r$ and $\nu' \in r'$ and a duration $d > 0$ such that $\nu' = \nu + d$. The set of successors of a region $r$ can be efficiently computed from the representation with atoms and ordering on clocks (see [2] for details). For a region $r$ where some clock $x$ has a constant value (the chosen atomic constraint on $x$ is of the form $x = k$), letting a duration $d > 0$ elapse means that for every $\nu \in r$ we have that $[\nu+d]$ is a successor of $r$, but $[\nu+d] \neq r$. For a region $r$ where no clock has a constraint of the form $x = k$, then for every valuation $\nu \in r$, there exists a duration $d > 0$ such that $\nu + d \in r$. In this type of region, some time can elapse without changing the equivalence class, and hence without changing the guards or invariants that are satisfied in $r$. Regions with constraints of the form $k-1 < \text{frac}(\nu(x)) < k$ only will be called *open regions*, and other regions will be called *closed region*.

**Proposition 1 (Properties of regions [3]).** $\forall r, r' \in \mathcal{R}$,

- $\forall g \in \Psi_X, \forall \nu, \nu' \in r, \text{ we have } \nu \models g \text{ iff } \nu' \models g: \text{ the valuations of a region satisfy the same guards and invariants. Consequently, it is sufficient to know the region of a valuation to decide which guards and invariants are satisfied, and hence which transitions are firable.}$

- $\exists \nu \in r, d \in \mathbb{R} \text{ such that } \nu + d \in r' \implies \forall \nu \in r, \exists d \in \mathbb{R} \text{ such that } \nu + d \in r': \text{ If one can let some time elapse from a valuation } \nu \text{ in } r \text{ and reach a region } r', \text{ then one can let some time elapse from any other valuation } \nu' \text{ of } r \text{ and reach a valuation in } r' \text{ (these durations do not need to be the same).}$

- $\forall Y \subseteq X, r_{[Y:=0]} \cap r' \neq \emptyset \implies r_{[Y:=0]} \subseteq r' : \text{ After resetting clocks, all valuations in } r \text{ are transformed into valuations of a single region } r'$.

**Proposition 2 (finiteness of the region set [3]).** Let $\mathcal{A} = (S, s_0, \text{Act}, X, T, I)$ be a timed automaton. Then, the number of regions is in $O(|X|! \cdot 2^{|X|} \cdot \Pi_{x \in X}(2c_x + 2))$, where $c_x$ is the maximal constant to which clock $x$ is compared.

**Definition 8 (Region automaton [3]).** Let $\mathcal{A} = (S, s_0, \text{Act}, X, T, I)$ be a timed automaton, $\mathcal{R}$ be its set of regions, and let $\nu_0$ be an initial valuation of clocks in $X$. We can define the region automaton $\mathcal{A}_{\mathcal{R}} = (S_{\mathcal{R}}, s_{0_{\mathcal{R}}}, \text{Act}_{\mathcal{R}}, T_{\mathcal{R}})$ a follows:
- $S_R \subseteq S \times \mathcal{R}$

- $s_{0R} = (s_0, r_0)$ where $r_0$ is the region of $\nu_0$

- $Act_R = Act \cup \{\perp\}$

- $T_R \subseteq S_R \times Act_R \times S_R$ is defined by:

• for every state $s$ and every region $r$, there is a transition $(s, r) \xrightarrow{\perp} (s, r')$ if $r'$ is a successor of $r$ and $r, r' \models I(s)$.

• For every discrete transition $t = s \xrightarrow{g, \alpha, Y} s' \in T$, there is a transition $(s, r) \xrightarrow{\alpha} (s', r')$ iff $r \models g \land I(s), r_{[Y:=0]} \subseteq r'$ and $r_{[Y:=0]} \models I(s')$.

Usually, the whole set $S \times \mathcal{R} \times S$ is not reachable, and one can build $S_R$ inductively starting from $s_{0R}$. The automaton $A_R$ is hence a finite automaton over $\Sigma \cup \{\perp\}$. A run of the region automaton is a sequence of steps of the form

$$ \hat{\rho} = (s_0, r_0) \xrightarrow{\sigma_1} (s_1, r_1) \xrightarrow{\sigma_2} \dots $$

Runs of the region automaton are said progressive iff for every clock $x$ there exists an infinite number of indexes $i$ such that $r_i \models x = 0 \lor x > C_{max}$. To distinguish between runs of $\mathcal{A}$ and runs of $A_R$ we will say that runs of $\mathcal{A}$ are concrete runs and runs of $A_R$ are abstract runs. The region projection of a concrete run $\rho = (s_0, \nu_0) \xrightarrow{d_0} (s_1, \nu_1) \xrightarrow{a_1} (s_2, \nu_2) \dots$ is an abstract run $\text{proj}_R(\rho) = (s_0, [\nu_0]) \xrightarrow{\perp} (s_1, [\nu_1]) \xrightarrow{a_1} (s_2, [\nu_2]) \dots$.

**Lemma 2 ([2]).** $\forall \rho$ run of $\mathcal{A}$, $\text{proj}_R(\rho)$ is a progressive abstract run of $A_R$.

**Lemma 3 ([2], Lemma 4.13).** For every progressive abstract run $\gamma$ of $A_R$ there exists a run $\mathcal{A}$ such that $\gamma = \text{proj}_R(\rho)$.

One can tweak the region automaton of definition 8 to make it progressive [2]. Slightly abusing our constructions, we will assume that our region automaton is already progressive. Now let us consider an abstract state $(s, r)$ of $A_R$ reachable from $(s_0, r_0)$. This means that there exists a run $\rho$ that ends in a state $(s, \nu)$ with $[\nu] = r$. If $r$ is a region and there exists a transition $(s, r) \xrightarrow{\perp} (s, r')$ in $A_R$, then for every valuation $\nu'$ of $r$, one can let some duration $d > 0$ elapse, and reach valuation $\nu' + d \in r'$. This is in particular true for $\nu$. Further, as $(s, r) \xrightarrow{\perp} (s, r')$ we have $r' \models I(s)$. Hence, $\rho$ can always be extended with a timed move, i.e. there is a run of $\mathcal{A}$ that spends some time in state $s$. The cost of states is extended the obvious way in the region automaton and its runs, i.e. $\text{Cost}((s, r)) = \text{Cost}(s)$. A direct consequence is that finding a run where energy transfer occurs amounts to finding a run of $A_R$ that contains a transition of the form $(s, r) \xrightarrow{\perp} (s, r')$ with $\text{Cost}(s) > 0$. This immediately gives us the following result:

**Lemma 4.** A concrete run $\rho$ of $\mathcal{A}$ has a positive cost iff $\text{proj}_R(\rho)$ is a run of $A_R$ that contains a transition of the form $(s, r) \xrightarrow{\perp} (s, r')$ such that $\text{Cost}(s) > 0$.

**Theorem 2.** The transfer problem for CTNs is in PSPACE.
*Proof.* The answer to the transfer problem for a CTN $\mathcal{N}$ is positive iff there exists a run $\rho$ of $\mathcal{N}$ that meets all frequency constraints and such that $Cost(\rho) > 0$. We have shown in Lemma 1 that we can build an automaton $A_{\mathcal{N}}$ with at most $n+p$ clocks that has the same set of runs as $\mathcal{N}$, and the same cost function. Hence, the answer to the transfer problem is positive if there exists a run $\rho = (s_0, v_0) \xrightarrow{e_0} \dots \xrightarrow{e_k} (s, v) \xrightarrow{\delta} \dots$ of $A_{\mathcal{N}}$ that does not violate frequency constraints, visits a configuration $(s, v)$ with $Cost(s) > 0$ and lets some duration $\delta > 0$ elapse in $(s, v)$.

As shown by lemma 4, this amounts to finding an accepting run in $A_{\mathcal{N},\mathbb{R}}$ (the region automaton of $A_{\mathcal{N}}$) that contains a transition of the form $(s, r) \xrightarrow{\perp} (s, r')$. Finding such a run $\pi$ boils down to finding an accepting path of length $< |A_{\mathcal{N},\mathbb{R}}|$ from $(s_0, [\nu_0])$ that contains a transition of the form $(s, r) \xrightarrow{\perp} (s, r')$ with $Cost(s) > 0$. Finding such an accepting path can be done in NLOGSPACE w.r.t the size of the region automaton, by a non-deterministic exploration of $A_{\mathcal{N},\mathbb{R}}$, and memorizing whether a transition is of the form $(s, r) \xrightarrow{\perp} (s, r')$, which requires an additional bit of information. The number of states in $A_{\mathcal{N}}$ is bounded by $(4.n)^p \cdot 4^n$, and the number of regions smaller than $(2 \cdot C_{max} + 2)^{n+p} \cdot (n+p)! \cdot 2^{n+p}$, that is the size of $A_{\mathcal{N},\mathbb{R}}$ is exponential in the number of clocks, and accessibility can be checked in NPSPACE, by exploring non-deterministically successors of $(s_0, [\nu_0])$ along paths of length at most $K = (4.n)^p \cdot 4^n \cdot (2 \cdot C_{max} + 2)^{n+p} \cdot (n+p)! \cdot 2^{n+p}$. As NPSPACE=PSPACE, we get the PSPACE membership. $\square$

# 5 The Ratio Problem

We can now address the ratio question for CTNs: For a given CTN, what is the maximal amount of energy saved by the network through transfer per time unit in average? Intuitively, an optimal strategy to save energy would be to repeat cyclic behaviors where the amount of energy saved by time unit is maximal. However, it is not sufficient to consider cycles of the timed automaton $A_{\mathcal{N}}$ nor of its region automaton to get an optimal strategy. Consider for instance the example of Figure 2, borrowed from [8]. In this example, Cassez et al. have shown that there exists a strategy to avoid the *Bad* state, namely playing $a.b.c^\omega$. The duration of a cycle is always 1. However, the sojourn stay in state $\ell_2$ must be shorter at each cycle to preserve invariant of $\ell_1$ and avoid *Bad*. We omit the details and refer the interested reader to [8]. Now, assume that the cost of $\ell_0, \ell_1$, *Bad* is 0 and the cost of $\ell_2$ some positive value $c_2$. That is, the gain in each occurrence of the cycle *a.b.c* decreases at each iteration. This cannot be observed in regions, where most of information on time is abstracted away. An interesting point raised by [8] is that there is no effective machine (i.e. with decisions occurring at a fixed rate) that can control this model to avoid the *Bad* state, as the allowed sojourn time in $\ell_2$ decreases. Another interesting point is that this issue cannot be observed of the region automaton. In the region automaton attached to this example, one will only see that a cycle occurs, that
some time can be spent in $\ell_2$ (witnessing a transfer), but as time is abstracted, one cannot decide whether the ratio is a positive value or converges to 0. An immediate conclusion it that the ratio question cannot be addressed directly as a property of the region automaton of a CTN. However, we will show hereafter that another abstract model called the *corner point abstraction* can be used to compute ratios.

<figure><img src="image_4.png" /><figcaption>**Fig. 2.** A gadget with decreasing amount of saved energy at each cycle iteration.</figcaption></figure>

Bouyer, et al. [6] consider a question similar to the ratio problem. They study double priced timed automata with two quantities: a reward, and a cost, and search for an infimum for the ratio $\frac{\text{cost}}{\text{reward}}$. The idea is to find a strategy giving the minimal cost to produce one unit of reward. The proposed solution only has to consider ratios of cycles, and the study is restricted to automata with non-negative costs and that are strongly reward diverging, i.e. such that for every infinite run $\rho$, $\text{Reward}(\rho) = +\infty$. Then, the authors build a corner-point abstraction of their initial automaton, and use Karp's algorithm (see [10] and Section 2) to compute optimal ratios.

The solution of [6] does not immediately answer our ratio problem. First, we are interested in a supremum rather than in an infimum over the set of infinite runs. However, we have seen in Section 2 that Karp's algorithm can be adapted easily to compute maximal ratios. Second, our setting measures the amount of energy that can be transferred per unit of time. Hence, we can reuse the setting of [6] using time as “reward” and saved energy “cost” only if time diverges in infinite runs, in other words, if the considered timed automaton is non-Zeno. Fortunately, this is always the case for CTNs.

**Proposition 3.** Let $\mathcal{N}$ be a cyclic transport network, and $\mathcal{A}_\mathcal{N}$ be the associated timed automaton. Then, $\mathcal{A}_{\text{CTN}}$ is non-Zeno.

*Proof.* Let us first show that every execution of a cycle in $\mathcal{A}_\mathcal{N}$ has a strictly positive duration. Let $C$ be a cycle of $\mathcal{A}_\mathcal{N}$ and let $\rho_C$ be an execution that visits
<figure><img src="image_5.png" /><figcaption>**Fig. 3.** An open region (in green) and its corner points (in blue).</figcaption></figure>

C. For each transition of C, there is a vehicle which changes state. Let $m$ be the vehicle which state changes in the first transition of $\rho_C$.

Let $C_m$ be the projection of $C$ on states of $\overline{M}_m$ (obtained by keeping only component $m$ of each tuple composing states of $C$). Then, $C_m$ is also a cyclic path, and contains at least all states of $\overline{M}_m$. Consider a pair of consecutive stations $St_i, St_{i \oplus 1}$ and the profile $P(St_i, St_{i \oplus 1}) = (a_i, c_i, b_i)$. Then, the minimal duration of an execution that visits a cyclic path of $\overline{M}_m$ is $m_c =$

$$ \sum_{St_i \in St} a_i + c_i + b_i + \delta_{min}, \text{ and } \mathcal{T}(\rho_C) \geq m_c > 0. $$
$$ P(St_i, St_{i \oplus 1}) = (a_i, c_i, b_i) $$

Now, let $\rho$ be an infinite run of $\mathcal{A}_N$, and let $\overline{\rho}_k$ be the suffix of $\rho$ starting after a prefix of size $k$. As the automaton is finite, there exists a finite set of cyclic paths $\mathcal{F}_C$ such that, after some index $K$, $\overline{\rho}_K$ only visits paths of $\mathcal{F}_C$, of strictly positive duration. We can then conclude that $\mathcal{T}(\rho) \geq \mathcal{T}(\rho_K) = +\infty$. $\square$

A corner point is an integral valuation of clocks. A corner point $\nu$ is associated with a region $r$ if it is in the closure of $r$. Intuitively, $\nu$ can be seen as a point (with integral coordinates) of the polyhedron that contains $r$ and its borders. If a region partitions its fractional parts into $q$ subsets (as proposed in the encoding $X_1...X_p$ in Section 4), then it has $p+1$ corner points. Figure 3 shows an example of a region (in green) for a set of clocks $X = \{x, y, z\}$, with $x \in ]0, 1[, y \in ]0, 1[, z \in ]0, 1[$ and $\text{frac}(x) < \text{frac}(y) < \text{frac}(z)$ and its 4 corner points (in blue). We are now ready to define a new abstraction, namely the Corner-Point automaton, with states of the form $(s, r, \nu)$, where $s$ is a state of $\mathcal{A}$, $r$ is one of its regions, and $\nu \in (\mathbb{N} \cup \{\top\})^X$ is a corner point of $r$. Intuitively, in a state of the form $(s, r, \nu)$, $\nu$ will indicate that valuations considered in the state are "close" to point $\nu$. This additional information will be useful to differentiate regions where time can elapse from regions in which elapsing time changes the region. For convenience, we use value $\top$ to mean that the value of clock $x$ has exceeded $C_{max}$ and hence is in region not bounded according to the coordinate $x$.

**Definition 9 (Corner-point automaton [6]).** Let $\mathcal{A} = (S, s_0, \text{Act}, X, T, I)$ be a timed automaton. The Corner-Point automaton of $\mathcal{A}$ is denoted by $\mathcal{A}_{CP}$. The automaton $\mathcal{A}_{CP} = (S_{CP}, s_{0CP}, \text{Act}_{CP}, T_{CP})$ is defined as follows:

$$ - S_{CP} = S \times \mathcal{R} \times CP \text{ where } \mathcal{R} \text{ are regions of } \mathcal{A} \text{ and } CP = \{0, 1, \dots, C_{\text{max}}, \top\}^X \text{ are the possible corner points of } \mathcal{A}. $$
- $s_{0CP} = (s_0, r_0, \nu_0)$

- $Act_{CP} = Act \cup \{\perp\}$

- $T_{CP}$ is built from the transition relation $T_R$ in the region automaton:

* inter-region waiting transitions: For every waiting transition of the form $(s, r) \xrightarrow{\perp} (s, r') \in T_R$, $T_{CP}$ contains a transition of the form $(s, r, \nu) \xrightarrow{\perp} (s, r', \nu)$, where $\nu$ is a vertex of both $r$ and $r'$.

* discrete transitions: for every discrete transition $(s, r) \xrightarrow{\alpha} (s', r') \in T_R$, $T_{CP}$ contains transitions of the form $(s, r, \nu) \xrightarrow{\alpha} (s', r', \nu')$ such that, if $Y \subseteq X$ is the set of clocks reset by the transition, then $\nu' = \nu_{[Y:=0]}$.

* intra-region waiting transitions: for each pair $(s, r) \in S \times \mathcal{R}$, if $\nu$ and $\nu + 1$ are two vertices of $r$, then $(s, r, \nu) \xrightarrow{\perp} (s, r, \nu + 1) \in T_{CP}$. This type of transition represents a delay elapsing in a region. We add, by convention, that if $\nu(x) \in \{C_{\max}, \top\}$ then $(\nu + 1)(x) = \top$.

Corner point automata do not yet contain information on energy, but we can easily decorate $\mathcal{A}_{CP}$ with a function $\mathcal{E}_{CP}$ giving the energy saved for each transition.

- $\forall t \in T_{CP}$, if $t$ is a discrete transition, or an inter-region transition via the same corner point, then $\mathcal{E}_{CP}(t) = 0$

- If $t$ is an intra-region waiting transition, i.e., if $t = (s, r, \nu) \xrightarrow{\perp} (s, r', \nu') \in T_{CP}$, then $\mathcal{E}_{CP}(t) = \mathcal{E}(s)$. Intuitively, the energy gain $\mathcal{E}(s)$ is the energy that can be saved in one time unit in state $s$, and $t$ symbolizes elapsing of one time unit.

As for region automata, corner point automata defines abstract runs of the form $\pi = (s_0, r_0, \nu_0) \xrightarrow{a_1} (s_1, r_1, \nu_1) \xrightarrow{a_2} (s_2, r_2, \nu_2) \dots$.

Consider a finite run $\pi = (s_0, r_0, \nu_0) \xrightarrow{a_1} \dots \xrightarrow{a_k} (s_k, r_k, \nu_k)$, or equivalently a prefix of an infinite run of size $k$, i.e. composed of $k$ consecutive transitions. Then we can define $\mathcal{E}_{CP}(\pi)$ as $\mathcal{E}_{CP}(\pi) = \sum_{i \in 1..k} \mathcal{E}_{CP}(t_i)$. We can also recover from an abstract run of a corner point automaton a duration: $T(\pi) = |\{t_i \mid t_i \text{ is an intra-region transition}\}|$. When $T(\pi) > 0$ then the ratio $rat(\pi) = \frac{\mathcal{E}(\pi)}{T(\pi)}$ is defined. Last, the ratio of an infinite run $\pi$ is: $rat(\pi) = \limsup_{k \to \infty} rat(\pi_{[0,k]})$ when it is defined. We can now define the optimal ratio in a corner point automaton as $rat_{CP}^* = \sup_{\pi \in \text{Runs}^\infty(\mathcal{A}_{CP})} rat(\pi)$.

**Proposition 4.** Let $\mathcal{N}$ be a cyclic timed network, and $(\mathcal{A}_\mathcal{N}, \text{Cost})$ the associated priced timed automaton. Then $rat^*$ and $rat_{CP}^*$ are always defined.

*Proof.* The ratio is computed on infinite runs, i.e. runs that contain a cycle of $\mathcal{A}$. As shown in Proposition 3, $\mathcal{A}_\mathcal{N}$ is always non-Zeno, so for every infinite run $\rho$ of $\mathcal{A}$, $\mathcal{E}(\rho) > 0$. Similarly, an infinite run of $\mathcal{A}_{CP}$ exists. Hence it visits a particular abstract state $(s, r, \nu)$ from which a cycle exists. As $\mathcal{A}$ is non-Zeno, every cycle of $\mathcal{A}$ contains at least one transition where time progresses, and hence the time progress of each cycle of $\mathcal{A}_{CP}$ can be of at least one time unit, i.e. there is a transition of the form $(s', r', \nu')$ to $(s', r', \nu' + 1)$ in the cycle. So, the duration of an abstract cycle in $\mathcal{A}_{CP}$ is strictly positive. $\square$
**Proposition 5.** $rat^*_{CP} \le rat^*$

*Proof.* The proof was shown in [6]. If guards of $\mathcal{A}$ use non-strict inequalities (which is the case for $\mathcal{A}_N$), then for every execution $\pi$ of $\mathcal{A}_{CP}$ there exists a concrete execution with the same valuations as the corner points of $\pi$, and with the same ratio. So, if $\pi$ is an optimal run of $\mathcal{A}_{CP}$, then $rat(\pi)$ is the ratio of a real execution of $\mathcal{A}$ that is not necessarily optimal, and hence $rat^*_{CP} \le rat^*$. $\square$

**Proposition 6.** $rat^*_{CP} \ge rat^*$

*Proof.* The proof also comes from [6]. Let $\gamma = (l_0, \nu_0) \to (l_1, \nu_1) \dots$ be a sequence of configurations in $\mathcal{A}$. Then the set $proj_{CP}(\gamma)$ is the set of sequences of states that are path of $\mathcal{A}_{CP}$ of the form:

$$ \pi = (l_0, [\nu_0], \alpha_{0,0}) \to (l_0, [\nu_0], \alpha_{0,1}) \dots (l_0, [\nu_0], \alpha_{0,p_0}) (l_1, [\nu_1], \alpha_{1,0}) \dots $$

where each $\alpha_{i,j}$ is a corner point of region $r_i = [\nu_i]$. [6] also shows that ratios are affine functions which min and max are reached on integral coordinates. Then, for a non-Zeno timed automaton $\mathcal{A}$, for every run $\gamma$ of $\mathcal{A}$, there exists a run $\pi$ of $proj_{CP}(\gamma)$ such that $rat(\pi) \ge rat(\gamma)$ that is built by choosing corner points with the coordinates that maximize ratios in each $r_i$. In other words, for every run $\gamma$ of $\mathcal{A}$, there exists a run $\pi$ of $\mathcal{A}_{CP}$ with greater ratio. $\square$

A direct consequence of Propositions 5 and 6 is that the optimal ratio computed on the corner point automaton $\mathcal{A}_{CP}$ is exactly the optimal ratio of $\mathcal{A}_N$, i.e. we have $rat^* = rat^*_{CP}$. It now remains to show that $rat^*_{CP}$ can be effectively computed. We show below that one can build a weighted graph $G_N$ such that, for every path $\rho$ of $\mathcal{A}_{CP}$ there exists a path $\rho_W$ of $G_N$ in which $Cost(\rho_W) = \mathcal{E}(\rho)$, and $\mathcal{T}(\rho) = |\rho_W|$.

We start from a corner-point automaton with a cost function $\mathcal{E}_{CP}: S \to \mathbb{Q}$ describing the energy attached to each state $s \in S$ of $\mathcal{A}$ (and hence to each state $(s, r, \nu)$ of $\mathcal{A}_{CP}$). Recall that $\mathcal{A}$ is non-Zeno. A consequence is that, in every cyclic behavior, there exists a minimal amount of time that must elapse. Recall also that transitions of $\mathcal{A}_{CP}$ are either discrete transitions, or inter-region transitions that represent moves of duration 0, or intra-region transitions that represent timed moves of duration up to 1. We denote respectively these sets of transitions $T_{d,CP}, T_{r,CP}, T_{i,CP}$. A consequence of propositions 5 and 6 and of the fact that guards use non-strict inequalities is that, as soon as some time can elapse in a region, then there is an execution visiting the same regions where the time spent in the region is 1 (otherwise ratios would be different in $\mathcal{A}$ and $\mathcal{A}_{CP}$). Further, using Proposition 4, we know that ratios are always defined for non-Zeno automata and in particular for $\mathcal{A}$. So, exploring paths of $\mathcal{A}_{CP}$ starting from a state $(s, r, \nu)$, it is guaranteed that in less than than $|\mathcal{A}_{CP}|$ steps, one will either find a deadlock state or a cycle with at least one intra-region timed transition. For a given state $(s, r, \nu)$ we define by $Seq(s, r, \nu)$ the set of sequences of transitions $\pi = t_0.t_1 \cdots t_k$ that start at $(s, r, \nu)$, and contain a single intra-region transition i.e. paths of duration 1 time unit. In sequence $\pi$ this implies among transitions of the form $t_i = (s_{i-1}, r_{i-1}, \nu_{i-1}) \xrightarrow{a_i} (s_i, r_i, \nu_i)$, a single
transition $t_j$ belongs to $T_{i,CP}$ and $a_j = \perp$, while other transitions $t_i$ with $i \neq j$ belong to $T_{d,CP} \cup T_{r,CP}$ and we have $a_i = 0$.

$$ \mathrm{Seq}(s, r, \nu) = \left\{ \pi = t_0.t_1 \cdots t_k \in \mathrm{Runs}(\mathcal{A}_{CP}) \mid \begin{array}{l} \pi \text{ starts from } (s, r, \nu) \\ \wedge \bigcup_{i \in 0..k} t_i \cap T_{i,CP} = 1 \end{array} \right\} $$

We are now ready to define the weighted automaton $\mathcal{G}_N = (S_{\mathcal{G}_N}, A, w)$:

- $S_{\mathcal{G}_N} = \{(s, r, \nu) \in S_{CP} \text{ accessible from } (s_0, r_0, \nu_0)\}$,

- $A = \{((s, r, \nu), (s', r', \nu')) \in S_{\mathcal{G}_N}^2 \mid \exists t_0.t_1 \cdots t_k \in \mathrm{Seq}(s, r, \nu), \\ t_0 = (s, r, \nu) \xrightarrow{a_0} (s_1, r_1, \nu_1) \wedge t_k = (s_{k-1}, r_{k-1}, \nu_{k-1}) \xrightarrow{a_k} (s', r', \nu')\}$

- For every arc $a \in A$, with $a = ((s, r, \nu), (s', r', \nu'))$ we set

$$ w(a) = \max_{\substack{\pi \in \mathrm{Seq}(s, r, \nu) \\ \pi \text{ ends in } (s', r', \nu')}} \mathcal{E}_{CP}(\pi) $$

**Proposition 7.** The maximal ratio $rat_{CP}^*$ is equal to the maximal ratio

$$ \mu^* = \max_{s \in S_{\mathcal{G}_N}} \mu^*(s) $$

*Proof.* Let $C = a_1 \dots a_k$ be the cycle of $\mathcal{G}_N$ that achieves ratio $\mu^*$. Then $C$ is accessible from $(s_0, r_0, \nu_0)$. So, there exists a cycle $\pi_1 = \pi_{1,1} \pi_{1,2} \cdots \pi_{1,k}$ in $\mathcal{A}_{CP}$ such that $\pi_{1,i}$ starts in $(s_i, r_i, \nu_i)$, ends in $(s'_i, r'_i, \nu'_i)$, $\pi_{1,i} \in \mathrm{Seq}(s_i, r_i, \nu_i)$ and $(s'_i, r'_i, \nu'_i) = (s_{i+1}, r_{i+1}, \nu_{i+1})$ and maximizes $\mathcal{E}$. Similarly, there exists a sequence of arcs $\pi_0$ from $(s_0, r_0, \nu_0)$ to $(s_1, r_1, \nu_1)$. The ratio of $C$ is $\frac{w(a_1)+\dots+w(a_k)}{k}$, and it is also the ratio of $\pi_1$. So, for every cycle in $\mathcal{G}_N$, there exists a cycle of $\mathcal{A}_{CP}$ with the same ratio. This is in particular true for the cycle with the best ratio, so $rat_{CP}^* = \mu^*$. Conversely, every path $\pi$ can be decomposed into finite sequences of transition that stop immediately after a transition of $T_{i,CP}$. These sequences give immediately a sequence of arcs in $\mathcal{G}_N$ with the same ratio. $\square$

Proposition 7 immediately gives an algorithm to compute the optimal ratio of transferred energy per time unit in a $\mathcal{N}$. The first step is to compute the timed automaton $\mathcal{A}_N$ by composition of the behaviors of the vehicles in the network, and the time constrained observers of the stations. The second step is to build $\mathcal{A}_{N,CP}$, the corner-point automaton of $\mathcal{A}_N$. The third step is to compute the weighted graph $\mathcal{G}_N$. The fourth step is to find the optimal ratio in connected components of $\mathcal{G}_N$. This can be done in polynomial time using first Tarjan's algorithm [11] to find connected components and then our modification of Karp's algorithm shown in Section 2 to compute optimal ratios for all connected components. Notice that the fourth step is polynomial in the number of states in $\mathcal{A}_{CP}$, which is equal to the number of states in $\mathcal{A}_R$ multiplied by the number of corner points, that is in $O((C_{max})^{n+p})$, where $C_{max}$ is the largest constant appearing in $\mathcal{A}_N$. We hence get the following result:

**Theorem 3.** There exists an algorithm that computes the optimal ratio of a CTN with an exponential computation time.
# 6 The threshold problem

Let us now consider the threshold problem: given a $\mathcal{N}$ and an energy threshold $\lambda$ we want to decide whether there exists a run of $\mathcal{N}$ for which the saved energy exceeds $\lambda$. The main idea behind this question is to ensure that there is a strategy for which the saved energy is significant. This problem differs from the transfer problem, as existence of a transfer does not guarantee that the transfer exceeds the lower bound $\lambda$. It also differs from the ratio problem, as one does not seek optimality. However, both problems are not disjoint. Consider a $\mathcal{N}$ for which a cyclic path $C_r$ of the corner-point automaton of $\mathcal{N}$ has a (non-necessarily optimal) ratio $r > 0$. Then, for any threshold $\lambda$, one can build a run that contains more than $\frac{\lambda}{r \cdot \mathcal{T}(C_r)}$ occurrences of $C_r$ and saves more than $\lambda$ energy units. However, even if all cycles of the corner point automaton of $\mathcal{N}$ have ratio zero, one may still find acyclic paths which energy level is greater than $\lambda$.

**Proposition 8.** Let $\mathcal{N}$ be a cyclic transport network, and $\lambda \in \mathbb{Q}$. Then, $\mathcal{N}$ has runs in which the saved energy exceeds $\lambda$ iff $A_{\mathcal{N},CP}$ has a reachable cycle of strictly positive ratio, or an acyclic path $\pi$ such that $\mathcal{E}(\pi) > \lambda$.

*Proof.* Recall from the proofs of Prop 6 that there is a correspondence (both is terms of visited transitions, regions and energy saved) between runs of $\mathcal{A}$ and paths of $A_{\mathcal{N},CP}$. Indeed, for a run $\gamma$ of $\mathcal{A}$, $\text{proj}_{CP}(\gamma)$ allows to find a run $\pi$ with a greater ratio. Further, for every execution $\pi$ of $A_{CP}$ there exists a concrete execution with the same valuations as the corner points of $\pi$, and with the same ratio. The set of paths in $A_{\mathcal{N},CP}$ is composed of paths that contain cycles, and acyclic paths. Assume that for every cycle $C$ of $A_{\mathcal{N},CP}$, we have $\frac{\mathcal{E}(C)}{\mathcal{T}(C)} = 0$. As $\mathcal{A}_{\mathcal{N}}$ is non-Zeno, this means in particular that $\mathcal{E}(C) = 0$. Let $\pi$ be a path of the form $\pi = \rho_1.\beta_1.\rho_2...$ where $\rho_i$'s are acyclic paths and $\beta'_j$s are cycles. Then, the amount of energy saved in $\pi$ is the same as the amount of energy saved in a path $\pi' = \rho_1.\rho_2...$ obtained by removing cycles. If $\rho_i$ and $\rho_j$ visit a common state, then $\pi'$ still contains a cycle, and can again be reduced to a finite path $\pi'' = \rho'_1.\rho'_2...\rho'_k$ where every $\rho'_i \neq \rho'_j$ have disjoint sets of states, and with the same energy level. Hence, the maximal energy level of a path in $A_{\mathcal{N},CP}$ is achieved in an acyclic path. Now assume that for every acyclic path $\pi$ of $A_{\mathcal{N},CP}$, the energy level $\mathcal{E}(\pi)$ is smaller than $\lambda$. Then, there exists no path of $A_{\mathcal{N},CP}$ and hence no run of $\mathcal{N}$ which allows to save more than $\lambda$ units of energy.

On the other hand, if $A_{\mathcal{N},CP}$ contains an accessible cycle $C$ of positive ratio, then there exists a path $\pi_1 = \rho \cdot C$ where $\rho$ is acyclic, and for every $k \in \mathbb{N}$, $\pi_k = \rho.C^k$ is also a path of $A_{\mathcal{N},CP}$. The energy saved in cycle $C$ is $\mathcal{E}(C) > 0$. So, the energy saved in $\pi_k$ is $\mathcal{E}(\pi_k) = \mathcal{E}(\rho) + k \cdot \mathcal{E}(c)$, and hence, for $k \ge \lceil \frac{\lambda}{\mathcal{E}(C)} \rceil$, $\mathcal{E}(\pi_k) \ge \lambda$. As $\pi_k$ is a path of $A_{\mathcal{N},CP}$, then there exists a concrete run $\rho$ of $\mathcal{N}$ which has $\pi_k$ as corner-point abstraction, and such that $\mathcal{E}(\rho) > \lambda$.

Conversely, if $A_{\mathcal{N},CP}$ contains a run (involving cycles or not) $\pi$ with $\mathcal{E}(\pi) \ge \lambda$, then there exists a run $\rho$ of $A_{\mathcal{N}}$ (and hence of $\mathcal{N}$) with $\mathcal{E}(\rho) = \mathcal{E}(\pi) \ge \lambda$. $\square$

Now notice that if there exists a cycle $C$ of $A_{\mathcal{N},CP}$ such that $\mathcal{E}(C) > 0$, then there exists an elementary cycle $C'$ of $A_{\mathcal{N},CP}$ (and of size smaller than
$|A_{N,CP}|$) that contains at least one of the transitions of C. With this property and using proposition 8, we can deduce that the threshold problem can be solved by exploring only acyclic paths of $A_{N,CP}$. We hence have:

**Theorem 4.** *The threshold problem for CTNs is in PSPACE.*

*Proof (Sketch).* The algorithm to check existence of a run $\pi$ of $A_{N,CP}$ with $E(\pi) \ge \lambda$ is a standard non-deterministic exploration of paths of size at most $|A_{N,CP}|$, that can be done in PSPACE (Complete proof is in Appendix A.3).

# 7 Conclusion & Discussion

In this paper, we have shown that one can check if a transport network modeled as a cyclic graph with tokens moving at predetermined speeds can be controlled in order to save energy via regenerative braking. The paper voluntarily keeps the model simple: all vehicles have the same speed profile (acceleration, cruise speed, braking, ...) between two stations, and similar ranges of possible dwell times at each station. The only possible way to transfer energy is to synchronize braking of a train and acceleration of another one around the same station. So, the only way to control energy transfer is to choose appropriate dwell times. This setting can be easily extended: we can consider different speed profiles for each train, and let a controller choose a particular profile in addition to the dwell time. Overall, these improvements of the model are harmless for the techniques proposed, as they still allow to build a timed automaton, its region/corner point abstractions, and to check transfer, ratio and threshold properties with a slight increase in the number of states in $A_N$. Considering complex network architectures (e.g. with forks and joins) also seems to preserve the formal setting of this paper, even if construction of $A_N$ could be more involved than a simple product. Another desirable extension of the model is to make the energy consumptions and transfers more accurate. If several speed profiles are allowed for vehicles, as far as we are concerned by energy saving, there is a tradeoff to find between the energy saved when synchronizing trains and the energy used to travel at higher speed. We also consider a rough approximation of transfer: when a train brakes near a station $St_i$ and its predecessor leaves, our model counts one unit of energy transferred per time unit around $St_i$. This is a coarse model, as the amount of energy that can be effectively transferred depends on the distance between vehicles. However, refining the model to handle variation of energy w.r.t. distances would call for more continuous models such as hybrid systems and the ratio or threshold problems may become undecidable, as reachability is already undecidable for hybrid automata [1].

Even for a simple model such as CTNs, several questions remain open. The first one is the lower bounds for transfer, optimal ratio, and threshold problems. We have shown that transfer and threshold problems are in PSPACE, and the calculus of an optimal ratio in EXPTIME. The PSPACE complexity comes from the translation of CTNs into equivalent timed automata, and from the reduction of transfer and threshold to reachability questions. The EXPTIME complexity
comes from the need to explore all cycles of the corner-point automaton. Now the
remaining question is whether the problems are respectively PSPACE complete
or EXPTIME complete. One can first notice that the translation from CTNs to
timed automata leads to a subclass where each component has its own clock, that
is reset at each transition. Yet, even restricted classes of timed automata such
as event-clock automata [4] have PSPACE complexities for standard emptiness
questions. The transfer problem, at least, seems of a very simple nature, and
some instances of the problem have a trivial answer.

Consider for instance the CTN described in Figure 4-left, with 4 stations and 2 vehicles. Assume the length of the network is 10 km, that the average speed of trains is 30km/h, that dwell times range from 1 to 2 minutes, and that the only constraint in the network is that one train leaves station $St_1$ at least every 30mn. Then, trivially, one can guide in a bounded amount of time the network to a situation represented in Figure 4-right where the two vehicles are close enough for energy transfer, without violating the constraint on station $St_1$. For the same example, if one imposes a train every 11 minute at station $St_1$, then one can only meet this constraint if vehicles are (up to distances covered during the dwell of the other vehicle) at opposite positions in the network. Obviously, this constraint and the existence of an energy transfer cannot be guaranteed with only two trains in the network, and this can be easily verified on the model.

<figure><img src="image_6.png" /><figcaption>**Fig. 4.** A simple CTN with two trains. Initial configuration (left) and configuration allowing energy transfer (right).</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>**Fig. 5.** Processes and transfer patterns for a pair of vehicles in a CTN</figcaption></figure>

Another remark is that transfer occurs as soon as a pair of trains can syn-
chronize their acceleration and braking phases. The behaviors of vehicles in a
network such as a metro is very regular, and is a succession of events such as departures, beginning of cruise phase, beginning of braking phase, stop. These systems have a lot of concurrency, as the only constraint among vehicles is that they cannot occupy the same position at a given instant (or too close positions). The way vehicles moves are orchestrated can be seen as a partial order, where a single vehicle's behavior is a total order, ordering sequence events $d_i, c_i, b_i, s_i$ denoting respectively departure from station $st_i$, beginning of cruise phase, beginning of braking phase, and stop at station $st_i$. Consider the example of Figure 5. It depicts the mission of two consecutive trains $V_k$ and $V_{k+1}$. In addition to the total ordering of events related to each train, we have an ordering $b'_i < d_{i+1} < c_{i+1} < s'_{i+1}$, meaning that train $k+1$ starts to brake before train $k$ reaches its cruise speed. These dependencies are symbolized by dashed arrow, and the whole pattern highlighted by a grey zone in the Figure. This representation of runs is similar to processes of a net, and there is no doubt that, starting from the initial configuration of a CTN, one could build inductively this type of process for CTNs.

Let $\Delta(e)$ denote a realization date for event $e$. Then, there is an energy transfer if we can find consistent dates such that $\Delta(b'_i) \le \Delta(d_{i+1}) \le \Delta(c_{i+1}) \le \Delta(s'_{i+1})$ and $[\Delta(d_{i+1}); \Delta(c_{i+1})] \cap [\Delta(b'_i); \Delta(s'_{i+1})]$ is not a singleton. So, the question of transfer amounts to finding appropriate patterns on a process while satisfying some constraints on its event dates. A natural question is whether a process view of CTN runs can reduce the complexity of energy problems. A second question is whether one can focus on a chosen pair of vehicles and abstract their environment. The orders generated by processes of CTNs seem to be regular (i.e. recognizable by some graph grammar). Now if the constraints attached to the times of generated processes also exhibit some form of regularity, that can be captured by Difference Bound Matrices, such a concurrent model could provide ways to solve efficiently energy transfer questions.

## References

1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995). https://doi.org/10.1016/0304-3975(94)00202-T, https://doi.org/10.1016/0304-3975(94)00202-T

2. Alur, R., Dill, D.: The theory of timed automata. In: Real-Time: Theory in Practice, REX Workshop. LNCS, vol. 600, pp. 45–73 (1991)

3. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

4. Alur, R., Fix, L., Henzinger, T.: Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci. 211(1-2), 253–273 (1999). https://doi.org/10.1016/S0304-3975(97)00173-4, https://doi.org/10.1016/S0304-3975(97)00173-4

5. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC System Structure and Control. pp. 447–452 (1998)

6. Bouyer, P., Brinksma, E., Larsen, K.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods Syst. Des. 32(1), 3–23 (2008)
7. Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N.: Timed automata with observers under energy constraints. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010. pp. 61–70. ACM (2010). https://doi.org/10.1145/1755952.1755963, https://doi.org/10.1145/1755952.1755963

8. Cassez, F., Henzinger, T., Raskin, J.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002. Lecture Notes in Computer Science, vol. 2289, pp. 134–148. Springer (2002)

9. Fahrenberg, U., Juhl, L., Larsen, K., Srba, J.: Energy games in multiweighted automata. In: Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium. LNCS, vol. 6916. Springer (2011)

10. Karp, R.: A characterization of the minimum cycle mean in a digraph. Discret. Math. 23(3), 309–311 (1978)

11. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)

# A Appendix

## A.1 Proof of Theorem 1

**Theorem 1.** Let $G = (S, A, w)$ be a strongly connected weighted graph with $|S| = g, s \in S$, and $\mu_G^*(s)$ be the maximal ratio for cycles containing $s$. Then,

$$ \mu_G^*(s) = \max_{v \in S} \min_{k \in [0, g-1]} \frac{P_{\max}(g, v) - P_{\max}(k, v)}{g-k} $$

*Proof.* To prove this equality, we will first consider the case when $\mu_G^*(s) = 0$, and we will then generalize.

- If $\mu_G^* = 0$, then there exists a cycle of weight 0 and no cycle of positive weight in $G$. As $G$ is strongly connected, then there exists a path between any pair of vertices in $G$. As there is no cycle of positive weight, for each pair of vertices there exists a maximal weight among paths between these two vertices.

For any vertex $v \in S$ let us denote by $\rho_v$ a path from $s$ to $v$ of maximal weight. Notice that we can choose $\rho_v$ acyclic, as all cycles have weight at most 0, and we can hence choose a path $\rho_v$ such that $|\rho_v| < g$. This property holds for any vertex $v$. We then have:

$$ w(\rho_v) = \max_{k \in [0, g-1]} P_{\max}(k, v) $$

which entails

$$ P_{\max}(g, v) - w(\rho_v) = \min_{k \in [0, g-1]} P_{\max}(g, v) - P_{\max}(k, v) $$

As $w(\rho_v)$ is maximal, $P_{\max}(g, v) - w(\rho_v)$ is non-positive. It hence remains to show that there exists a vertex $v$ for which this value is equal to 0, i.e. show that $P_{\max}(g, v) = w(\rho_v) = 0$ to prove equality 1.
Let $C$ be a cycle with weight $w(C) = 0$, and let $v_0$ be a vertex of $C$. One can remark that $\rho_{v_0} \cdot C^g$ is a path of maximal weight from $s$ to $v_0$. Each of its prefixes is then also a path of maximal weight from $s$ to its final vertex. Let $\gamma: s \rightsquigarrow v^*$ be the prefix of $\rho_{v_0} \cdot C^g$ of size $g$. We then have: $w(\gamma) = P_{\max}(g, v^*) = w(\rho_{v^*})$. Hence, $v^*$ is a vertex such that $P_{\max}(g, v^*) - w(\rho_{v^*}) = 0$.

- We can now consider the general case. Let $G_0$ be the graph $G_0 = (S, A, w^0 = w - \mu_G^*)$. For every path $\rho$ of $G_0$, we have $w^0(\rho) = w(\rho) - |\rho| \times \mu_G^*$. We can then deduce that $\mu_{G_0}^* = \mu_G^* - \mu_G^* = 0$. Following the first step of the proof for ratio zero, this gives in particular that

$$ \mu_{G_0}^* = \max_{v \in S} \min_{k \in [0, g-1]} \frac{P_{\max}^{G_0}(g, v) - P_{\max}^{G_0}(k, v)}{g-k} $$

or, using the property of $w^0(\rho)$, that

$$ \mu_{G_0}^* = \max_{v \in S} \min_{k \in [0, g-1]} \frac{(P_{\max}^G(g, v) - g \times \mu_G^*) - (P_{\max}^G(k, v) - k \times \mu_G^*)}{g-k} = 0 $$

We hence get

$$ \max_{v \in S} \min_{k \in [0, g-1]} \frac{P_{\max}^G(g, v) - P_{\max}^G(k, v)}{g-k} = \mu_G^* \quad \square $$

## A.2 Proof of Lemma 1

**Lemma 1.** Let $\mathcal{N} = (ST, P, E, freq)$ be a cyclic transport network with $n$ stations. Then, there exists a timed automaton $\mathcal{A}_{\mathcal{N}}$ of size in $O((4.n)^p \cdot 4^n)$ such that $\text{Runs}(\mathcal{N}) = \text{Runs}(\mathcal{A}_{\mathcal{N}})$.

Let $\mathcal{N} = (ST, P, E, freq)$ be a CTN with $n$ stations and consider a fleet of $p$ vehicles. For simplicity, we assume that in the initial configuration $C_0$, each vehicle $i$ is stopped in a station $init(i)$. For every vehicle $i \in 1..p$, we compute a priced timed automaton $\overline{M}_i = (Q_i, s_0^i, Act_i, X_i, T_i, I_i, cost_i)$ with:

- $Q_i = ST \times \{i\} \times \{A, B, C, S\}$;

- $s_0^i = init(i) \times \{i\} \times \{S\}$;

- $Act_i = \{leave_s | s \in ST\} \cup \{cruise_s | s \in ST\} \cup \{brake_s | s \in ST\}$;

- $X_i = \{x_i\} \cup \{(s_k, i, S), \delta_{min} \le x_m \le \delta_{max}, leave St_k, \{x_m\}(s_k, i, A)\}$

- $T_i = \cup \{(s_k, i, A), x_m = a_k, cruise St_k, \{x_m\}(s_k, i, C)\} \cup \{(s_k, i, C), x_m = c_k, brake St_k, \{x_m\}(s_k, i, B)\}$

$$ \cup \{(s_k, i, B), x_m = b_k, Stop St_k, \{x_m\}, (s_k \oplus 1, i, S)\} $$
$$ - I_i(q) = \begin{cases} x_m \le \delta_{max} & \text{if } q = (ST_k, \{i\}, S) \\ x_m \le a_k & \text{if } q = (ST_k, \{i\}, A) \\ x_m \le c_k & \text{if } q = (ST_k, \{i\}, C) \\ x_m \le b_k & \text{if } q = (ST_k, \{i\}, B) \end{cases} \\ \text{cost} : E_i \cup T_i \to 0 $$

<figure><img src="image_8.png" /><figcaption>Fig. 6. Automaton $\overline{M_i}$</figcaption></figure>

Then, for every station $ST_k$, $k \in 1..n$ we can build an automaton $\overline{T_k}$ that will be synchronized with $M_i$'s and recognize situations where a train brakes to stop at $St_k$ and another one leaves $St_k$. This automaton is represented Figure 7, and we set $Cost(T) = 1$.

## A.3 Proof of Theorem 4

**Theorem 4.** The threshold problem for $\mathcal{N}$ is in PSPACE.

*Proof.* We know from proposition 8 and from the remark above that the threshold problem amounts to finding a positive cycle of a path $\pi$ of length smaller that $|\mathcal{A}_{\mathcal{N},CP}|$ with $\mathcal{E}(\pi) \ge \lambda$. First, the size of $\mathcal{A}_{\mathcal{N},CP}$ is in $O(C_{max}^{n+p} \cdot (4 \cdot n)^p \cdot 4^n \cdot (2 \cdot C_{max} + 2)^{n+p} \cdot (n+p)! \cdot 2^{n+p})$. Hence each state can be encoded with a number of bits that is polynomial in the size of $\mathcal{N}$. Similarly, each state of the form $(s, r, \nu)$ has at most $T_{\mathcal{N}} + 2$ successors (the discrete transitions of $\mathcal{A}_{\mathcal{N}}$ from $s$, moves from $r$ to $r'$ with the same corner point, and moves from corner point $\nu$ to corner point
<figure><img src="image_9.png" /><figcaption>Fig. 7. The observer automaton $\overline{T}_k$ at station $St_k$ when $St_k \in ST_C$</figcaption></figure>

$\nu+1$). Note also that in $\mathcal{A}_N$ the number of transition leaving $s$ is upper bounded by the number of vehicles in the system. So, successors of each state in $(s, r, \nu)$ in $\mathcal{A}_{N,CP}$ can be enumerated and one of them randomly chosen in PSPACE. We can now apply the following procedure. We first check non-deterministically the existence of a finite path of length $\le |\mathcal{A}_{N,CP}|$ and measure its energy level. We start from $(s_0, r_0, \nu_0)$, $n=0$, $E=0$. At each step, let $x_i = (s_i, r_i, \nu_i)$ be the $i^{th}$ state visited. We choose non-deterministically a successor $x_{i+1}$ for $x_i$ and if $x_i \xrightarrow{a_i} x_{i+1}$ is an intra-region move, we set $E = E + \mathcal{E}(s_i)$. If $E > \lambda$ we can stop an claim that a run of $N$ saves more than $\lambda$ units of energy. Otherwise we set $n = n + 1$ and proceed. if $n > |\mathcal{A}_{N,CP}|$ then the exploration fails. Otherwise we continue exploration from $x_{i+1}$. This exploration requires to store the current state, an integer bounded by $|\mathcal{A}_{N,CP}|$, and an energy level smaller that $\lambda$. It hence runs in NPSPACE.

Similarly, we can explore cycles of $\mathcal{A}_{N,CP}$. We can randomly select an initial state $x_0 = (s, r, \nu)$, maintain a boolean positive originally false, the length $n$ of the explored path. At each step, we can select a successor $x_{i+1}$ for the current state $x_i$ as above, incrementing $n$. If $x_i \xrightarrow{a_i} x_{i+1}$ is an intra-region move, we set positive to true. Then if $x_{i+1} = x_0$ and positive = true, we have found a cycle with positive energy level, and stop, claiming that the energy threshold can be exceeded. If $x_{i+1} = x_0$ and positive = false the exploration fails. Last, if $n = |\mathcal{A}_{N,CP}|$ the exploration fails. Again, the exploration of cycles can be done in NPSPACE. $\square$