Load Management for Two Batteries
There are two fully charged batteries and a control system balancing the load between these batteries
to achieve longer lifetime (adapted from [1]).
The total charge $g_i$ and kinetic energy $d_i$ of the battery $i = 1, 2$
changes according to the controller’s modes: $\mathit{on}$ $\textsf{(On)}$, $\mathit{off}$ $\textsf{(Off)}$, and $\mathit{dead}$ $\textsf{(Dead)}$.
The dynamics for each battery is given as follows:
\begin{equation*}
\dot{d_i} =
\begin{cases}
L/c - 0.5 d_i & \textsf{(On)} \\
- 0.5 d_i & \textsf{(Off)} \\
0 & \textsf{(Dead)}
\end{cases}
\quad\quad\quad
\dot{g_i} =
\begin{cases}
-L & \textsf{(On)} \\
0 & \textsf{(Off)} \\
0 & \textsf{(Dead)}
\end{cases}
\end{equation*}
where $L$ is load of the battery and $c \in [0, 1]$ is a threshold constant. If the charge $g_i$ greater than $(1 - c)d_i$, the battery is dead.
Otherwise, it can be either on or off.
For simplification, we use the following dynamics:
\begin{align*}
\dot{d_1} &= 1,& \dot{g_1} &= -0.3,& \dot{d_2} &= 1,& \dot{g_2} &= -0.3 & \textsf{(}\textsf{On}_{\textsf{1}}\textsf{On}_{\textsf{2}}\textsf{)} \\
\dot{d_1} &= 0.8,& \dot{g_1} &= -0.5,& \dot{d_2} &= -0.166,& \dot{g_2} &= 0 & \textsf{(}\textsf{On}_{\textsf{1}}\textsf{Off}_{\textsf{2}}\textsf{)} \\
\dot{d_1} &= -0.166,& \dot{g_1} &= 0,& \dot{d_2} &= 0.8,& \dot{g_2} &= -0.5 & \textsf{(}\textsf{Off}_{\textsf{1}}\textsf{On}_{\textsf{2}}\textsf{)} \\
\dot{d_1} &= 0.7,& \dot{g_1} &= -7,& \dot{d_2} &= 0,& \dot{g_2} &= 0 & \textsf{(}\textsf{On}_{\textsf{1}}\textsf{Dead}_{\textsf{2}}\textsf{)} \\
\dot{d_1} &= 0,& \dot{g_1} &= 0,& \dot{d_2} &= 0.7,& \dot{g_2} &= -7 & \textsf{(}\textsf{Dead}_{\textsf{1}}\textsf{On}_{\textsf{2}}\textsf{)} \\
\dot{d_1} &= 0,& \dot{g_1} &= 0,& \dot{d_2} &= 0,& \dot{g_2} &= 0 & \textsf{(}\textsf{Dead}_{\textsf{1}}\textsf{Dead}_{\textsf{2}}\textsf{)}
\end{align*}
Figure [1] shows a hybrid automaton of the battery system. The controller starts to use both batteries as an energy source, selecting at least one battery until both of them become dead.
Figure 1: A hybrid automaton of the battery system
Table [1] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $\lozenge_{[4,10]} (d_2 \geq 4 \rightarrow \square_{[4,10]} (b_2 = 2))$ | For some time point in interval $[4, 10]$, if $d_2$ is greater than or equal to $4$, then $b_2$ is always equal to $2$ during time interval $[4, 10]$. |
| $\textsf{f2}$ | $(\lozenge_{[1,5]} g_2 \leq 5) \mathbf{R}_{[5,20]} (d_2 \geq 4.5)$ | Within time interval $[5,20]$, $d_2$ is greater than or equal to $4.5$ until $g_2$ is less than or equal to $5$ for some time point in interval $[1, 5]$. |
| $\textsf{f3}$ | $\square_{[0,0.25]}(g_2>4\rightarrow\lozenge_{[0,0.25]}(d_2>1))$ | During the first 0.25 time units, whenever $g_2>4$, $d_2>1$ must hold within the following 0.25 time units. |
Table 1: STL properties for the battery system
An STLmc Input Model
We use the STLmc language to describe the battery model (battery.model) as follows:
real b1; real b2;
[0, 10] g1; [0, 10] g2;
[0, 10] d2; [0, 10] d1;
# state
# 1: ON, 2: OFF, 3: DEAD
{ mode: b1 = 1; b2 = 1;
inv: g1 >= 0.5; g2 >= 0.5;
flow: d/dt[d1] = 1; d/dt[d2] = 1;
d/dt[g1] = -0.3; d/dt[g2] = -0.3;
jump: g1 >= 2 => (and (b1' = 1) (b2' = 2)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
g1 <= 1 => (and (b1' = 3) (b2' = 1)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
g2 >= 2 => (and (b1' = 2) (b2' = 1)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
g2 <= 1 => (and (b1' = 1) (b2' = 3)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
}
{ mode: b1 = 1; b2 = 2;
inv: g1 >= 0.5;
flow: d/dt[d1] = 0.8; d/dt[d2] = -0.166;
d/dt[g1] = -0.5; d/dt[g2] = 0;
jump: g2 >= 2 => (and (b1' = 2) (b2' = 1)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
g1 <= 1 => (and (b1' = 3) (b2' = 1)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
}
{ mode: b1 = 2; b2 = 1;
inv: g2 >= 0.5;
flow: d/dt[d1] = -0.166; d/dt[d2] = 0.8;
d/dt[g1] = 0; d/dt[g2] = -0.5;
jump: g1 >= 2 => (and (b1' = 1) (b2' = 2)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
g2 <= 1 => (and (b1' = 1) (b2' = 3)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
}
{ mode: b1 = 3; b2 = 1;
inv: g1 <= 1; g2 >= 0.5;
flow: d/dt[d1] = 0; d/dt[d2] = 0.7;
d/dt[g1] = 0; d/dt[g2] = -7;
jump: g2 <= 1 => (and (b1' = 3) (b2' = 3)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
}
{ mode: b1 = 1; b2 = 3;
inv: g1 >= 0.5; g2 <= 1;
flow: d/dt[d1] = 0.7; d/dt[d2] = 0;
d/dt[g1] = -7; d/dt[g2] = 0;
jump: g1 <= 1 => (and (b1' = 3) (b2' = 3)
(d1' = d1) (d2' = d2)
(g1' = g1) (g2' = g2));
}
{ mode: b1 = 3; b2 = 3;
inv:
flow: d/dt[d1] = 0; d/dt[d2] = 0;
d/dt[g1] = 0; d/dt[g2] = 0;
jump:
}
init: b1 = 1; b2 = 1;
0 <= d1; d1 <= 0.1; 8.4 <= g1; g1 <= 8.5;
0 <= d2; d2 <= 0.1; 7.4 <= g2; g2 <= 7.5;
proposition:
# bound: 20, timebound: 30, solver: yices
goal:
[f1]: <>[4, 10] ((d2 >= 4) -> [][4, 10] (b2 = 2)); # threshold: 0.1
[f2]: (<>[1, 5] g2 <= 5) R[5, 20] (d2 >= 4.5); # threshold: 3.5
[f3]: [][0, 0.25] (g2 > 4 -> <>[0, 0.25] d2 > 1); # threshold: 0.1
Run
The following settings and example measurements use STLmc. A counterexample is a trace below the specified robustness threshold; a satisfied result applies only to the bounds shown. Timings vary by machine.
stlmc ./battery.model -bound 20 -time-bound 30 -threshold 3.5 -goal f2 -solver yices -visualize -logic QF_LRA
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
8 | 30 | 30 | 0.1 | yices | one-step | 34.222 | satisfied up to bound 8 |
f2 |
20 | 30 | 30 | 3.5 | yices | one-step | 42.373 | violated at bound 8 |
f3 |
20 | 1 | 1 | 0.1 | yices | one-step | 4.541 | violated at bound 0 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Visualization
The plot shows the f2 counterexample for battery.model
with the settings above. Its sampled robustness is compared with the threshold.
Reference
[1]. Fox, M., Long, D., & Magazzeni, D. (2012). Plan-based Policies for Efficient Multiple Battery Load Management. J. Artif. Intell. Res., 44, 335-382 (arXiv).