Closed kimukook closed 3 years ago
Hi Muhan Zhao,
Some regions of LieV are positive because the candidate Lyapunov function is not a valid Lyapunov function (it doesn’t pass the verification from dReal).
I run the inverted pendulum jupyter notebook with dReal: v4.19.02.1 and Pytorch: 1.2.0. The candidate can pass and the LieV plot shown as below:
The different versions of the tool might need to use different parameters and iteration to pass the verification. Thank you :)
Hi Ya-Chien,
I tried to run your inverted pendulum case on my own laptop and plot the Lyapunov function and its Lie derivative as shown below:
![NNLF_Vdot2](https://user-images.githubusercontent.com/22064903/113354144-9043c200-92f3-11eb-8463-7a02311691e0.png)
There are some regions that Lie derivative of V is positive. Also I found it is pretty weird but I am not sure which part I did it incorrectly, running the same code from Jupiter notebook on my laptop does not show Lyapunov conditions are satisfied from
CheckLyapunov
usingdReal
. Any suggestion on this? Thank you!