Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
105
Gurobi is thus expected to outperform an SMT solver in this specific task. However these variables do not represent real numbers, but floating point numbers
that are approximated at machine precision. The second learner instead employs Z3, which is numerically sound and not affected by machine precision. Z3
solves an SMT instance to synthesise V (x): it asserts the satisfiability of Eq. (3)
F (V (¯ x i )) for all collected counterexamples ¯
x i .
As mentioned earlier, the number of inequalities to be solved depends on the
number of counterexamples, which can grow to be quite large. Whilst the verifier
ought to generate useful counterexamples, the learner is optimised to output a
matrix ¯
P i that is easy to handle. The comparison between a numerical learner
(running on Gurobi) and a sound one (based on Z3) shows that the compromise
between speed and soundness results is evident (cf. Section 4). Z3 is sound, yet
slower when compared to the numerical learner.
Z3 offers an incremental feature to the learner. During each CEGIS loop,
on the verification side the memory is cleared from the previous constraints as
the verifier re-initialises the verification problem with a new candidate V (x).
On the other hand, the learner keeps the previous synthesis instance adding a
new constraint related to the latest counterexample. This incremental approach
reduces the computational effort, as the learner does not initialise a new problem
for every CEGIS loop.
3.2 Lyapunov Function Synthesis for Non-linear Models
The problem of synthesizing Lyapunov functions and their region of validity for
a general non-linear system ˙
x = f (x(t)) is approached via linearisation or via
direct computation.
The linearisation approach consists of three steps for the learner: we first
linearise the f (x(t)), obtaining
˙
˜
x(t) = A L ˜
x(t),
where A L is the Jacobian of f (x(t)) evaluated at x e ; we then compute matrix
P – and quadratic Lyapunov function V (x) = x
T P x – on the linearised system;
finally, we find R, defined as the set in which the linear Lyapunov function
is valid. Next, we detail the synthesis of region R. Consider, without loss of
generality, an autonomous non-linear system with (at least one) equilibrium
point x e = 0. Assume the CEGIS procedure is successful, i.e. it finds a Lyapunov
function V L (x) = x
T P x that guarantees the asymptotic stability of system ˙
˜
x =
A L ˜
x around x e . We now compute the region where V L (x) guarantees stability
with the original system, i.e. ˙
x = f (x). In view of the existence of V L (x) and by
definition of linearisation, there exists a neighbourhood of the origin B 0 in which
the derivative of the Lyapunov function ˙
V (x) is non-positive; formally such set
is defined as
B 0 = {x ∈ R
n
\{0} | ˙
V (x) ≤ 0},
where ˙
V (x) is computed on the original system, namely
˙
V (x) = ∇V L (x) · f (x).
105
Gurobi is thus expected to outperform an SMT solver in this specific task. However these variables do not represent real numbers, but floating point numbers
that are approximated at machine precision. The second learner instead employs Z3, which is numerically sound and not affected by machine precision. Z3
solves an SMT instance to synthesise V (x): it asserts the satisfiability of Eq. (3)
F (V (¯ x i )) for all collected counterexamples ¯
x i .
As mentioned earlier, the number of inequalities to be solved depends on the
number of counterexamples, which can grow to be quite large. Whilst the verifier
ought to generate useful counterexamples, the learner is optimised to output a
matrix ¯
P i that is easy to handle. The comparison between a numerical learner
(running on Gurobi) and a sound one (based on Z3) shows that the compromise
between speed and soundness results is evident (cf. Section 4). Z3 is sound, yet
slower when compared to the numerical learner.
Z3 offers an incremental feature to the learner. During each CEGIS loop,
on the verification side the memory is cleared from the previous constraints as
the verifier re-initialises the verification problem with a new candidate V (x).
On the other hand, the learner keeps the previous synthesis instance adding a
new constraint related to the latest counterexample. This incremental approach
reduces the computational effort, as the learner does not initialise a new problem
for every CEGIS loop.
3.2 Lyapunov Function Synthesis for Non-linear Models
The problem of synthesizing Lyapunov functions and their region of validity for
a general non-linear system ˙
x = f (x(t)) is approached via linearisation or via
direct computation.
The linearisation approach consists of three steps for the learner: we first
linearise the f (x(t)), obtaining
˙
˜
x(t) = A L ˜
x(t),
where A L is the Jacobian of f (x(t)) evaluated at x e ; we then compute matrix
P – and quadratic Lyapunov function V (x) = x
T P x – on the linearised system;
finally, we find R, defined as the set in which the linear Lyapunov function
is valid. Next, we detail the synthesis of region R. Consider, without loss of
generality, an autonomous non-linear system with (at least one) equilibrium
point x e = 0. Assume the CEGIS procedure is successful, i.e. it finds a Lyapunov
function V L (x) = x
T P x that guarantees the asymptotic stability of system ˙
˜
x =
A L ˜
x around x e . We now compute the region where V L (x) guarantees stability
with the original system, i.e. ˙
x = f (x). In view of the existence of V L (x) and by
definition of linearisation, there exists a neighbourhood of the origin B 0 in which
the derivative of the Lyapunov function ˙
V (x) is non-positive; formally such set
is defined as
B 0 = {x ∈ R
n
\{0} | ˙
V (x) ≤ 0},
where ˙
V (x) is computed on the original system, namely
˙
V (x) = ∇V L (x) · f (x).