Parabola, cubic and exponential behaviours

Parabola, cubic and exponential behaviours

Parabola

We study an integrator put under different initial conditions and guards, formalized by the following automaton:

The trajectories are of the form "x = y*y + a*y + b". The purpose of the different guards is to demonstrate the ability of the technique to perform non-linear deductions.

• The analysis results of parabola_i0.lts can be seen here.

  l	#e	running time	file
  1	4		parabola_i0_l1.ps
  2	8		parabola_i0_l2.ps
  4	32		parabola_i0_l4.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)

• If we replace the initial condition with "0 <= x <= 2" and "0 <= y <= 2", we obtain these results:

  l	#e	running time	file
  1	4		parabola_i1_l1.ps
  2	8		parabola_i1_l2.ps
  4	32		parabola_i1_l4.ps

• If we replace the initial condition with "-2 <= x <= 2" and "0-2 <= y <= 2", we obtain these results:

  l	#e	running time	file
  1	4		parabola_i2_l1.ps
  2	8		parabola_i2_l2.ps
  4	32		parabola_i2_l4.ps

Cubic behaviour

Let add now a variable, in order to get a cubic behaviour.

The trajectories are now of the form "x=z*z*z + a*z*z + b*z+c" and "y=z*z + d*z + e".

• The analysis results of cubic_i0.lts can be seen here.

  l	#e	running time	file
  1	9		cubic_i0_l1.ps
  2	27		cubic_i0_l2.ps
  4	93		cubic_i0_l4.ps

• If we replace the initial condition with "0 <= x <= 2" and "0 <= y <= 2" and "0 <= z <= 2", we obtain these results:

  l	#e	running time	file
  1	9		cubic_i1_l1.ps
  2	27		cubic_i1_l2.ps
  4	93		cubic_i1_l4.ps

• If we replace the initial condition with "-2 <= x <= 2" and "-2 <= y <= 2" and "-2 <= z <= 2", we obtain these results:

  l	#e	running time	file
  1	9		cubic_i2_l1.ps
  2	27		cubic_i2_l2.ps
  4	93		cubic_i2_l4.ps

Exponential behaviour

We also analyse the example exp_div.lts:

Parabola, cubic and exponential behaviours