# Kleene Algebra to Compute Invariant Sets of Dynamical Systems
## 4 Kleene Algebra of Automorphisms
### Intervals  
Given a lattice \((\mathcal{L},\leq,\wedge,\vee)\) and an automorphism \(f\in\mathcal{A}(\mathcal{L})\), we want to compute \(f^{*}(a)\) where \(a\in\mathcal{L}\). We consider also a machine lattice \(\mathcal{L}_{M}\) of \(\mathcal{L}\). An automorphism of \(\mathcal{L}_{M}\) is called a _machine automorphism_. As seen in Subsection 3.2, since \(\mathcal{A}(\mathcal{L})\) is a Kleene algebra, we can define intervals in \(\mathcal{A}(\mathcal{L})\).  
**Definition 2**.: _An interval of \(\mathcal{A}(\mathcal{L})\) is a subset \([f]\) of \(\mathcal{A}(\mathcal{L})\), which can be written as_  
\[[f]=[f^{-},f^{+}]=\{f\in\mathcal{A}(\mathcal{L})|f^{-}\leq f\leq f^{+}\} \tag{18}\]  
_where \(f^{-},f^{+}\) belong to \(\mathcal{A}(\mathcal{L}_{M})\)._  
**Proposition 5**.: _We have_  
\[\text{Fix}\big{(}(f^{-})^{*}\big{)}\subset\mathcal{L}_{M}\cap\text{Fix}(f^{* })\subset\text{Fix}\big{(}(f^{+})^{*}\big{)}. \tag{19}\]  
Proof.: Let us first prove the first inclusion. First, since \((f^{-})^{*}\in\mathcal{A}(\mathcal{L}_{M})\), all its fixed points are inside \(\mathcal{L}_{M}\). We have  
\[\begin{array}{llll}a\in\text{Fix}\big{(}(f^{-})^{*}\big{)}&\Rightarrow&(f^ {-})^{*}(a)=a,\\ &\Leftrightarrow&a\wedge f^{-}(a)=a\qquad\text{(see (\ref{eq:10}))}\\ &\Rightarrow&a\wedge f(a)\geq a\qquad\text{(since $f^{-}\leq f$)}\\ &\Leftrightarrow&a\wedge f(a)=a\qquad\text{(since $a\wedge x\leq a$)}\\ &\Leftrightarrow&f^{*}(a)=a\qquad\text{(see (\ref{eq:10})).}\end{array}\]  
Let us now prove the second inclusion. We have  
\[\begin{array}{llll}&a\in\mathcal{L}_{M}\cap\text{Fix}(f^{*})\\ \Rightarrow&f^{*}(a)=a,a\in\mathcal{L}_{M}\\ \Leftrightarrow&a\wedge f(a)=a,a\in\mathcal{L}_{M}\qquad\text{(see (\ref{eq:10}))}\\ \Rightarrow&a\wedge f^{+}(a)\geq a\qquad\text{(since $f\leq f^{+}$)}\\ \Leftrightarrow&a\wedge f^{+}(a)=a\qquad\text{(since $a\wedge x\leq a$)}\\ \Leftrightarrow&(f^{+})^{*}(a)=a\qquad\text{(see (\ref{eq:10}))}\end{array}\]  
**Theorem 1**.: _If \(a\in[a^{-},a^{+}]\), where \(a^{-},a^{+}\) both belong to \(\mathcal{L}_{M}\), then_  
\[\begin{array}{ll}(i)&f^{*}(a)\in\big{[}(f^{-})^{*}(a^{-}),(f^{+})^{*}(a^{+}) \big{]}\\ (ii)&f^{*}\circ(f^{-})^{*}(a^{-})=(f^{-})^{*}(a^{-})\\ (iii)&f^{*}(a)\leq(\text{Id}\wedge f^{+})^{\dagger}(a^{+}),\forall i\geq 0 \end{array} \tag{20}\]  
**Remark 3**.: _The membership relation (\(i\)) means that we are able to compute in a finite time an enclosure of the fixed point \(f^{*}(a)\). Relation (ii) states that the fixed point obtained by \((f^{-})^{*}\) is a fixed point of \(f^{*}\). However, this is not true for \(\left(f^{+}\right)^{*}\). Relation (iii) tells us that at each iteration \(i\), we have an upper bound for the solution \(f^{*}(a)\), but we need to reach the fixed point to get a lower approximation \(\left(f^{-}\right)^{*}(a^{-})\) of \(f^{*}(a)\)._  
Proof.: (i) is a consequence of the fact that \(f^{i}(a)\in\left[\left(f^{-}\right)^{i}(a^{-}),\left(f^{+}\right)^{i}(a^{+}) \right]\).  
(ii) Since \(\left(f^{-}\right)^{*}\circ\left(f^{-}\right)^{*}(a^{-})=\left(f^{-}\right)^{* }(a^{-})\), the quantity \(\left(f^{-}\right)^{*}(a^{-})\) is a fixed point of \(\left(f^{-}\right)^{*}\). Now, from (19), we have \(\operatorname{Fix}\left(\left(f^{-}\right)^{*}\right)\subset\operatorname{ Fix}(f^{*})\). Therefore, \(\left(f^{-}\right)^{*}(a^{-})\) is also a fixed point of \(f^{*}\), i.e., \(f^{*}\circ\left(f^{-}\right)^{*}(a^{-})=\left(f^{-}\right)^{*}(a^{-})\).  
(iii) We have  
\[f^{*}(a) = \left(\operatorname{Id}\wedge f\right)^{\infty}(a)\quad\leq \quad\left(\operatorname{Id}\wedge f\right)^{i}(a)\] \[\leq \left(\operatorname{Id}\wedge f^{+}\right)^{i}(a)\quad\leq \quad\left(\operatorname{Id}\wedge f^{+}\right)^{i}(a^{+})\]  
The inclusion (iii) is illustrated by Figure 2 where the grid corresponds to \(\mathcal{L}_{M}\), the magenta points correspond to \(\operatorname{Fix}\left(\left(f^{-}\right)^{*}\right)\), the blue points correspond to \(\operatorname{Fix}\left(\left(f^{+}\right)^{*}\right)\), and the light red polygon corresponds to \(\operatorname{Fix}(f^{*})\).