Experiments and Comparisons

Experiments and Comparisons

name	CFG	type	nbvars	Kleene	Jordan vs Kleene	Kleene time	Jordan time	Ellipsoid applicable
parabola_i1	single loops	unstable with guard	3	14/60	+8, +17	0.014	0.007	no
parabola_i2	single loops	unstable with guard	3	24/60	+18, +6	0.016	0.008	no
cubic_i1	single loops	unstable with guard	4	26/80	+18, +26	0.077	0.013	no
cubic_i2	single loops	unstable with guard	4	46/80	+38, +9, -2	0.086	0.012	no
exp_div	single loops	unstable with guard	2	6/24	+2, +6, -1	0.007	0.004	no
oscillator_i0	single loop	both types without guard	2	27/28	+23, +0, -1	0.013	0.004	yes
oscillator_i1	single loop	both types without guard	2	28/28	+23, +0, -1	0.013	0.004	yes
inv_pendulum	single loop	stable without guard	4	36/40	+36,0 +0	0.538	0.009	yes
thermostat	nested loops	stable with guard	3	6/24	+6, +1, -1	0.012	0.003	no
oscillator2_16	nested loops	stable and unstable with guard	3	39/48	+39, +0	0.141	0.003	no
oscillator2_32	nested loops	stable and unstable with guard	3	39/48	+39, +0	0.355	0.003	no

We took templates of the form

where the m's are the coefficients of the powers of the Jordan normal form, and l is a parameter, set to l=2 for most experiments, except oscillator2_xx that need l=3 to show finite bounds everywhere, as well waiting from the 3rd iteration before applying widening (needed because of the outer loop).

About the numbers: we take the bounding boxes of the inferred polyhedra at each control point (except initial ones), and we measure the improvements on bounds.

"Kleene": nb of infinite bounds / total nb of bounds;
"Jordan vs Kleene": nb of bounds becoming finite, nb of improved finite bounds [, nb of worse finite bounds] (can be reduced to 0 by increasing l to 3 or 4).
"Kleene time" and "Jordan time": times in seconds.

About the examples:

parabola_i1 and parabola_i2: loops of the type
t=0; while (guard){ x=x+y; y=y+1; t=t+1; }

with different formula for guard, presented in *. Trajectories are discretized parabola.

i1 refers to the initial set x,y in [0,2], i2 to x,y in [-2,2], which makes the evolution of x non-monotonic.
cubic_i1 and cubic_i2: loops of the type
t=0; while (guard){ x=x+y; y=y+z; z=z+1; t=t+1; }

with different formula for guard.

i1 refers to the initial set x,y,z in [0,2], i2 to x,y,z in [-2,2], which makes the evolution of x and y non-monotonic.
oscillator_i0 and oscillator_i1 implement the (naive) discretization of the differential equation

with w=0.125 and different values for k, presented in *. Trajectories are inward (or outward int the unstable case) spirals.

i0 refers to the initial set theta(0)=8, dtheta/dt(0)=0, i1 to theta(0)=8, dtheta/dt(0)=8.
inv_pendulum is a PID-controlled inverted pendulum, with eigenvalues very close to 1.
thermostat is the thermostat example discussed in *. Trajectories are successions of pieces of exponentials.
oscillator2_16 and oscillator2_32 are the damped oscillator with three modes discussed in *. 16 (resp. 32) corresponds to a damping factor of 1/16 (resp. 1/32) of the central part/mode. Trajectories are successions of pieces of inward/outward spirals. In the case of oscillator2_16, the damping is strong enough and the analysis precise enough to show that the mobile point cannot pass a second time in the central part/mode from a negative position.

If we now set the template parameter l to l=4 for all examples, to give an idea of the improvement in precision w.r.t. standard analysis and the increase in runing times, we get the following table:

name	CFG	type	nbvars	Kleene	Jordan vs Kleene	Kleene time	Jordan time	Ellipsoid applicable
parabola_i1	single loops	unstable with guard	3	14/60	+8, +19	0.020	0.007	no
parabola_i2	single loops	unstable with guard	3	24/60	+18, +9	0.022	0.008	no
cubic_i1	single loops	unstable with guard	4	26/80	+18, +26	0.258	0.013	no
cubic_i2	single loops	unstable with guard	4	46/80	+38, +11	0.524	0.012	no
exp_div	single loops	unstable with guard	2	6/24	+2, +7	0.010	0.004	no
oscillator_i0	single loop	both types without guard	2	27/28	+23, +0, -1	0.033	0.004	yes
oscillator_i1	single loop	both types without guard	2	28/28	+24, +0	0.033	0.004	yes
inv_pendulum	single loop	stable without guard	4	36/40	+36,+0	96.229	0.012	yes
thermostat	nested loops	stable with guard	3	6/24	+6, +1, -1	0.017	0.003	no
oscillator2_16	nested loops	stable and unstable with guard	3	39/48	+39, +0	0.300	0.003	no
oscillator2_32	nested loops	stable and unstable with guard	3	39/48	+39, +0	0.706	0.003	no

The increase in running time become moderate in general, less than the worst-case if one look to the increase of the number of template constraints. The exception is the inverted pendulum example.

Experiments and Comparisons