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_{[4,14]}(g_2 > 4 \rightarrow \lozenge_{[0, 10]} (d_2 > 1))$	$g_1$ is greater than 1 for $4$ time units, until $d_1$ is greater than or equal to $2$

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]: [][4, 14] (g2 > 4 -> <>[0, 10] d2 > 1);       # threshold: 0.1

---

Run

For the input model, we use a time bound $\tau = 30$ and a discrete bound $N = 20$ as input parameters. Because the model has linear dynamics, we use $\textsf{yices}$ for an underlying solver with the default algorithm $\textsf{1-step}$. For the formulas $\textsf{f1}$, $\textsf{f2}$, and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 0.1$, $\epsilon_2 = 3.5$, and $\epsilon_3 = 0.1$, respectively.

The formula $\textsf{f1}$ is safe, while STLmc finds counterexamples for the two formulas: $\textsf{f2}$ and $\textsf{f3}$. The following command finds a counterexample of the formula $\textsf{f2}: (\lozenge_{[1,5]} g_2 \leq 5) \mathbf{R}_{[5,20]} (d_2 \geq 4.5)$ at bound $5$ with respect to $\epsilon_2=3.5$ in $6$ seconds using yices.

stlmc ./battery.model -bound 20 -time-bound 30 -threshold 3.5 \
        -goal f2 -solver yices -visualize

Label	$\epsilon$	$| \Psi |$	Time	Result	$k$	Alg.
$\textsf{f1}$	$0.1$	$12.9$	$137$	$\top$	-	$\textsf{1-step}$
$\textsf{f2}$	$3.5$	$2.76$	$5.71$	$\bot$	$5$	$\textsf{1-step}$
$\textsf{f3}$	$0.1$	$3.8$	$22.1$	$\bot$	$8$	$\textsf{1-step}$

Table 2: Verification results of the STL properties for the battery system

---

Visualization

Figure 2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 3.5$)

Figure [2] shows the visualization graphs generated for $\textsf{f2} = (\lozenge_{[1, 5]} g_2 \leq 5) \mathbf{R}_{[5, 20]} d_2 \geq 4.5$ with the subformulas:

\begin{align*} \textsf{f2}_{\textsf{1}} = \lozenge_{[1,5]} (g_2 \leq 5) \qquad \textsf{f2}_{\textsf{2}} = d_2 \geq 4.5 \qquad \textsf{f2}_{\textsf{3}} = g_2 \leq 5 \end{align*}

The robustness degree of $\textsf{f2}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f2}_{\textsf{2}}$ is always less than $\epsilon$ in the interval $[5, 20]$.

---

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