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\geq13)\mathbf{U}_{[0,\infty)}(x_1\leq22))$ | At some time in $[0,3]$, $x_1\leq22$ holds then or later, with $x_0\geq13$ until that time. |
| $\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>23)\mathbf{R}_{[0,\infty)}(x_0-x_1\geq4))$ | At every time in $[0,10]$, the metric release condition relates $x_0-x_1\geq4$ to $x_0>23$. |
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
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 ./therm-ode.model -bound 5 -time-bound 14 -threshold 2 -goal f2 -solver dreal -time-horizon 14 -visualize -path-strategy explicit -ode-order 10 -smt-preprocess -two-step -parallel -parallel-core 4
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
1 | 5 | 5 | 1 | dreal | one-step | 20.961 | satisfied up to bound 1 |
f2 |
5 | 14 | 14 | 2 | dreal | two-step | 0.851 | violated at bound 1 |
f3 |
5 | 12 | 12 | 2 | dreal | two-step | 0.152 | violated at bound 0 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Use the shown two-step parallel options for f2 and f3; omit
-two-step -parallel -parallel-core 4 for f1.
Visualization
The plot shows the f2 counterexample for therm-ode.model
with the settings above. Its sampled robustness is compared with the threshold.
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