The heuristic for the property based abstraction described in
\Sref{sec:property_based_abstraction} selects properties for loop heads. It
relies on the fact that loops with corresponding loop-heads are found. In our
implementation we detect loops with the algorithm described by
\citeauthor{johnson1975}\cite{johnson1975}. The algorithm returns loops where
the first location is the smallest location with respect to some arbitrary
ordering. By ordering the locations topologically from the starting location,
the first location on the loop is always the closest location to the starting
location, which would naturally be considered as the loop-head. 
Johnson's algorithm returns a set of loops $L_1, \dots, \Loc_n \subset \Loc_\Prog$.
It is sufficient to mark only one location per loop for abstraction. The loop
detection by \citeauthor{johnson1975} can return many overlapping loops and
hence we might mark more than one location per loop for abstraction. The
abstraction operation is expensive, since it requires many calls to an \gls{smt}
solver for the entailment check, hence reducing the number of locations marked
for abstraction can improve the performance of the partial evaluation and also
increases the precision of the evaluation. We propose a different approach to
finding loop heads. By computing the \gls{fvs} on the loops, the number of
locations marked for abstraction is minimized. At the same time every loop still
contains a location marked for abstraction and the evaluation is guaranteed to
eventually terminate. 
The problem of finding the \textit{Feedback Vertex Set} or \textit{Feedback Node
Set} is one of Karp's 21 NP-complete problems.\cite{karp2010reducibility}. 
\begin{definition}[Feedback Vertex Set Problem]
    Given a directed graph $G = (V, E)$. Find the minimal subset $R \subseteq
    V$ such that every (directed) cycle of $G$ contains a node in $R$.
\end{definition}
 We already detected the loops with \citeauthor{johnson1975}s algorithm. The
 problem can instead be formulated as a hitting set problem. 
\begin{definition}[Hitting Set Problem]
    Given a finite collection of finite sets $S = \{S_1, \dots, S_n\}$, where
    each $S_i \subseteq U$ for some set $U$, find a minimal set $R$ such that
    $R\intersect S_i \neq \emptyset$ for all $i = 1,\dots,n$.
\end{definition}
A hitting set problem can be formulated as a \gls{ilp} and solved by readily
available \gls{smt} solvers. In the following the \gls{ilp} used for finding the
feedback vertex set of an integer program with locations $L$ and a total of $N$
loops $a_1, \dots, a_N$ is constructed. For a set of loops $L = L_1, \dots,L_2$ a
linear integer optimization problem is formulated and solved using an
\gls{smt}-solver.
\begin{mini!}
    {}{\sum_{i=1}^{n} x_i\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}
    \addConstraint{\sum_{i : l_i \in \text{Loc}(a_j)} x_i}{\geq
    0,\protect\quad\label{eq:lip1-hit}}{j = 1,\dots,N}
    \addConstraint{ x_i }{\leq 1,\protect\quad\label{eq:ilp-leq1}}{i = 1,\dots,n}
    \addConstraint{ x_i }{\geq 0,\protect\quad\label{eq:ilp-geq0}}{i = 1,\dots,n}
\end{mini!}
Every variable $x_i$ of the \gls{ilp} \ref{eq:ilp-vfs} indicates if a location
is part of the hitting set in which case the variable is assigned to 1, or not
in which case the variable is assigned the value 0. The constraints
\ref{eq:ilp-hit} guarantees that every loop is \enquote{hit}, while
\ref{eq:ilp-leq1} and \ref{eq:ilp-geq0} enforce that every location is only
selected at most once. The optimization goal \ref{eq:ilp-vfs} being to select
the fewest locations possible.
Computing the feedback vertex set of a program is independent of the partial
evaluation and can be done a-priori. It is thus considered to be an offline
method. It shall be noted that the locations inside the feedback vertex set do
not need to be the closed location to the start location of a loop. For
determination of properties it might be necessary to rotate the loop so that the
marked locations are the first location in the loop. 
\todo{prove upper bound on program size}
\subsection{Property-based abstraction}
\subsection{Unfolding}
Recall Lemma \ref{lem:nonprop_update} and the Definition \ref{def:unfold} of the
unfold operation which computes a new (target) version for a source version and
a transition. For a version $\langle \ell, \varphi\rangle \in \vers_\Prog$, and
a transition $t = (\ell, p, \tau, \eta, \ell') \in \T_\Prog$, we have
\begin{equation*}\begin{gathered}
        \tilde{\eta}(\varphi \Land \tau \Land \lfloor \eta\rceil) = ((\varphi
        \land \tau \Land \lfloor\eta\rceil \LAnd_{x\in \PV} x' =
        \tilde{\eta}(x))|_{\PV'})[x'/x]_{x\in \PV} \\
        \varphi' = \unfold(\varphi \Land \tau, \eta) = \begin{cases}
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil) & \text{if } \varphi
            \Land \tau \text{ is satisfiable},\\
            \texttt{false} & \text{otherwise}
        \end{cases}\\
        \unfold(\langle \ell,\varphi\rangle, t) = (\langle \ell, \varphi\rangle,
        p, \tau\Land\varphi, \eta,\langle \ell', \varphi' \rangle) 
\end{gathered}\end{equation*}
We illustrate the unfolding on the abstract domain of convex Polyhedra. In
practice any other abstract domain can be used as well. Let $\texttt{proj}: 2^\V
\times \Poly \rightarrow \Poly$ be the projection, and $\texttt{update}: (\PV
\rightarrow \Z[\V]) \times \Poly \rightarrow \Poly$ be an update in an abstract
domain. We can convert to and from polyhedra with the $\texttt{polyh} : \C
\rightarrow \Poly$ and $\texttt{constr}: \Poly \rightarrow \Lin$ function. An
implementation of the unfold operation is shown in Algorithm \ref{alg:unfold}.
\begin{algorithm}
    \caption{Unfolding\label{alg:unfold}}
    \KwData{ A PIP $\Prog$ } 
    \SetKwFunction{FUnfold}{unfold}
    \SetKwProg{Fn}{Function}{:}{end}
    \Fn{\FUnfold{$\langle\ell,\varphi\rangle \in \vers_\Prog$, $(\ell_1, p,
    \tau, \eta,\ell_2) \in \T_\Prog$}}{
        \textbf{assert} $\ell = \ell_1$\;
            \uIf{$\varphi \Land \tau$ is satisfiable} {
            $P \leftarrow \texttt{polyh}(\varphi \land \tau \Land \lfloor\eta\rceil)$\;
            $P \leftarrow \texttt{update}(\tilde{\eta}, P)$\;
            $P \leftarrow \texttt{proj}(\PV_\Prog, P)$\;
            $\varphi' \leftarrow \texttt{constr}(P)$\;
        } \Else{
            $\varphi' \leftarrow \texttt{false}$\;
        }
        $t' \leftarrow (\langle \ell_1, \varphi\rangle, p, \varphi \Land \tau,
        \eta, \langle\ell_2,\varphi'\rangle)$\;
        \Return{$t'$}
    }
\end{algorithm}
\subsection{Partial evaluation}
The partial evaluation can be computed with a \gls{dfs} over the original
program starting at the initial location $\ell_0$. The \gls{dfs} backtracks
whenever it encounters a version already added to the program.
\begin{algorithm}
    \caption{Evaluate a Program $\Prog$ with abstraction
    $\alpha$.\label{alg:evaluate_abstr}}
    \KwData{ A PIP $\Prog$, abstraction function $\alpha$, and
    abstraction oracle $S_\alpha$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
    \subset \GT_\text{PE}$}
    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    $\GTG \leftarrow \emptyset$\;
    \Fn{\FEvaluate{$G$, $v$}}{
        $\langle l, \varphi\rangle \leftarrow v$\;
        \For{$g \in \GTPout(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 \FEvaluate{G, v'}$\;
                    }
                    \Else {
                        $G \leftarrow G + t$\label{alg:abstr_line_addt}\;
                    }
                }
                $\GTG \leftarrow \GTG + g^*$\;
            }
        }
        \Return {$G$}
    }
    $v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
    $G \leftarrow (\{v_0\}, \emptyset)$\;
    $G \leftarrow $\FEvaluate{$G$, $v_0$}\;
    \Return $G, \GTG$
\end{algorithm}
\section{Technical details}\label{sec:technical_details}
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}\cite{apron} and the \gls{ppl}\cite{bagnara2008socp}, which can be
used as an abstract domain in apron.
Both 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 component of a program, where implemented. 
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. It might
be used by other tools in the future, that want to profit from partial
evaluation on probabilistic programs. 
The evaluation on sub-\gls{scc} was integrated into \gls{koat}s analysis similar
to iRankFinder as described in \cite{giesl2022lncs}, 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.
\section{Selecting the Abstract domain}\label{sec:abstract_domain}
In the implementation, the projection is computed using an abstract domain.
Thanks to the \gls{apron}\cite{apron} library, the new implementation is generic
over the specific abstract domain used. We decided to use the abstract domain of
polyhedra (see. \Sref{ssec:polyhedra}), since they are exact on linear
constraints. In practice only small components are partially evaluated, making
the performance disadvantage acceptable. \gls{apron} uses the
\gls{ppl}\cite{bagnara2008socp} under the hood for polyhedra. Other abstract
domains supported by \gls{apron} might be used in the future. In addition to the
projection operation, the library supports updates as-well, which is used when
possible. The \gls{ppl} ignores all non-linear constraints, over-approximating
the set of constraints in the process. In turn the projection is
over-approximated as well. One could decide to over-approximate non-linear
constraints manually, in order to achieve tighter projections. For example
quadratic polynomials have an easy to compute minimum and maximum, which could
be transformed into a single linear constraint. 
\subsection{Property-based abstraction}
We implemented the property based abstraction (recall
\Sref{sec:property_based_abstraction}) proposed by
\citeauthor{Domenech19}. The heuristic uses backwards-propagation as one
source of properties. Our implementation applies the backwards-propagation for
every loop a location marked for abstraction is on, possibly aggregating
properties from multiple loops.
The properties are projected onto the program variables, in order to reduce
their number, and because values for temporary variables do not propagate
throughout the program. The entailment checks of properties are done using
Z3 and Lemma \ref{lem:entailment}. Since a set of constraints is checked
against many properties, an incremental solver is used in order avoid
recomputing the model for the set of constraints every time.
Once a set of constraints is abstracted, it is replaced by the set of entailed
properties. 
Recall Algorithm \ref{alg:evaluate_abstr}. When adding a new transition to the
partial evaluation graph, we check, if the version is already present in the
graph. Instead of checking for equivalence on every version, we use structural
equality, which might not detect equivalent versions on non-abstracted
constraints, but works for the abstracted versions with properties, since the
properties are reused during abstraction.
\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}.
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{giesl2022lncs} 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{giesl2022lncs} 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{giesl2022lncs} 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{Domenech19}. However, other abstract domains can be trivially
chosen as well, which would be interesting future research. 

This chapter will present the implementation of a (sub-\gls{scc})
partial-evaluation with property-based abstraction as described in the previous
\Cref{ch:theory}. In \Sref{sec:implementation} we describe an implementation
using pseudo-code and focusing mostly on the practical aspects of the partial
evaluation. \Sref{sec:abstract_domain} will briefly discuss the possible
abstract domains and the reasons why we decided to use the abstract domain of
Polyhedra. \Sref{sec:loop_heads} will focus on the different possibilities to
mark locations for abstraction, which is part of the history-dependent aspect of
the abstraction layer. \Sref{sec:technical_details} describes the technical
details of the actual implementation and finally in \Sref{sec:performance} the
correctness and performance of the implementation is evaluated practically. 

This chapter will present the implementation of partial-evaluation with
localised property-based abstraction as introduced in the previous
\Cref{ch:theory}. In \Sref{sec:implementation} we describe the implementation
using pseudo-code. We will mostly on the practical aspects of the partial
evaluation. 
% \Sref{sec:abstract_domain} will briefly discuss the possible
% abstract domains and the reasons why we decided to use the abstract domain of
% Polyhedra. \Sref{sec:loop_heads} will focus on the different possibilities to
% mark locations for abstraction, which is part of the history-dependent aspect of
% the abstraction layer. \Sref{sec:technical_details} describes the technical
% details of the actual implementation and finally in \Sref{sec:performance} the
% correctness and performance of the implementation is evaluated practically. 

In this section we present a pseudo-code implementation for the $\unfold$

In this section, we present a pseudo-code implementation for the $\unfold$

\Sref{sec:partialevaluation} using location dependent property based
abstraction. Then the algorithm is adapted to a sub-\gls{scc} evaluation where
only a component of the program is partially evaluated.

\Sref{sec:partialevaluation} using localised property-based abstraction. First,
we will present two variants for selecting locations on all the loops such that
the property from Lemma \ref{lem:localized_pba_finite} is satisfied. Second, we
will introduce the heuristic for property generation, that was put forward by
\citeauthor{Domenech19} \cite{Domenech19} and give an implementation as a
pseudo-code algorithm. Third, we will describe the technique for selecting
components during analysis of a program on which the control-flow-refinement via
partial evaluation is then applied, similarly to the technique presented by
\citeauthor{giesl2022lncs} \cite{giesl2022lncs}. Finally, an implementation for
unfolding and partial evaluation on subsets of transitions is presented as a
pseudo-code algorithm.
\subsection{Selecting Loops for Abstraction}\label{sec:loop_heads}
Recall Lemma \ref{lem:localized_pba_finite}. As long as the localized
abstraction function has one location per loop for which every version at that
location is abstracted onto a finite abstraction space, the partial evaluation
graph is finite. The native approach to assert this property is to use a global
abstraction function with a finite abstraction space. However, when using
property-based abstraction, every abstraction involves many entailment checks,
which require a call to the \gls{smt}-solver. This call is expensive and as was
demonstrated in Example \ref{ex:global_abstr}, a global abstraction function
does not yield the smallest partial evaluations, which makes successive analysis
even slower. 

\subsection{Detecting Loops and Loop-heads}\label{sec:loop_heads}
The heuristic for the property based abstraction described in
\Sref{sec:property_based_abstraction} selects properties for loop heads. It
relies on the fact that loops with corresponding loop-heads are found. In our
implementation we detect loops with the algorithm described by
\citeauthor{johnson1975}\cite{johnson1975}. The algorithm returns loops where

In our implementation, we detect loops with the algorithm described by
\citeauthor{johnson1975} \cite{johnson1975}. The algorithm returns loops where

location, which would naturally be considered as the loop-head. 

location, which would naturally be considered as the loop-head.

Johnson's algorithm returns a set of loops $L_1, \dots, \Loc_n \subset \Loc_\Prog$.

The loops and loop-heads found by this method can be used for localised
property-based abstraction. We propose a second variant that minimises the
number of loop-heads by computing the feedback-vertex set. Reducing the number
of loop-heads makes successive evaluation faster, and the partial-evaluation
graph more precise in the mostly linear parts, where abstraction is not
necessary.

It is sufficient to mark only one location per loop for abstraction. The loop
detection by \citeauthor{johnson1975} can return many overlapping loops and
hence we might mark more than one location per loop for abstraction. The
abstraction operation is expensive, since it requires many calls to an \gls{smt}
solver for the entailment check, hence reducing the number of locations marked
for abstraction can improve the performance of the partial evaluation and also
increases the precision of the evaluation. We propose a different approach to
finding loop heads. By computing the \gls{fvs} on the loops, the number of
locations marked for abstraction is minimized. At the same time every loop still
contains a location marked for abstraction and the evaluation is guaranteed to
eventually terminate. 

Set} is one of Karp's 21 NP-complete problems.\cite{karp2010reducibility}. 

Set} is one of Karp's 21 NP-complete problems \cite{karp2010reducibility}. 

 We already detected the loops with \citeauthor{johnson1975}s algorithm. The
 problem can instead be formulated as a hitting set problem. 

The loops have already been detected with \citeauthor{johnson1975}s algorithm.
The problem can instead be formulated as a hitting set problem. 

A hitting set problem can be formulated as a \gls{ilp} and solved by readily
available \gls{smt} solvers. In the following the \gls{ilp} used for finding the
feedback vertex set of an integer program with locations $L$ and a total of $N$
loops $a_1, \dots, a_N$ is constructed. For a set of loops $L = L_1, \dots,L_2$ a
linear integer optimization problem is formulated and solved using an
\gls{smt}-solver.

An instance of a hitting set problem can be solved using \gls{ilp} and an
\gls{smt}-solver. For loops $L_1, \dots, L_N$, we formulate the following
\gls{ilp} instance, where the variables $x_{\ell_0}, \dots,x_{\ell_n}$ are variables
for every location in the program.

    {}{\sum_{i=1}^{n} x_i\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}
    \addConstraint{\sum_{i : l_i \in \text{Loc}(a_j)} x_i}{\geq

    {}{\sum_{i=1}^{N} x_{\ell_i}\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}
    \addConstraint{\sum_{\ell_i \in L_j} x_{\ell_i}}{>

    \addConstraint{ x_i }{\leq 1,\protect\quad\label{eq:ilp-leq1}}{i = 1,\dots,n}
    \addConstraint{ x_i }{\geq 0,\protect\quad\label{eq:ilp-geq0}}{i = 1,\dots,n}

    \addConstraint{ x_{\ell_i} }{\geq 0,\protect\quad\label{eq:ilp-geq0}}{i = 1,\dots,n}
    \addConstraint{ x_{\ell_i} }{\leq 1,\protect\quad\label{eq:ilp-leq1}}{i = 1,\dots,n}

Every variable $x_i$ of the \gls{ilp} \ref{eq:ilp-vfs} indicates if a location
is part of the hitting set in which case the variable is assigned to 1, or not
in which case the variable is assigned the value 0. The constraints
\ref{eq:ilp-hit} guarantees that every loop is \enquote{hit}, while
\ref{eq:ilp-leq1} and \ref{eq:ilp-geq0} enforce that every location is only
selected at most once. The optimization goal \ref{eq:ilp-vfs} being to select
the fewest locations possible.

The value for the location variables are constrained to $0 \leq x_{\ell_j}\leq
1$ for all $\ell_j \in \Loc_\Prog$ by \eqref{eq:ilp-geq0} and
\eqref{eq:ilp-leq1}. For an assignment $\sigma : \Loc_\Prog \rightarrow \N$ a
value $\sigma(x_{\ell_j}) = 1$ indicates that the location $\ell_j$ is part of
the hitting set; a value $\sigma(x_{\ell_j}) = 0$ indicates that it is not. The
constraints \eqref{eq:lip1-hit} guarantees that at least one location on every
loop is selected, and the optimization goal \eqref{eq:ilp-vfs} minimizes the
number of selected locations.

Computing the feedback vertex set of a program is independent of the partial
evaluation and can be done a-priori. It is thus considered to be an offline
method. It shall be noted that the locations inside the feedback vertex set do
not need to be the closed location to the start location of a loop. For
determination of properties it might be necessary to rotate the loop so that the
marked locations are the first location in the loop. 

The computation of the feedback-vertex-set and loops is independent of the
partial evaluation and can be done a-priori. 

\todo{prove upper bound on program size}

\subsection{Property-based abstraction}
Once loops $L_1, \dots, L_N \subseteq \Loc_\Prog$ of a \gls{pip} $\Prog$ are
detected and the loop-heads or locations marked for abstraction $L \subseteq
\union_{i=1}^N L_i$ are selected, one needs to select an appropriate localised
abstraction function. \citeauthor{Domenech19} proposed a heuristic which
identifies the properties that are relevant for an iteration of a loop
\cite{Domenech19}. We will just briefly describe this heuristic. For a location
$\ell \in L$, the following heuristics are defined.

\begin{align*}
    \PRh(\ell) &= \set{\psi}{t = (\ell, \_, \tau, \_, \_) \in
    \TPout(\ell), \psi \in \tau|_\PV}\\
    \PRhv(\ell) &= \set{x \diamond c}{t = (\ell, \_, \tau, \_, \_) \in
    \TPout(\ell), x \in \PV, \diamond \in \{\leq, \geq\}, \tau \models x \diamond c}\\
    \PRc(\ell) &= \set{\psi}{t = (\_, \_, \tau, \eta, \ell) \in
    \TPin(\ell), \psi \in \tilde{\eta}(\tau \land \lfloor\eta\rceil))}\\
    \PRcv(\ell) &= \set{x \diamond c}{t = (\_, \_, \tau, \eta, \ell)
    \in \TPin(\ell), x \in \PV, \diamond \in \{\leq, \geq\}, \tilde{\eta}(\tau \land \lfloor\eta\rceil) \models x \diamond c}\\
\end{align*}

$\PRh$ captures properties that must be met on any outgoing transition. $\PRhv$
computes bounds for all program variables that might not be captured otherwise,
because they they implicitly implied by the guard.
$\PRc$ and $PRcv$ do the same for all incoming transition. In addition, a
heuristic $\PRd$ is defined that propagates properties backwards through a loop,
capturing the conditions that are required to iterate through the loop without
leaving the loop. The loops are first transformed into transition loops
$T_{L_1},\dots, T_{L_n} \subseteq \TP$, as described in
\Sref{sec:graph_operations}. Then for every transition loop 

\subsection{Property-based abstraction}

For a transition loop $T = \{t_0, \dots, t_m\}$ and a location $\ell \in L_j$
on that loop, a backwards propagation function $\back : \T \times \C \rightarrow
\C$ and the heuristic $\PRd$ is defined as follows:
\begin{align*}
    \back(t, \varphi) &= \varphi [x / \tilde{\eta}] \land \lfloor\eta\rceil \land
    \tau \text{ where } t = (\_, \_, \tau, \eta, \_) \\
    \PRd(T, \ell) &= \back(t_1, \dots \back(t_m, \texttt{true})\dots)
\end{align*}

\subsection{Unfolding}
Recall Lemma \ref{lem:nonprop_update} and the Definition \ref{def:unfold} of the
unfold operation which computes a new (target) version for a source version and
a transition. For a version $\langle \ell, \varphi\rangle \in \vers_\Prog$, and
a transition $t = (\ell, p, \tau, \eta, \ell') \in \T_\Prog$, we have

\begin{equation*}
    \Psi_\ell = \PRh(\ell) \union \PRhv(\ell) \union \PRc(\ell)  \union \PRcv
    \union \Union_{\substack{T \in T_{L_i}\\ L_i\;:\;\ell \in L_i}} \PRd(T,
    \ell)
\end{equation*}

\begin{equation*}\begin{gathered}
        \tilde{\eta}(\varphi \Land \tau \Land \lfloor \eta\rceil) = ((\varphi
        \land \tau \Land \lfloor\eta\rceil \LAnd_{x\in \PV} x' =
        \tilde{\eta}(x))|_{\PV'})[x'/x]_{x\in \PV} \\
        \varphi' = \unfold(\varphi \Land \tau, \eta) = \begin{cases}
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil) & \text{if } \varphi
            \Land \tau \text{ is satisfiable},\\
            \texttt{false} & \text{otherwise}
        \end{cases}\\
        \unfold(\langle \ell,\varphi\rangle, t) = (\langle \ell, \varphi\rangle,
        p, \tau\Land\varphi, \eta,\langle \ell', \varphi' \rangle) 
\end{gathered}\end{equation*}

The localised property-based abstraction using those properties for the
locations marked for abstraction is used by our implementation.
\subsection{Selecting Transitions $T$}
During \gls{koat}s analysis of a program size and runtime-complexity bounds for
every transition are computed. Whenever the analysis fails at finding linear
runtime-complexity bounds for a transition, this transition is added to a set of
transitions $\T_\text{nl}$ which need further refinement. The set of transitions
$T$ used for control-flow-refinement is generated by selecting the smallest loop
for all transitions in $\T_\text{nl}$ and expanding it to all parallel
transitions. The algorithm is describe in details by

We illustrate the unfolding on the abstract domain of convex Polyhedra. In
practice any other abstract domain can be used as well. Let $\texttt{proj}: 2^\V
\times \Poly \rightarrow \Poly$ be the projection, and $\texttt{update}: (\PV
\rightarrow \Z[\V]) \times \Poly \rightarrow \Poly$ be an update in an abstract
domain. We can convert to and from polyhedra with the $\texttt{polyh} : \C
\rightarrow \Poly$ and $\texttt{constr}: \Poly \rightarrow \Lin$ function. An
implementation of the unfold operation is shown in Algorithm \ref{alg:unfold}.

\begin{algorithm}
\end{algorithm}

\subsection{Partial Evaluation on $T$}

\subsection{Partial evaluation}
The partial evaluation can be computed with a \gls{dfs} over the original
program starting at the initial location $\ell_0$. The \gls{dfs} backtracks
whenever it encounters a version already added to the program.

\begin{algorithm}
    \caption{Evaluate a Program $\Prog$ with abstraction
    $\alpha$.\label{alg:evaluate_abstr}}
    \KwData{ A PIP $\Prog$, abstraction function $\alpha$, and
    abstraction oracle $S_\alpha$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
    \subset \GT_\text{PE}$}
    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    $\GTG \leftarrow \emptyset$\;
    \Fn{\FEvaluate{$G$, $v$}}{
        $\langle l, \varphi\rangle \leftarrow v$\;
        \For{$g \in \GTPout(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 \FEvaluate{G, v'}$\;
                    }
                    \Else {
                        $G \leftarrow G + t$\label{alg:abstr_line_addt}\;
                    }
                }
                $\GTG \leftarrow \GTG + g^*$\;
            }
        }
        \Return {$G$}
    }
    $v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
    $G \leftarrow (\{v_0\}, \emptyset)$\;
    $G \leftarrow $\FEvaluate{$G$, $v_0$}\;
    \Return $G, \GTG$
\end{algorithm}
\section{Technical details}\label{sec:technical_details}

\section{Technical Details}\label{sec:technical_details}

\section{Selecting the Abstract domain}\label{sec:abstract_domain}
In the implementation, the projection is computed using an abstract domain.
Thanks to the \gls{apron}\cite{apron} library, the new implementation is generic
over the specific abstract domain used. We decided to use the abstract domain of
polyhedra (see. \Sref{ssec:polyhedra}), since they are exact on linear
constraints. In practice only small components are partially evaluated, making
the performance disadvantage acceptable. \gls{apron} uses the
\gls{ppl}\cite{bagnara2008socp} under the hood for polyhedra. Other abstract
domains supported by \gls{apron} might be used in the future. In addition to the
projection operation, the library supports updates as-well, which is used when
possible. The \gls{ppl} ignores all non-linear constraints, over-approximating
the set of constraints in the process. In turn the projection is
over-approximated as well. One could decide to over-approximate non-linear
constraints manually, in order to achieve tighter projections. For example
quadratic polynomials have an easy to compute minimum and maximum, which could
be transformed into a single linear constraint. 
\subsection{Property-based abstraction}
We implemented the property based abstraction (recall
\Sref{sec:property_based_abstraction}) proposed by
\citeauthor{Domenech19}. The heuristic uses backwards-propagation as one
source of properties. Our implementation applies the backwards-propagation for
every loop a location marked for abstraction is on, possibly aggregating
properties from multiple loops.
The properties are projected onto the program variables, in order to reduce
their number, and because values for temporary variables do not propagate
throughout the program. The entailment checks of properties are done using
Z3 and Lemma \ref{lem:entailment}. Since a set of constraints is checked
against many properties, an incremental solver is used in order avoid
recomputing the model for the set of constraints every time.
Once a set of constraints is abstracted, it is replaced by the set of entailed
properties. 

Recall Algorithm \ref{alg:evaluate_abstr}. When adding a new transition to the
partial evaluation graph, we check, if the version is already present in the
graph. Instead of checking for equivalence on every version, we use structural
equality, which might not detect equivalent versions on non-abstracted
constraints, but works for the abstracted versions with properties, since the
properties are reused during abstraction.

\section{Performance}

\section{Performance and Correctness}\label{sec:performance}

\todo{discuss the results}

\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{Domenech19}. However, other abstract domains can be trivially
chosen as well, which would be interesting future research. 

\rem{We dropped the requirement for a finite abstraction space for now and will
reintroduce it in a slightly altered form later on, in order to still guarantee
a finite partial evaluation graph.}

\begin{rem}
    We dropped the requirement for a finite abstraction space for now and will
    reintroduce it in a slightly altered form later on, in order to still
    guarantee a finite partial evaluation graph.
\end{rem}

\rem{

\begin{rem}

}

\end{rem}

                        (\ell_g, p, \tau_g, \eta, \varphi') \in g'_i}

                        (\ell_g, p, \tau_g, \eta, \ell') \in g'_i, \varphi' \in
                        \Phi}

    described in Definition \ref{def:partial_evaluation}, let $\simu:

    described in Definition \ref{def:partial_evaluation} with localised
    abstraction function $S$ and component $T$, let $\simu_{\Prog,S,T}:

        \simu((\ell, t, s)) = (\langle \ell, \texttt{true}\rangle,
            \unfold_{\Prog,\alpha}(\langle \ell, \texttt{true}\rangle, t), s) \\
        \simu(\varf (\ell, t, s)) = \varf' (\langle \ell, \varphi\rangle,
            \unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t), s) \\ 
        \text{ where } \varf' = \simu(\varf) = \dots{}(\ell, \_, \_)

            \simu_{\Prog,S,T}((\ell, t, s)) = 
            \begin{cases}
            (\langle \ell, \texttt{true}\rangle,
                \unfold_{\Prog,S}(\langle \ell, \texttt{true}\rangle, t), s) & t
                = (\ell, \_,\_, \_,\_) \in T \\
            (\langle \ell, \texttt{true}\rangle,
                (\langle\ell,\texttt{true}\rangle,p,\tau,\eta,\langle\ell',\texttt{true}),
                s) & t = (\ell,p,\tau,\eta,\ell') \not\in T
            \end{cases}\\
            \simu_{\Prog,S,T}(\varf (\ell, t, s)) = 
            \begin{cases}
            \varf'(\langle \ell, \texttt{true}\rangle,
                \unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t), s) & t
                = (\ell, \_,\_, \_,\_) \in T \\
            \varf'(\langle \ell, \varphi\rangle,
                (\langle\ell,\varphi\rangle,p,\tau,\eta,\langle\ell',
                \texttt{true}), s) & t = (\ell,p,\tau,\eta,\ell') \not\in T
            \end{cases} \\ 
            \text{ where } \varf' = \simu(\varf) =
            \dots{}(\langle\ell,\varphi\rangle, \_, \_)

    $\Prog$. 

    $\Prog$ with localised abstraction function $S$ and component $T$. 

            \Rt_\Prog(\varf) = \Rt_{\Prog'}(\simu(\varf))

            \Rt_\Prog(\varf) = \Rt_{\Prog'}(\simu_{\Prog,S,T}(\varf))

            \simu(f_1) \neq \simu(f_2)

            \simu_{\Prog,S,T}(\varff_1) \neq \simu_{\Prog,S,T}(\varff_2)

    described in Definition \ref{def:partial_evaluation}, there exists a
    Markovian scheduler $\scheduler' \in \MDS_{\Prog'}$, such that for all
    admissible finite prefixes $f\in\fpath_\Prog$ with $\prSs(\varf) > 0$
    there exists a finite prefix $\varf' = \simu(\varf)

    described in Definition \ref{def:partial_evaluation} with localised
    abstraction function $S$ and component $T$. There exists a Markovian
    scheduler $\scheduler' \in \MDS_{\Prog'}$, such that for all admissible
    finite prefixes $f\in\fpath_\Prog$ with $\prSs(\varf) > 0$ there exists a
    finite prefix $\varf' = \simu_{\Prog,S,T}(\varf)

    \set{unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t) }{ t \in g }$.

    \set{\unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t) }{ t \in g \text{
        and } t \in T} \union
    \set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land \tau_{g_i},
    \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g, \eta, \ell')
    \in g, \varphi' \in \Phi, \text{ but } t \not\in T}$. $g'$ is the general
    transition that contains all the unfolded and copied transitions for $t \in
    g$. For better readability we define a function $\texttt{eval}_{\Prog,S,T} : \GTP
    \rightarrow \GTPn$ where 
    \begin{align*}
        \texttt{eval}_{\Prog,S,T} (g) = &\set{\unfold_{\Prog,S}(\langle \ell,
        \varphi\rangle, t) }{ t \in g \cap t \in T} \union \\ 
        &\set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land
        \tau_{g_i}, \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g,
        \eta, \ell') \in g \backslash T, \varphi' \in \Phi}.
    \end{align*}

                \neq t_\bot, s' \models \varphi, \\ 
                &\scheduler(\ell, \bar{t'}, s') = (g, \tilde{s}), g \neq g_\bot\text{, and}\\
                &g' = \set{\unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t) }{ t \in g }

            \neq t_\bot, s' \models \varphi, \\ &\scheduler(\ell, \bar{t'}, s')
            = (g, \tilde{s}), g \neq g_\bot\text{, and}\\ &g' =
            \texttt{eval}_{\Prog,S,T}(g)

                \neq t_\bot, s' \models \varphi\text{, and}\\ 

                \neq t_\bot, s' \not\models \varphi\text{, and}\\ 

    $\tau_{g'} = \varphi \Land \tau_g$. Since $\tilde{s} \models \tau_g$ and
    $\tilde{s}|_\PV = s'$, it follows $\tilde{s} \models \varphi \Land \tau_g$. 

    $\tau_{g'} = \varphi \Land \tau_g$ by construction and $g'$ is part of the
    evaluation graph. Since $\tilde{s} \models \tau_g$ and $\tilde{s}|_\PV =
    s'$, it follows $\tilde{s} \models \varphi \Land \tau_g$. 

    We conclude that the constructed scheduler $\scheduler'$ is a valid
    Markovian scheduler for $\Prog'$.

    \fpath_\Prog$ of length $n \leq \N$ with $\prSs(f_n) > 0$, $c_i =

    \fpath_\Prog$ of length $n \leq \N$ with $\prSs(\varff_n) > 0$, $c_i =

    $\varf'_n = \simu(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:

    $\varfpi{n} = \simu(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:

        \item $s_n \models \varphi_n$ where $\varf'_n = \dots{}(\langle \_,

        \item $s_n \models \varphi_n$ where $\varfpi{n} = \dots{}(\langle \_,

    t_\text{in},s_0)$. Set $\varf'_0= c'_0 = \simu(\varf) = (\langle
    \ell_0,\texttt{true}\rangle,s_0,t_\text{in})$. $\langle l_0,

    t_\text{in},s_0)$. Set $\varfpi{0} = c'_0 = \simu(\varf) = (\langle
    \ell_0,\texttt{true}\rangle,s_0,t_\text{in})$. $\langle \ell_0,

    a finite prefix $\varf'_n = \simu(f_n) = c'_0\dots{}c'_{n} \in

    a finite prefix $\varfpi{n} = \simu(f_n) = c'_0\dots{}c'_{n} \in

        \item $\prSs(f_n) = \prSns'(\varf'_n)$, and
        \item $s_n \models \varphi_n$ where $\varf'_n = \dots{}(\langle _,

        \item $\prSs(f_n) = \prSns'(\varfpi{n})$, and
        \item $s_n \models \varphi_n$ where $\varfpi{n} = \dots{}(\langle _,

    finite prefix $\varf'_{n+1} =\simu(f_{n+1})= \simu(f_n)c'_{n+1}$ to 

    finite prefix $\varfpi{{}n+1} =\simu(f_{n+1})= \simu(f_n)c'_{n+1}$ to 

        \tau_{n+1}, \eta_{n+1}, \langle \ell_{n+1}, \varphi_{n+1}\rangle)\\
        &= \unfold(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in \T_\Prog',\\

        \tau_{n+1}, \eta_{n+1}, \langle \ell_{n+1}, \varphi_{n+1}\rangle)\\ &=
        \texttt{eval}_{\Prog,S,T}(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in
        \T_\Prog',\\

    The last step on the finite prefix $\varf'_{n+1}$ has the same probability

    The last step on the finite prefix $\varfpi{n+1}$ has the same probability

        &=  \prSs(\varf'_n) \cdot \prSs(c'_n \rightarrow c'_{n+1}) =
        \prSns(\varf_{n+1})

        &=  \prSs(\varfpi{n}) \cdot \prSs(c'_n \rightarrow c'_{n+1}) =
        \prSns(\varff_{n+1})

    because the Markovian $\scheduler$ can select general transitions $g_1$ and
    $g_2$ at version $\langle \ell, \varphi_1\rangle, \langle \ell,
    \varphi_2\rangle \in \Loc_\Prog'$, whereas the Markovian scheduler would be
    forced to always select the same transition $g \in \GT$ at location $\ell$.
    As we will see, this won't matter when considering the worst-case.

    because the Markovian $\scheduler$ can select general transitions $g_1, g_2
    \in \GTPn$ with $g_1 \neq g_2$ at the version $\langle \ell,
    \varphi_1\rangle$ and $\langle \ell, \varphi_2\rangle \in \Loc_\Prog'$,
    whereas the Markovian scheduler would be forced to always select the same
    transition $g \in \GTP$ at location $\ell$. As demonstrated in Lemma
    \ref{lem:hdsvsmds} this does not matter when considering the worst-case.

    $\varf'_0 = c'_0 = (\ell_0, t_\text{in}, s_0)$ which is by construction the

    $\varfpi{0} = c'_0 = (\ell_0, t_\text{in}, s_0)$ which is by construction the

    0$. By induction hypothesis a finite prefix $\varf'_n  = c'_0\dots{}c'_{n}

    0$. By induction hypothesis a finite prefix $\varfpi{n}  = c'_0\dots{}c'_{n}

    to be the last configuration of $\varf'_{n+1}=\varf'_{n}c'_{n+1}$.

    to be the last configuration of $\varfpi{{}n+1}=\varfpi{{}n}c'_{n+1}$.

    \textbf{Case 1}: $g \neq g_\bot$. Then, the constructed scheduler selects
    $\scheduler'(c'_{n+1}) = (\bar{g},\tilde{s})$ by construction and since the
    guard $\tau_{\bar{g}}$ is less restrictive than the guard $\tau_g$, $\tilde{s}
    \models \tau_{\bar{g}}$ and 
    \begin{equation*}
        \prSs(c_n \rightarrow c_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s})(s_{n+1}(x)) \cdot
        \prod_{u\in\V\backslash\PV} \delta_{\tilde{s}_n(u),s_n(u)} = \prSns(c'_n
        \rightarrow c'_{n+1})
    \end{equation*}

    \todo{continue here}

    \textbf{Case 2}: $g = g_\bot$. In that case the constructed scheduler
    selects $\scheduler'(c'_{n+1}) = (g_bot,s)$ as well. Which is correct
    because every outgoing general transition of $\Prog$ at $\ell$ was unfolded
    or copied and added to the partial evaluation with more restrictive guards.
    Hence, no general transition in $\Prog$
    satisfiable 
    By using the induction hypothesis we get 
    \begin{equation*}
        \prSs(f_nc_{n+1}) = prSns(f'_{n+1}c'_{n+1}) 
    \end{equation*}
    \todo{ Beweis ist noch unsauber}

        Lemma \ref{lem:constrfgeq}. Analogously to Theorem \ref{thm:correctness}
        the following relation holds:

        Lemma \ref{lem:constrfgeq}. Analogously to Theorem
        \ref{thm:correctness}, the following relation holds:

        scheduler doesn't matter in the supremum and we get

        scheduler doesn't matter in the supremum and we get the following
        inequality, concluding our proof.

Overall by Theorem \ref{thm:correctness} and Theorem \ref{thm:thightness} we
get:

Overall by Theorem \ref{thm:correctness} and Theorem \ref{thm:thightness}, we
conclude

\subsection{Graph Operations}

\section{Graph Operations}\label{sec:graph_operations}

\cleardoublepage
% \begin{vplace}
%     \textit{
%     Hanna and Thibaud, I would like to express my deepest gratitude
%     for your continuous encouragement and assistance. Your unwavering belief
%     in my abilities and your willingness to lend a helping hand during challenging
%     times have been instrumental in the successful completion of this thesis. Thank
%     you, from the bottom of my heart. 
%     }
% \end{vplace}

\newcommand{\varff}[0]{\,f}
\newcommand{\varfpi}[1]{\,f\,'\!\!_{#1}}

\newcommand{\PRh}[0]{\texttt{PR}_\text{h}}
\newcommand{\PRhv}[0]{\texttt{PR}_\text{hv}}
\newcommand{\PRc}[0]{\texttt{PR}_\text{c}}
\newcommand{\PRcv}[0]{\texttt{PR}_\text{cv}}
\newcommand{\PRd}[0]{\texttt{PR}_\text{d}}
\newcommand{\back}{\texttt{back}}