diff options
Diffstat (limited to 'tex/thesis/contribution/contribution.tex')
-rw-r--r-- | tex/thesis/contribution/contribution.tex | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex index 5b3acb9..1709d40 100644 --- a/tex/thesis/contribution/contribution.tex +++ b/tex/thesis/contribution/contribution.tex @@ -49,9 +49,9 @@ In this chapter the main theoretical contribution of this thesis is presented: an extension on a $\max$-strategy iteration algorithm for solving fixpoint equations over the integers with monotonic -operators\cite{Gawlitza:2007:PFC:1762174.1762203} (see Section -\ref{sec:gawlitza-algorithm}). We devise an algorithm which performs -considerably better for practical equation systems. +operators~\cite{Gawlitza:2007:PFC:1762174.1762203}. We devise an +algorithm which performs considerably better for practical equation +systems. In this chapter we will begin by presenting the Work-list Depth First Search (W-DFS) fixpoint algorithm developed by Seidl et @@ -61,12 +61,11 @@ chapter will conclude with our Demand-driven Strategy Improvement (DSI) algorithm to perform efficient strategy iteration and fixpoint iteration. % TODO: fix me, or something -The existing algorithm as presented in Section -\ref{section:basic-algorithm} consists of two iterative operations: -fixpoint iteration and max-strategy iteration. Each of these -operations consists of naively ``evaluating'' the system repeatedly -until a further evaluation results in no change. Gawlitza et -al.~proved that these iterations converge in a finite number of +The existing algorithm consists of two iterative operations: fixpoint +iteration and max-strategy iteration. Each of these operations +consists of naively ``evaluating'' the system repeatedly until a +further evaluation results in no change. Gawlitza et al.~proved that +these iterations converge in a finite number of steps\cite{Gawlitza:2007:PFC:1762174.1762203} , but in practice this naive approach performs a large number of re-calculations of results which are already known. |