We explain how to use our tool to analyze hybrid systems using the two networked thermostats model. The tutorial consists of the following sections:
- Prerequisite
- Two Networked Thermostat Systems
- STLmc Input Model
- Running the STLmc Tool
- Analyzing the Counterexample
Prerequisite
Before the tutorial, please download the STLmc tool, following the instructions.
The tool is available for Linux (64-bit) and macOS (64-bit).
Two Networked Thermostat Systems
We consider the following hybrid automaton (Figure [1]) with three STL properties (Table [1]). To see the detailed explanation of the model and properties, please refer to this page.
Fig.1: A hybrid automaton of thermostat controllers
| Label | STL formula |
|---|---|
| $\textsf{f1}$ | $\lozenge_{[0,3]} ((x_0 \geq 13) \mathbf{U}_{[1,\infty)} (x_1 < 22))$ |
| $\textsf{f2}$ | $\square_{[2,4]} ((x_0 - x_1 \geq 4) \to \lozenge_{[3,10]} (x_0 - x_1 \leq -3))$ |
| $\textsf{f3}$ | $\square_{[0,10)} ((x_0 - x_1 \geq 4) \mathbf{R}_{[0,\infty)} (x_0 - x_1 \leq -3))$ |
Table.1: STL properties for thermostat
STLmc Input Model
The following code shows the STLmc input model of the above two thermostat controllers:
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
We use the STLmc modelling language to specify the model and its properties. To see more detailed explanation of the langauge, please refer to our technical report or this page.
Running the STLmc Tool
We can run the STLmc tool for the $\textsf{f2}$ formula of the thermostat model with a time bound $\tau = 30$, a discrete bound $N = 5$, and a threshold $\epsilon_2 = 2.0$ as input parameters as follows:
./stlmc ./therm.model -bound 5 -time-bound 30 -threshold 2 \
-goal f2 -solver dreal -two-step -parallel -time-horizon 30 -visualize
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 use the $\textsf{parallel}$ option. For the formulas $\textsf{f1}$ and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 1.0$ and $\epsilon_3 = 2.0$, respectively.
We can run the STLmc tool using the following command:
./stlmc [model file] [option1] [option2] ...
To see more command line options, use ./stlmc -h or refer to this page
Analyzing the Counterexample
The formula $\textsf{f2}$ is violated. The following command generates visualization graphs from the extra data for the visualization.
./stlmc-vis ./therm.counterexample -output html
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]$.