# Systematic Analysis and Design of Control Systems Based on [PERSON]'s Direct Method
## 4 Controller Design  
### Control Lyapunov Function  
Consider the system (31) with an equilibrium at the origin. In the controller design, the question arises whether this equilibrium can be stabilized with a state feedback  
\[u=k(x). \tag{48}\]  
This problem leads to the concept of the control Lyapunov functions. In this generalization of the Lyapunov function, the focus is not on stability, but on stabilizability ([10] Theorem 4.1). Theorem 4.2 (Artstein's Theorem): _Let the function \(V:\mathbb{R}^{n}\to[0,\infty)\) be continuously differentiable, positive definite, and radially unbounded. A system of the form (31) is stabilizable with a state feedback (48) if and only if_  
\[\forall x\
eq 0:\quad\inf_{u}\dot{V}(x,u)<0 \tag{49}\]  
_holds._  
A function \(V\) satisfying the conditions of Theorem 4.2 is called a _control Lyapunov function_ (_CLF_). For an input affine system  
\[\dot{x}=f(x)+g(x)u \tag{50}\]  
with vector fields \(f,g:\mathbb{R}^{n}\to\mathbb{R}^{n}\), the function \(V\) along the system dynamics has the time derivative  
\[\dot{V}(x,u)=L_{f}V(x)+L_{g}V(x)u.\]  
Thus, the condition (49) can be expressed in the form  
\[\forall x\
eq 0:\quad\inf_{u}\Bigl{(}L_{f}V(x)+L_{g}V(x)u\Bigr{)}<0. \tag{51}\]The condition (51) can also be specified via the expression  
\[\forall x\
eq 0:\quad L_{g}V(x)=0\implies L_{f}V(x)<0, \tag{52}\]  
if no access to the system dynamics is possible via the control input because of \(L_{g}V(x)=0\), the system must be stable in its dynamics (\(L_{f}V(x)<0\)), see, e.g., [11; 58]. Once a control Lyapunov function has been found for a given system (50), then the system can be stabilized via a state feedback (48) of the form  
\[u=k(x)= \begin{cases}0&\text{for }b=0\\ -\frac{1}{b}\Big{(}a+\sqrt{a^{2}+b^{4}}\Big{)}&\text{for }b\
eq 0,\end{cases}  \tag{53}\]  
with \(a=L_{f}V(x)\) and \(b=L_{g}V(x)\). To justify this, consider the time derivative of \(V\) along the solution of the closed-loop system  
\[\dot{V}(x,k(x))=a+b\,k(x)= \begin{cases}\quad a<0&\text{for }b=0,x\
eq 0,\\ -\sqrt{a^{2}+b^{4}}&\text{for }b\
eq 0,x\
eq 0,\end{cases} \]  
which is negative definite. Thus, the closed-loop equilibrium \(x=0\) is globally asymptotically stable. The state feedback (53) is called _[PERSON]'s formula_[9; 58]. Similar formulas are also obtained via other approaches, such as inverse or modified optimal control [59; 60; 61] if the control Lyapunov function is known. The question now arises whether a CLF \(V\) exists and respectively how such a function can be found. For this purpose, one sets up an approach \(V(x,q)\) for a positive definite function with a parameter vector \(q\), e.g., as a quadratic form  
\[V(x,q)=x^{T}P(q)\,x\quad\text{with}\quad P(q)=P^{T}(q)\succ 0,\]  
where the vector \(q\) contains the free entries of the positive definite matrix \(P\). The positive definiteness of the functions \(V\) is then ensured [41] via [PERSON]'s theorem (minimum-maximum principle). As more general approaches, functions with even powers can be used [57]. For a positive definite initial function \(V(x,q)\) and a system of the form (31), the condition (49) can be expressed by the prenex formula  
\[\exists q\,\forall x\,\exists u:\quad x\
eq 0\implies L_{F}V(x,u,q)<0 \tag{54}\]  
and thus address it by quantifier elimination. Here, the statement (54) formulates a decision problem that verifies the suitability of the approach \(V(x,q)\) as a CLF. For an input affine system (50), the condition (52) leads to the prenex formula  
\[\exists q\,\forall x:\ \big{(}x\
eq 0\wedge L_{g}V(x,q)=0\big{)}\implies L _{f}V(x,q)<0. \tag{55}\]  
If after quantifier elimination it is evident that the conditions (54) or (55) are satisfied, then the entries of the parameter vector \(q\) can be chosen as free variables and the admissible parameter values can be determined step by step. This is performed by successively removing the corresponding existential quantifiers at the individual elements of the vector \(q\) and performing quantifier elimination.