# Kleene Algebra to Compute Invariant Sets of Dynamical Systems
## 5 Application to Dynamical Systems
### Invariant Set  
In this section, we now show that the automorphism is linked to invariant sets by a Kleene star operator. More precisely, we will show that \(\mathrm{Inv}^{+}(\mathbb{A})=\overrightarrow{f}^{*}(\mathbb{A})\). As a consequence, an interval evaluation of \(\overrightarrow{f}^{*}(\mathbb{A})\) will allow us to have an inner and an outer approximation of an invariant set \(\mathrm{Inv}^{+}(\mathbb{A})\).  
Theorem 5.1: _The set \(\overrightarrow{f}^{*}(\mathbb{A})\) contains the greatest positive invariant subset of \(\mathbb{A}\), i.e.,_  
\[\mathit{Inv}^{+}(\mathbb{A})\subset\overrightarrow{f}^{*}(\mathbb{A}). \tag{29}\]  
Proof: The proof is by contradiction. Assume that (6) is false. Thus, there exists the largest integer \(i\) such that \(\mathrm{Inv}^{+}(\mathbb{A})\subset\mathbb{B}=(\mathrm{Id}\cap\overrightarrow {f})^{i}(\mathbb{A})\). Equivalently, there exists \(\mathbf{a}\) (see Figure 6) such that  
\[\left\{\begin{array}{ll}(\mathrm{i})&\mathbf{a}\in\mathbb{B}\\ (\mathrm{ii})&\mathbf{a}\
otin\left(\mathrm{Id}\cap\overrightarrow{f}\right) (\mathbb{B})\\ (\mathrm{iii})&\mathbf{a}\in\mathrm{Inv}^{+}(\mathbb{B})\end{array}\right. \tag{30}\]  
now  
\[\left(\mathrm{Id}\cap\overrightarrow{f}\right)(\mathbb{B})=\Big{\{}\mathbf{x} \in\mathbb{B}\,|\,\mathbf{\Psi}_{\gamma|\mathcal{P}(\mathbf{x})}(\mathbf{x}) \subset\mathbb{B}\Big{\}}, \tag{31}\]  
thus  
\[\left\{\begin{array}{ll}\mathbf{a}\in\mathrm{Inv}^{+}(\mathbb{B})&\text{( see (\ref{eq:10}, \mathrm{iii}))}\\ \mathbf{\Psi}_{\gamma|\mathcal{P}(\mathbf{a})}(\mathbf{a})\
ot\subset\mathbb{B}& \text{(since (\ref{eq:10}, \mathrm{ii}))}\end{array}\right. \tag{32}\]  
which is inconsistent with Proposition 6.  
Theorem 5.2: _We have_  
\[\overrightarrow{f}^{*}(\mathbb{A})\subset\mathit{Inv}^{+}(\mathbb{A}). \tag{33}\]  
Proof: The proof is by contradiction, i.e., we assume that \(\overrightarrow{f}^{*}(\mathbb{A})\
ot\subset\mathrm{Inv}^{+}(\mathbb{A})\). In such a case, there exists \(\mathbf{a}\in\overrightarrow{f}^{*}(\mathbb{A})\), which is not in \(\mathrm{Inv}^{+}(\mathbb{A})\), as illustrated by Figure 7. For such a point \(\mathbf{a}\), the trajectory \(\mathbf{\varphi}_{\gamma}(t,\mathbf{a}),t\geq 0\) leaves \(\overrightarrow{f}^{*}(\mathbb{A})\) at the point \(\mathbf{b}=\mathbf{\varphi}_{\gamma}(t_{b},\mathbf{a})\) for some \(t_{b}>0\) and then leaves \(\mathbb{A}\) at point \(\mathbf{d}\). In the figure, the set \(\mathbf{\Psi}_{\gamma|\mathcal{P}(\mathbf{b})\cap\mathbb{A}}(\mathbf{b})\) corresponds to the trajectory between \(\mathbf{b}\) and \(\mathbf{c}\). Therefore, we can write  
\[\begin{array}{ll}(i)&\mathbf{b}\in\mathrm{boundary}\Big{(}\overrightarrow {f}^{*}(\mathbb{A})\Big{)}\\ (ii)&\mathbf{b}\
otin\left(\mathrm{Id}\cap\overrightarrow{f}\right)\left( \overrightarrow{f}^{*}(\mathbb{A})\right)\end{array}, \tag{34}\]  
Figure 5: Forward Eulerian predictor \(\overrightarrow{f}(\mathbb{A})\) eliminating points that will escape from \(\mathbb{A}\).  
however, also, there exists a neighborhood \(\mathcal{V}_{\mathbf{b}}\) of \(\mathbf{b}\) such that  
\[\forall\mathbf{b}^{\prime}\in\mathcal{V}_{\mathbf{b}},\mathbf{b}^{\prime}\
ot\in \underbrace{\left(\mathrm{Id}\cap\overrightarrow{f}\right)\left(\overrightarrow {f}^{*}(\mathbb{A})\right)}_{=\overrightarrow{f}^{*}(\mathbb{A})} \tag{35}\]  
which is inconsistent with (34, (_i_)).  
**Corollary 1**.: _The set-valued function_  
\[\overleftarrow{f}\left(\mathbb{A}\right) = \Big{\{}\mathbf{x}|\boldsymbol{\
abla}_{-\boldsymbol{\gamma}| \mathcal{P}(\mathbf{x})}(\mathbf{x})\subset\mathbb{A}\Big{\}} \tag{36}\]  
_is an automorphism. Moreover, \(\overleftarrow{f}^{*}(\mathbb{A})\) corresponds to the greatest negative invariant subset of \(\mathbb{A}\), i.e.,_  
\[\overleftarrow{f}^{*}(\mathbb{A})=\text{Inv}^{+}(-\boldsymbol{\gamma}, \mathbb{A})\overset{(\mathbb{A})}{=}\Big{\{}\mathbf{a}|\forall t\geq 0, \boldsymbol{\varphi}_{\boldsymbol{\gamma}}(-t,\mathbf{a})\in\mathbb{A}\Big{\}}. \tag{37}\]