Skip to content

Commit

Permalink
corrected the report, so we dont have conducted any experiments
Browse files Browse the repository at this point in the history
  • Loading branch information
sebastianbot6969 committed Jan 13, 2025
1 parent f9733be commit 480e33b
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 32 deletions.
10 changes: 5 additions & 5 deletions report/src/sections/01-introduction.tex
Original file line number Diff line number Diff line change
Expand Up @@ -13,19 +13,19 @@ \section{Introduction}\label{sec:introduction}
Despite their advanced capabilities, these tools lack native support for parameter estimation, which is crucial for learning models from data.
Conversely, tools like Jajapy~\cite{reynouard2023jajapy} and SUDD~\cite{p7} focus on parameter estimation but lack integration with symbolic model-checking frameworks.

By leveraging \glspl{add} in all algorithm steps for the Baum-Welch algorithm, we achieve significant improvements in runtime performance and scalability compared to matrix-based approaches.
Our work builds on the symbolic techniques introduced in SUDD but expands their application to the entire parameter estimation process for \glspl{hmm}.
By leveraging \glspl{add} in all algorithm steps for the Baum-Welch algorithm, we achieve significant improvements in runtime performance and scalability compared to recursive-based approaches.
Our work builds on the symbolic techniques introduced in SUDD~\cite{p7} but expands their application to the entire parameter estimation process for \glspl{hmm}.

Our contributions are as follows:
Our contribution are as follows:
\begin{itemize}
\item We implement the complete Baum-Welch algorithm symbolically, including forward-backward computations and parameter updates.
\item We provide a comparative evaluation of our approach against Jajapy.
%\item We provide a comparative evaluation of our approach against Jajapy.
\end{itemize}

\subsection{Related Works}\label{subsec:related-works}
Several tools have been developed for parameter estimation in Markov models.
Jajapy is a Python-based tool that uses the Baum-Welch algorithm to estimate parameters in various models, including \glspl{hmm}~\cite{reynouard2023jajapy}.
It employs a matrix representation of the model and implements the necessary operations for parameter estimation through standard matrix computations without standard matrix libraries, such as NumPy~\cite{harris2020array}.
It employs a matrix representation of the model and implements a iterative approach based on a recursive definition.

While accessible and straightforward, Jajapy is hindered by the space complexity inherent in its iterative-based calculation.
This limitation makes it computationally expensive for large-scale models, as memory requirements grow quadratically with the number of states in the system.
Expand Down
5 changes: 3 additions & 2 deletions report/src/sections/03-implementation.tex
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,8 @@ \subsubsection{Kronecker Product}\label{subsubsec:kronecker-product}

Here rows($B$) and columns($B$) represents the number of rows and columns in matrix $B$, respectively.

This operation is not natively supported in the CUDD library, therefore we implemented it explicitly as a custom function.
This operation is not natively supported in the CUDD library, we have not implemented it as a custom function.

The Kronecker product of matrices $A$ and $B$ is:
\[
A \otimes B = \begin{bmatrix}
Expand All @@ -264,7 +265,7 @@ \subsubsection{Khatri-Rao Product}
\item The elements of row $i$ in the first matrix are multiplied element-wise with the entire row $i$ in the second matrix.
\item The resulting row is constructed symbolically within the \gls{add}.
\end{enumerate}
This operation is not natively supported in the CUDD library, therefore we implemented it explicitly as a custom function.
This operation is not natively supported in the CUDD library, we have not implemented it as a custom function.
The Khatri-Rao product of matrices $A$ and $B$ is:
\[
A \bullet B = \begin{bmatrix}
Expand Down
51 changes: 26 additions & 25 deletions report/src/sections/04-experiments.tex
Original file line number Diff line number Diff line change
@@ -1,18 +1,19 @@
\section{Experiments}\label{sec:experiments}
This section describes the experiment used to evaluate the proposed symbolic implementation of the Baum-Welch algorithm in CuPAAL.
The experiment is designed to compare CuPAAL with another implementation: Jajapy, which uses a recursive approach to the Baum-Welch algorithm.
The experiment is conducted to answer the following research question:
This section describes the experiment that would be used to evaluate the proposed symbolic implementation of the Baum-Welch algorithm in CuPAAL.
The experiment was designed to compare CuPAAL with another implementation: Jajapy, which uses a recursive approach to the Baum-Welch algorithm.
The experiment would be conducted to answer the following research question:

\begin{itemize}
\item \textbf{Question:} How does the scalability of CuPAALs symbolic implementation compare to Jajapy as the number of model states increases?
\end{itemize}

This question is used to evaluate the computational efficiency of the symbolic implementation in CuPAAL. The insights gained will highlight the strengths and potential weknesses of the symbolic approach to the Baum-Welch algorithm.
This question would evaluate the computational efficiency of the symbolic implementation in CuPAAL.
The insights gained would highlight the strengths and potential weaknesses of the symbolic approach to the Baum-Welch algorithm.

\subsection{Experimental Setup}
The experiment evaluates how each implementation scales with increasing model states.
We conduct a single experiment to evaluate the proposed method.
The machine used to conduct the experiment has the specifications seen in \autoref{tab:machine-specs}.
The experiment would evaluate how each implementation scales with increasing model states.
We would conduct a single experiment to evaluate the proposed method.
The machine that would be used to conduct the experiment has the specifications seen in \autoref{tab:machine-specs}.
\begin{table}[htb!]
\centering
\caption{Machine Specifications from AAU Strato}
Expand All @@ -28,27 +29,27 @@ \subsection{Experimental Setup}
\end{tabular}
\end{table}

The following implementations are used for comparison.
The following implementations would used for comparison.

\begin{itemize}
\item \textbf{Jajapy}: A matrix-based implementation of the Baum-Welch algorithm \cite{reynouard2023jajapy}.
\item \textbf{Jajapy}: A recursive implementation of the Baum-Welch algorithm~\cite{reynouard2023jajapy}.
\item \textbf{CuPAAL}: The fully symbolic implementation proposed in this work.
\end{itemize}

The chosen implementations are either fully recursive to fully symbolic approaches, providing a comprehensive comparison of methodologies.

\subsection{Experiment Dataset}
The experiment uses synthetic datasets; The dataset has five different labels \{"A", "B", "C", "D", "E"\} and the same observation sequence for all runs of the experiment.
We use 1 observation sequence of length 20, as our implementation is not set up to handle multiple observation sequences.
The number of states in the model is varied from 20 to 1020, with increments of 100 states.
The initial model is generated with random parameters, and the observation sequence is the same for all runs of the experiment.
The model always starts in the same initial state, and the transition matrix and emission matrix are generated randomly.
Where the emission matrix is generated such that one state can emit a maximum of three different labels.
All implementations are tested on the same dataset to ensure fair comparison.
The experiment would use synthetic datasets; The dataset would have five different labels \{"A", "B", "C", "D", "E"\} and the same observation sequence for all runs of the experiment.
We would use 1 observation sequence of length 20, as our implementation is not set up to handle multiple observation sequences.
The number of states in the model would be varied from 20 to 1020, with increments of 100 states.
The initial model would be generated with random parameters, and the observation sequence would be the same for all runs of the experiment.
The model would always start in the same initial state, and the transition matrix and emission matrix would be generated randomly.
Where the emission matrix would be generated such that one state can emit a maximum of three different labels.
All implementations would tested on the same dataset to ensure fair comparison.

\subsection{Experimental Procedure}
The experiment assesses how the runtime of each implementation changes as the number of states in a synthetic model incrementally increases from 20 to 1020.
The process is done as follows:
The experiment would assesses how the runtime of each implementation changes as the number of states in a synthetic model incrementally increases from 20 to 1020.
The process would be done as follows:

\begin{enumerate}
\item Load the initial model and observation sequence.
Expand All @@ -57,21 +58,21 @@ \subsection{Experimental Procedure}
\item Repeat steps 2-3 for each implementation until the maximum number of states is reached.
\end{enumerate}

Scalability is evaluated by examining runtime trends as model size increases.
This provides insight into how each implementation scales with larger models and is critical for understanding the practical applicability of symbolic versus recursive-based implementations.
The specific link for the experiment\footnote{\url{https://github.com/AAU-Dat/P7-sudd/blob/P9-experiments/scaling_experiment.py}}.

Results will be visualized using plots to illustrate trends and highlight differences in scalability between implementations.
Scalability would be evaluated by examining runtime trends as model size increases.
This would provide insight into how each implementation scales with larger models and is critical for understanding the practical applicability of symbolic versus recursive-based implementations.

Results would be visualized using plots to illustrate trends and highlight differences in scalability between implementations.

\subsection{Discussion of Metrics and Methods}
The runtime is the primary evaluation metric, as it directly reflects the computational efficiency of each implementation when handling larger models.
By plotting runtime along side the number of states, we aim to identify patterns and scalability limits for each approach.
The runtime would be the primary evaluation metric, as it directly reflects the computational efficiency of each implementation when handling larger models.
By plotting runtime along side the number of states, we would aim to identify patterns and scalability limits for each approach.

We wanted to track the memory consumption of the implementations, as this is a critical factor in the scalability of the Baum-Welch algorithm, and symbolic approaches are expected to be more memory-efficient.
However, tracking memory consumption is challenging, and is therefore left for future work.
Instead we focus on runtime as the primary metric, as it provides a clear and comparable measure of computational efficiency.

\footnote{The specific link \url{https://github.com/AAU-Dat/P7-sudd/blob/P9-experiments/scaling_experiment.py}}.


\begin{figure}[htb!]
\centering
Expand Down
4 changes: 4 additions & 0 deletions report/src/sections/07-future_works.tex
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
\section{Future Works}\label{sec:future_works}
This section outlines potential future works and extensions of the symbolic Baum-Welch algorithm.

Our first step would be to implement the Kronecker product and Katri-Rao product in the symbolic approach.
These operations are essential for the Baum-Welch algorithm, as they are used to update the transition and emission matrices.
Implementing these operations would complete the symbolic approach, enabling the full Baum-Welch algorithm to be executed symbolically.

Since no experiments were conducted on the implementation, this is something that would be a good starting point for future work, as we could compare the performance of the symbolic approach to the recursive Jajapy implementation.
This comparison would assess the scalability of the symbolic implementation as the number of model states increases.
Runtime and memory usage would be core parameters to evaluate, providing insights into the computational efficiency of the symbolic approach in the context of the Baum-Welch algorithm.
Expand Down

0 comments on commit 480e33b

Please sign in to comment.