Add very tiny explenation of cascade product and Krohn-Rhodes Theorem

1 files changed, 23 insertions, 0 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 72624e6..6977f4a 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -421,6 +421,29 @@ The last step of the algorithm is converting the Muller automaton to an LTL form
 The decomposition of finite automata was first described by K. Krohn and J. Rhodes as is known as the Krohn-Rhodes theorem~\cite{Krohn1965}.
 This theorem, in combination with the work of A. Meyer~\cite{Meyer1969} allows for the translation of Muller automaton to LTL.
 
+\begin{definition}[Cascade Product~\cite{Maler2010}]
+	Let $A = (Q, \Sigma, \delta)$ be an automaton, and let $B = (Q \times \Sigma, Q', \delta')$ be an automaton such that for all $q \in Q$ and $q' \in Q'$, either $\delta'(q',(q,\sigma))$ is defined for all $\sigma \in \Sigma$ or it is undefined for every $\sigma$.
+	The cascade product $A \circ B$ is the automaton $C = (\Sigma, Q'', \delta'')$ where
+	\[
+		Q'' = \{(q, q') \mid \delta'(q',(q,\sigma))\ is\ defined\}
+	\]
+	and
+	\[
+		\delta''((q,q'),\sigma) = (\delta(q',\sigma),\delta'(q',(q,\sigma)))
+	\]
+\end{definition}
+\begin{theorem}[Krohn-Rhodes Theorem]
+	For every automaton $A$ there exists a cascade $C = B_1 \circ B_2 \circ \dots \circ B_n$ such that:
+	\begin{enumerate}
+		\item Each $B_i$ is a permutation-reset automaton\footnote{Definition ommited for brevity}
+		\item There is a homomorphism\footnotemark[10] $\phi$ from $C$ to $A$
+		\item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$
+	\end{enumerate}
+\end{theorem}
+
+The cascade product can then be used to create star-free regular sets.
+These sets can then be transformed into LTL formulae.
+
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL
 %TODO: Provide algorithm via automata to convert PLTL to LTL