Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
109
Results comparing the numerical learner using Gurobi and the sound learner
using Z3 are reported in Table 1. The average values, as well as the minimum
and maximum value among the N random systems, are computed on the synthesis tests that have not timed out. The number of timed out procedures are
also listed in the Table.
With regards to non-linear and parametric models, we assess our approach
over a suite of examples taken from related work on Lyapunov function synthesis
[18], [19], [20], [23], which are reported in the following. The value c from Eq. (2)
is set heuristically as ceil(d/2), where d is the order of the system (this choice
follows the common interpretation of Lyapunov maps as storage functions). Due
to ease of implementation, only Z3-CEGIS performs the synthesis with c > 1
and in the case of parametric models. Results in terms of computational time
and iterations are reported in Table 2. Experiments are run on a 4-core Dell
laptop with Fedora 30 and 8GB RAM.
Example 5. Consider the model [18]
˙
x 1 = −x
2
1 − 4x
3
2 − 6x 3 x 4 ,
˙
x 4 = x 1 x 3 + x 3 x 6 − x
3
4 ,
˙
x 2 = −x 1 − x 2 + x
3
5 ,
˙
x 5 = −2x
3
2 − x 5 + x 6 ,
˙
x 3 = x 1 x 4 − x 3 + x 4 x 6 ,
˙
x 6 = −3x 3 x 4 − x
3
5 − x 6 .
Z3-CEGIS finds the Lyapunov function V (x) = 2x
2
1 +4x
4
2 +x
2
3 +11x
2
4 +2x
4
5 +4x
2
6 ,
ensuring stability over the whole state space. SOSTOOLS fails to find a 2
nd
−
or 4
th
−order Lyapunov function for this model.
Example 6. Consider the model [23]
˙
x = −x
3 + y
˙
y = −x − y.
Gurobi-CEGIS finds the Lyapunov function V (x) = 5 · 10
−5 x
2 + 5 · 10
−5 y
2 ,
whereas Z3-CEGIS finds V (x) = 0.5x
2 + 0.5y
2 , both ensuring global stability.
The linearised Gurobi-CEGIS finds V (x) = 3.2 · 10
−3 x
2 + 3.2 · 10
−3 y
2 , whereas
SOSTOOLS finds V (x) = 0.7844(x
2 + y
2 ), also ensuring stability over the whole
state space.
Example 7. Consider the system [20]
⎧
⎪
⎪
⎨
⎪
⎪
⎩
˙
x 1 = −x
3
1 − x 1 x
2
3 ,
˙
x 2 = −x 2 − x
2
1 x 2 ,
˙
x 3 = −x 3 −
3x 3
x 2
3 + 1
+ 3x
2
1 x 3 .
Note that the term x
2
3 +1 is always non-negative, therefore we can consider ˙
V (x)·
(x
2
3 + 1) ≤ 0. Gurobi-CEGIS finds the Lyapunov function V (x) = 32 · 10
−4 x
2
1 +
32 · 10
−4 x
2
2 + 8 · 10
−4 x
2
3 , whereas Z3-CEGIS finds V (x) = 3x
2
1 + x
2
2 + x
2
3 , and
finally SOSTOOLS finds the function V (x) = 6.659x1
2 + 4.628x2
2 + 2.073x3
2 ,
all ensuring global stability.
109
Results comparing the numerical learner using Gurobi and the sound learner
using Z3 are reported in Table 1. The average values, as well as the minimum
and maximum value among the N random systems, are computed on the synthesis tests that have not timed out. The number of timed out procedures are
also listed in the Table.
With regards to non-linear and parametric models, we assess our approach
over a suite of examples taken from related work on Lyapunov function synthesis
[18], [19], [20], [23], which are reported in the following. The value c from Eq. (2)
is set heuristically as ceil(d/2), where d is the order of the system (this choice
follows the common interpretation of Lyapunov maps as storage functions). Due
to ease of implementation, only Z3-CEGIS performs the synthesis with c > 1
and in the case of parametric models. Results in terms of computational time
and iterations are reported in Table 2. Experiments are run on a 4-core Dell
laptop with Fedora 30 and 8GB RAM.
Example 5. Consider the model [18]
˙
x 1 = −x
2
1 − 4x
3
2 − 6x 3 x 4 ,
˙
x 4 = x 1 x 3 + x 3 x 6 − x
3
4 ,
˙
x 2 = −x 1 − x 2 + x
3
5 ,
˙
x 5 = −2x
3
2 − x 5 + x 6 ,
˙
x 3 = x 1 x 4 − x 3 + x 4 x 6 ,
˙
x 6 = −3x 3 x 4 − x
3
5 − x 6 .
Z3-CEGIS finds the Lyapunov function V (x) = 2x
2
1 +4x
4
2 +x
2
3 +11x
2
4 +2x
4
5 +4x
2
6 ,
ensuring stability over the whole state space. SOSTOOLS fails to find a 2
nd
−
or 4
th
−order Lyapunov function for this model.
Example 6. Consider the model [23]
˙
x = −x
3 + y
˙
y = −x − y.
Gurobi-CEGIS finds the Lyapunov function V (x) = 5 · 10
−5 x
2 + 5 · 10
−5 y
2 ,
whereas Z3-CEGIS finds V (x) = 0.5x
2 + 0.5y
2 , both ensuring global stability.
The linearised Gurobi-CEGIS finds V (x) = 3.2 · 10
−3 x
2 + 3.2 · 10
−3 y
2 , whereas
SOSTOOLS finds V (x) = 0.7844(x
2 + y
2 ), also ensuring stability over the whole
state space.
Example 7. Consider the system [20]
⎧
⎪
⎪
⎨
⎪
⎪
⎩
˙
x 1 = −x
3
1 − x 1 x
2
3 ,
˙
x 2 = −x 2 − x
2
1 x 2 ,
˙
x 3 = −x 3 −
3x 3
x 2
3 + 1
+ 3x
2
1 x 3 .
Note that the term x
2
3 +1 is always non-negative, therefore we can consider ˙
V (x)·
(x
2
3 + 1) ≤ 0. Gurobi-CEGIS finds the Lyapunov function V (x) = 32 · 10
−4 x
2
1 +
32 · 10
−4 x
2
2 + 8 · 10
−4 x
2
3 , whereas Z3-CEGIS finds V (x) = 3x
2
1 + x
2
2 + x
2
3 , and
finally SOSTOOLS finds the function V (x) = 6.659x1
2 + 4.628x2
2 + 2.073x3
2 ,
all ensuring global stability.