Parabola, cubic and exponential behaviours

Thermostat experiment

Thermostat experiment

The model

We start from the following differential linear hybrid automaton.

The variables are the room temperature (T), the external temperature (T_e) and the time clock (t). The upper location corresponds to the heating mode, the lower one to the cooling mode. The goal is to maintain the room temperature around 20 degrees. If this temperature is less than 18, the heating is switched on. If it exceeds 22, heating is switched off (there is an hysteresis).

This small system is first (very naively) discretized using a sampling time of 1 second.

and then transformed for acceleration:

The corresponding input model of our prototype is thermostat.lts In it, the keyword "jordan" give the decomposition of the assignement M into S^-1JS where J is the real Jordan form of M. The last, fourth dimension corresponds to the added variable xi always equal to 1.

The analysis

We type the command


jordan.byte -debug 1 -print box -dot thermostat1.dot -log 1 thermostat.lts &&
dot -Tps thermostat1.dot >thermostat1.ps

where the "-log l" option indicates that when abstracting matrices with template polyhedra, we consider the set of template expressions of the form

If d is the number of different coefficients of the set of matrices to abstract, this generates d(d-1)(2^l-1) + d template expressions to be lower and upper bounded.

The other options are related to the output.

The result can be viewed at the last page of the thermostat1.ps file.

Some observations:

In each location is displayed the computed invariant, under the form of a set of constraints, followed by the bounding box of the corresponding polyhedron.
Looking at location "heat1", one observes that temperature T in [16,22.5] in heating mode, and looking at location "noheat1", one observes that T in [17.75,22.5] in cooling mode.
Looking at location "heat2", the analysis infers that the system spents at least 1.18 and at most 9.98 consecutive seconds in the heating mode, whereas looking at location "noheat2", the analysis infers that the system spents at least 1.41 and at most 12.99 consecutive seconds in this mode.
The non-zero lower bounds indicates that the hysteresis works: the system mode is not switched infinitely often in a finite time.

It is instructive to see how these significant numbers are improved if one increases the precision with the "-log l" option. The following table synthesizes our experiments.

l	#e	heating mode		cooling mode		running time	file
		T	time	T	time
1	4	[16,22.5]	[1.19,9.99]	[17.75,22.5]	[1.41,12.99]		thermostat1.ps
2	8	[16,22.5]	[1.78,9.96]	[17.75,22.5]	[2.35,12.97]		thermostat2.ps
3	16	[16,22.5]	[2.96,9.92]	[17.75,22.5]	[4.24,12.93]		thermostat3.ps
4	32	[16,22.5]	[5.33,9.82]	[17.75,22.5]	[8.00,12.86]		thermostat4.ps
5	64	[16,22.5]	[5.33,9.82]	[17.75,22.5]	[10.71,12.86]		thermostat5.ps
6	128	[16,22.5]	[6.25,9.76]	[17.75,22.5]	[10.71,12.80]		thermostat6.ps
8	512	[16,22.5]	[6.28,9.76]	[17.75,22.5]	[10.72,12.79]		thermostat8.ps

l	:	corresponds to "-log l" option
#e	:	number of template expressions on the coefficients of Jordan normal form
		(related to the number "l" and the number of different coefficient of the Jordan normal form)
T	:	regulated temperature
time	:	time spent in each mode

The temperature intervals do not change, but the lower bound for time improves a lot up to l=4, and slightly afterwards.

In the sequel, in the Postscript files we display only the bounding boxed of the inferred polyhedra (used option "-print box" instead of "-print boxpoly").

Thermostat experiment