Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
99
for stable matrices inside a predefined convex set, resulting in an approximate
Lyapunov function for the given model. Alternative approximate methods include [1] ε-bounded numerical methods, techniques leveraging series expansion
of a function, the construction of functions from trajectory samples, and the
framework of linear matrix inequalities. The approach in [17] uses sum-of-squares
(SOS) polynomials to synthesise Lyapunov functions, however its scalability remains an issue. The work in [18] uses SOS decomposition to synthesise Lyapunov
functions for (non-polynomial) non-linear systems: the algorithmic implementation is know as SOSTOOLS [19,20]. [21] focuses on an analytical result involving
a summation over finite time interval, under a stability assumption. Recent developments are in [22] and subsequent work, whereas surveys on this topic are
in [1,2].
In conclusion, existing constructive approaches either rely on complex candidate functions (whether rational or polynomial), on semi-analytical results, or
alternatively they involve state-space partitions (for which scalability with the
state-space dimension is problematic) accompanied by correspondingly complex
or large optimisation problems. These approximate methods evidently lack either
numerical robustness, being bound by machine precision, or algorithmic soundness: they cannot provide formal certificates of reliability which, in safety-critical
applications, can be an evident limit.
In [23] Lyapunov functions are soundly found within a parametric framework, by constructing a system of linear inequality constraints over unknown
coefficients. A twofold linear programming relaxation is made: it includes interval evaluation of the polynomial form and “Handelman representations” for
positive polynomials. Simulations are used in [24] to generate constraints for a
template Lyapunov function, which are then resolved via LP, resulting in candidate solutions. Whilst the authors refer to traces as counterexamples, they do
not employ the CEGIS framework, as in this work. When no counterexamples are
found, [24] further uses dReal [25] and Mathematica [26] to verify the obtained
candidate Lyapunov functions. The sound technique, which is not complete, is
tested on low-dimensional models with non-linear dynamics.
The cognate work in [7,8,27] is the first to employ a CEGIS-based approach
to synthesise Lyapunov functions. [7,8] focuses on such synthesis for switching
control models - a more general setup that ours. [7] employs an SMT solver for
the learner, and towards scalability solves an optimisation problem over LMI
constraints for the verifier over a given domain (unlike our approach). As such,
counterexamples are matrices, not points over the state space, and furthermore
the use of LMI solvers does not in principle lead to sound outcomes. Along the
above line, [8] expands this approach towards robust synthesis; [27] instead employs MPC (Model Predictive Control) techniques within the learner to suggest
template functions, which are later verified via semi-definite programming relaxations (again, possibly generating counterexamples by solving optimisation
problems over a given domain). Whilst inspired by this line of work, our contribution provides a simple (with interpretable counterexamples that are points
over the state space) yet effective (scalable to at least 10-dimensional models)
99
for stable matrices inside a predefined convex set, resulting in an approximate
Lyapunov function for the given model. Alternative approximate methods include [1] ε-bounded numerical methods, techniques leveraging series expansion
of a function, the construction of functions from trajectory samples, and the
framework of linear matrix inequalities. The approach in [17] uses sum-of-squares
(SOS) polynomials to synthesise Lyapunov functions, however its scalability remains an issue. The work in [18] uses SOS decomposition to synthesise Lyapunov
functions for (non-polynomial) non-linear systems: the algorithmic implementation is know as SOSTOOLS [19,20]. [21] focuses on an analytical result involving
a summation over finite time interval, under a stability assumption. Recent developments are in [22] and subsequent work, whereas surveys on this topic are
in [1,2].
In conclusion, existing constructive approaches either rely on complex candidate functions (whether rational or polynomial), on semi-analytical results, or
alternatively they involve state-space partitions (for which scalability with the
state-space dimension is problematic) accompanied by correspondingly complex
or large optimisation problems. These approximate methods evidently lack either
numerical robustness, being bound by machine precision, or algorithmic soundness: they cannot provide formal certificates of reliability which, in safety-critical
applications, can be an evident limit.
In [23] Lyapunov functions are soundly found within a parametric framework, by constructing a system of linear inequality constraints over unknown
coefficients. A twofold linear programming relaxation is made: it includes interval evaluation of the polynomial form and “Handelman representations” for
positive polynomials. Simulations are used in [24] to generate constraints for a
template Lyapunov function, which are then resolved via LP, resulting in candidate solutions. Whilst the authors refer to traces as counterexamples, they do
not employ the CEGIS framework, as in this work. When no counterexamples are
found, [24] further uses dReal [25] and Mathematica [26] to verify the obtained
candidate Lyapunov functions. The sound technique, which is not complete, is
tested on low-dimensional models with non-linear dynamics.
The cognate work in [7,8,27] is the first to employ a CEGIS-based approach
to synthesise Lyapunov functions. [7,8] focuses on such synthesis for switching
control models - a more general setup that ours. [7] employs an SMT solver for
the learner, and towards scalability solves an optimisation problem over LMI
constraints for the verifier over a given domain (unlike our approach). As such,
counterexamples are matrices, not points over the state space, and furthermore
the use of LMI solvers does not in principle lead to sound outcomes. Along the
above line, [8] expands this approach towards robust synthesis; [27] instead employs MPC (Model Predictive Control) techniques within the learner to suggest
template functions, which are later verified via semi-definite programming relaxations (again, possibly generating counterexamples by solving optimisation
problems over a given domain). Whilst inspired by this line of work, our contribution provides a simple (with interpretable counterexamples that are points
over the state space) yet effective (scalable to at least 10-dimensional models)