106
D. Ahmed et al.
Let us define the boundary of B 0 as ∂B 0 = {x ∈ R
n
\{0} | ˙
V (x) = 0}. This set
may be composed by single points or regions of the state space: in this case, we
find r, the closest point to the equilibrium that belongs to ∂B 0 , as
r = min
x∈∂B0
l
x(l)
2 .
We finally compute region R as a hyper-sphere of radius r,
R = {x ∈ R
n
\{0} | |x
2 < r
2
},
(4)
defining the region where the Lyapunov function is valid. Finally, region R is
tested with the verifier: formula F (V (x)) from Eq. (3) is passed to Z3 with
D = R. Our implementation uses a numerical optimisation technique to compute a value for r that is passed to Z3, as Z3 does not natively handle non-linear
optimisation problems. With this selection, the region R represents a sound
under-approximation of the maximal stability region. The linearisation method
is used in view of its rapid and effective synthesis capability. However, it produces a Lyapunov function that does not ensures global stability when one of
the eigenvalues of A L is equal to zero. This is a well-known limitation of the
linearisation, which suggests a more formal approach, called direct computation
method.
The direct computation method, as the name suggests, analytically computes
V (x) and ˙
V (x) from a template V (x) as in Eq. (2). The learner is tasked with
resolving conditions ψ obtained by a light relaxation of the two inequalities in
(1), namely
V (x) ≥ 0, ˙
V (x) = ∇V (x) · f (x) ≤ 0.
Note that the first inequality is not strict: this relaxation allows for a faster
computation of a candidate. The verifier, on the other hand, produces counterexamples for V (x) > 0, thus retaining soundness of the overall procedure.
The CEGIS framework allows the separation between synthesis and verification.
So whilst the learner might propose candidates being completely independent
from domain D, the verifier is responsible to assert or to find the domain of
validity D. Our implementation establishes that at first the verifier checks the
validity of V (x) on the whole state space D = R
n ; if the computation is not successful – namely, the computational time is greater than a predefined timeout –
the verifier checks its validity over a smaller region, e.g. D = [−1, 1]
n , and so on.
If also this program fails, the algorithm returns an empty V (x). Recall that our
algorithm is in general not complete - indeed, consider the trivial problem of the
synthesis of a Lyapunov function for an unstable system, which is not possible:
in this case, the CEGIS procedure will surely return an empty V (x).
3.3 Lyapunov Function Synthesis for Parametric Models
Parametric models represent a challenge for both sound and numerical solvers.
Let us remark that both Gurobi and Z3 cannot synthesise functions in the presence of uncertainty, whereas Z3 can provide counterexamples using one or more
variables as fixed parameters, using the quantifier ForAll.
D. Ahmed et al.
Let us define the boundary of B 0 as ∂B 0 = {x ∈ R
n
\{0} | ˙
V (x) = 0}. This set
may be composed by single points or regions of the state space: in this case, we
find r, the closest point to the equilibrium that belongs to ∂B 0 , as
r = min
x∈∂B0
l
x(l)
2 .
We finally compute region R as a hyper-sphere of radius r,
R = {x ∈ R
n
\{0} | |x
2 < r
2
},
(4)
defining the region where the Lyapunov function is valid. Finally, region R is
tested with the verifier: formula F (V (x)) from Eq. (3) is passed to Z3 with
D = R. Our implementation uses a numerical optimisation technique to compute a value for r that is passed to Z3, as Z3 does not natively handle non-linear
optimisation problems. With this selection, the region R represents a sound
under-approximation of the maximal stability region. The linearisation method
is used in view of its rapid and effective synthesis capability. However, it produces a Lyapunov function that does not ensures global stability when one of
the eigenvalues of A L is equal to zero. This is a well-known limitation of the
linearisation, which suggests a more formal approach, called direct computation
method.
The direct computation method, as the name suggests, analytically computes
V (x) and ˙
V (x) from a template V (x) as in Eq. (2). The learner is tasked with
resolving conditions ψ obtained by a light relaxation of the two inequalities in
(1), namely
V (x) ≥ 0, ˙
V (x) = ∇V (x) · f (x) ≤ 0.
Note that the first inequality is not strict: this relaxation allows for a faster
computation of a candidate. The verifier, on the other hand, produces counterexamples for V (x) > 0, thus retaining soundness of the overall procedure.
The CEGIS framework allows the separation between synthesis and verification.
So whilst the learner might propose candidates being completely independent
from domain D, the verifier is responsible to assert or to find the domain of
validity D. Our implementation establishes that at first the verifier checks the
validity of V (x) on the whole state space D = R
n ; if the computation is not successful – namely, the computational time is greater than a predefined timeout –
the verifier checks its validity over a smaller region, e.g. D = [−1, 1]
n , and so on.
If also this program fails, the algorithm returns an empty V (x). Recall that our
algorithm is in general not complete - indeed, consider the trivial problem of the
synthesis of a Lyapunov function for an unstable system, which is not possible:
in this case, the CEGIS procedure will surely return an empty V (x).
3.3 Lyapunov Function Synthesis for Parametric Models
Parametric models represent a challenge for both sound and numerical solvers.
Let us remark that both Gurobi and Z3 cannot synthesise functions in the presence of uncertainty, whereas Z3 can provide counterexamples using one or more
variables as fixed parameters, using the quantifier ForAll.