Two Networked Watertank Systems
Two water tanks are connected by pipes, where water flows from one tank to another (adpated from [1]).
The water level $x_i$ of tank $i = 0,1$ is controlled by its pump.
There are two pump modes: $\textsf{On}$ and $\textsf{Off}$.
Each pump changes its mode according to the water level of
its tank and the other water tank.
The continuous dynamics of $x_i$ is defined as follows:
\begin{equation*}
\dot{x}_i =
\begin{cases}
q_i + a \sqrt{2g} (\sqrt{x_{i - 1}} - \sqrt{x_i}) & \textsf{(On)} \\
a \sqrt{2g} (\sqrt{x_{i - 1}} - \sqrt{x_i}) & \textsf{(Off)}
\end{cases}
\label{water}
\end{equation*}
where $a$ and $q_i$ depend on the width of the pipe and the pump’s power, and $g$ is the standard gravity constant.
Figure [1] shows a hybrid automaton $H_1$ of one water tank (the other component is similar).
Figure 1: A hybrid automaton of one water tank controller $H_1$
For simplicity, we consider the following dynamics to obtain linear flow conditions.
\begin{equation*}
\dot{x}_0 =
\begin{cases}
0.9 & \textsf{(On)}\\
-0.8 & \textsf{(Off)}
\end{cases}
%%
\quad\quad\quad
%%
\dot{x}_1 =
\begin{cases}
1 & \textsf{(On)}\\
-0.6 & \textsf{(Off)}
\end{cases}
\end{equation*}
Table [1] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $\square_{[1,3]} ((x_0 \leq 7) \mathbf{R}_{[1,10]} (x_1 \leq 3))$ | For time interval $[1,3]$, $x_1$ is less than or equal to $3$, until $x_0$ is less than or equal to $7$ for time interval $[1,10]$. |
| $\textsf{f2}$ | $(\lozenge_{[1,10]} (x_1 < 5.5)) \mathbf{U}_{[2,5]} (x_0 \geq 5)$ | Within time interval $[1, 10]$, $x_1$ is less than $5.5$, until $x_0$ is greater than or equal to $5$ in time interval $[2, 5]$. |
| $\textsf{f3}$ | $(\lozenge_{[4,10]} (x_0 \geq 4 \rightarrow \square_{[2, 5]} x_1 \leq 2)$ | For some time point in interval $[4, 10]$, if $x_0$ is greater than or equal to $4$ then $x_1$ is always less than or equal to $2$ during time interval $[2,5]$. |
Table 1: STL properties for watertank
An STLmc Input Model
We use the STLmc language to describe the watertank model (water.model) as follows:
bool a; bool b;
[0, 10] x1; [0, 10] x2;
{ mode: a = false; b = false;
inv: x1 >= 1; x2 >= 1;
flow: d/dt[x1] = -0.8;
d/dt[x2] = -0.6;
jump: x1 <= 2 => (and a' (not b')
(x1' = x1) (x2' = x2));
x2 <= 3 => (and (not a') b'
(x1' = x1) (x2' = x2));
x1 <= 2 => (and a' b' (x1' = x1)
(x2' = x2));
x2 <= 3 => (and a' b' (x1' = x1)
(x2' = x2));
}
{ mode: a = false; b = true;
inv: x1 >= 1; x2 <= 9;
flow: d/dt[x1] = -0.8;
d/dt[x2] = 1;
jump: x2 >= 6 => (and (not a') (not b')
(x1' = x1) (x2' = x2));
x1 <= 2 => (and a' b' (x1' = x1)
(x2' = x2));
x2 >= 6 => (and a' (not b')
(x1' = x1) (x2' = x2));
x1 <= 2 => (and a' (not b')
(x1' = x1) (x2' = x2));
}
{ mode: a = true; b = false;
inv: x1 <= 8; x2 >= 1;
flow: d/dt[x1] = 0.9;
d/dt[x2] = -0.6;
jump: x1 >= 5 => (and (not a') (not b')
(x1' = x1) (x2' = x2));
x2 <= 3 => (and a' b' (x1' = x1)
(x2' = x2));
x1 >= 5 => (and (not a') (b') (x1' = x1)
(x2' = x2));
x2 <= 3 => (and (not a') b' (x1' = x1)
(x2' = x2));
}
{ mode: a = true; b = true;
inv: x1 <= 9; x2 <= 9;
flow: d/dt[x1] = 0.9;
d/dt[x2] = 1;
jump: x1 >= 5 => (and (not a') b' (x1' = x1)
(x2' = x2));
x2 >= 6 => (and a' (not b') (x1' = x1)
(x2' = x2));
x1 >= 5 => (and (not a') (not b') (x1' = x1)
(x2' = x2));
x2 >= 6 => (and (not a') (not b') (x1' = x1)
(x2' = x2));
}
init: not(a); 4.4 <= x1; x1 <= 4.5;
not(b); 5.9 <= x2; x2 <= 6;
proposition:
# bound: 20, timebound: 20, solver: yices
goal:
[f1]: [][1, 3]((x1 <= 7) R[1, 10] (x2 <= 3)); # threshold: 2.5
[f2]: (<>[1, 10) x2 < 5.5) U[2, 5] (x1 >= 5); # threshold: 0.1
[f3]: <>[4, 10] (x1 >= 4 -> [][2, 5] x2 <= 2); # threshold: 0.01
Run
For the input model, we use a time bound $\tau = 20$ 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 = 2.5$, $\epsilon_2 = 0.1$, and $\epsilon_3 = 0.01$, respectively.
The formulas $\textsf{f1}$ and $\textsf{f3}$ are safe, while the following command found a counterexample of the STL formula $\textsf{f2}: (\lozenge_{[1,10)} (x_1 < 5.5)) \mathbf{U}_{[2,5]} (x_0 \geq 5)$ at bound $4$ with respect to $\epsilon_2=0.1$ in $5$ seconds using yices.
stlmc ./water.model -bound 20 -time-bound 20 -threshold 0.1 \
-goal f2 -solver yices -visualize
| Label | $\epsilon$ | $| \Psi |$ | Time | Result | $k$ | Alg. |
|---|---|---|---|---|---|---|
| $\textsf{f1}$ | $2.5$ | $18.8$ | $26.2$ | $\top$ | - | $\textsf{1-step}$ |
| $\textsf{f2}$ | $0.1$ | $1.9$ | $4.22$ | $\bot$ | $4$ | $\textsf{1-step}$ |
| $\textsf{f3}$ | $0.01$ | $11.2$ | $20.2$ | $\top$ | - | $\textsf{1-step}$ |
Table 2: Verification results of the STL properties for watertank
Visualization
Figure 2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 0.1$)
Figure [2] shows the visualization graphs generated for $\textsf{f2} = (\lozenge_{[1, 10)} (x_1 < 5.5)) \mathbf{U}_{[2, 5]} x_0 \geq 5$ with the subformulas: \begin{align*} \textsf{f2}_{\textsf{1}} = \lozenge_{[1,10)} (x_1 < 5.5) \qquad \textsf{f2}_{\textsf{2}} = x_0 \geq 5 \qquad \textsf{f2}_{\textsf{3}} = x_1 < 5.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}}$ goes below $\epsilon$ in the interval $[2, 5]$.
Reference
[1]. Raisch J., Klein E., Meder C., Itigin A., O’Young S. (1999) Approximating Automata and Discrete Control for Continuous Systems — Two Examples from Process Control. In: Antsaklis P., Lemmon M., Kohn W., Nerode A., Sastry S. (eds) Hybrid Systems V. HS 1997. Lecture Notes in Computer Science, vol 1567. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49163-5_16