108
D. Ahmed et al.
4 Case Studies and Experiments
In this Section we outline a few experiments to challenge the validity of our
approach. Our technique is coded in Python 2.7 [30], using external libraries as
the numerical solver Gurobi and the SMT solver Z3 (cf. Section 2). Specifically,
we compare two CEGIS architectures:
1. Gurobi learner and Z3 verifier,
2. Z3 learner and Z3 verifier,
later denoted as Gurobi-CEGIS and Z3-CEGIS, respectively, against the optimisation toolbox SOSTOOLS. Whilst Z3 is an efficient verifier, it carries the weight
of exact representations. We therefore compare its use within the learner to that
of a numerical solver such as Gurobi - recall that the learner does not need to be
sound. A relevant feature of the synthesis procedure is its linearity in the entries
of matrix P : we expect an efficient LP solver to outperform an SMT solver. As
such, we study the expected tradeoff between speed and precision. As specified
earlier, the initial candidate for the learner ¯
P 0 is arbitrary: we challenge the procedure by setting ¯
P 0 = −I, which does not satisfy the first positivity condition
for Lyapunov functions, thus showing that even with an ill-suited initial guess
the procedure can rapidly synthesise a valid Lyapunov function. SOSTOOLS is a
sum-of-squares optimisation toolbox available for MATLAB, equipped with the
solver SeDuMi [31]. It can be used to solve a wide range of problems, from mixed
continuous-discrete optimisations to finding Lyapunov functions for polynomial
dynamical systems.
We consider linear, non-linear and parametric ODEs with the origin as (one
of) the equilibrium(a), and aim to obtain a Lyapunov function guaranteeing the
stability of such equilibrium point. The procedure entails the following steps:
a) a function f (x), x ∈ R
n , is fed as the input;
b) a Lyapunov function V (x), as in Eq. (2), is computed;
c) in the linearisation case, the stability region R in Eq. (4) for V (x) is found.
Let us emphasise that Z3 is unable to fully handle non-polynomial terms, which
represents the only limitation of our approach. Unlike most of the literature,
counterexamples are not limited to a finite set but searched over the whole R
n .
Linear models are certainly an easier task than polynomial systems. The
study with linear models focuses mainly on the scalability of the method, encompassed by the average and maximum/minimum computational time, and the
number of iterations performed. We generate N = 100 random linear models of
dimension n ∈ [3, 10]. For each linear system, the entries of matrix A range
within [−1000, 1000] ∈ R. For each test we set c = 1 (cf. Eq. (2)), namely we
impose a quadratic structure to the Lyapunov function, and collect the number of iterations of the procedure, i.e. the number of counterexamples needed to
compute a valid Lyapunov function, and the total elapsed time. Recall that the
initial synthesiser’s candidate is ¯
P 0 = −I, which challenges the reliability of our
method with a bad initial condition. A 180 seconds timeout is set for every run.
D. Ahmed et al.
4 Case Studies and Experiments
In this Section we outline a few experiments to challenge the validity of our
approach. Our technique is coded in Python 2.7 [30], using external libraries as
the numerical solver Gurobi and the SMT solver Z3 (cf. Section 2). Specifically,
we compare two CEGIS architectures:
1. Gurobi learner and Z3 verifier,
2. Z3 learner and Z3 verifier,
later denoted as Gurobi-CEGIS and Z3-CEGIS, respectively, against the optimisation toolbox SOSTOOLS. Whilst Z3 is an efficient verifier, it carries the weight
of exact representations. We therefore compare its use within the learner to that
of a numerical solver such as Gurobi - recall that the learner does not need to be
sound. A relevant feature of the synthesis procedure is its linearity in the entries
of matrix P : we expect an efficient LP solver to outperform an SMT solver. As
such, we study the expected tradeoff between speed and precision. As specified
earlier, the initial candidate for the learner ¯
P 0 is arbitrary: we challenge the procedure by setting ¯
P 0 = −I, which does not satisfy the first positivity condition
for Lyapunov functions, thus showing that even with an ill-suited initial guess
the procedure can rapidly synthesise a valid Lyapunov function. SOSTOOLS is a
sum-of-squares optimisation toolbox available for MATLAB, equipped with the
solver SeDuMi [31]. It can be used to solve a wide range of problems, from mixed
continuous-discrete optimisations to finding Lyapunov functions for polynomial
dynamical systems.
We consider linear, non-linear and parametric ODEs with the origin as (one
of) the equilibrium(a), and aim to obtain a Lyapunov function guaranteeing the
stability of such equilibrium point. The procedure entails the following steps:
a) a function f (x), x ∈ R
n , is fed as the input;
b) a Lyapunov function V (x), as in Eq. (2), is computed;
c) in the linearisation case, the stability region R in Eq. (4) for V (x) is found.
Let us emphasise that Z3 is unable to fully handle non-polynomial terms, which
represents the only limitation of our approach. Unlike most of the literature,
counterexamples are not limited to a finite set but searched over the whole R
n .
Linear models are certainly an easier task than polynomial systems. The
study with linear models focuses mainly on the scalability of the method, encompassed by the average and maximum/minimum computational time, and the
number of iterations performed. We generate N = 100 random linear models of
dimension n ∈ [3, 10]. For each linear system, the entries of matrix A range
within [−1000, 1000] ∈ R. For each test we set c = 1 (cf. Eq. (2)), namely we
impose a quadratic structure to the Lyapunov function, and collect the number of iterations of the procedure, i.e. the number of counterexamples needed to
compute a valid Lyapunov function, and the total elapsed time. Recall that the
initial synthesiser’s candidate is ¯
P 0 = −I, which challenges the reliability of our
method with a bad initial condition. A 180 seconds timeout is set for every run.