Methods used for Positive Matrix Definition for revalidation at code level

1

Good Morning,
I am currently addressing the study of Lyapunov functions to address stability in the context of V&V through formal methods. I am currently using CVX to compute the P matrix of the usual LMI.

I am interested in extrapolating as much information as possible from the solved objective and dual problems (as well as characteristics of the computed P matrix). Such information will be useful to perform the accurate revalidation at code level: the framework currently used is very pessimistic and at times models are not revalidated at code level.

Thus, I woud like to find more information on what is the process used in CVX (currently I used SDPT3 solver, but planning on using also MOSEK) to assure that the generated matrix is positive definite, when I impose the following constraints in MATLAB:

cvx_begin sdp
dual variable dvar % dual variables for matrix P
variable P(n,n) symmetric
dvar : A’PA - P <= -0.0000000000001eye(n) % close to 0
0.0000000000001eye(n) <= P
cvx_end

I am familiarising myself with semidefinite programming and convex optimisation, but I do not find the topics straightforward. In the CVX User Guide, I didn’t notice any explanation on the actual computation performed and I only read that the I should validate the result by adding:

min(eigenvalues of P) > 0

Could you please provide any guidance to documentation and particular notions I should address in my research, so that I may extrapolate further information on the problem that will allow to prove at code level what was proven at model level through MATLAB?

Thank you in advance!

2

I will just make the note that 0.0000000000001 is probably not a good value to use to ensure strict positive definiteness. A number such as 1e-6 or 1e-5 is probably better to use (assuming the rest of your problem is well-scaled), and certainly not smaller than 1e-8.

Do you really need to know how the SDP (LMI) solvers work, or just that they produce an optimal solution within solver tolerance of feasibility?

3

Dear Mark, thank you for your suggestion.
I believe it will be useful for me to know how the solvers work, or what they compute specifically, because I cannot assume the soundness of their solution when going down to code level, and I would need to do additional computations to validate the solution.

4

I think you should concentrate on validating the solution. Also, pay attention to the final status reported.

Also, try to make sure your problem is as well-scaled numerically as possible. Mosek is the most numerically robust of the SDP solvers, and also reports the best diagnostic information. make sure to pay attention to any warnings it might issue in the solver output.

5

Actually it is a not a bad idea to verify the solution independently. The solver returns the primal and dual solution, which is computed up to some tolerances. Using these solutions you can, even treating the solver as a black box, verify if the solution is both feasible and optimal, and if it is so up to your desired tolerances. So, no need to trust the solver on anything.