\input{abbrv}

    \chapter{Introduction}

    \chapter{Introduction}\label{ch:introduction}

    \chapter{Preliminaries}

    \chapter{Preliminaries} \label{ch:preliminaries}

    \chapter{Theory}

    \chapter{Theory}\label{ch:theory}

    \chapter{Implementation}

    \chapter{Implementation}\label{ch:implementation}

    \chapter{Conclusion}

    \chapter{Conclusion}\label{ch:conclusion}

}
@InProceedings{llvm2kittel,
  author    = {Stephan Falke and Deepak Kapur and Carsten Sinz},
  booktitle = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, {RTA} 2011, May 30 - June 1, 2011, Novi Sad, Serbia},
  title     = {Termination Analysis of {C} Programs Using Compiler Intermediate Languages},
  year      = {2011},
  editor    = {Manfred Schmidt{-}Schau{\ss}},
  pages     = {41--50},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  series    = {LIPIcs},
  volume    = {10},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/rta/FalkeKS11.bib},
  doi       = {10.4230/LIPIcs.RTA.2011.41},
  groups    = {Tools},
  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
  url       = {https://doi.org/10.4230/LIPIcs.RTA.2011.41},

@Misc{tpdb,
  title  = {The Termination Problems Data Base},
  groups = {Tools},
  url    = {https://termination-portal.org/wiki/TPDB},
}
@InProceedings{z3,
  author    = {Leonardo Mendon{\c{c}}a de Moura and Nikolaj S. Bj{\o}rner},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
  title     = {{Z3:} An Efficient {SMT} Solver},
  year      = {2008},
  editor    = {C. R. Ramakrishnan and Jakob Rehof},
  pages     = {337--340},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
  doi       = {10.1007/978-3-540-78800-3\_24},
  timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
  url       = {https://doi.org/10.1007/978-3-540-78800-3\_24},
}
@InProceedings{apron,
  author    = {Bertrand Jeannet and Antoine Min{\'{e}}},
  booktitle = {Computer Aided Verification, 21st International Conference, {CAV} 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  title     = {Apron: {A} Library of Numerical Abstract Domains for Static Analysis},
  year      = {2009},
  editor    = {Ahmed Bouajjani and Oded Maler},
  pages     = {661--667},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5643},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/cav/JeannetM09.bib},
  doi       = {10.1007/978-3-642-02658-4\_52},
  groups    = {Polyhedra, Octagons, Boxes},
  timestamp = {Tue, 14 May 2019 10:00:43 +0200},
  url       = {https://doi.org/10.1007/978-3-642-02658-4\_52},
}

\section{Future Work}

\section{Future Work}\label{sec:future_work}

\begin{comment}
    Satisfiability and entailment checks are computed using the SMT-Solver Z3.
    projections are calculated using the library Apron and the Parma polyhedra
    library included therein. Both, Z3 and Apron are already in use in
    \gls{koat} and are fit for the task.
    Boxes and other special polyhedra can be used trivially through the apron
    api and provide quicker but less tight alternative to polyhedra. However,
    we will consider them out of scope for this thesis.

This section delves into the implementation details of the evaluation algorithms
for \gls{pip} described in \Sref{ch:theory}. The whole implementation is done in
\gls{ocaml}. For solving satisfiability of constraints and formulas in general
Z3\cite{z3} was used as it is already used in other parts of \gls{koat}. For
projections of constraints and handling polyhedra we recurred \gls{apron} and
the \gls{ppl}\cite{bagnara2008socp}, which can be used as an abstract domain in
apron.

    Base Algorithm 
    fun find_loops_in(P)
        loop_heads = {}
        // Dijkstra
        on loop_back from l' -> l_h:
            loop_heads := loop_heads + l_h
        return loop_heads
    end

The Algorithm \ref{alg:cfr_pip} which applies control-flow-refinement via
partial evaluation on an entire \gls{pip} and the Algorithm \ref{alg:cfr_subscc}
which evaluates a set of transitions in a program, where implemented natively in 
\gls{ocaml}.

    fun heuristic(L: Loop)
        // same as original paper
    end

The evaluation of a whole program is not used in \gls{koat}s analysis per-se due
to performance reasons, but made available through a new sub command
\texttt{cfr}. It might be used by other tools in the future, that want to profit
from partial evaluation on probabilistic programs. 

    fun partial_evaluation(Program P = (PV, L, GT, l_0))
        let lh := loop_heads(P)
        let properties := heuristic(P)
        let initial_state := (l_0, [])
        let P' := ({l_0}, l_0, {locations: P.l_0, {}) // todo

The evaluation on sub-\gls{scc} was integrated into \gls{koat}s analysis similar
to iRankFinder as described in \cite{giesl2022arxiv}, possibly replacing the old
implementation in the future. The analysis command was expanded with new
settings, which allow to select the various parameters of the evaluation, such
the selection of locations for abstraction.

        for gt in GT: 
            let gt' = {}
            for t in gt: 
                (s', l_t') := evaluate(P, s, t)
                if l_t \in lh:

\subsection{Loops}
\subsection{Sub-\gls{scc} evaluation}
% \begin{comment}
    % Base Algorithm 
    % fun find_loops_in(P)
    %     loop_heads = {}
    %     // Dijkstra
    %     on loop_back from l' -> l_h:
    %         loop_heads := loop_heads + l_h
    %     return loop_heads
    % end
    % fun heuristic(L: Loop)
    %     // same as original paper
    % end
    % fun partial_evaluation(Program P = (PV, L, GT, l_0))
    %     let lh := loop_heads(P)
    %     let properties := heuristic(P)
    %     let initial_state := (l_0, [])
    %     let P' := ({l_0}, l_0, {locations: P.l_0, {}) // todo
    %     for gt in GT: 
    %         let gt' = {}
    %         for t in gt: 
    %             (s', l_t') := evaluate(P, s, t)
    %             if l_t \in lh:

                else : 
                gt' := gt' + 
            end
        end
    Claims: 
    Every path in P has an equivalent path in the evaluation graph EG
    Every path in EG has an equivalent path in P'

    %             else : 
    %             gt' := gt' + 
    %         end
    %     end
    % Claims: 
    % Every path in P has an equivalent path in the evaluation graph EG
    % Every path in EG has an equivalent path in P'

    SCC Algorithm:
    similar to above but stops at SCC boundaries. 
\end{comment}

    % SCC Algorithm:
    % similar to above but stops at SCC boundaries. 
% \end{comment}

\section{Modules}
The code specific to this thesis is split into a couple of modules. The code is
fully commented. Nonetheless, this section gives a short overview over the
modules to ease the understanding of the code. 
\subsection{Loops}
\subsection{PartialEvaluation}
\subsection{Abstraction}

% \section{Modules}

\section{Command-Line Interface}
The techniques described above were implemented natively in Koat2. They are
available as part of the normal analysis via the flags \texttt{--cfr-native}.
The old option for control-flow refinement \texttt{--cfr} was renamed to
\texttt{--cfr-ir}, and can probably be removed in the future. 
During normal analysis the control-flow refinement is done on every \gls{scc}
and the bounds of the resulting scc is compared to the previous bounds. 

% \section{Command-Line Interface}
% The techniques described above were implemented natively in Koat2. They are
% available as part of the normal analysis via the flags \texttt{--cfr-native}.
% The old option for control-flow refinement \texttt{--cfr} was renamed to
% \texttt{--cfr-ir}, and can probably be removed in the future. 
% During normal analysis the control-flow refinement is done on every \gls{scc}
% and the bounds of the resulting scc is compared to the previous bounds. 

A full program can be refined using the native control-flow refinement with a
separate command \texttt{cfr}. For the new control-flow refinement the option is
added to switch between the various method to select location for abstraction
and the abstraction method itself (see \Sref{sec:abstraction}). An summary of
the compatible options is given in \tref{tab:options}. 

% A full program can be refined using the native control-flow refinement with a
% separate command \texttt{cfr}. For the new control-flow refinement the option is
% added to switch between the various method to select location for abstraction
% and the abstraction method itself (see \Sref{sec:abstraction}). An summary of
% the compatible options is given in \tref{tab:options}. 

As discussed in \Sref{sec:updateinvariants} the polyhedra computed during
evaluation are tighter than the invariants computed during preprocessing. In
order to update the invariants after the partial evaluation a new option
\texttt{--update-invariants} is added and activated by default. 

% As discussed in \Sref{sec:updateinvariants} the polyhedra computed during
% evaluation are tighter than the invariants computed during preprocessing. In
% order to update the invariants after the partial evaluation a new option
% \texttt{--update-invariants} is added and activated by default. 

The implementation is \gls{koat} can be 
\section{Correctness}

\section{Performance and Correctness}\label{sec:performance}
This section will evaluate the performance and correctness of the new
implementation. The performance is analysed for classical and probabilistic
programs using benchmarks on test sets from the \gls{tpdb}\cite{tpdb}. The
results are compared to benchmarks on the same data sets using the latest
version of \gls{koat}. In addition to the performance comparison, the
correctness is asserted by comparing the upper bounds found by the new
implementation to lower bounds proven by the analysis tool \gls{loat}.

\section{Performance}
The project was compiled with OCaml 4.14.0. 

All code was compiled using OCaml 4.14.0. Among the more important dependencies
is the SMT library \textit{Z3} in version 4.11.0.0, \textit{Apron} in version
0.9.13, and the \gls{ppl} in version 1.2. \gls{koat} and all dependencies are
build inside a docker container. All benchmarks are done on a AMD Ryzen 7 5800X
8-Core Processor with 32 GB RAM. 8 benchmarks are executed in parallel each in
their own Ubuntu 20.04 docker container. The measured computation time for each
test includes the upstart and take down time of the docker container, but the
timeout is measured internally in \gls{koat}.
\subsection{Performance on classical programs}\label{ssec:perf_classic}
As a baseline, four configurations are used that have been used in the past to
measure \gls{koat}s performance.\cite{giesl2022arxiv} The at the time of writing
latest version on the master branch is used. 
\gls{koat}\footnote{commit \texttt{a2eb156ac31db0f4daaa89822786a413632e637f}} is
evaluated with four different settings: 
The new implementation is tested with four different settings: 
\begin{itemize}
    \item \enquote{\acrshort{koat}} is the simplest configuration. It uses \gls{mprf}
        with an $\textit{mdepth} = 1$, i.e. it computes only linear ranking
        functions. \cite{giesl2022arxiv} No control-flow-refinement is used.
    \item \enquote{\acrshort{koat} + \acrshort{mprf}5} is the configuration that
        uses \gls{mprf} with a $\textit{mdepth} = 5$. That is the typical maximum
        depth used in competitions.\cite{giesl2022arxiv} Still, no
        control-flow-refinement is used.
    \item \enquote{\acrshort{koat} + iRF} is the configuration
        that uses sub-\gls{scc} control-flow-refinement refinement but limits
        the maximum depth of linear ranking functions to $\textit{mdepth} = 1$.
        The control-flow-refinement is done by calling iRankFinder as a
        black-box.
    \item \enquote{\acrshort{koat} + \acrshort{mprf}5 + iRF}
        activates sub-\gls{scc} control-flow-refinement with iRankFinder
        and \gls{mprf} with an $\textit{mdepth}=5$.
\end{itemize}
The new implementation is evaluated on classical integer programs using four
configurations:
\begin{itemize}
    \item \enquote{new-\acrshort{koat}} as a correctness check, this
        configuration uses the same settings as \enquote{\acrshort{koat}} and
        is expected to have similar result. 
    \item \enquote{new-\acrshort{koat} + \acrshort{mprf}5} as is this configuration that has the
        same settings as \enquote{\acrshort{koat} + \acrshort{mprf}5}.
    \item \enquote{new-\acrshort{koat} + nat.\acrshort{cfr}} uses the new
        sub-\gls{scc} control-flow-refinement described in Algorithm
        \ref{alg:sub_scc_cfr}.
    \item \enquote{new-\acrshort{koat} + nat.-\acrshort{cfr}} uses the new
        sub-\gls{scc} control-flow-refinement described in Algorithm
        \ref{alg:sub_scc_cfr} and \gls{mprf} with a maximum depth
        $\textit{mdepth}=5$.
\end{itemize}
The benchmarking for classical integer programs is done on two test sets from
the \gls{tpdb}. The first test set it called \enquote{Complexity\_ITS} that is
comprised of 801 integer programs from various literature. The results of this
benchmark are displayed in \fref{fig:results_complexity_its}.
\begin{figure}[h]
    \centering
    \setlength{\tabcolsep}{0.1em}
    \begin{tabular}{l|c|c|c|c|c|c||c|c}
        & $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
        $\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
        [s]$ \\ \hline
        \acrshort{koat} & 128 & 218 & 95 & 10 & 6 & 457 & 4.69 & 8.84 \\ \hline
        \acrshort{koat} + \acrshort{mprf}5 & 128 & 235 & 98 & 14 & 6 & 481 & 5.58 &
        12.36 \\ \hline
        \acrshort{koat} + old-\acrshort{cfr} & 133 & 244 & 98 & 9 & 6 & 490 & 6.12 &
        20.84 \\ \hline
        \acrshort{koat} + \acrshort{mprf}5 + iRF & 133 & 254 & 99 & 13
        & 6 & 505 & 7.66 & 25.05 \\ \hline
        \hline
        new-\acrshort{koat} & & & & & & & \\ \hline
        new-\acrshort{koat} + \acrshort{mprf}5 & & & & & & & \\ \hline
        new-\acrshort{koat} + nat.-\acrshort{cfr} & & & & & & &\\ \hline
        new-\acrshort{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & &\\ \hline
    \end{tabular}
    \caption{Performance results on the \gls{tpdb} test set
    \enquote{Complexity\_ITS}.\label{fig:results_complexity_its}}
\end{figure}
\todo{discuss the results}
The second data set is called \enquote{Complexity\_C\_Integer} and contains C
programs using only integers. Because \gls{koat} can only work on integer
programs, C programs are transformed integer programs using the tool
\textit{llvm2kittel}\cite{llvm2kittel}. The results of this benchmark are
displayed in \fref{fig:results_complexity_c_integer}.
\begin{figure}[h]
    \centering
    \setlength{\tabcolsep}{0.1em}
    \begin{tabular}{l|c|c|c|c|c|c||c|c}
        & $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
        $\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
        [s]$ \\ \hline
        \gls{koat} & 23 & 175 & 68 & 10 & 0 & 276 & 3.74 & 4.69 \\ \hline
        \gls{koat} + \acrshort{mprf}5 & 23 & 203 & 96 & 10 & 0 & 305 & 4.43 &
        6.32 \\ \hline
        \gls{koat} + old-\acrshort{cfr} & 25 & 215 & 68 & 9 & 0 & 317 & 5.76 &
        13.85 \\ \hline
        \gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr} & 24 & 228 & 69 & 8 &
        0 & 329 & 7.10 & 17.24 \\ \hline
        \hline
        new-\acrshort{koat} & & & & & & & \\ \hline
        new-\acrshort{koat} + \acrshort{mprf}5 & & & & & & & \\ \hline
        new-\acrshort{koat} + nat.-\acrshort{cfr} & & & & & & &\\ \hline
        new-\acrshort{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & &\\ \hline
    \end{tabular}
    \caption{Performance results on the \gls{tpdb} test set
    \enquote{Complexity\_C\_Integer}.\label{fig:results_complexity_c_integer}}
\end{figure}
\todo{discuss results}
\subsection{Correctness}\label{ssec:impl_correctness}
For both data sets we observed that the new implementation yields similar
results with the configurations \enquote{new-\acrshort{koat}} and
\enquote{new-\acrshort{koat} + nat.-\acrshort{cfr}} to the old version,
indicating that the new implementation works as expected.
The tool \gls{loat}\cite{frohn2022ijcar} proves lower complexity bounds for
classical integer programs. The upper bounds found by the new \gls{koat} version
must not be lower than the lower bounds found by \gls{loat}. For every program
in the test sets above a lower bound is computed with \gls{loat} and compared to
the analysis results of the new implementation using the configuration
\enquote{\gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr}} and for no program
the upper bounds were smaller than the lower bounds proven by \gls{loat}, which
assures the correctness of the new implementation.
\section{Performance on probabilistic integer programs}\label{ssec:perf_prob}
The performance on probabilistic programs is evaluating using a collection
of examples from the literature; namely \todo{citations} and the examples
used in this thesis.
\begin{figure}
    \centering
    \setlength{\tabcolsep}{0.1em}
    \begin{tabular}{l|c|c|c|c|c|c||c|c}
        & $\bigo(1)$ & $\bigo(n)$ & $\bigo(n^2)$ & $\bigo(n^{>2})$ &
        $\bigo(\text{EXP})$ & $< \infty$ & $\text{AVG}^+ [s]$ & $\text{AVG}
        [s]$ \\ \hline
        \gls{koat} &  &  &  &  &  &  &  &  \\ \hline
        \gls{koat} + \acrshort{mprf}5 &  &  &  &  &  &  &  & \\ \hline
        \gls{koat} + \acrshort{mprf}5 + old-\acrshort{cfr} & & & & & & & \\ \hline
        \hline
        \gls{koat} + \acrshort{mprf}5 + iRF-\acrshort{cfr} & & & & & & & \\ \hline
        \gls{koat} + \acrshort{mprf}5 + nat.-\acrshort{cfr} & & & & & & & \\ \hline
        \gls{koat} + iRF-\acrshort{cfr} & & & & & & & \\ \hline
        \gls{koat} + nat.-\acrshort{cfr} & & & & & & & \\ \hline
    \end{tabular}
    \caption{Performance results on the probabilistic test set.}
\end{figure}
\todo{discuss results}
\section{Further considerations}
\todo{rewrite}
Although this thesis was focused primary on integer arithmetic, Z3 can solve
constraints with real arithmetic as well. At first glance, nothing forced the
restriction to  integer arithmetic. It is well known, that SMT gets easier for
real arithmetic and Apron can work with real arithmetic as well. One could look
into the possibility to use the implementation of this algorithm for real-valued
programs as well.
Apron can use other abstract domains as well. We decided to use polyhedra with
the \gls{ppl} since this was the abstract domain chosen by
\citeauthor{domenech2019arxiv}. However, other abstract domains can be trivially
chosen as well, which would be interesting future research. 

\begin{definition}[Partial Evaluation]
    A graph $G = (\vers, \T_{PE})$ is a \textit{partial evaluation} of a
    \gls{pip} $\Prog$ when for every admissible path $c_0c_1\dots{}c_n \in
    \fpath$ of $\Prog$ with $c_i = (l_i, s_i, t_i)$ and $t_i = (l_{i-1}, \tau_i,
    \eta_i, p_i, l_i)$ for all $i = 1, \dots, n$, there exists a path
    $v_0'v_1'\dots{}v_n'$ in G with the following properties:
    \begin{enumerate}
        \item $v'_i = (\langle l_i, \varphi_i\rangle, t_i')$ with some $\varphi_i
            \in \C$ and $t_i' \in \T_{PE}$,
        \item $t'_i = (\langle l_{i-i}, \varphi_{i-1}\rangle, p_i, \tau_i, \eta_i, 
            \langle l_i, \varphi_i\rangle)$, and
        \item $s_i \models \varphi_i$
    \end{enumerate}
\end{definition}

% \begin{definition}[Partial Evaluation]
%     A graph $G = (\vers, \T_{PE})$ is a \textit{partial evaluation} of a
%     \gls{pip} $\Prog$ when for every admissible path $c_0c_1\dots{}c_n \in
%     \fpath$ of $\Prog$ with $c_i = (l_i, s_i, t_i)$ and $t_i = (l_{i-1}, \tau_i,
%     \eta_i, p_i, l_i)$ for all $i = 1, \dots, n$, there exists a path
%     $v_0'v_1'\dots{}v_n'$ in G with the following properties:
%     \begin{enumerate}
%         \item $v'_i = (\langle l_i, \varphi_i\rangle, t_i')$ with some $\varphi_i
%             \in \C$ and $t_i' \in \T_{PE}$,
%         \item $t'_i = (\langle l_{i-i}, \varphi_{i-1}\rangle, p_i, \tau_i, \eta_i, 
%             \langle l_i, \varphi_i\rangle)$, and
%         \item $s_i \models \varphi_i$
%     \end{enumerate}
% \end{definition}

from the original \gls{pip} that starts in the same location $l \in \L$ as the

from the original \gls{pip} that starts in the same location $l \in \Loc$ as the

        \} & \text{if } t = (l, p, \tau, \eta, l') \\ &

        \} & \text{if } t = (l, p, \tau, \eta, \kappa, l') \\ &

\begin{lemma}\label{lem:unfold_t}
    L $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s,
    s' \in \Sigma$ assignments, and let $\varphi \in \C$. If $s \in \llbracket\varphi\rrbracket$ and
    $\prSs((l,t,s) \rightarrow (l',t',s')) > 0$ for any scheduler $\scheduler$
    and starting state  $s_0 \in \Sigma$ then

\begin{lemma}[Similarity of unfolded transitions]\label{lem:unfold_t_similar}
    For some $\tilde{l, l_1, l_2} \in \Loc_\Prog$, probability $p \in [0,1]$,
    update $\eta: \PV \rightarrow \Z[V\union\D]$, and cost $\kappa \in \R$, let $t
    = (l_1, p, \tau \eta, \kappa, l_2)\in \T_\Prog$. Moreover let $\varphi$ be an
    arbitrary \gls{fo}-formula.
    If $\unfold^*(\langle l, \varphi\rangle, t) \neq \emptyset$ then 

        \item\label{itm:lequal} $l = l_1$, 

            \{t^*\}$ for some $t^* \in \T_\text{PE}$, 
        \item\label{itm:t_equal} $t^* = (\langle l, \varphi\rangle, p, \tau,
            \eta, \langle l', \varphi'\rangle)$ for some $\varphi' \in \C$, and 

            \{t^*\}$ for some $t^* \in \T_\text{PE}$,
        \item\label{itm:t_similar} $t^* = (\langle l, \varphi\rangle, p, \tau,
            \eta, \kappa, \langle l_2, \varphi'\rangle)$ for some $\varphi' \in \C$, and 
    \end{enumerate}
    \begin{proof}
        The unfolding returns a non empty set if and only if the location $l$ of
        the given version is equal to the start location $l_1$ of the location.
        The unfolding returns only an empty set or a set containing a single
        transition. That new transition contains $p$, $\tau$, $\eta$, and $\kappa$
        which were copied from the original transition. The source and target
        version of the new transition have by construction the same locations as
        the original transition.
    \end{proof}
\end{lemma}
\begin{lemma}[Existance of unfolded transitions]\label{lem:unfold_t_exists}
    L $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s, s' \in
    \Sigma$ assignments, and let $\varphi$ be an \gls{fo}-formula over variables
    $\PV$. If $s \in \llbracket\varphi\rrbracket$ and $\prSs((l,t,s) \rightarrow
    (l',t',s')) > 0$ for any scheduler $\scheduler$ and starting state  $s_0 \in
    \Sigma$ then
    \begin{enumerate}
        \item Items \ref{itm:lequal} to \ref{itm:t_similar} from Lemma
            \ref{lem:unfold_t_similar} hold, and

        \GT$ with $t' \in g'$, and $\tilde{s}\in\Sigma$ must exist and $t' = (l,
        p, \tau, \eta, l')$ for some $p \in [0,1]$, $\tau \in C$, and $\eta :
        \PV \rightarrow \Z[\V \union \D]$. It remains to be shown that item
        \ref{itm:smodelsphi} $s' \models \varphi' = \unfold(\varphi \land \tau,
        t)$ holds, then \ref{itm:t_exists} and \ref{itm:t_equal} follow from
        construction. 
         

        \GT$ with $t' \in g'$, and $\tilde{s}\in\Sigma$ must exist with $t' =
        (l, p, \tau, \eta, \kappa, l')$ for some $p \in [0,1]$, $\tau \in C$, $\eta
        : \PV \rightarrow \Z[\V \union \D]$, and $\kappa \in \R$. It remains to be
        shown that $s' \models \varphi' = \unfold(\varphi \land \tau, t)$. The
        rest follows by construction and Lemma \ref{lem:unfold_t_similar}.

        \tau$, and $s = \tilde{s}|_\PV$. It follows that $\tilde{s} \models

        \tau$, and $s|_\PV = \tilde{s}|_\PV$. It follows that $\tilde{s} \models

% \begin{lemma}[Similarity of unfolded general
%     transitions]\label{lem:unfold_g_similar}
%     $\unfold^*(\langle l, \varphi\rangle, g) \neq \emptyset$ if and only if
%     $\unfold^*(\langle l, \varphi\rangle, t_i \neq\emptyset$ for all $t_i \in
%     g$, and 
% \end{lemma}

        Follows immediately from Lemma \ref{lem:unfold_t}.

        Follows immediately from Lemma \ref{lem:unfold_t_exists}.

    For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g \in \GT$
    with guard $\tau_g$, either $unfold(\langle l, \varphi\rangle, g) =
    \emptyset$ or $unfold(\langle l, \varphi\rangle, g) = \{t_1, \dots{},t_n\}$
    where $t_i = (\_, p_i, \tau_g, \_,\_)$ for some $p_i \in [0,1]$ for all
    $i=1,\dots,n$ and $\sum_{i=1}^n p_i = 1$.

    For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g = \{t_1,
    \dots{},t_n\} \in \GTP$ with guard $\tau_g$. Either $unfold(\langle l,
    \varphi\rangle, g) = \emptyset$ or $unfold(\langle l, \varphi\rangle, g) =
    \{t_1', \dots{},t_n'\}$ where for all $i=1,\dots{},n$:
    \begin{enumerate}
        \item $\{t_i'\} = \unfold^*(\langle l, \varphi\rangle,t_i)$,
        \item $t_i' = (\langle l, \varphi\rangle, p_i, \tau_g, \eta_i,
            \kappa_i,\langle l',\varphi\rangle)$ when $t_i = (l, p_i, \tau_g, \eta_i,
            \kappa_i, l')$ for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
            \Z[\V\union\D]$, $\kappa_i\in\R$, and $l' \in \Loc_P$.
    \end{enumerate}
    This implies especially that the probabilities of transitions $t_1' \dots
    t'_n$ add up to 1.

        Let $g = \{t_1, \dots, t_n\} \in \GT$ with $t_i =
        (l,p_i,\tau_i,\eta_i,\_,\_)$. By Definition \ref{def:pip}, the
        probabilities of all transition in a general transition add up to 1.
        \begin{equation*}
            \sum_{i=1}^n p_i = 1,
        \end{equation*}
        and the share the same guard $\tau_g = t_i$ for all $i = 1,\dots,n$. All
        transitions are unfolded exactly once by construction. If $\models
        \varphi \Land \tau_g$, then by Lemma \ref{lem:supp_update_not_empty} and
        Lemma \ref{lem:prob_update} so is $ \models \tilde{\eta}(\varphi \Land
        \tau_g \lfloor\eta\rceil)$. Hence by Lemma \ref{lem:unfold} all $\models

        Let $g = \{t_1, \dots, t_n\} \in \GTP$ with $t_i =
        (l_g,p_i,\tau_i,\eta_i,\kappa_i,l'_i)$. 
        By Definition \ref{def:pip} all transitions $t_1,\dots t_n$share the
        same guard $t_i = t_g$ for all $i=1,\dots,n$. All transitions are
        unfolded exactly once by construction. If $\models \varphi \Land
        \tau_g$, then by Lemma \ref{lem:supp_update_not_empty} and Lemma
        \ref{lem:prob_update} so is $ \models \tilde{\eta}(\varphi \Land \tau_g
        \lfloor\eta\rceil)$. Hence by Lemma \ref{lem:unfold} all $\models

        \varphi\rangle, t_i) = \{t_i'\}$ for some $t_i \in \GT_\text{PE}$ and
        $i=1,\dots,n$. 

        \varphi\rangle, t_i) = \{t_i'\}$ for some $t_i \in 2^{\T_\text{PE}}$ and
        $i=1,\dots,n$. And by Lemma \ref{lem:unfold_t_similar} they have the
        same probability, guard, update and cost.

        The probabilities of all transition $t_1,\dots, t_n$ in the general
        transition $g$ add up to 1 and so do the probabilities of all
        transitions $t'_1,\dots,t'_n$, because the probabilities are just
        copied.

Let $\GT_\text{PE}$ be the set of general transitions over $\T_\text{PE}$. The
operation is overloaded a last time, with a function $\unfold^* : \vers
\rightarrow 2^{\GT_\text{PE}}$ unfolding all outgoing general transitions in the
\gls{pip} $\Prog$.

Let $\GT_\text{PE}$ be the set of general transitions over $\T_\text{PE}$. 
% The
% operation is overloaded a last time, with a function $\unfold^* : \vers
% \rightarrow 2^{\GT_\text{PE}}$ unfolding all outgoing general transitions in the
% \gls{pip} $\Prog$.

\begin{align*}
    \unfold^*(\langle l, \varphi\rangle) = \set{unfold^*(\langle l,
    \varphi\rangle, g_i)}{g\in \GT_{out}(l)}
\end{align*}

% \begin{align*}
%     \unfold^*(\langle l, \varphi\rangle) = \set{unfold^*(\langle l,
%     \varphi\rangle, g_i)}{g\in \GT_{out}(l)}
% \end{align*}

describing (at least) all states reachable from the source constraint via a
given transition. A version describes a set of states at a given location. The
overloaded unfoldings create new transitions between (possibly new versions),
where every state reachable via an original transition from a state in the
source version, is contained in the target version. The properties, such as
probability, guard, update, and cost are just copied, without alteration. 

which describes a polyhedron that containins (at least) all states reachable
from the source constraint via a given transition. A version describes a set of
states at a given location. The overloaded unfolding create new transitions
between (possibly new versions), where every state reachable via an original
transition from a state in the source version, is contained in the target
version. The properties, such as probability, guard, update, and cost are just
copied, without alteration. 

\textit{true}\rangle$. The evaluation unfolds the version. It adds all created
transitions to the evaluation graph and proceeds with unfolding all newly
encountered version. The algorithm is shown in Algorithm
\ref{alg:naive_evaluation}

\textit{true}\rangle$. The evaluation unfolds all general transitions starting
at the same location as the version. It adds all created transitions to the
evaluation graph and proceeds with unfolding all newly encountered version. The
algorithm is displayed in Algorithm \ref{alg:naive_evaluation}

    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GT_G

    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG

    $\GT_G \leftarrow \emptyset$\;

    $\GTG \leftarrow \emptyset$\;

        $N \leftarrow \unfold^*(v)$\;
        \For{$g \in N$}{
            \For{$t = (v, \tau, \eta, p, v') \in g, $}{

        $\langle l, \varphi\rangle \leftarrow v$\;
        \For{$g \in \GTout(l)$} {
            $g' \leftarrow \unfold^*(v, g)$\;
            \For{$t = (v, \tau, \eta, p, \kappa, v') \in g'$}{

            $\GT_G \leftarrow \GT_G + g$\;

            $\GTG \leftarrow \GTG + g'$\;

    \Return $G, \GT_G$

    \Return $G, \GTG$

In general, the abstraction can be arbitrary chosen, as long as the properties above are
satisfied. One possible abstraction, the so called property-based abstraction,
described in \Sref{sec:property-based-abstraction}. For now, the exact details
of abstraction will be omitted. Just know that although necessary for the
algorithm to terminate, they are rather expensive and loose precision.

In general, the abstraction can be arbitrary chosen, as long as the properties
above are satisfied. One possible abstraction, the so called property-based
abstraction, described in \Sref{sec:property-based-abstraction}. For now, the
exact details of abstraction will be omitted. Just know that although necessary
for the algorithm to terminate, they are rather expensive and loose precision.

    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GT_G

    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG

    $\GT_G \leftarrow \emptyset$\;

    $\GTG \leftarrow \emptyset$\;

        $N \leftarrow \unfold^*(v)$\label{alg:abstr_line_unfold_v}\;
        \For{$g \in N$}{
            $g' \leftarrow \emptyset$\;
            \For{$t = (v, p, \tau, \eta, \nu, \langle l', \varphi\rangle) \in g, $}{
                \If {$S_\alpha$} {
                    $t \leftarrow (v, p, \tau, \eta, \nu, \langle l',
                    \alpha(\varphi)\rangle)$\label{alg:abstr_line_abstraction}\;
                }
                $g' \leftarrow g' + t$\label{alg:abstr_line_addtog}\;
                \uIf {$v' \not\in V(G)$}{
                    $G \leftarrow G + t$\;
                    $G \leftarrow evaluate(G, v')$\;
                }
                \Else {
                    $G \leftarrow G + t$\;

        $\langle l, \varphi\rangle \leftarrow v$\;
        \For{$g \in \GTout(l)$} {
            $g' \leftarrow \unfold^*(v, g)$\label{alg:abstr_line_unfold_g}\;
            \If {$g^* \neq \emptyset$ \label{alg:abstr_line_filteremptyg}}{
                $g^* \leftarrow \emptyset$\;
                \For{$t = (v, p, \tau, \eta, \langle l', \varphi\rangle) \in g$}{
                    \If {$S_\alpha$} {
                        $t \leftarrow (v, p, \tau, \eta, \langle l',
                        \alpha(\varphi)\rangle)$\label{alg:abstr_line_abstraction}\;
                    }
                    $g^* \leftarrow g^* + t$\label{alg:abstr_line_addtog}\;
                    \uIf {$v' \not\in V(G)$}{
                        $G \leftarrow G + t$\;
                        $G \leftarrow evaluate(G, v')$\;
                    }
                    \Else {
                        $G \leftarrow G + t$\label{alg:abstr_line_addt}\;
                    }

                $\GTG \leftarrow \GTG + g^*$\;

            $\GT_G \leftarrow \GT_G + g$\;

    \Return $G, \GT_G$

    \Return $G, \GTG$

The algorithm does a depth-first search on the original program $\P$ and

The algorithm does a depth-first search on the original program $\Prog$ and

From the partial evaluation graph a new program is constructed.
\begin{definition}[Partial evaluation]\label{def:partial_evaluation}
    Let $\Prog$ as defined by Definition \ref{def:pip} and $G$ and $\GTG$ be
    the results of Algorithm \ref{alg:evaluate_abstr} on $\Prog$.
    A new \gls{pip} is defined as $\Prog' = (\PV, \Loc_{\Prog'}, \GTPn,
    \langle l_0, \textit{true}\rangle)$ where $\Loc_{\Prog'} = E(G)$, and
    $\GTPn = \GTG$.
    $\Prog'$ is called the \textit{partial evaluation} of $P$.
\end{definition}
\begin{lemma}[Original transitions]
    Let $\Prog'$ be the partial evaluation of $\Prog$ as defined in Definition
    \ref{def:partial_evaluation}. 
    \begin{enumerate}
        \item For every transition $t = (\langle l_1,
            \varphi_1\rangle, p, \tau, \eta, \langle l_2, \varphi_2\rangle) \in
            \T_{\Prog'}$ where $p \in [0,1]$, $\tau$ is an \gls{fo}-formula, and
            $\eta: \PV \rightarrow \Z[\V\union\D]$ one can find a unique
            transition denoted as $\bar{t}\in\T_\Prog$ for which 
            \begin{equation*}
                {\bar{t}} = (l, p, \tau, \eta, l_2)
            \end{equation*}
        \item For every general transition $g = \{t_1, \dots,t_n\} \in
            \GTPn$ one can find a unique general transition denoted as
            $\bar{g}\in\GT_Prog$ for which
            \begin{equation*}
                \bar{g} = \{\bar{t_1}\dots\bar{t_n}\}
            \end{equation*}
    \end{enumerate}
    \begin{proof}
        Any transition $t' = (\langle l_1, \varphi_1\rangle, p, \tau, \eta,
        \langle l_2, \varphi_2\rangle)\in\T_{\Prog'}$ must have been added in
        line \ref{alg:abstr_line_addt} in Algorithm \ref{alg:evaluate_abstr} and
        the transition was found by an unfolding of a general transition $g$ in
        line \ref{alg:abstr_line_unfold_g} and an unfolding of a transition $t
        \in g$. By Lemma \ref{lem:unfold_t_similar} follows $t = (l, p, \tau,
        \eta, l_2)$. We set $\bar{t'}=t$.
        A general transition $g'\in\GTPn$ must have been added in line
        \ref{alg:abstr_line_addtog} in Algorithm \ref{alg:evaluate_abstr} by an
        unfolding of a general transition $g$. And $g' \neq \emptyset$ due to
        the condition checked in \ref{alg:abstr_line_filteremptyg}. For all
        transitions $t'_i\in g'$ the same argument as above holds and we find
        $\bar{t_i} = t_i$ for all transitions, that must all exist due to Lemma
        \ref{lem:unfold_sound}. We set $\bar{g} = g$.
    \end{proof}
\end{lemma}

    Let $\Loc_{\Prog'} = E(G)$, $\GT_{\Prog'} = \GT_G$ and $\Prog' = (\PV, E(G), GT_G,
    \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and $\GT_G$
    where found by the Algorithm \ref{alg:evaluate_abstr} on some input program
    $\Prog$.

    Let $\Loc_{\Prog'} = E(G)$, $\GTPn = \GTG$ and $\Prog' = (\PV, E(G),
    GT_G, \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and
    $\GTG$ where found by the Algorithm \ref{alg:evaluate_abstr} on some input
    program $\Prog$.

        Lemma \ref{lem:unfold_sound} asserts all general transitions found on line
        \ref{alg:abstr_line_unfold_v} are sound general transitions. As the
        abstraction on line \ref{alg:abstr_line_abstraction} doesn't change anything
        about the transition except the target version, and the new transitions are
        all added to a new general transition $g'$ on line
        \ref{alg:abstr_line_addtog'}, $g'$ is also a sound general transition, and
        they all end up in $\GT_G$.

        Lemma \ref{lem:unfold_sound} asserts all general transitions found on
        line \ref{alg:abstr_line_unfold_g} are sound general transitions. As the
        abstraction on line \ref{alg:abstr_line_abstraction} doesn't change
        anything about the transition except the target version, and the new
        transitions are all added to a new general transition $g'$ on line
        \ref{alg:abstr_line_addtog}, $g'$ is also a sound general transition,
        and they all end up in $\GTG$.

\subsection{Expected Runtime Complexity}

    using the the previously constructed scheduler. 

    using the previously constructed scheduler. 

    markovian scheduler $\scheduler': \confs' \rightarrow \GT' \union \{g'_\bot\}$. 
    Note, that in this section primed items are items for $\Prog'$ and unprimed
    items denote items for $\Prog$. 
    % Also recall $\confs = \L \union \{l_\bot\}
    % \times \T \union \{t_\text{in}, t_\bot\}\times \Sigma$.

    markovian scheduler $\scheduler': \confs_\Prog \rightarrow \GTP \union
    \{g_\bot\}$. 

    Note that for any transition $t' \in \T'$ of the evaluated program, one can
    find a unique transition $t \in \T$ of the original program that was
    unfolded to $t'$, since every transition is created by exactly one unfold
    operation in on line \ref{alg:abstr_line_unfold_v} of Algorithm
    \ref{alg:evaluate_abstr}. 
    For all versions $\langle l, \varphi\rangle \in \vers$, let $(g, \tilde{s})
    = \scheduler((l, t, s))$ be the decision taken by the original scheduler. 

    Let $\langle l, \varphi\rangle \in \vers$ be a version on location
    $l\Loc_\Prog$ and formula $\varphi$. Moreover let $(g, \tilde{s}) =
    \scheduler((l, t, s))$ be the decision taken by the original scheduler. 

            $\varphi_i \in \C$, $t'_i \in \T'$, and $i = 1, \dots, n$ \label{itm:location_in_version}

            $\varphi_i \in \C$, $t'_i \in \T'$, and $i = 1, \dots, n$
            \label{itm:location_in_version}

\begin{theorem}\label{thm:correctness}
    For a pip $\Prog$, the evaluation $\Prog'$ as described in
    Definition \ref{def:partial_evaluation}, and a starting state $s_0
    \in\Sigma$ the following holds:
    \begin{equation*}
        \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
        \sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\
    \end{equation*}
    \begin{proof}
        Let $\Prog$ be an arbitrary \gls{pip}, $\Prog'$ be its evaluation and
        $s_0 \in \Sigma$ be any starting state. For any scheduler $\scheduler
        \in \Pi_\text{MD}$ let $\scheduler' \in\Pi_\text{MD}$ be constructed as
        in Lemma \ref{lem:constrfleq}.
        \todo{reference literature, probabilistic}
        \begin{align*}
            \ESs(\Cost(\Prog)) &= \sum_{i=1}^\infty i \cdot P(\Rt(\Prog)=i) 
            = \sum_{i=1}^\infty P(\Cost(\Prog) \leq i) 
            = \sum_{\substack{f \in \fpath_\Prog\\ \Rt(f) \leq
            i}}^\infty \prSs(f) \\
            \ESns(\Cost(\Prog')) &= \sum_{i=1}^\infty i \cdot P(\Rt(\Prog)=i) 
            = \sum_{i=1}^\infty P(\Cost(\Prog) \leq i) 
            = \sum_{\substack{f \in \fpath_\Prog\\ \Rt(f) \leq
            i}}^\infty \prSs(f) \\
            % & \leq \sum_{\substack{f \in \fpath_{\Prog}\\ \Rt(f) \leq i}}^\infty
            % \prSns(f) 
            % = \ESns(\Rt(\Prog'))
        \end{align*}
        \begin{align}
            \sum_{\substack{f \in \fpath_\Prog\\ \Rt(f) \leq i}}^\infty \prSs(f)
            &\leq \sum_{\substack{f \in \fpath_{\Prog'}\\ \Rt(f) \leq i}}^\infty
            \prSns(f) \label{eq:sumsleq} \\
            \Leftrightarrow \ESs(\Cost(\Prog)) &\leq \ESns(\Cost(\Prog')) \label{eq:esleq}
        \end{align}
        By Lemma \ref{lem:constrfleq}, for every finite prefix $f\in
        \fpath_\Prog$ with non-zero probability, one can construct a path of
        equal probability $f' \in \fpath_{\Prog'}$. The constructed paths must
        all be pairwise different, since it is also asserted, that every
        configuration of $f'$ shares the same state and (version) location as
        the original configuration. 
        Hence (at least) all constructed paths $f'$ contribute with equal
        probability to the sum on the right side of of (\ref{eq:sumsleq}). 
        Taking the supremum over all schedulers on both sides of
        (\ref{eq:esleq}) doesn't change the relation, since we just found for
        every scheduler of $\Prog$ a scheduler with equal or larger expected
        runtime for $\Prog'$. 
        \begin{equation*}
            \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
            \sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\
        \end{equation*}
    \end{proof}
\end{theorem}
The following theorem shows, that the partial evaluation hasn't got worse
either than the original program. Note, that doesn't imply that a perfectly
tight bound for the worst-case expected runtime can be found.
\begin{theorem}\label{thm:thightness}
    For a pip $\Prog$, the evaluation $\Prog'$ as described in
    Definition \ref{def:partial_evaluation}, and a starting state $s_0
    \in\Sigma$. The following holds:
    \begin{equation*}
        \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
        \sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\
    \end{equation*}
    \begin{proof}
        Let $\Prog$ be an arbitrary \gls{pip}, $\Prog'$ be its evaluation and
        $s_0 \in \Sigma$ be any starting state. For any scheduler $\scheduler
        \in \Pi_\text{MD}$ let $\scheduler' \in\Pi_\text{HD}$ be constructed as
        in Lemma \ref{lem:constrfleq}.
        Analogously to Theorem \ref{thm:correctness} the following relation
        holds:
        \begin{equation*}
            \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
            \sup_{\scheduler' \in \HDS}(\ESns(\Rt(\Prog'))) \\
        \end{equation*}
        It is known from literature that for a markovian decision process the
        best expected reward using a history dependent scheduler is the same as
        the best expected reward using a markovian scheduler(see. Theorem
        \todo{cite literature} of \cite{puterman1994markov}). Since a run on the
        program is equivalent to a markovian decision process as explained in
        \Sref{ssec:markov}, the Theorem applies to the expected value and the
        following holds:
        \begin{equation*}
            \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq \sup_{\scheduler'
            \in \HDS}(\ESns(\Rt(\Prog'))) = \sup_{\scheduler' \in
            \MDS}(\ESns(\Rt(\Prog')))\\
        \end{equation*}
    \end{proof}
\end{theorem}
Overall by Theorem \ref{thm:correctness} and Theorem \ref{thm:thightness} we
get:
\begin{align*}
    \sup_{\scheduler \in \Pi_\text{HD}}(\ESs(\Rt(\Prog))) &= \sup_{\scheduler'
    \in \Pi_\text{HD}}(\ESns(\Rt(\Prog'))) \\
\end{align*}
We have shown in Theorem \ref{thm:correctness}, that for any starting state, the
new program has a worst-case expected runtime and worst-case expected cost at
least as large as the original program. Hence any bounds found for the partial
evaluation are bounds for the original program. Theorem \ref{thm:thightness} has
shown additionally, that the worst-case expected runtime and costs don't get
worse with a partial evaluation.
\subsection{Expected Size bounds}

\label{ch:preliminaries}
\newcommand{\V}[0]{\mathcal{V}} % Variables
\newcommand{\PV}[0]{\mathcal{PV}} % Program variables
\newcommand{\TV}[0]{\mathcal{TV}} % Program variables
\newcommand{\C}[0]{\mathcal{C}} % Set of polynomial constraints
\newcommand{\D}[0]{\mathcal{D}} % variable distributions 
\newcommand{\Lin}{\mathcal{LC}} % Set of linear constraints
\newcommand{\Loc}{\mathcal{L}} % Set of locations
\newcommand{\F}[0]{\mathcal{F}} % Program variables
\newcommand{\Z}[0]{\mathbb{Z}} % whole numbers, integers
\newcommand{\N}[0]{\mathbb{N}} % natural numbers
\newcommand{\R}[0]{\mathbb{R}} % real numbers
\newcommand{\Zs}[0]{\mathfrak{Z}} % the structure of integer arithmetic.
\newcommand{\Rs}[0]{\mathfrak{R}} % the structure of real arithmetic.
\newcommand{\GT}[0]{\mathcal{GT}} % General transitions
\newcommand{\T}[0]{\mathcal{T}} % General transitions
\newcommand{\RB}[0]{\mathcal{RB}} % Runtime bound
\newcommand{\SB}[0]{\mathcal{SB}} % Size bound
\newcommand{\B}[0]{\mathcal{B}} %Bounds
\newcommand{\Cost}[0]{\mathcal{R}} % Costs
\newcommand{\Rt}[0]{\mathcal{R}^1} %Runtime
\newcommand{\E}[0]{\mathbb{E}} % Expected 
\newcommand{\A}[0]{\mathcal{A}} % Abstract values
\newcommand{\scheduler}[0]{\mathfrak{S}}
\newcommand{\ESs}[0]{\mathbb{E}_{\scheduler,s_0}} % Expected 
\newcommand{\Prog}[0]{\mathcal{P}} % A PIP
\newcommand{\GRV}[0]{\mathcal{GRV}} % General result variables
\renewcommand{\S}[0]{\mathcal{S}} % grv variable
\newcommand{\RBe}[0]{\mathcal{RB}_\E} % Expected Runtime bound
\newcommand{\SBe}[0]{\mathcal{SB}_\E} % Expected Size bound
\newcommand{\with}[0]{\text{ with }}
\newcommand{\union}[0]{\cup}
\newcommand{\Union}[0]{\bigcup}
\newcommand{\intersect}[0]{\cap}
\newcommand{\Intersect}[0]{\bigcap}
\newcommand{\Land}[0]{\wedge}
\newcommand{\LAnd}[0]{\bigwedge}
\newcommand{\set}[2]{\left\{ #1\hspace{0.5em}|\hspace{0.5em}#2\right\}}
\newcommand{\pathto}[0]{\overset{*}{\rightarrow}}
\newcommand{\npathto}[1]{\overset{#1}{\rightarrow}}
\newcommand{\confs}[0]{\textbf{\textsf{Conf}}}
\newcommand{\runs}[0]{\textbf{\textsf{Runs}}}
\newcommand{\fpath}[0]{\textbf{\textsf{FPath}}}
\newcommand{\unfold}[0]{\mathrm{unfold}}
\newcommand{\vers}[0]{\textbf{\textsf{Version}}}
\newcommand{\pr}[0]{\textit{pr}}
\newcommand{\prSs}[0]{\textit{pr}_{\scheduler, s_0}}
\newcommand{\prSns}[0]{\textit{pr}_{\scheduler'_n, s_0}}
\newcommand{\prSnns}[0]{\textit{pr}_{\scheduler'_{n+1}, s_0}}
\newcommand{\PrSs}[0]{\mathbb{P}_{\scheduler, s_0}}
\newcommand{\G}[0]{\mathcal{G}}
\newcommand{\Tin}[0]{\T_\mathrm{in}}
\newcommand{\Tout}[0]{\T_\mathrm{out}}
\newcommand{\GTin}[0]{{\mathcal{G}\mathcal{T}_\text{in}}}
\newcommand{\GTout}[0]{{\mathcal{G}\mathcal{T}_\text{out}}}
\newcommand{\support}[0]{\mathrm{supp}}
This thesis uses a lot of notation. For ease of reading, the reader is provided
with this overview of commonly encountered symbols and their usage.

For ease of reading, the reader is provided with this overview of commonly
encountered symbols and their usage. \todo{update table}

    \begin{tabular}{|l|l|}

    \begin{tabular}{|r|l|}

Let $\overline{\N} = \N \union \{\infty\}$. Let $[\cdot\backslash{}\cdot]$
denote the syntactical substitution where one symbols is replaced by
another. For example $(x<y)[x\backslash{}1] = (1 < y)$. 
For $n \in \N$ consecutive substitutions they also denoted using a shortened
notation. For example $[x_i\backslash{}y_i] =
[x_0\backslash{}y_0]\dots[x_n\backslash{}y_n]\dots$ for some $i = 0,\dots, n$. 

Some general notation is introduced as follows. Let $\overline{\N} = \N
\union \{\infty\}$. The set of all integer polynomials over some indeterminates
$A$ is denoted by $\Z[A]$. A syntactical substitution where one symbol is
replaced by another is denoted with $[\cdot\backslash{}\cdot]$. For example
$(x<y)[x\backslash{}1] = (1 < y)$. 
For a finite set $A = {x_1,\dots,x_n}$, the process of $n$ consecutive
substitutions $[x_i\backslash{}y(i)]$ where the replacement expression $y$
varies only in some index $i$ is denoted using a shortened notation:
$[x_i\backslash{}y_i]_{x_i \in A} = [x_1\backslash{}y(1)] \dots
[x_n\backslash{}y(n)]$. For example $[x_i\backslash{}i]_{x_i\in A} =
[x_0\backslash{}0]\dots[x_n\backslash{}n]\dots$, is the substution where every
variable is replaced by its index in $A = \{x_0, \dots, x_n\}$.

Constraints are a subset of FO-formulas and thus their semantics shall be
defined accordingly.

Constraints are a subset of formulas in \gls{fo} logic.Thus, their semantics
shall be defined accordingly using the $\models$ relation from \gls{fo} logic.

    Let $\varphi$ be an FO-formula. $\llbracket \varphi \rrbracket$ is defined
    as the set of all satisfying assignments or the \textit{solutions} of the
    formula $\varphi$.

    Let $\varphi$ be an \gls{fo}-formula. $\llbracket \varphi \rrbracket$ is
    defined as the set of all satisfying assignments or the \textit{solutions}
    of the formula $\varphi$.

Let $\varphi_1,\varphi_2 \in \C$ and $C \subseteq \C$, the following properties
hold. Hence, conjunctions and sets of constraints can be used interchangeably.

Let $\psi_1,\psi_2\in \C$ and $C \subseteq \C$, the following properties hold,
hence, conjunctions and sets of constraints can be used interchangeably.

    \textit{equivalent}, denoted as $\varphi_1 \equiv \varphi_2$ when there

    \textit{equivalent}, denoted as $\varphi_1 \equiv \varphi_2$ when their

When talking about integer arithmetic on only refers to linear constraints. 

When talking about integer arithmetic one only refers to linear constraints. 

            transitions $t = (l, p, \tau, \eta, \nu, l') \in \T_\Prog \subseteq

            transitions $t = (l, p, \tau, \eta, \kappa, l') \in \T_\Prog \subseteq

                \item an associated cost $\nu\in\R$

                \item an associated cost $\kappa\in\R$

        \Cost(\Prog)(c_0c_1\dots) = |\set{\nu_{t_i}}{c_i = (l_i, t_i, s_i) \text{

        \Cost(\Prog)(c_0c_1\dots) = |\set{\kappa_{t_i}}{c_i = (l_i, t_i, s_i) \text{

transition has an associated cost of $\nu_t=1$ for all $t \in \T$. Then 

transition has an associated cost of $\kappa_t=1$ for all $t \in \T$. Then 

    \tau, \nu, l)$. 

    \tau, \kappa, l)$. 

\section{Background}

\section{Background}\label{sec:background}

\section{Goal}

\section{Goal}\label{sec:goal}

\newacronym{fo}{FO}{first-order}
\newacronym{ocaml}{OCaml}{Objective CAML}
\newacronym{apron}{Apron}{The Apron Numerical Abstract Domain Library}