Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
107
Let us consider variable x, a parameter μ and a formula ψ(x, μ): Z3 can find
a counterexample for all values of μ by validating ForAll(μ, ψ). If μ belongs
to a range [l, u], Z3 can find a counterexample by checking ψ ∧ μ ≥ l ∧ μ ≤ u.
This provides a counterexample (¯ x, ¯
μ) for x and μ, respectively.
The synthesis procedure is split into two steps, in view of the inability of
Z3 and Gurobi to propose parametric solutions. The first step synthesises a
candidate Lyapunov function solely using the constraint V (x) > 0, in which no
parameter appears. The second step evaluates the constraint ˙
V ≤ 0 to propose
a parametric Lyapunov function exploiting the results from the first step. The
following example details the procedure.
Example 4. Consider a two-dimensional linear parametric system [23] and a candidate Lyapunov function
˙
x = y
˙
y = −(2 + μ)x − y
, V (x, y) = p 1 x
2 + p 2 y
2 .
Assume the first guess of the learner is invalid, i.e. the verifier finds a counterexample for the validity of V (x, y). The counterexample (¯ x, ¯
y) is then sent to the
learner. The synthesis procedure is split into two steps: the first step entails the
synthesis solely accounting for V (¯ x, ¯
y) > 0. The learner is tasked to solve
V (¯ x, ¯
y) = p 1 ¯
x
2 + p 2 ¯
y
2 > 0,
where p 1 , p 2 are the variables of the inequality. The learner will propose values ¯
p 1
and ¯
p 2 satisfying the inequality. The second step removes one of the synthesised
¯
p i , e.g. ¯
p 1 , in order to re-synthesise it including the parameters found in ˙
V . In
practical terms, the expression of ˙
V is evaluated at ¯
x, ¯
y and ¯
p 2 , as
˙
V = 2p 1 ¯
x¯ y − 2¯ p 2 ¯
y
2
− 2(μ + 2)¯ x¯ y ≤ 0 =⇒ p 1 ≤ ¯
p 2
¯
y
¯
x
+ 2 + μ
.
We choose the value p 1 that satisfies the equality. The candidate Lyapunov
function thus results in V (x, y) = ¯
p 2
¯
y
¯
x + 2 + μ
· x
2 + ¯
p 2 · y
2 . This procedure
holds as long as ¯
x = 0: if this is not the case, we can either choose to synthesise
a new value for p 2 or simply maintain the numerical values obtained after the
first step. In the latter case, once the candidate Lyapunov function is passed to
the verifier, a new counterexample will be generated and the procedure can be
repeated until a parametric Lyapunov function is found and verified. Another
possible approach is based on the mixed-terms removal: p 1 is synthesised so
that the terms carrying ¯
x¯ y cancel out. Further, the choice of p 1 satisfying the
equality is arbitrary: we can add a negative constant to its value to solve the
strict inequality instead. Finally, more than one parameter ¯
p i can be removed
in the second step: this can spread the parametric coefficients among more than
one p i . However, this is likely to increase the computational cost in view of the
inequality being a function of more than one variable.
107
Let us consider variable x, a parameter μ and a formula ψ(x, μ): Z3 can find
a counterexample for all values of μ by validating ForAll(μ, ψ). If μ belongs
to a range [l, u], Z3 can find a counterexample by checking ψ ∧ μ ≥ l ∧ μ ≤ u.
This provides a counterexample (¯ x, ¯
μ) for x and μ, respectively.
The synthesis procedure is split into two steps, in view of the inability of
Z3 and Gurobi to propose parametric solutions. The first step synthesises a
candidate Lyapunov function solely using the constraint V (x) > 0, in which no
parameter appears. The second step evaluates the constraint ˙
V ≤ 0 to propose
a parametric Lyapunov function exploiting the results from the first step. The
following example details the procedure.
Example 4. Consider a two-dimensional linear parametric system [23] and a candidate Lyapunov function
˙
x = y
˙
y = −(2 + μ)x − y
, V (x, y) = p 1 x
2 + p 2 y
2 .
Assume the first guess of the learner is invalid, i.e. the verifier finds a counterexample for the validity of V (x, y). The counterexample (¯ x, ¯
y) is then sent to the
learner. The synthesis procedure is split into two steps: the first step entails the
synthesis solely accounting for V (¯ x, ¯
y) > 0. The learner is tasked to solve
V (¯ x, ¯
y) = p 1 ¯
x
2 + p 2 ¯
y
2 > 0,
where p 1 , p 2 are the variables of the inequality. The learner will propose values ¯
p 1
and ¯
p 2 satisfying the inequality. The second step removes one of the synthesised
¯
p i , e.g. ¯
p 1 , in order to re-synthesise it including the parameters found in ˙
V . In
practical terms, the expression of ˙
V is evaluated at ¯
x, ¯
y and ¯
p 2 , as
˙
V = 2p 1 ¯
x¯ y − 2¯ p 2 ¯
y
2
− 2(μ + 2)¯ x¯ y ≤ 0 =⇒ p 1 ≤ ¯
p 2
¯
y
¯
x
+ 2 + μ
.
We choose the value p 1 that satisfies the equality. The candidate Lyapunov
function thus results in V (x, y) = ¯
p 2
¯
y
¯
x + 2 + μ
· x
2 + ¯
p 2 · y
2 . This procedure
holds as long as ¯
x = 0: if this is not the case, we can either choose to synthesise
a new value for p 2 or simply maintain the numerical values obtained after the
first step. In the latter case, once the candidate Lyapunov function is passed to
the verifier, a new counterexample will be generated and the procedure can be
repeated until a parametric Lyapunov function is found and verified. Another
possible approach is based on the mixed-terms removal: p 1 is synthesised so
that the terms carrying ¯
x¯ y cancel out. Further, the choice of p 1 satisfying the
equality is arbitrary: we can add a negative constant to its value to solve the
strict inequality instead. Finally, more than one parameter ¯
p i can be removed
in the second step: this can spread the parametric coefficients among more than
one p i . However, this is likely to increase the computational cost in view of the
inequality being a function of more than one variable.