# Kleene Algebra to Compute Invariant Sets of Dynamical Systems
## 4 Kleene Algebra of Automorphisms
### Automorphisms  
Given a complete lattice \((\mathcal{L},\leq,\wedge,\vee,\bot,\top)\), an automorphism of \(\mathcal{L}\) is a function \(f\colon\mathcal{L}\to\mathcal{L}\) such that  
\[ \begin{array}{rll}\text{(i)}&f(\top)&=&\top\\ \text{(ii)}&f(a\wedge b)&=&f(a)\wedge f(b)\end{array} . \tag{7}\]  
As we will see later (see, e.g., Table 2), no property is assumed concerning the operator \(\vee\). We denote by \(\mathcal{A}(\mathcal{L})\) the set of automorphisms of \(\mathcal{L}\). Proposition 2: If \(f,g\) are in \(\mathcal{A}(\mathcal{L})\), then:  
\[ \begin{array}{rll}\text{(i)}&a\leq b\Rightarrow f(a)\leq f(b)\\ \text{(ii)}&f\wedge g\in\mathcal{A}(\mathcal{L})\\ \text{(iii)}&f\circ g\in\mathcal{A}(\mathcal{L})\\ \text{(iv)}&\text{Id}\wedge f\wedge f^{2}\wedge f^{3}\wedge\cdots\in\mathcal{ A}(\mathcal{L})\end{array}  \tag{8}\]  
where the function \(f\wedge g\) is defined by \((f\wedge g)(a)=f(a)\wedge f(a)\). Proof: (i) We have  
\[ \begin{array}{rll}a\leq b&\Leftrightarrow&a=b\wedge a\\ &\Rightarrow&f(a)=f(b\wedge a)\\ &\Leftrightarrow&f(a)=f(b)\wedge f(a)\end{array} \qquad\text{(see Eq \ref{eq:f},ii)} \tag{9}\]  
(ii) We have \((f\wedge g)(\top)=\top\wedge\top=\top\). Moreover,\[(f\wedge g)(a\wedge b) = (f(a\wedge b))\wedge(g(a\wedge b))\] \[= f(a)\wedge f(b)\wedge g(a)\wedge g(b)\] \[= (f\wedge g)(a)\wedge(f\wedge g)(b)\]  
(iii) We have \(f\circ g(\top)=f(\top)=\top\). Moreover,  
\[ \begin{array}{rcl}(f\circ g)(a\wedge b)&=&f(g(a)\wedge g(b))\\ &=&(f\circ g)(a)\wedge(f\circ g)(b)\end{array}  \tag{11}\]  
(iv) It corresponds to the Kleene operator and is a direct consequence of (ii), (iii). **Proposition 3**. : _Assume that for \(f\in\mathcal{A}(\mathcal{L})\), \(f^{*}=\text{Id}\wedge f\wedge f^{2}\wedge f^{3}\wedge\ldots\) exists (star-continuity assumption), then the set \((\mathcal{A}(\mathcal{L}),\wedge,\circ,*)\) is a Kleene algebra._  
Proof. : We need to check all properties of Table 2. In the two tables, the symbols of the operators changed: \(+\) corresponds to \(\wedge\), \(*\) corresponds to \(\circ\), and \(\geq\) corresponds to \(\leq\). To prove the distributivity \(f\circ(g\wedge h)=(f\circ g)\wedge(f\circ h)\), we proceed as follows:  
\[ \begin{array}{rcl}f\circ(g\wedge h)(a)&=&f\circ(g(a)\wedge h(a))\\ &\stackrel{{(\ref{eq:f})}}{{=}}&(f\circ g)(a)\wedge(f\circ h)(a). \end{array}  \tag{12}\]  
All other properties can be proved similarly. **Remark 2**. : _The relation order for automorphism has been chosen backward (i.e., \(\geq\) instead of \(\leq\)). This choice is motivated by the fact that the inclusion order will be used later, and we will have the following correspondences: \(\leq\leftrightarrow\subset\), \(\wedge\leftrightarrow\cap\)._  
**Proposition 4**. : _The fixed points of \(\text{Id}\wedge f\) correspond to that of \(f^{*}\), i.e.,_  
\[\text{Fix}(f^{*})=\{a|f^{*}(a)=a\}=\text{Fix}(\text{Id}\wedge f) \tag{13}\]  
Proof. : The proof is decomposed in two parts. In the first part, we prove that \(\text{Fix}(\text{Id}\wedge f)\subset\text{Fix}(f^{*})\) and in the second part, we prove the inverse. \begin{table}
\begin{tabular}{c c} \hline \hline
**Kleene Algebra** & \((\mathcal{A}(\mathcal{L}),\wedge,\circ,*)\) \\ \hline Addition & \(f\wedge g\) \\ \hline Product & \(f\circ g\) \\ \hline Associativity & \(f\wedge(g\wedge h)=(f\wedge g)\wedge h\) \\  & \(f\circ(g\circ h)=(f\circ g)\circ h\) \\ \hline Commutativity & \(f\wedge g=g\wedge f\) \\ \hline Distributivity & \(f\circ(g\wedge h)=(f\circ g)\wedge(f\circ h)\) \\  & \((g\wedge h)\circ f=(g\circ f)\wedge(h\circ f)\) \\ \hline Zero & \(f\wedge\top=f\) \\ \hline One & \(f\circ\text{Id}=\text{Id}\circ f=f\) \\ \hline Annihilation & \(f\circ\top=\top\) \\ \hline Idempotency & \(f\wedge f=f\) \\ \hline Partial order & \(f\geq g\Leftrightarrow f\wedge g=g\) \\ \hline Kleene star & \(f^{*}=\text{Id}\wedge f\wedge f^{2}\wedge f^{3}\wedge\ldots\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: The set of automorphisms forms a star-continuous Kleene algebra.