Automated and Sound Synthesis
of Lyapunov Functions with SMT Solvers
Daniele Ahmed
1,2 , Andrea Peruffo
1 , and Alessandro Abate
1
1 Department of Computer Science, University of Oxford, OX1 3QD Oxford, UK
name.surname@cs.ox.ac.uk
2 Amazon Inc, London, UK
Abstract. In this paper we employ SMT solvers to soundly synthesise
Lyapunov functions that assert the stability of a given dynamical model.
The search for a Lyapunov function is framed as the satisfiability of a
second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions
of the model. We synthesise Lyapunov functions for linear, non-linear
(polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function.
We exploit an inductive framework to synthesise Lyapunov functions,
starting from parametric templates. The inductive framework comprises
two elements: a learner proposes a Lyapunov function, and a verifier
checks its validity - its lack is expressed via a counterexample (a point
over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the
procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach
based again on Z3. The overall technique is evaluated over a broad set
of benchmarks, which shows that this methodology not only scales to
10-dimensional models within reasonable computational time, but also
offers a novel soundness proof for the generated Lyapunov functions and
their domains of validity.
Keywords: Lyapunov functions, automated synthesis, inductive synthesis,
counter-example guided synthesis
1 Introduction
Dynamical systems represent a major modelling framework in both theoretical
and applied sciences: they describe how objects move by means of the laws
governing their dynamics in time. Often they encompass a system of ordinary
differential equations (ODE) with nontrivial solutions.
This work aims at studying the stability property of general ODEs, without
knowledge of their analytical solution. Stability analysis via Lyapunov functions
is a known approach to assert such property. As such, the problem of constructing
relevant Lyapunov functions for stability analysis has drawn much attention in
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 97–114, 2020.
https://doi.org/10.1007/978-3-030-45190-5 6
of Lyapunov Functions with SMT Solvers
Daniele Ahmed
1,2 , Andrea Peruffo
1 , and Alessandro Abate
1
1 Department of Computer Science, University of Oxford, OX1 3QD Oxford, UK
name.surname@cs.ox.ac.uk
2 Amazon Inc, London, UK
Abstract. In this paper we employ SMT solvers to soundly synthesise
Lyapunov functions that assert the stability of a given dynamical model.
The search for a Lyapunov function is framed as the satisfiability of a
second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions
of the model. We synthesise Lyapunov functions for linear, non-linear
(polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function.
We exploit an inductive framework to synthesise Lyapunov functions,
starting from parametric templates. The inductive framework comprises
two elements: a learner proposes a Lyapunov function, and a verifier
checks its validity - its lack is expressed via a counterexample (a point
over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the
procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach
based again on Z3. The overall technique is evaluated over a broad set
of benchmarks, which shows that this methodology not only scales to
10-dimensional models within reasonable computational time, but also
offers a novel soundness proof for the generated Lyapunov functions and
their domains of validity.
Keywords: Lyapunov functions, automated synthesis, inductive synthesis,
counter-example guided synthesis
1 Introduction
Dynamical systems represent a major modelling framework in both theoretical
and applied sciences: they describe how objects move by means of the laws
governing their dynamics in time. Often they encompass a system of ordinary
differential equations (ODE) with nontrivial solutions.
This work aims at studying the stability property of general ODEs, without
knowledge of their analytical solution. Stability analysis via Lyapunov functions
is a known approach to assert such property. As such, the problem of constructing
relevant Lyapunov functions for stability analysis has drawn much attention in
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 97–114, 2020.
https://doi.org/10.1007/978-3-030-45190-5 6