Linear Thermostat

Linear Thermostat [1] is a simple hybrid system simulating the temperature control system of the building.

Dynamics

MODE 0

$$\left \{ \begin{array}{l} \dot x = 40-0.5 x \end{array} \right.$$

invariant

$$x \leq 75$$

MODE 1

$$\left \{ \begin{array}{l} \dot x = 30-0.5 x \end{array} \right.$$

invariant

$$x \geq 65$$

Properties

Please see details in the attached file

Reachtube generated by C2E2

Link to the example file: linThermo.hyxml

references:

[1] Fehnker, Ansgar, and Franjo Ivančić. “Benchmarks for hybrid systems verification.” In Hybrid Systems: Computation and Control, pp. 326-341. Springer Berlin Heidelberg, 2004.