102
D. Ahmed et al.
Example 3 (CEGIS Operation). Assume the task is the synthesis of a function
g(x) that satisfies the following formula F (g(x)):
∃ g(x) ∀x ∈ R : ψ, where ψ(g(x)) = g(x) + 1 > 0.
The learner L offers an initial (often na¨ ıve, random or default) candidate, e.g.
g(x) = x, and passes it to the verifier Z. The verifier checks the validity of
ψ(x) = x + 1 > 0, ∀x ∈ R, by searching an instance ¯
x that might invalidate
the formula. Z finds that ¯
x = −1 invalidates the formula, thus sends ¯
x to L,
which incorporates this counterexample to synthesise a new g(x). The learner
now adds a constraint on the next candidate, as
C := g(−1) + 1 > 0, ∀x ∈ R,
such that the new candidate solution satisfies the formula at ¯
x = −1. The
learner now proposes g(x) = x
2 , which satisfies C, and passes it to Z. The
verifier searches for a counterexample to ψ(x
2 ), but cannot find any. Thus, it
exits the loop with an UNSAT answer, which proves that the synthesised function
g(x) = x
2 is valid ∀x ∈ R.
L
Z
¯
x
S
done
Fig. 1. CEGIS-based inductive synthesis. The iterative procedure loops between a
learner L and a verifier Z. L provides a candidate solution S to the verifier Z, which
asserts its validity or outputs a counterexample ¯
x. The learner provides a new solution
encompassing also ¯
x. The procedure stops once no counterexamples are found.
3 Automated and Sound Synthesis of Lyapunov
Functions via CEGIS and SMT
Consider a dynamical system ˙
x = f (x), where f : R
n
→ R
n , and assume that
the point x e ∈ R
n is an equilibrium, namely such that f (x e ) = 0 – without
loss of generality, we assume that x e = 0 (the origin). The goal is assessing
the stability of such equilibrium point via the synthesis of a Lyapunov function
V (x) : R
n
→ R. The stability of an equilibrium guarantees that trajectories
starting by the equilibrium remain close to it at all times (how close can often be
quantified, as done later in this work). If V (x) fulfils the following two conditions,
∀x ∈ D,
V (x) > 0, ˙
V (x) = ∇V (x) · f (x) ≤ 0,
(1)
D. Ahmed et al.
Example 3 (CEGIS Operation). Assume the task is the synthesis of a function
g(x) that satisfies the following formula F (g(x)):
∃ g(x) ∀x ∈ R : ψ, where ψ(g(x)) = g(x) + 1 > 0.
The learner L offers an initial (often na¨ ıve, random or default) candidate, e.g.
g(x) = x, and passes it to the verifier Z. The verifier checks the validity of
ψ(x) = x + 1 > 0, ∀x ∈ R, by searching an instance ¯
x that might invalidate
the formula. Z finds that ¯
x = −1 invalidates the formula, thus sends ¯
x to L,
which incorporates this counterexample to synthesise a new g(x). The learner
now adds a constraint on the next candidate, as
C := g(−1) + 1 > 0, ∀x ∈ R,
such that the new candidate solution satisfies the formula at ¯
x = −1. The
learner now proposes g(x) = x
2 , which satisfies C, and passes it to Z. The
verifier searches for a counterexample to ψ(x
2 ), but cannot find any. Thus, it
exits the loop with an UNSAT answer, which proves that the synthesised function
g(x) = x
2 is valid ∀x ∈ R.
L
Z
¯
x
S
done
Fig. 1. CEGIS-based inductive synthesis. The iterative procedure loops between a
learner L and a verifier Z. L provides a candidate solution S to the verifier Z, which
asserts its validity or outputs a counterexample ¯
x. The learner provides a new solution
encompassing also ¯
x. The procedure stops once no counterexamples are found.
3 Automated and Sound Synthesis of Lyapunov
Functions via CEGIS and SMT
Consider a dynamical system ˙
x = f (x), where f : R
n
→ R
n , and assume that
the point x e ∈ R
n is an equilibrium, namely such that f (x e ) = 0 – without
loss of generality, we assume that x e = 0 (the origin). The goal is assessing
the stability of such equilibrium point via the synthesis of a Lyapunov function
V (x) : R
n
→ R. The stability of an equilibrium guarantees that trajectories
starting by the equilibrium remain close to it at all times (how close can often be
quantified, as done later in this work). If V (x) fulfils the following two conditions,
∀x ∈ D,
V (x) > 0, ˙
V (x) = ∇V (x) · f (x) ≤ 0,
(1)