Convoy Car exampleTopInverted pendulumDamped oscillator with two modes

Damped oscillator with two modes

We saw that the (naive) discretized version of the undamped oscillator diverges. We now consider an oscillator where only the central part is damped:

We still add to split the central mode into two modes (kind of trace partitioning) to prove that the behaviour is bounded, despite the two extremal modes being unstables.

The actual source files are either oscillation2_16.lts (k=1/16) or oscillation2_32.lts (k=1/32).

The results can be seen here (we apply widening only ath the 3rd iteration):

l

#e k running time file
2 4 1/16 oscillation2_16_l2w3.ps
3 8 1/16 oscillation2_16_l3w3.ps
4 32 1/16 oscillation2_16_l4w3.ps
2 4 1/32 oscillation2_32_l2w3.ps
3 8 1/32 oscillation2_32_l3w3.ps
4 32 1/32 oscillation2_32_l4w3.ps

We need l >= 3 to prove global stability. Moreover, if it is the case and in the case k=1/16, we prove that the system cannot exit from location "dampedn".


Convoy Car exampleTopInverted pendulumDamped oscillator with two modes