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!