Two Networked Thermostats
Consider two rooms interconnected by an open door. The temperature $x_i$ of each room, $i = 0, 1$, changes depending on the heater’s mode $q_i \in \{\textsf{On}, \textsf{Off}\}$ and the temperature of the other room (adapted from [1,2]). We consider a nonlinear polynomial dynamics model and a nonlinear ODE dynamics model.
Nonlinear Polynomial Dynamics. The dynamics of $x_1$ and $x_2$ are given as follows:
\begin{align*}
\dot{x}_1 &= \begin{cases}
0.05 t^2 + 0.5t + x_1(0) & \textsf{(On)} \\
-0.0175t^2 - 0.35t + x_1(0) & \textsf{(Off)}
\end{cases}\\
\dot{x}_2 &= \begin{cases}
0.06 t^2 + 0.6t + x_2(0) & \textsf{(On)} \\
-0.275t^2 - 0.55t + x_2(0) & \textsf{(Off)}
\end{cases}
\end{align*}
where $t$ and $x_i(0)$ are time and initial value after a transition, respectively.
Table [1] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $(\square_{[2,10]} x_2 > 17) \mathbf{U}_{[1,4]} (x_1 \geq 22)$ | During the time interval $[2,10]$, $x_2$ is greater than $17$, until $x_1$ is greater than or equal to $22$ for time interval $[1, 4]$. |
| $\textsf{f2}$ | $\lozenge_{[0,5]} (x_1 > 22 \to \square_{[2,5)} x_1 < 18)$ | For some time point in interval $[0, 5]$, if $x_1$ is greater than $22$ then $x_1$ is always less than $18$ for time interval $[2, 5)$. |
| $\textsf{f3}$ | $\lozenge_{[0,10]} (x_2 \leq 25) \mathbf{R}_{[0,\infty)} (x_0 - x_1 \leq -3))$ | For the first $5$ time units, $x_0 - x_1$ is less than or equal to $-3$ until $x_0 - x_1$ is greater than or equal to $4$ within time interval $[0, \infty)$. |
Table 1: STL properties for polynomial model
Nonlinear ODE Dynamics. The continuous dynamics of $x_i$ for each mode can be specified as the ODEs: $\dot{x_i} = K_i(h_i-(c_ix_i-d_ix_{1-i}))$ for $\textsf{On}$, and $\dot{x_i} = -K_i(c_ix_i-d_ix_{1-i})$ for $\textsf{Off}$, where $K_i, h_i, c_i, d_i$ are determined by the size of the room, the heater’s power, and the size of the door.
Figure [1] shows a hybrid automaton of thermostat controllers. Initially, both heaters are off and the temperatures are between $18$ and $22$. The jumps between modes then define a control logic to keep the temperatures within a certain range with only one heater on.
Figure 1: A hybrid automaton of thermostat controllers
Table [1] shows the STL properties.
| Label | STL formula | Description |
|---|---|---|
| $\textsf{f1}$ | $\lozenge_{[0,3]} ((x_0 \geq 13) \mathbf{U}_{[1,\infty)} (x_1 < 22))$ | For some time point in interval $[0,3]$, $x_0$ is greater than or equal to $13$, until $x_1$ is less than $22$ during time interval $[1, \infty)$. |
| $\textsf{f2}$ | $\square_{[2,4]} ((x_0 - x_1 \geq 4) \to \lozenge_{[3,10]} (x_0 - x_1 \leq -3))$ | During time interval $[2, 4]$, if $x_0 - x_1$ is greater than or equal to $4$ then $x_0 - x_1$ is less than or equal to $-3$ for some time point in time interval $[3, 10]$. |
| $\textsf{f3}$ | $\square_{[0,10)} ((x_0 - x_1 \geq 4) \mathbf{R}_{[0,\infty)} (x_0 - x_1 \leq -3))$ | For the first $5$ time units, $x_0 - x_1$ is less than or equal to $-3$ until $x_0 - x_1$ is greater than or equal to $4$ within time interval $[0, \infty)$. |
Table 2: STL properties for nonlinear ODE model
An STLmc Input Model
We use the STLmc language to describe the thermostat model (therm-ode.model) as follows:
int on0; int on1;
[10, 35] x0; [10, 35] x1;
const k0 = 0.015; const k1 = 0.045;
const h0 = 100; const h1 = 200;
const c0 = 0.98; const c1 = 0.97;
const d0 = 0.01; const d1 = 0.03;
{ mode: on0 = 0; on1 = 0;
inv: x0 > 10; x1 > 10;
flow:
d/dt[x0] = - k0 * (c0 * x0 - d0 * x1);
d/dt[x1] = - k1 * (c1 * x1 - d1 * x0);
jump:
x0 <= 17 => (and (on0' = 1) (on1' = on1)
(x0' = x0) (x1' = x1));
x1 <= 16 => (and (on1' = 1) (on0' = on0)
(x0' = x0) (x1' = x1));
}
{ mode: on0 = 0; on1 = 1;
inv: 10 < x0; x1 < 30;
flow:
d/dt[x0] = - k0 * (c0 * x0 - d0 * x1);
d/dt[x1] = k1 * (h1 - (c1 * x1 - d1 * x0));
jump:
x0 <= 17 => (and (on0' = 1) (on1' = 0)
(x0' = x0) (x1' = x1));
x1 >= 26 => (and (on1' = 0) (on0' = on0)
(x0' = x0) (x1' = x1));
}
{ mode: on0 = 1; on1 = 0;
inv: x0 < 30; x1 > 10;
flow:
d/dt[x0] = k0 * (h0 - (c0 * x0 - d0 * x1));
d/dt[x1] = - k1 * (c1 * x1 - d1 * x0);
jump:
x1 <= 16 => (and (on0' = 0) (on1' = 1)
(x0' = x0) (x1' = x1));
x0 >= 25 => (and (on0' = 0) (on1' = on1)
(x0' = x0) (x1' = x1));
}
init: on0 = 0; 18 <= x0; x0 <= 22;
on1 = 0; 18 <= x1; x1 <= 22;
proposition:
[p1]: x0 - x1 >= 4; [p2]: x0 - x1 <= -3;
goal:
# bound: 5, timebound: 30, solver: dreal
[f1]: <>[0, 3](x0 >= 13 U[0, inf) x1 <= 22); # threshold: 1.0, time-horizon: 7
[f2]: [][2, 4](p1 -> <>[3, 10] p2); # threshold: 2.0, time-horizon: 30
[f3]: [][0,10] (x0 > 23 R[0,inf) p1); # threshold: 2.0, time-horizon: 7
Run
For the input model, we use a time bound $\tau = 30$ and a discrete bound $N = 5$ as input parameters. Because the model has nonlinear dynamics, we use $\textsf{dReal}$ for an underlying solver with the algorithm $\textsf{2-step}$. For efficient model checking, we also use the $\textsf{parallel}$ option. For the formulas $\textsf{f1}$, $\textsf{f2}$, and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 1.0$, $\epsilon_2 = 2.0$, and $\epsilon_3 = 2.0$, respectively.
STLmc finds counterexamples for $\textsf{f2}$ and $\textsf{f3}$, while $\textsf{f1}$ is safe. The following shows the command finding a counterexample for the STL formula $\textsf{f2}: \square_{[2, 4]}((x_0 - x_1 \geq 4) \rightarrow \lozenge_{[3, 10]} (x_0 - x_1 \leq -3))$ at bound $2$ with respect to $\epsilon_2=2$ in $8$ seconds using dReal.
./stlmc ./therm-ode.model -bound 5 -time-bound 30 -threshold 2 -goal f2 -solver dreal -two-step -parallel -time-horizon 30 -visualize
| Label | $\epsilon$ | $| \Psi |$ | Time | Result | $k$ | Alg. | #$\pi$ |
|---|---|---|---|---|---|---|---|
| $\textsf{f1}$ | $1.0$ | $1.2$ | $817$ | $\top$ | - | $\textsf{2-step}$ | $3,646$ |
| $\textsf{f2}$ | $2.0$ | $0.7$ | $7.46$ | $\bot$ | $2$ | $\textsf{2-step}$ | $47$ |
| $\textsf{f3}$ | $2.0$ | $1.2$ | $59.3$ | $\bot$ | $4$ | $\textsf{2-step}$ | $212$ |
Table.2: Verification results of the STL properties for thermostat
Visualization
Fig.2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 2.0$)
Figure [2] shows the visualization graphs for $\textsf{f2} = \square_{[2, 4]} (x_0 - x_1 \geq 4 \rightarrow \lozenge_{[3, 10]} (x_0 - x_1 \leq -3))$ with the subformulas:
\begin{align*} \textsf{f2}_{\textsf{1}} &= x_0 - x_1 \geq 4 \rightarrow \lozenge_{[3, 10]} (x_0 - x_1 \leq -3) \qquad \textsf{f2}_{\textsf{2}} = \neg (x_0 - x_1 \geq 4) \\\ \textsf{f2}_{\textsf{3}} &= \lozenge_{[3, 10]} (x_0 - x_1 \leq -3) \qquad \textsf{f2}_{\textsf{4}} = x_0 - x_1 \leq -3 \qquad \textsf{f2}_{\textsf{5}} = x_0 - x_1 \geq 4 \end{align*}
The robustness degree of $\textsf{f2}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f2}_{\textsf{1}}$ goes below $\epsilon$ in the interval $[2, 4]$, which is because both the degrees of $\textsf{f2}_{\textsf{2}}$ and $\textsf{f2}_{\textsf{3}}$ are less than $\epsilon$ in $[2, 4]$. The robustness degree of $\textsf{f2}_{\textsf{3}}$ is less than $\epsilon$ in $[2, 4]$, since the robustness degree of $\textsf{f2}_{\textsf{4}}$ is less than $\epsilon$ in $[5, 14] = [2, 4] + [3, 10]$.
Reference
[1]. K. Bae and S. Gao, “Modular SMT-based analysis of nonlinear hybrid systems,” 2017 Formal Methods in Computer Aided Design (FMCAD), 2017, pp. 180-187, doi: 10.23919/FMCAD.2017.8102258.
[2]. Henzinger T.A. (2000) The Theory of Hybrid Automata. In: Inan M.K., Kurshan R.P. (eds) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol 170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59615-5_13