Finding a Strict Lyapunov Function for $\ddot{x} + \dot{x} + x^3 = 0$ Consider the system $\dot{x}=y$ and $\dot{y}=-x^3-y$. We know that the function $V(x,y)=0.5y^2+0.25x^4$ is a Lyapunov function for the system and thus, the system is stable. However, we know that the system is globally asymptotically stable (by looking at the vector field). How can we prove global asymptotic stability of this system?
Thank you, in advance, for your response!
 A: We can use the function $V=x^2+2xy+2y^2+x^4$.
We can see that $\dot{V}=-2x^4-2y^2 < 0$. Since the function $V$ is coercive and defined on $\mathbb{R}^2$, the system is globally asymptotically stable according to the Lyapunov theorem.
Another interesting solution to this question is to use the Barbashin-Krasovskii theorem as @AVK mentioned.
A: We can use the Barbashin-Krasovskii theorem (see, for instance, H.Khalil, Nonlinear systems, Corollary 4.2):
$\bullet$ Let $x=0$ be an equilibrium point for $\dot x=f(x)$. Let $V:\mathbb R^n\to\mathbb R$ be a continuously differentiable, radially unbounded, positive definite function such that $\dot V\le 0$ for all $x\in\mathbb R^n$. Let $S=\{x\in\mathbb R^n \;|\; \dot V(x)=0\}$ and suppose that no solution can stay identically in $S$, other than the trivial solution $x(t)\equiv 0$. Then, the origin is globally asymptotically stable. $\bullet$
The derivative 
$$
\dot V= x^3\dot x+y\dot y=x^3y-x^3y-y^2=-y^2\le 0
$$
is equal to zero in
$S=\{(x,y)\in\mathbb R^2: y=0\}$;
for any point $(x,y)\in S$ we have 
$$\dot y=-x^3,$$
hence, if $x\ne 0$, i.e. the solution is not trivial, then the solution can't stay in $S$. Thus, the conditions of the theorem are satisfied.
