98
D. Ahmed et al.
the literature [1,2]. A brief introduction to the concepts of Lyapunov stability is
presented in Section 3. By and large, existing approaches leverage Linear Algebra
or Convex Optimisation solutions, and are not fully automated nor numerically
sound.
Contributions We apply an inductive synthesis framework, known as CounterExample Guided Inductive Synthesis (CEGIS) [3,4] and recently employed in a
number of control applications [5,6,7,8], to construct Lyapunov functions for
linear, polynomial and parametric ODEs, and (for non-linear ODEs) to constructively characterise their domain of validity. CEGIS, originally developed for
program synthesis based on the satisfiability of second-order logical formulae, is
employed in this work with template Lyapunov functions and in conjunction
with a Satisfiability Modulo Theory (SMT) solver [9]. Our results offer a formal
guarantee of correctness in combination with a simple algorithmic implementation.
The synthesis of a Lyapunov function V can be written as a second-order logic
formula F := ∃V ∀x : ψ, where x represents the state variables and ψ represents
requirements that V needs to satisfy in order to be a Lyapunov function.
The CEGIS architecture is structured as a loop between two components, a
“learner” and a “verifier”. The learner provides a candidate function V and the
verifier checks the validity of ψ over the set of x; if the function is not valid, the
verifier provides a counterexample, namely a point ¯
x in the state space where the
candidate function does not satisfy ψ. The learner incorporates the generated
counterexample ¯
x, subsequently computes a new candidate function, and passes
it back to the verifier.
We exploit SMT solvers to (repeatedly) assert the validity of ψ, given V , over
a domain in the space of x. Satisfiability Modulo Theory (SMT) is a powerful
tool to assert the existence of such a function. An SMT problem is a decision
problem – a problem that can be formulated as a yes/no question – for logical
formulae within one or more theories, e.g. the theory of arithmetics over real
numbers. The generation of simple counterexamples ¯
x is a key new feature of
our technique.
Furthermore, in this work we provide two alternative CEGIS implementations: 1) a numerical learner and an SMT-based verifier, and 2) an SMT-based
learner and verifier. The numerical generation of Lyapunov functions is based
on the optimisation tool Gurobi [10], whereas the SMT-based one leverages Z3
[11].
Related Work The construction of Lyapunov functions is recognisably an important yet hard problem, particularly for non-linear ODE models, and it has
been the objective of classical studies [12,13,14]. A know constructive result has
been introduced in [15], which additionally provides an estimate of the domain
of attraction. It has led to further work based on recursive procedures. Broadly,
these approaches are numerical and based on the solution of optimisation problems. For instance, linear programming is exploited in [16] to iteratively search
D. Ahmed et al.
the literature [1,2]. A brief introduction to the concepts of Lyapunov stability is
presented in Section 3. By and large, existing approaches leverage Linear Algebra
or Convex Optimisation solutions, and are not fully automated nor numerically
sound.
Contributions We apply an inductive synthesis framework, known as CounterExample Guided Inductive Synthesis (CEGIS) [3,4] and recently employed in a
number of control applications [5,6,7,8], to construct Lyapunov functions for
linear, polynomial and parametric ODEs, and (for non-linear ODEs) to constructively characterise their domain of validity. CEGIS, originally developed for
program synthesis based on the satisfiability of second-order logical formulae, is
employed in this work with template Lyapunov functions and in conjunction
with a Satisfiability Modulo Theory (SMT) solver [9]. Our results offer a formal
guarantee of correctness in combination with a simple algorithmic implementation.
The synthesis of a Lyapunov function V can be written as a second-order logic
formula F := ∃V ∀x : ψ, where x represents the state variables and ψ represents
requirements that V needs to satisfy in order to be a Lyapunov function.
The CEGIS architecture is structured as a loop between two components, a
“learner” and a “verifier”. The learner provides a candidate function V and the
verifier checks the validity of ψ over the set of x; if the function is not valid, the
verifier provides a counterexample, namely a point ¯
x in the state space where the
candidate function does not satisfy ψ. The learner incorporates the generated
counterexample ¯
x, subsequently computes a new candidate function, and passes
it back to the verifier.
We exploit SMT solvers to (repeatedly) assert the validity of ψ, given V , over
a domain in the space of x. Satisfiability Modulo Theory (SMT) is a powerful
tool to assert the existence of such a function. An SMT problem is a decision
problem – a problem that can be formulated as a yes/no question – for logical
formulae within one or more theories, e.g. the theory of arithmetics over real
numbers. The generation of simple counterexamples ¯
x is a key new feature of
our technique.
Furthermore, in this work we provide two alternative CEGIS implementations: 1) a numerical learner and an SMT-based verifier, and 2) an SMT-based
learner and verifier. The numerical generation of Lyapunov functions is based
on the optimisation tool Gurobi [10], whereas the SMT-based one leverages Z3
[11].
Related Work The construction of Lyapunov functions is recognisably an important yet hard problem, particularly for non-linear ODE models, and it has
been the objective of classical studies [12,13,14]. A know constructive result has
been introduced in [15], which additionally provides an estimate of the domain
of attraction. It has led to further work based on recursive procedures. Broadly,
these approaches are numerical and based on the solution of optimisation problems. For instance, linear programming is exploited in [16] to iteratively search