104
D. Ahmed et al.
passes it to the verifier (in case of a linear function, the learner offers a matrix
¯
P i ). The goal of the verifier is to assert the validity of formula F from (3) according to the specification ψ in (1). The check is performed by negating F : if
there exists a vector ¯
x that satisfies ¬F , it is a counterexample for F ; if it does
not exist, formula F is valid and the candidate Lyapunov function is an actual
Lyapunov function. The domain D is encoded as an additional formula. Assume,
as an example, the domain is an hyper-sphere of radius one: D can be written
formally as d: ||x||
2
≤ 1. The final formula thus results in ¬F ∧ d.
A counterexample ¯
x must satisfy the formula V (¯ x) ≤ 0∨ ˙
V (¯ x) > 0. Reasoning
on either condition, it is easy to show that if there exists a counterexample ¯
x
invalidating a matrix ¯
P , then there exists an infinite number of counterexamples
for this ¯
P . Thus, particularly for high-dimensional models the generation of
meaningful counterexamples is crucial to find a Lyapunov function quickly.
Let us denote ¯
x i , i = 1, . . . , the series of counterexamples provided by the
verifier and ¯
P i the series of candidate Lyapunov function matrices provided by
the learner. In this setting, the learner proposes the first default candidate matrix
¯
P 0 ; the verifier will (possibly) provide a counterexample ¯
x 0 ; the learner includes
¯
x 0 in the set of constraints (cf. Section 3.1) and offers a new candidate ¯
P 1 .
In this work, we let Z3 generate counterexamples without any further goals.
However, counterexamples can be generated adding constraints, e.g. linear independence or orthogonality. Intuitively, more constraints might generate “better”
candidates by the learner, albeit at an increase in computational cost.
As intuition suggests, if we were to work with models having a diagonal matrix A, then the synthesis of diagonal candidates ¯
P i and of a diagonal solution P
would reduce the number of variables needed, thus speeding up the computation.
As such, if A is not diagonal but diagonalisable, the algorithm pre-computes the
system diagonalisation and feeds it to the CEGIS architecture returning a matrix P for the diagonal system, which is then converted to a solution for the
original model.
Learner A learner is the CEGIS component designated to suggest a candidate
solution for the problem under consideration. Within our framework, a learner
solves linear inequalities derived from F (V (¯ x)) as per Eq. (3), while memorising
the set of counterexamples {¯ x i | ¬F (¯ x i )} generated by the verifier. Whilst the
verifier works over continuous domains, note that the learner only considers a
finite number of points to synthesise the candidate Lyapunov function. At each
iteration i, the learner is tasked to solve 2i linear inequalities: i inequalities for
V ≥ 0 and i for ˙
V ≤ 0 – this is two inequalities per counterexample, so a set of
useful counterexamples is vital to achieve efficiency.
We implement two learners, for comparison: 1) a numerical and 2) a Z3based learner. However, our CEGIS architecture can in principle accommodate
any learner. The first learner uses Gurobi [10], a fast, commercial optimisation
solver for, among others, linear and quadratic programming problems, supporting continuous variables. Notice that the synthesis is a linear program: variables
p i,j , the entries of matrix P , appear linearly within the inequalities in F (V (¯ x i )).
D. Ahmed et al.
passes it to the verifier (in case of a linear function, the learner offers a matrix
¯
P i ). The goal of the verifier is to assert the validity of formula F from (3) according to the specification ψ in (1). The check is performed by negating F : if
there exists a vector ¯
x that satisfies ¬F , it is a counterexample for F ; if it does
not exist, formula F is valid and the candidate Lyapunov function is an actual
Lyapunov function. The domain D is encoded as an additional formula. Assume,
as an example, the domain is an hyper-sphere of radius one: D can be written
formally as d: ||x||
2
≤ 1. The final formula thus results in ¬F ∧ d.
A counterexample ¯
x must satisfy the formula V (¯ x) ≤ 0∨ ˙
V (¯ x) > 0. Reasoning
on either condition, it is easy to show that if there exists a counterexample ¯
x
invalidating a matrix ¯
P , then there exists an infinite number of counterexamples
for this ¯
P . Thus, particularly for high-dimensional models the generation of
meaningful counterexamples is crucial to find a Lyapunov function quickly.
Let us denote ¯
x i , i = 1, . . . , the series of counterexamples provided by the
verifier and ¯
P i the series of candidate Lyapunov function matrices provided by
the learner. In this setting, the learner proposes the first default candidate matrix
¯
P 0 ; the verifier will (possibly) provide a counterexample ¯
x 0 ; the learner includes
¯
x 0 in the set of constraints (cf. Section 3.1) and offers a new candidate ¯
P 1 .
In this work, we let Z3 generate counterexamples without any further goals.
However, counterexamples can be generated adding constraints, e.g. linear independence or orthogonality. Intuitively, more constraints might generate “better”
candidates by the learner, albeit at an increase in computational cost.
As intuition suggests, if we were to work with models having a diagonal matrix A, then the synthesis of diagonal candidates ¯
P i and of a diagonal solution P
would reduce the number of variables needed, thus speeding up the computation.
As such, if A is not diagonal but diagonalisable, the algorithm pre-computes the
system diagonalisation and feeds it to the CEGIS architecture returning a matrix P for the diagonal system, which is then converted to a solution for the
original model.
Learner A learner is the CEGIS component designated to suggest a candidate
solution for the problem under consideration. Within our framework, a learner
solves linear inequalities derived from F (V (¯ x)) as per Eq. (3), while memorising
the set of counterexamples {¯ x i | ¬F (¯ x i )} generated by the verifier. Whilst the
verifier works over continuous domains, note that the learner only considers a
finite number of points to synthesise the candidate Lyapunov function. At each
iteration i, the learner is tasked to solve 2i linear inequalities: i inequalities for
V ≥ 0 and i for ˙
V ≤ 0 – this is two inequalities per counterexample, so a set of
useful counterexamples is vital to achieve efficiency.
We implement two learners, for comparison: 1) a numerical and 2) a Z3based learner. However, our CEGIS architecture can in principle accommodate
any learner. The first learner uses Gurobi [10], a fast, commercial optimisation
solver for, among others, linear and quadratic programming problems, supporting continuous variables. Notice that the synthesis is a linear program: variables
p i,j , the entries of matrix P , appear linearly within the inequalities in F (V (¯ x i )).