RuikunZhou / Unknown_Neural_Lyapunov

Neural Lyapunov control of unknown nonlinear systems with stability guarantees
11 stars 0 forks source link

Issues with Path Following Dynamics and Lyapunov condition #2

Closed jlwu002 closed 3 months ago

jlwu002 commented 7 months ago

Dear Ruikun,

Thank you for your interesting work. We have conducted a follow-up study on your research, where we solved for a controller and certified the Lyapunov conditions for arbitrary nonlinear dynamical systems in the discrete-time setting: https://github.com/jlwu002/nlc_discrete (NeurIPS 2023), paper.

While reproducing your work, we found the following two issues:

1) Issue with Path Following Dynamics. There appears to be a typo in the path following dynamics formula: the dynamic for $\dot{\theta}$ (angle error) should use $\dot{d_e}$ in the denominator (where $d_e$ is the distance error), instead of $d_e$ as currently written in the paper and code. The correct dynamic should be: $\dot{\theta}_e = \frac{\omega - v\kappa(s) \cos(\theta_e)}{1 - \dot{d_e}\kappa(s)}$, instead of: $\dot{\theta}_e = \frac{\omega - v\kappa(s) \cos(\theta_e)}{1 - d_e\kappa(s)}$ (Snider [2009], Chang [2019])

2) Issue with Lyapunov conditions. In your code, the function "CheckLyapunov" checks for the condition V >= 0 and lie_derivative_ofV <= epsilon. However, there is another critical constraint for Lyapunov conditions: V(0) = 0. Since the neural network structure used in your work include bias terms (z1 = np.dot(vars,w1.T)+b1; z2 = np.dot(a1,w2.T)+b2; V_learn = tanh(z2.item(0))), V(0) = 0 is not guaranteed. This will cause issues, for example, the system cannot distinguish between the equilibrium point and other points with the same value. We need to check V(x_t) - V(0) > 0.

Thank you! Junlin

RuikunZhou commented 6 months ago

Hi Junlin,

Thanks for your comments and for sharing your interesting work.

Regarding the two issues you mentioned, please see the following responses.

  1. I believe the formula for the unicycle path following in my paper is correct, which is Eq. (20) in the appendix. Firstly, we used the unicycle model from Carona [2008] in our experiments, instead of the bicycle model. Also, regarding the bicycle model for path following, we carefully investigated this example when writing this paper. It seems that the derivation of the formula in the paper you cited is incorrect, which might also result in the incorrect formula for the path following example in the appendix of the Neural Lyapunov Control paper. Here is why: In that paper, they use $\dot{\theta_p}(s) = \kappa(s)\dot{s}$ and $\dot{s}=v_1 \cos(\theta_e) + \dot{\thetap} e{ra}$ to derive Eq. (12). By substituting the former one into the latter one, we have: $(1-\kappa(s) e_{ra}) \dot{s} = v_1 \cos(\theta_e)$. Clearly, we have $\dot{s} = \frac{\cos(\thetae)}{1 - e{ra}\kappa(s)} v_1$. Substituting this and $\dot{\theta_p}(s) = \kappa(s)\dot{s}$ into $\dot{\theta_e} = \dot{\theta} - \dot{\theta_p}(s)$, yields, $$\dot{\theta_e} = ( \frac{\tan(\delta)}{L} - \frac{\kappa(s)\cos(\thetae)}{1 - e{ra}\kappa(s)} ) v1.$$ Clearly, in the second term in the bracket, it should be $e{ra}$ in the denominator, instead of $\dot{e}_{ra}$. If you are interested in the derivation of the kinematics model of the bicycle, I strongly recommend you to see the detailed and correct derivation in De Luca [2005].

More importantly, with the correct formula as Eq. (20) in our paper, by setting $\kappa(s) = 1$, we have it is a 2-dimensional autonomous system. However, if we have $\dot{d_e}$ in the denominator, it is obviously not.

  1. As we discussed during the rebuttal on Openreview (response to Q4 from Reviewer KQuS), the condition $V(0) = 0$ is not computational enforceable with the SMT solver, dReal. It is not rigorously a Lyapunov function, but with reasonable assumptions, Assumptions 3 & 4, we showed the origin is asymptotically stable.

Moreover, we fixed this issue by proposing more rigorous verification process with mathematical proofs as a side result in our newly published papers.

Thanks.