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
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 ./water.model -bound 20 -time-bound 20 -threshold 0.1 -goal f2 -solver yices -visualize -logic QF_LRA
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
20 | 20 | 20 | 2.5 | yices | one-step | 35.194 | satisfied up to bound 20 |
f2 |
20 | 20 | 20 | 0.1 | yices | one-step | 5.972 | violated at bound 7 |
f3 |
20 | 20 | 20 | 0.01 | yices | one-step | 84.216 | satisfied up to bound 20 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Visualization
The plot shows the f2 counterexample for water.model
with the settings above. Its sampled robustness is compared with the threshold.
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