Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
103
where D is a domain of interest containing x e then the Lyapunov function ensures boundedness of the trajectories. In other words, for every initial point
in a neighbourhood of x e , the trajectories of the model do not escape from D
(with reference to notations introduced above, the condition in (1) represents
the requirement ψ, and D denotes the set of inputs I). We use the following
polynomial expression for the Lyapunov function
V (x) =
c
l=1
(x
l )
T P l x
l ,
(2)
where x
l represents the element-wise exponentiation of vector x, i.e. element
x(j) to the power l, ∀j = 1, . . . , n; P l ∈ R
n×n is a weighting matrix associated
with x
l , and 2c is the order of the polynomial function. In order to obtain a
proper Lyapunov function V (x), the synthesiser is asked to verify the specification expressed by the formula
F (V (x)) : ∀x ∈ D, V (x) > 0 ∧ ˙
V (x) ≤ 0.
(3)
This specification requires the Lyapunov function to be positive definite, and
not to increase along the trajectories of the model. For linear systems, unless
otherwise stated, we consider D = R
n
\ {0} and c = 1, as it is known that
quadratic functions are sufficient to prove the stability of linear models over the
whole state space. Formula (3) keeps the elements of P uninterpreted, and thus
they are parameters to be found. Notice that the second-order formula
∃P ∈ R
n×n : ∀x ∈ D, V (x) > 0 ∧ ˙
V (x) ≤ 0,
would return a boolean value, i.e. True or False: to obtain the synthesised V (x)
function, we remove the existential quantifier.
3.1 The CEGIS Architecture for Lyapunov Function Synthesis
We introduce the CEGIS architecture to find Lyapunov functions. To better illustrate the methodology, we start by considering linear models (the non-linear
case is further discussed in Section 3.2). As mentioned earlier, two components
characterise the CEGIS approach: a learner and a verifier. The CEGIS architecture takes the system matrix A and outputs a matrix P as the key component
of the function V (x), verifying the conditions in Eq. (1). We denote by ¯
P i ,
i = 0, 1, 2, . . . the candidate matrices yet to be verified, i.e. the outputs of the
learner. As anticipated earlier, referring to Eq. (2), we set c = 1 and D = R
n
\{0}.
Verifier The scope of a verifier is twofold: generate a counterexample to the
validity of the candidate Lyapunov function, or certify its validity over a domain
of interest. We implement the verifier in Z3.
The methodology to assert the correctness of a Lyapunov function is as follows. Assume the learner computes a candidate Lyapunov function V (x) and
103
where D is a domain of interest containing x e then the Lyapunov function ensures boundedness of the trajectories. In other words, for every initial point
in a neighbourhood of x e , the trajectories of the model do not escape from D
(with reference to notations introduced above, the condition in (1) represents
the requirement ψ, and D denotes the set of inputs I). We use the following
polynomial expression for the Lyapunov function
V (x) =
c
l=1
(x
l )
T P l x
l ,
(2)
where x
l represents the element-wise exponentiation of vector x, i.e. element
x(j) to the power l, ∀j = 1, . . . , n; P l ∈ R
n×n is a weighting matrix associated
with x
l , and 2c is the order of the polynomial function. In order to obtain a
proper Lyapunov function V (x), the synthesiser is asked to verify the specification expressed by the formula
F (V (x)) : ∀x ∈ D, V (x) > 0 ∧ ˙
V (x) ≤ 0.
(3)
This specification requires the Lyapunov function to be positive definite, and
not to increase along the trajectories of the model. For linear systems, unless
otherwise stated, we consider D = R
n
\ {0} and c = 1, as it is known that
quadratic functions are sufficient to prove the stability of linear models over the
whole state space. Formula (3) keeps the elements of P uninterpreted, and thus
they are parameters to be found. Notice that the second-order formula
∃P ∈ R
n×n : ∀x ∈ D, V (x) > 0 ∧ ˙
V (x) ≤ 0,
would return a boolean value, i.e. True or False: to obtain the synthesised V (x)
function, we remove the existential quantifier.
3.1 The CEGIS Architecture for Lyapunov Function Synthesis
We introduce the CEGIS architecture to find Lyapunov functions. To better illustrate the methodology, we start by considering linear models (the non-linear
case is further discussed in Section 3.2). As mentioned earlier, two components
characterise the CEGIS approach: a learner and a verifier. The CEGIS architecture takes the system matrix A and outputs a matrix P as the key component
of the function V (x), verifying the conditions in Eq. (1). We denote by ¯
P i ,
i = 0, 1, 2, . . . the candidate matrices yet to be verified, i.e. the outputs of the
learner. As anticipated earlier, referring to Eq. (2), we set c = 1 and D = R
n
\{0}.
Verifier The scope of a verifier is twofold: generate a counterexample to the
validity of the candidate Lyapunov function, or certify its validity over a domain
of interest. We implement the verifier in Z3.
The methodology to assert the correctness of a Lyapunov function is as follows. Assume the learner computes a candidate Lyapunov function V (x) and