Thermostat with controller


type # of discrete variables # of clocks # of rest variables # of controller modes # of plant modes # of jumps
original 0 0 8 6 2 18
timed 0 1 7 6 2 18
discrete 5 0 3 6 2 18
timed & discrete 5 1 7 6 2 18
Type Continuous dynamics Guards & Invariants Resets
hybrid linear polynomial hyperplane & half-space constant


SpaceEx spaceEx_files
HyPro hypro_files

Model description

In this benchmark a heater with a thermostat controller is modelled. Initially, the temperature is $\temperature = 20^\circ C$ and the heater is on.  The controller keeps the temperature between $16^\circ C$ and $24^\circ C$.  The heater is switched off if the temperature rises above $23^\circ C$ and it is switched on at a
temperature below $18^\circ C$. Adding a controller to the model introduces new variables for the low and high temperature sensors in the controller, a variable for the actuator (heater) state in the plant and the controller, and a variable to store the controller mode. Additionally, we introduce a new clock for the cycle time of the PLC. The global time horizon is 10 seconds and the PLC cycle time is 0.5 seconds.

The dynamics of the temperature is defined by the following differential equations:

    \[\dot{T} = \left\{ \begin{array}{l l} $-0.1*T+ 3 & \quad \text{if the heater is on}\\ $-0.1*T$ & \quad \text{if the heater is off}\\ \end{array} \right. \]

Reachability settings

We consider an initial set of

  • T = 20
  • \text{low} = 1
  • \text{high} = 0
  • H = H\_{\text{plc}} = 1
  • \text{nextSfcLoc} = 1
  • \text{cycle\_time} = 0
  • \text{global\_time} = 0

and the starting location \text{clock\_\_switch\_on\_in\_\_comm}, a time horizon $\text{global\_time}=10s$, a PLC cycle duration of $\delta = 0.5s$, and a time step $r=0.01s$ .


Fig.1 shows the flowpipes computed for the above-mentioned parameters using a) Hypro and b) SpaceEx.

Figure 1: Flowpipe of the thermostat system with controller


[1] J. Nellen. Analysis and synthesis of hybrid systems in engineering applications. PhD Thesis, RWTH Aachen University, 2016.

[2] S. Schupp et al.. Divide and conquer: Variable set separation in hybrid systems reachability analysis. Submitted to (QAPL’17).