112
D. Ahmed et al.
Example #
Gurobi-CEGIS
Z3-CEGIS
SOSTOOLS
5
6
7
8
9
10
11
Time [sec] Iterations
–
–
0.32
2
0.37
4
0.16
2
–
–
–
–
–
–
Time [sec] Iterations
18.38
4
1.27
5
0.60
3
0.27
2
9.26
3
0.14
3
0.23
3
Time [sec]
–
3.66
4.38
3.83
21.31
–
–
Table 2. Comparison between Gurobi-CEGIS, Z3-CEGIS and SOSTOOLS for nonlinear models (see Examples description in main text). The result for Gurobi-CEGIS
in Example 8 is obtained via linearisation.
5 Conclusions and Future Work
In this work, we have studied the problem of automated and sound synthesis
of Lyapunov functions. We have exploited a CEGIS framework, equipped with
a sound verifier (the Z3 SMT solver) and with either a numerical LP solver
(Gurobi) or a sound (Z3) learner.
We have provided a simple – yet effective – methodology to synthesise Lyapunov functions for linear, polynomial and parametric systems and shown evidence of scalability and reliability of our method using benchmarks from the
literature. We have in particular synthesised quadratic Lyapunov functions for
linear models and verified their validity on the whole state space. We have tackled non-linear models following two approaches: either 1) the computation of
Lyapunov functions over the linearised system and the synthesis of its validity
region; or 2) the direct computation of a higher-order Lyapunov function.
Future work includes the implementation of synthesis techniques for GurobiCEGIS for high-order and parametric models, together with the study of optimisation techniques for the synthesis in Z3-CEGIS: the tuning of the SMT solvers
leaves much room, for example in order to provide insightful counterexamples
or to additionally optimise an objective function. Further, we aim at embedding
CEGIS with neural networks (as function approximators) to replace the learner,
whilst maintaining the verification in the hands of an SMT solver - this approach
has been recently pursued also in [32].
References
1. P. Giesl and S. Hafstein, “Review on Computational Methods for Lyapunov Functions,” Discrete and Continuous Dynamical Systems-Series B, vol. 20, no. 8, pp.
2291–2331, 2015.
2. C. M. Kellett, “Classical Converse Theorems in Lyapunov’s Second Method,” Discrete Continuous Dyn. Syst. Series B, vol. 20, no. 8, pp. 2333–2360, 2015.
D. Ahmed et al.
Example #
Gurobi-CEGIS
Z3-CEGIS
SOSTOOLS
5
6
7
8
9
10
11
Time [sec] Iterations
–
–
0.32
2
0.37
4
0.16
2
–
–
–
–
–
–
Time [sec] Iterations
18.38
4
1.27
5
0.60
3
0.27
2
9.26
3
0.14
3
0.23
3
Time [sec]
–
3.66
4.38
3.83
21.31
–
–
Table 2. Comparison between Gurobi-CEGIS, Z3-CEGIS and SOSTOOLS for nonlinear models (see Examples description in main text). The result for Gurobi-CEGIS
in Example 8 is obtained via linearisation.
5 Conclusions and Future Work
In this work, we have studied the problem of automated and sound synthesis
of Lyapunov functions. We have exploited a CEGIS framework, equipped with
a sound verifier (the Z3 SMT solver) and with either a numerical LP solver
(Gurobi) or a sound (Z3) learner.
We have provided a simple – yet effective – methodology to synthesise Lyapunov functions for linear, polynomial and parametric systems and shown evidence of scalability and reliability of our method using benchmarks from the
literature. We have in particular synthesised quadratic Lyapunov functions for
linear models and verified their validity on the whole state space. We have tackled non-linear models following two approaches: either 1) the computation of
Lyapunov functions over the linearised system and the synthesis of its validity
region; or 2) the direct computation of a higher-order Lyapunov function.
Future work includes the implementation of synthesis techniques for GurobiCEGIS for high-order and parametric models, together with the study of optimisation techniques for the synthesis in Z3-CEGIS: the tuning of the SMT solvers
leaves much room, for example in order to provide insightful counterexamples
or to additionally optimise an objective function. Further, we aim at embedding
CEGIS with neural networks (as function approximators) to replace the learner,
whilst maintaining the verification in the hands of an SMT solver - this approach
has been recently pursued also in [32].
References
1. P. Giesl and S. Hafstein, “Review on Computational Methods for Lyapunov Functions,” Discrete and Continuous Dynamical Systems-Series B, vol. 20, no. 8, pp.
2291–2331, 2015.
2. C. M. Kellett, “Classical Converse Theorems in Lyapunov’s Second Method,” Discrete Continuous Dyn. Syst. Series B, vol. 20, no. 8, pp. 2333–2360, 2015.