Networked Thermostat Model

We consider a network of classical thermostat hybrid automata. A number of rooms are interconnected by open doors. The temperature of each room is separately controlled by its own thermostat controller that turns the heater on and off.

Dynamics

The temperature of each room depends on the mode \(m \in \{on, off\}\) of the heater and the temperatures of the other rooms. E.g., for three rooms \(I = \{0,1,2\}\), the temperature \(x_i\) of room \(i \in I\) changes according to the ordinary differential equations:

\begin{aligned} \dot{x}_i &= K_i (h_i - ((1- 2 c) x_i + c x_{i-1} + c x_{i+1})) &&\mbox{if}\; m_i = m_\texttt{on} \\
\dot{x}_i &= - K_i ((1- 2 c) x_i + c x_{i-1} + c x_{i+1}) && \mbox{if}\; m_i = m_\texttt{off} \end{aligned}

where \(K_i, h_i \in \mathbb{R}\) are constants depending on the size of room \(i\) and the heater’s power, respectively, and \(c \in \mathbb{R}\) is determined by the size of the open door.

In this model, every thermostat controller synchronously performs its transitions for each period \(T = 1\,\mathrm{s}\). In each transition, a controller turns on the heater if \(x_i \leq T_m\), and turns it off if \(x_i > T_M\).

The safety property is that the temperature of each room is in the range \(I = [T_m - \eta, T_M + \eta]\) for a certain \(\eta > 0 \). That is, \(\mathit{safe}(T_M,T_m,\eta) = \wedge_i x_i \in I\)

Bounded Reachability

We first consider the cases of networks of two and three thermostats with the parameters \(K_1 = 0.015\), \(K_2 = 0.045\), \(K_3 = 0.03\), \(h_1 = 100\), \(h_2 = 200\), \(h_3 = 300\), \(k_1^2 = k_2^1 = 0.01\), \(k_2^3 = k_3^2 = 0.05\) and \(k_1^3 = k_3^1 = 0.02\).

We have performed bounded model checking up to \(k = 5\) from the initial condition \(\wedge_i 19 < x_i < 21\), for \(\mathit{safe}_t = \mathit{safe}(20,20,5)\) (the reachability of \(\neg\mathit{safe}_t\) unsat) and \(\mathit{safe}_f = \mathit{safe}(20,20,1)\) (the reachability of \(\neg\mathit{safe}_f\) sat) using a vertion 2 of dReal. We set a timeout of 30 hours for the experiments.

Files

To generate SMT files for this model in the new/standard encodings, we have developed a simple python script. For example, for the unsat case of the double thermostat model with bound \(k = 2\), we can run the following commands to generate the SMT file using the new encoding and check its satisfiability using dReal provided that the library file gen.py is in the same directory:

python thermostat-double-p.py 2 > thermostat-double-p_2.smt2
dReal thermostat-double-p_2.smt2

For the dReach scripts, we use the option -k N -l N to set both lower and upper bound to \(N\). For example, for the double thermostat dReach model, we can set \(N = 2\) using the following command:

dReach -k 2 -l 2 thermostat-double.drh

The following are the python scripts (to generate SMT files) and the dReach models for the networked thermostat models.

• SMT generation script: gen.py
• Two networked thermostats
  • Unsat: New encoding, Standard encoding, dReach script
  • Sat: New encoding, Standard encoding, dReach script
• Three networked thermostats
  • Unsat: New encoding, Standard encoding, dReach script
  • Sat: New encoding, Standard encoding, dReach script

Inductive analysis

We have performed inductive analysis to verify that the property \(\mathit{safe}(20,20,9)\) holds at the end \(\tau > 0.99\) of each period.

Files

The same python scripts are used with \(k = 1\) for inductive analysis. The following are the python scripts (to generate SMT files) for the networked thermostat models.

• Two networked thermostats
  • Inductive: New encoding, Standard encoding
• Three networked thermostats
  • Inductive: New encoding, Standard encoding

Compositional analysis

We have then verified the safety property \(\forall t.\; x_i \in I\) for any number of interconnected thermostat controllers by inductive and compositional analysis. For a subinterval \(I’ = [T_m - \eta’, T_M + \eta’]\subseteq I\), provided that both \(x_{i-1} \in I\) and \(x_{i+1} \in I\) always hold, we show that \(x_i \in I’\) is an inductive condition, and \(x_i \in I\) always holds if \(x_i \in I’\) at the beginning of each round.

In this analysis, we also take into account local clock skews (bounded by \(\epsilon > 0 \), input sampling time \(t_I\), and actuator response time \(t_R\) for each thermostats. That is, each controller begins its \(i\)-th period at time \(u_0 \in (iT - \epsilon, iT + \epsilon)\), reads the current temperature at time \(u_0 + t_I\), and changes the switch of the thermostat at time \(u_0 + t_R\).

We have used the parameters \(K = 0.015\), \(h = 100\), \(c = 0.01\), \(T_M = 21\), \(T_m = 19\), \(\eta = 3\), and \(\eta’ = 2\). For \(\epsilon = 2\,\mathrm{ms}\), \(t_I = 10\,\mathrm{ms}\), and \(t_R = 200\,\mathrm{ms}\), we have proved the compositional safety property for any number of thermostats, in 2.6 seconds using dReal3 with precision \(\delta = 0.001\).

Files

The following SMT2 files contains the SMT formulas used for the compositional analysis. Both are negated formulas for compositional conditions, and we check the unsatisfiability of those formulas.

The first SMT file contains the negation of the formula stating that if \(x_k \in I’\) at the beginning of each period, then \(x_k \in I’\) at the end of the period, provided that both \(x_{i-1} \in I\) and \(x_{i+1} \in I\) always hold (given by user-defined precision in dReal3). The following three SMT files contain the negations of the formulas stating that \(x_i \in I\) always holds for each stage if \(x_i \in I’\) at the beginning of each round. The last SMT2 file shows an counterexample of the compositional condition when \(\epsilon = 150\,\mathrm{ms}\).

• compositional condition
• sampling stage
• response stage
• wait stage
• compositional counterexample