110
D. Ahmed et al.
Example 8. Consider the system [23]
˙
x = −x − 1.5x
2 y
3 ,
˙
y = −y
3 + 0.5x
3 y
2 .
Z3-CEGIS finds V (x) = 1/3x
2 + y
2 , valid on the whole R
2 , whereas SOSTOOLS finds V (x) = 0.4707x
2 + 1.412y
2 , with a stability region of radius
r = 68. Gurobi-CEGIS returns an error, as it finds V (x) = 1.00066454641347x
2 +
2.99933545358653y
2 that is not a valid Lyapunov function. The correct solution,
V (x) = x
2 + 3y
2 , can not be attained in view of lack of convergence of the optimisation algorithm. On the other hand, the linearised Gurobi-CEGIS delivers
V (x) = 32 · 10
−4 x
2 + 2 · 10
−4 y
2 with a radius r = 1.25.
Example 9. Consider the system [23]:
˙
x 1 = −x 1 + x
3
2 − 3x 3 x 4 ,
˙
x 3 = x 1 x 4 − x 3 ,
˙
x 2 = −x 1 − x
3
2 ,
˙
x 4 = x 1 x 3 − x
3
4 .
Z3-CEGIS finds the Lyapunov function V (x) = 2x
2
1 + x
4
2 + 3201/1024x
2
3 +
2943/1024x
2
4 , ensuring global stability. SOSTOOLS, on the other hand, finds
a complex 4
th order polynomial, omitted here for brevity, with a stability region
that is hard to characterise analytically.
Example 10. Consider the parametric linear system [23]
˙
x = y,
˙
y = −(2 + μ)x − y,
where μ ∈ (−2, 5]. Z3-CEGIS discovers the Lyapunov function V (x) = (μ +
2)x
2 + y
2 , ensuring stability on the whole state space. On the other hand, SOSTOOLS fails to find a solution when setting V (x, μ) to be independent from,
linear in, or quadratic in μ.
Example 11. Consider the parametric system [23]
˙
x = −(1 + μ 1 )x + (4 + μ 2 )y,
˙
y = −(1 + μ 3 )x − μ 4 y
3 ,
where μ i ∈ [0, 100] for i = 1, . . . 4. Z3-CEGIS discovers the Lyapunov function
V (x) =
μ 3 + 1
μ 2 + 4
x
2 + y
2 that asserts stability on the whole state space, whereas
SOSTOOLS can not find a solution considering V (x) independent from, linear
in, or quadratic in μ i , where i = 1, . . . , 4.
As expected, Gurobi is faster than Z3 in terms of iterations and computational time. The gap becomes larger with a high-dimensional system, as the SMT
D. Ahmed et al.
Example 8. Consider the system [23]
˙
x = −x − 1.5x
2 y
3 ,
˙
y = −y
3 + 0.5x
3 y
2 .
Z3-CEGIS finds V (x) = 1/3x
2 + y
2 , valid on the whole R
2 , whereas SOSTOOLS finds V (x) = 0.4707x
2 + 1.412y
2 , with a stability region of radius
r = 68. Gurobi-CEGIS returns an error, as it finds V (x) = 1.00066454641347x
2 +
2.99933545358653y
2 that is not a valid Lyapunov function. The correct solution,
V (x) = x
2 + 3y
2 , can not be attained in view of lack of convergence of the optimisation algorithm. On the other hand, the linearised Gurobi-CEGIS delivers
V (x) = 32 · 10
−4 x
2 + 2 · 10
−4 y
2 with a radius r = 1.25.
Example 9. Consider the system [23]:
˙
x 1 = −x 1 + x
3
2 − 3x 3 x 4 ,
˙
x 3 = x 1 x 4 − x 3 ,
˙
x 2 = −x 1 − x
3
2 ,
˙
x 4 = x 1 x 3 − x
3
4 .
Z3-CEGIS finds the Lyapunov function V (x) = 2x
2
1 + x
4
2 + 3201/1024x
2
3 +
2943/1024x
2
4 , ensuring global stability. SOSTOOLS, on the other hand, finds
a complex 4
th order polynomial, omitted here for brevity, with a stability region
that is hard to characterise analytically.
Example 10. Consider the parametric linear system [23]
˙
x = y,
˙
y = −(2 + μ)x − y,
where μ ∈ (−2, 5]. Z3-CEGIS discovers the Lyapunov function V (x) = (μ +
2)x
2 + y
2 , ensuring stability on the whole state space. On the other hand, SOSTOOLS fails to find a solution when setting V (x, μ) to be independent from,
linear in, or quadratic in μ.
Example 11. Consider the parametric system [23]
˙
x = −(1 + μ 1 )x + (4 + μ 2 )y,
˙
y = −(1 + μ 3 )x − μ 4 y
3 ,
where μ i ∈ [0, 100] for i = 1, . . . 4. Z3-CEGIS discovers the Lyapunov function
V (x) =
μ 3 + 1
μ 2 + 4
x
2 + y
2 that asserts stability on the whole state space, whereas
SOSTOOLS can not find a solution considering V (x) independent from, linear
in, or quadratic in μ i , where i = 1, . . . , 4.
As expected, Gurobi is faster than Z3 in terms of iterations and computational time. The gap becomes larger with a high-dimensional system, as the SMT