\settypeblocksize{700pt}{1.2\lxvchars}{*}

\settypeblocksize{650pt}{1.2\lxvchars}{*}

    \end{proof}
\end{apdxlemma}
\begin{apdxlemma}{\ref{lem:pba}}\label{apdx:lem:pba}
    The property based abstraction is a valid abstraction function. For all
    $\varphi \in \Phi$ and finite set of properties $\Psi \subset \C$, the
    following holds.
    \begin{equation*}
        \llbracket \varphi\rrbracket \subseteq \llbracket\alpha_\Psi\rrbracket
    \end{equation*}
    \begin{proof}
        Let $\varphi \in \Phi$ and $\Psi \subset \C$ be a finite set of
        properties. Let $s \in \llbracket \varphi \rrbracket$ be a satisfying
        assignment of $\varphi$.
        \begin{align*}
            s \in \llbracket \varphi \rrbracket 
            &\Rightarrow s \in \llbracket \psi_i \rrbracket \text{ for all }
            \psi_i \in \Psi
            &\Rightarrow s \in \llbracket \Join_{\psi_i \in \Psi} \llbracket
            \psi_i \rrbracket
            &\Rightarrow s \in \llbracket \alpha_\Psi(\varphi) \rrbracket
        \end{align*}

\Cref{ch:theory}. In \Sref{sec:implementation} the implementation is described
using pseudo-code focusing mostly on the practical aspects of the partial

\Cref{ch:theory}. In \Sref{sec:implementation} we describe an implementation
using pseudo-code and focusing mostly on the practical aspects of the partial

In this section we present a pseudo-code implementation for the $\unfold$
operation, and the partial evaluation of an entire program as described in
\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.

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.

\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
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, \L_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}

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. 

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.

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.

\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}.

    \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}

        \For{$g \in \GTout(l)$} {

        \For{$g \in \GTPout(l)$} {

\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.

\subsection{Selecting Loop Heads}\label{sec:loop_heads}
The abstraction relies on the fact that every loop contains at least one
location marked for abstraction. The loop detection is implemented using the
algorithm described by \citeauthor{johnson1975}\cite{johnson1975}. By default
the first location of the loop is selected, which by design of
\citeauthor{johnson1975}'s algorithm is the smallest location with regard to an
arbitrary order. In our implementation the locations were ordered topologically
from the start of the program.

Optionally, the \gls{fvs} can be computed on the detected loops to minimize the
number of locations marked for abstraction.

    \begin{equation*}\begin{gathered} \unfold(\langle l,\varphi\rangle, t) =

    \begin{equation*}\begin{gathered} \unfold(\langle \ell,\varphi\rangle, t) =

outgoing transitions $t \in \Tout(\ell)$. 

outgoing transitions $t \in \TPout(\ell)$. 

        \Tout(\ell)}

        \TPout(\ell)}

In general, the abstraction can be arbitrarily chosen, as long as the properties
above are satisfied. One common abstraction method is is the so called
property-based abstraction\cite{Domenech19} which selects a subset of properties
from a set finite set of properties, that are all entailed by the original
constraint set.

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. 

\begin{definition}[Property based abstraction]
    Let $\Psi = \{\psi_1, \dots,\psi_n\}\subset \C$ be a finite set of
    properties. Let $\neg \Psi = \{\neg \psi_1, \dots, \neg \psi_n\}$. The
    abstraction space of the property-based abstraction is defined $\A_\Psi =
    2^{\Psi \union \neg \Psi}$ which is also finite. The abstraction function
    $\alpha_\Psi : \Phi \rightarrow \A_\Psi$ is defined as
    \begin{equation*}
        \alpha_\Psi(\varphi) = \set{\psi_i}{ \llbracket\varphi\rrbracket
        \subseteq \llbracket \psi_i \rrbracket, \psi_i \in \A_\Psi}
    \end{equation*}
\end{definition}
\begin{lemma}\label{lem:pba}
    The property based abstraction is a valid abstraction function. For all
    $\varphi \in \Phi$ and finite set of properties $\Psi \subset \C$, the
    following holds.
    \begin{equation*}
        \llbracket \varphi\rrbracket \subseteq \llbracket\alpha_\Psi\rrbracket
    \end{equation*}
    \proof{see Appendix on \pref{apdx:lem:pba}}
\end{lemma}

    \text{, and } t \in \Tout(\ell)}

    \text{, and } t \in \TPout(\ell)}

    G_\alpha^* = \evaluate_{\Prog,\alpha}^*(G_0) = \lim_{n\rightarrow\infty}\evaluate_\Prog^n(G_0)

    G_\alpha^* = \evaluate_{\Prog,\alpha}^*(G_0) =
    \lim_{n\rightarrow\infty}\evaluate_{\Prog,\alpha}^n(G_0)

        \_\rangle$ for every outgoing transitions $t \in \Tout(\ell)$ only. 
        Since $\Tout(\ell) \subseteq \T_\Prog$ is finite, only finitely many

        \_\rangle$ for every outgoing transitions $t \in \TPout(\ell)$ only. 
        Since $\TPout(\ell) \subseteq \T_\Prog$ is finite, only finitely many

\begin{example}

\begin{example}\label{ex:global_abstr}

    The abstraction function $alpha$ uses the abstraction space $\A$. The

    The abstraction function $\alpha$ uses the abstraction space $\A$. The

        \eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3\}\rangle) \\

        \eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle) \\

        \eta_{1b},\langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\

        \eta_{1b},\langle \ell_1, \{\psi_1\psi_2,\psi_4\}\rangle) \\

        t_{1a,2} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3\}\rangle) \\
        t_{1b,2} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1b}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{2,1} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 1, \tau_2 \Land
        \psi_1 \Land \psi_3, \eta_2,\langle \ell_2,
        \{\psi_1,\psi_3,\psi_5\}\rangle)\\
        t_{1a,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 0.5, \tau_1 \Land
        \psi_2 \Land \psi_4, \eta_{1a}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{1b,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1b}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{2,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 1, \tau_2 \Land
        \psi_1 \Land \psi_3, \eta_2, \langle \ell_2, \{\psi_2,\psi_4,\psi_5\}\rangle) \\
        t_{3,1} &= (\langle \ell_2, \{\psi_5\}\rangle, 1, \tau_3 \Land
        \psi_5, \eta_{3}, \langle \ell_2, \{\psi_2,\psi_4,\psi_5\}\rangle) \\
        G_2 &= G_1 + \{t_{1a,2}, t_{1b,2},t_{2,2},t_{1a,3},

        t_{1a,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
        \tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1a}, \langle
        \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle) \\
        t_{1b,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
        \tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1b}, \langle
        \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
        t_{2,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 1, \tau_2
        \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_2,\langle \ell_2,
        \{\psi_1,\psi_3,\psi_4,\psi_5\}\rangle)\\
        t_{1a,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 0.5,
        \tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1a}, \langle
        \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
        t_{1b,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 0.5,
        \tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1b}, \langle
        \ell_1, \{\psi_1,\psi_2\}\rangle) \\
        t_{2,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 1, \tau_2
        \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_2, \langle \ell_2,
        \{\psi_1,\psi_2,\psi_4,\psi_5\}\rangle) \\
        t_{3,1} &= (\langle \ell_2, \{\psi_5\}\rangle, 1, \tau_3 \Land \psi_5,
        \eta_{3}, \langle \ell_1, \{\psi_6\}\rangle) \\
        G_3 &= G_2 + \{t_{1a,2}, t_{1b,2},t_{2,2},t_{1a,3},

\end{example}
\subsection{Dynamic abstraction}
Example \ref{ex:global_abstr} illustrates that a program get's large very
quickly and that using the same abstraction function at every location captures
unnecessary properties that are not really important for the flow of a program.
We introduce a \emph{localized} abstraction function that can take the evaluation
history and the location at which the constraint is abstracted into account. 
\begin{definition}[Localized abstraction]
    A \emph{localized} abstraction is a function $S : \vers_\Prog
    \rightarrow \vers_\Prog$ is a function that \emph{can} abstract the
    constraint of a version, but is not required to do so. For any version
    $\langle \ell,\varphi\rangle \in \vers_\Prog$ the abstraction is required to
    be of the form $S (\langle \ell, \varphi' \rangle)$ with
    $\llbracket\varphi\rrbracket \subseteq \llbracket \varphi'\rrbracket$
\end{definition}
\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.}
The unfold operation is adapted to accommodate the dynamic abstraction function.
\begin{equation*}
    \begin{gathered}
        \unfold_{S}(\langle l,\varphi\rangle, t) = (\langle \ell,
        \varphi\rangle, p, \tau\Land\varphi, \eta,S(\langle
        \ell',\varphi'\rangle) \\ \text{for } t = (\ell, p, \tau, \eta,
        \ell') \in \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau,
        \eta) \\
    \end{gathered}
\end{equation*}
\begin{equation*}
    \evaluate_{\Prog,S}(G) = G + \set{ \unfold_{S}(\langle \ell, \varphi
    \rangle, t)}{ \langle \ell, \varphi\rangle \in E(G) \text{, and } t \in
    \TPout(\ell)}
\end{equation*}
\begin{equation*}
    G_{S}^* = \evaluate_{\Prog,S}^*(G_0) =
    \lim_{n\rightarrow\infty}\evaluate_{\Prog,S}^n(G_0)
\end{equation*}
The localized abstraction function allows us to select different abstraction
functions for every location. When using property-based abstraction, we can
select different properties for every location, or not abstract at all. 
\begin{definition}[Localized property-based
    abstraction]\label{def:localized_pba}
    Let $\Psi_{\ell_0},\dots,\Psi_{ell_n} \in (2^\C \union \{\bot\})$ be
    properties for the locations $\ell_0,\dots,\ell_n \in \Loc_\Prog$. $\bot$
    indicates that the location shall not be abstracted at all. We define the
    localized property-based abstraction function
    $S_{\Psi_{\ell_0},\dots,\Psi_{\ell_n}} : \vers_\Prog \rightarrow \C$ with
    \begin{equation*}
        S_{\Psi_{\ell_0},\dots,\Psi_{\ell_n}}(\langle\ell,\varphi\rangle) =
        \begin{cases}
            \alpha_{\Psi_\ell}(\varphi) & \text{if } \Psi_\ell \neq \bot \\
            \varphi & \text{otherwise}
        \end{cases}
    \end{equation*}
\end{definition}
\begin{example}
    Lets return to our example program $\Prog_3$. Location $\ell_0$ and $\ell_2$
    are good candidates to not abstract at all, since they are a linear part of
    the program and no branching will occur there. Besides, we select the same
    properties $\Psi_{\ell_1} = \psi_1,\dots,\psi_6$ as in Example
    \ref{ex:global_abstr}.
    The localized property-based abstraction function
    $S_{\bot,\Psi_{\ell_1},\bot}$ is used in every evaluation step.
    The evaluation starts again with the graph containing only the version
    $\langle\ell_0,\texttt{true}\rangle$. We will skip the details of every
    evaluation step, and just show the final evaluation graph. It looks very
    similar to before, but we saved some entailment checks on location $\ell_2$,
    in return the versions at $\ell_2$ are not collapsed anymore.
    One can clearly see the disadvantage of abstracting fewer locations. In
    practice the abstraction is expensive and abstracting fewer locations, can
    speed up the partial evaluation. The real strength of localized abstraction
    will be seen when only evaluating a component of $\Prog_3$.

The property based abstraction crafted in Example \ref{ex:localized_abstr} was
carefully crafted to guarantee a finite abstraction graph. In fact we will see
that the localized abstraction function must abstract on at least one location
per loop in the original program. This is formalized by the following lemma.
\begin{lemma}
    Let $S_\alpha$ be a dynamic abstraction function. The partial evaluation
    graph $G_{S_\alpha}^*$ is finite if every loop $L$ in $\Prog$ contains a
    location $\ell \in L$ such that
    $\set{S_\alpha(\langle\ell,\varphi\rangle)}{\varphi \in \Phi}$ is finite.
    \begin{proof}
        \todo{Proof}
    \end{proof}
\end{lemma}
Clearly, a global abstraction function is a special case of a dynamic
abstraction function, where every location is abstracted with the same
abstraction function. How to select properties for the localized property-based
abstraction is discussed in \Cref{ch:implementation}.
Next, we will adapt the evaluation a final time. Instead of evaluating the
entire program, the evaluation will unfold only transitions in a given component
$T$. The component is not required to be connected. How to select the component
for best results ins discussed in \Cref{ch:implementation}.
\todo{continue here}

                &g'^* \in \GTout(\langle \ell,\varphi\rangle) \text{ and }

                &g'^* \in \GTPout(\langle \ell,\varphi\rangle) \text{ and }

    \GTout(\ell) \times \Sigma$ with $\tilde{s}|_\PV = s'$ and $\tilde{s}
    \models \tau_g$ exist, then so can't any $(g', \tilde{s'}) \in \GTout(\ell')
    \times \Sigma$, because all general transitions in $\GTout(\ell')$ have more

    \GTPnout(\ell) \times \Sigma$ with $\tilde{s}|_\PV = s'$ and $\tilde{s}
    \models \tau_g$ exist, then so can't any $(g', \tilde{s'}) \in \GTPout(\ell')
    \times \Sigma$, because all general transitions in $\GTPout(\ell')$ have more

\begin{lemma}[Proposition 7.1.1 in
    \cite{puterman1994markov}]\label{lem:hdsvsmds}
    For a random variable $X$ describing the total reward of a Markovian
    decision process, and if the expected reward $\ESs(X)$ is finite for all
    schedulers $\scheduler \in \HDS$, and initial states $s_0$ the following
    holds:
    \begin{equation*}
        \sup_{\scheduler \in \HDS}{\ESs(X)} = \sup_{\scheduler \in
        \MDS}{\ESs(X)} 
    \end{equation*}
\end{lemma}

\begin{lemma}\label{lem:hdsvsmds}
    For a \gls{pip} $\Prog$ and an initial state $s_0\in\Sigma$ the following
    holds
    \begin{align*}
        \sup_{\scheduler\in\HDS}\ESs(\Rt_\Prog) =
        \sup_{\scheduler\in\MDS}\ESs(\Rt_\Prog)
    \end{align*}
    That means, that it doesn't matter if we use Markovian or history dependent
    scheduler when considering the worst-case expected runtime complexity.
    \begin{proof}
        We define $\nu^\scheduler$ to be the expected runtime for any scheduler
        $\scheduler$ -- Markovian or history dependent -- on a program $\Prog$
        with an initial state $s_0\in\Sigma$.
        \begin{equation*}
            \nu^\scheduler = \ESs(\Rt_\Prog) = \lim_{n \rightarrow \infty}
            \sum_{\substack{|\varf| = n \\ \varf \in
            \fpath}}\Rt_\Prog(\varf)\cdot\prSs(\varf)
        \end{equation*}
        Let $\scheduler \in HDS$ be a \emph{history dependent} scheduler with an
        expected reward $\nu^\scheduler$. 
        We argue that $\sup_{\scheduler' \in \MDS} \nu^{\scheduler'} \geq
        \nu^\scheduler$.
        Let $N \in \N$ and $\fpath_N = \set{f \in \fpath_\Prog}{ |\varf| = N }$
        be the set of finite prefixes of length $N$. This set can contain
        infinitely many prefixes, since there can be infinitely many
        assignments. We approach the set $\fpath_N$ with a series of sets $F_1,
        F_2, \dots \subseteq\fpath$ and 
        \begin{equation*}
            \lim_{i \rightarrow \infty} \prSs(F_i) = \lim_{i \rightarrow \infty}
        \sum_{\varf \in F_i} \prSs(\varf) = 1.
        \end{equation*}

        Next, we define a set of Markovian schedulers that are restricted to
        select general transitions and assignments (actions) only for prefixes
        in $F_i$ which we call $\MDS_{F_i}$. As $F_i$ is finite, a Markovian
        scheduler $\scheduler' \in \MDS_{F_i}$ has only finitely many possible
        actions to select from.
        By Lemma 7.1.9 in \cite{puterman1994markov} an \emph{optimal} scheduler
        in $\HDS_{F_i}$ exists. Let $\nu_i$ be the reward of this optimal
        scheduler.
        With $i$ approaching infinity the optimal scheduler must still always be
        as good or better than the history dependent scheduler $\scheduler$. We
        get the following:
        \begin{equation*}
            \lim_{i\rightarrow\infty}\nu_i \geq \sum_{\varf\in\fpath_N}
            \Rt(\varf) \cdot \prSs(\varf)
        \end{equation*}
        Finally, we let $N$ grow to infinity. Where $\nu_{i,N}$ is now the
        expected reward of the optimal Markovian scheduler as described above.
        \begin{equation*}
            \sup_{\scheduler' \in \MDS_\Prog} \nu^{\scheduler'}\geq
            \lim_{N\rightarrow\infty}\lim_{i\rightarrow\infty}\nu_{i,N} \geq
            \lim_{N\rightarrow\infty}\sum_{\varf \in
            \fpath_N}\Rt_\Prog(\varf)\cdot\prSs(\varf) = \nu^\scheduler
        \end{equation*}
        Since the above holds for any history scheduler, it also holds for the
        supremum and we get 
        \begin{equation*}
            \sup_{\scheduler \in \MDS_\Prog} \geq \sup_{\scheduler \in \HDS_\Prog}
        \end{equation*}
        The inverse holds because every Markovian scheduler can be used as a
        history dependent scheduler. 
        \begin{equation*}
            \sup_{\scheduler \in \MDS_\Prog} \leq \sup_{\scheduler \in
        \HDS_\Prog}
        \end{equation*}
    \end{proof}
\end{lemma}

% visits to a transition in the program over all admissible runs, whereas a size
% bound describes the highest value of a program variable observed at a
% transition over all admissible runs. Because the values observed in a run are
% highly dependent on the decisions made by the scheduler $\scheduler$, the bounds 
% we take the supremum over all $\scheduler$. One can also picture the scheduler 
% as an adversary that always takes the worst decision possible for runtime and
% size-bounds.

    % Analogously, $\RB \in \B$ is a cost bound for $s_0$ if 
    % \begin{equation}
    %     \RB \geq \sup \Cost(\Prog) = \sup \ESs(\Rt(\Prog))
    % \end{equation}

    \ESs(\Rt) = \Rt(c_0c_1\dots)

    \ESs(\Rt_\Prog) = \Rt(c_0c_1\dots)

The operations $\Tin : \Loc \rightarrow 2^\T$, $\Tout : \Loc \rightarrow 2^\T$,
$\GTin : \Loc \rightarrow 2^\GT$, and $\GTout: \Loc \rightarrow 2^\GT$ return
the set of (general) transitions starting or ending in the given location. A
\gls{pip} $\Prog$ describes a graph $G_\Prog$ with vertices $\Loc_\Prog$ and
edges $\T_\Prog$. Let $\G$ be the set of graphs over vertices $\Loc$ and
transitions $\T$. Adding a transition and possibly new vertices(locations)
therein to a graph is denoted by the plus operator $+: \G \times \T \rightarrow
\G$. Removing a transitions from a graph, while preserving the vertices therein,
is denoted by the minus operator $- : \G \times \T \rightarrow \G$.
\begin{definition}[\Acrfull{scc}]
    A set of transitions $\S \subseteq \T_\Prog$ is called a \emph{component} of
    $\Prog$ with locations $V(\S)= \set{\ell, \ell'}{(\ell, \_, \_, \_,\ell')
    \in \S}$. A component $\S \subseteq \T_\Prog$ is \emph{strongly connected}
    when for every two locations $\ell, \ell' \in V(\S)$ there exists a path
    between the two using only the transitions from $\S$.
\end{definition}
% -----
% In probabilistic programs not only the worst case is of interest, but also the
% probable case. For example a program might run indefinitely in the worst case
% but the worst-case has a probability approaching zero. The expected bounds are
% defined using the expected value of random variables in the probability space
% $(\runs, \F, \PrSs)$ defined in \Sref{ssec:probabilityspace}. Moreover, recall
% definition \ref{def:expected_value}.
% \begin{definition}[Expected Runtime Complexity, \acrshort{past}
%     \cite{meyer2021tacas}\label{def:past}]
%     For $g \in \GT$ its runtime is the random variable $\Rt(g)$ where $R: \GT
%     \rightarrow \runs \rightarrow \overline{\N}$ with 
%     \begin{equation}
%         \Rt(g)((\_,t_0,\_)(\_,t_i,\_)\dots) = |\set{i}{t_i \in g}|. 
%     \end{equation}
%     For a scheduler $\scheduler$ and starting state $s_0\in\Sigma$, the expected
%     runtime complexity of $g\in\GT$ is $\E_{\scheduler,s_0}(\Rt(g))$ and the
%     expected runtime complexity of $\Prog$ is $\sum_{g\in\GT}\E_{\scheduler,
%     s_0}(\Rt(g)))$.
%     If $\Prog$'s expected runtime complexity is finite for every scheduler
%     $\scheduler$ and every initial state $s_0$, then $\Prog$ is called
%     \acrfull{past}
% \end{definition}
% The expected size bound is defined similarly 
% \begin{definition}[Expected Size
%     Complexity\cite{meyer2021tacas}\label{def:expectedcomplexity}]
%     The set of general result variables is $\GRV = \set{(g,l,x)}{g\in\GT,
%     x\in\PV, (\_,\_,\_,\_,l) \in g}$. The size of $\alpha = (g,l,x) \in \GRV$ is
%     the random variable $\S(\alpha)$ where $\S : \GRV \rightarrow (\runs
%     \rightarrow \overline{N})$ with
%     \begin{equation}
%         \S(g,l,x)((l_0,t_0,s_0)(l_1,t_1,s_1)\dots) = \sup \set{|s_i(x)|}{l_i =
%         l, t_i \in g}.
%     \end{equation}
%     For a scheduler $\scheduler$ and starting state $s_0$, the expected size
%     complexity of $\alpha \in \GRV$ is $\E_{\scheduler,s_0}(\S(\alpha))$.
% \end{definition}
% \begin{definition}[Expected Runtime and Size
%     Bounds\cite{meyer2021tacas}\label{def:expectedbounds}]\phantom{ }
%     \begin{itemize}
%         \item $\RBe : \GT \rightarrow \B$ is an expected runtime bound if for
%             all $g\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
%             have $|s_0|(\RBe(g)) \geq \ESs(\Rt(g))$.
%         \item $\SBe : \GRV \rightarrow \B$ is an expected size bound if for
%             all $\alpha\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
%             have $|s_0|(\SBe(g)) \geq \ESs(\S(g))$.
%     \end{itemize}
% \end{definition}
% \begin{example}
% \end{example}
% \begin{definition}[Total worst-case runtime complexity \label{def:wc_rt_complexity}]
%     For a \gls{pip} $\Prog$, the overall worst-case runtime complexity $\Rt_\Prog :
%     \runs \rightarrow \overline{\N}$ is defined as the \textit{random variable}
%     \begin{equation}
%         \Rt_\Prog(\vartheta)= \sum_{g\in\GT}\Rt(g)(\vartheta)
%     \end{equation}
% \end{definition}
% The following holds for any $\vartheta = (\_,t_0,\_)(\_,t_1,\_)\dots \in \runs$:
% \begin{align}
%     \Rt_P(\vartheta) &= \sum_{g\in\GT}\Rt(g)(\vartheta) & \text{by Definition
%     \ref{def:wc_rt_complexity}} \\
%     &= \sum_{g\in\GT} |\set{i}{t_i \in g}| & \text{by Definition \ref{def:past}}
%     \\
%     &= | \set{i}{t_i \in g, g\in\GT} & \text{for all } g \neq g', g\intersect{}g' = \emptyset 
% \end{align}
% \begin{rem}
%     $t_\bot \in g_\bot \not\in \GT$, hence terminating runs have a finite
%     overall runtime complexity.
% \end{rem}
% The worst-case total runtime complexity, for an initial state $s_0\in\Sigma$ and
% all scheduler $\scheduler$, is the supremum over all admissible runs:
% \begin{align}
%     \sup \set{\Rt_\Prog (\vartheta)}{\vartheta \in \runs, \PrSs(\vartheta) > 0}
% \end{align}
% The expected total runtime complexity is the expected value of the random
% variable $\ESs(\Rt_\Prog)$
% \subsection{Costs}
% It is useful to add the notion of costs to a transition to reflect variable
% complexity of transitions. The accumulative costs of a run are the sum of costs
% for each transition taken. Accumulative costs can simulated by an additional
% program variable $\mathbf{c} \in \PV$ that is updated only by polynomials of the
% form $\eta(\mathbf{c}) = \mathbf{c} + c_t$, where $c_t \in
% \Z$ is the cost associated with the transition $t\in\T$.
% For a given size bound $\SB$ for the \gls{pip} $\Prog$ and a starting assignment
% $s_0$, the cost bound is defined as $|s_0|(\SB(t_\bot,\mathbf{c}))$, and given
% an expected size bound $\SBe$, the expected cost bound is defined as
% $|s_0|\SBe(t_\bot, mathbf{c})$.
\begin{comment}
\subsection{Graph operations}
A \gls{pip} contains a directed graph with vertices $\L$ and edges $\T$. We will
define some graph operations that will become useful during the thesis. The set
of directed graphs over locations $\L$ and transitions $\T$ is denoted by $\G$. 
% The graph $G(P)$ denotes the graph contained within a \gls{pip} $P$ and is
% defined as $G(P) = (L, \T)$. The following graph operations will be defined on
% graphs only, but work equally well for \glspl{pip} by using the contained graph
% operation first. However, the result might not be a valid integer program, per-se.
A set of transitions $T \subseteq \T$ induces a sub-graph $G(T)$ in a program $P$,
with $\G: 2^\T \rightarrow \G$. Similarly a set of locations $L \subseteq \Loc$
induces a sub-graph $G(L)$ in $P$, with $G: 2^\Loc \rightarrow \G$.
\begin{rem}
    The resulting graphs cannot allways be lifted to a valid \gls{pip}, since
    cumulative probability of general transitions are not necessarily preserved.
\end{rem}
\begin{definition}[Transition relation]
    A relation $\rightarrow_P \,\subseteq L \times L$ is defined for the
    \gls{pip} $P$, with $l \rightarrow_P l'$ if and only if there exists a
    general transition $g \in GT$ and a transition $t \in g$ with $t = (l, p,
    \tau, \kappa, l)$. 
\end{definition}
\begin{definition}[Path relation]
    For $n \in \N$ and the \gls{pip} $P$, a relation $\npathto{n}_P\,\subseteq L
    \times L$ is defined with $l \npathto{n}_P l'$ if and only if there exist a
    (finite) sequence of locations $(l_{k_0}, \dots l_{k_n})\in L^n$, with
    $l_{k_i}\rightarrow_P l_{k_{i+1}}$ for $i \in [0, n-1]$, $l_{k_0} = l$, and
    $l_{k_n} = l'$. We say there exists a \textit{path} of length $n$ from $l$
    to $l'$.
    In addition, the relation $l \pathto_P l'$ denotes that there exists a path
    of arbitrary length, $l \npathto{>n}_P l'$ that there exists a path of
    length
    at least $n$. 
\end{definition}
\begin{rem} 
    \begin{itemize}
        \item A path of length 0 and the relation $\npathto{0}$ are perfectly
            legal. With a zero-length path being a sequence of length one
            containing only a single location;
        \item the relation $\rightarrow_P$ is neither \textit{reflexive},
            \textit{transitive} nor \textit{symmetric} in the general case, but
            might be depending on the program.
        \item the relation $\npathto{0}_P$ is always \textit{reflexive},
            \textit{transitive}, and \textit{symmetric};
        \item the relation $\npathto{<n}_P$ is always \textit{reflexive};
        \item the relation $\npathto{>n}_P$ is always \textit{transitive};
            whereas 
        \item the relation $\npathto{>0}_P \, = \,\pathto_P$ is always
            \textit{reflexive} and \textit{transitive}.
    \end{itemize}
    \todo{proof needed?}
\end{rem}
Notation-wise, whenever the program is obvious from the context, the subscript
$P$ can be dropped from the relation. 
\begin{rem}
    The transition and path relation describe the mere existens of transitions
    and not if the transition is at all walkable. 
\end{rem}
\begin{definition}[SCC]
    A set of locations $A \subseteq L$ is \textit{strongly connected} in P when
    for every two locations $l, l' \in A$ there exists a path between the two
    locations $l \pathto_P l'$. And it is a \textit{strongly connected
    component} when the set is maximal. That is, there exists no location $l'' \in
    L\backslash A$ such that $A \union \{l''\}$ is also strongly connected.
\end{definition}
\begin{lemma}\label{lem:scc_expand}
    Let $A \subseteq L$ be strongly connected set of locations in $P$. Given a
    location $l \in L$, and a location $l_A \in A$, if $l \pathto l_A$ and $l_A
    \pathto l$ then $A \union \{l\}$ is also strongly connected in $P$.
    \begin{proof}
        \todo{proof needed?}
    \end{proof}
\end{lemma}
\begin{lemma}
    \label{lem:scc_disjunct}
    Two strongly connected components $A, B \subseteq L$ of $P$ are either equal
    or disjunct.
    \begin{proof}
        Let two strongly connected components $A, B \subseteq L$ be not
        disjunct, and $l_{AB} \in A\intersect B$. 
        Assume there is a location $l_A \in A \backslash B$. Then $l_A \pathto
        l_{AB}$ and for all $l_B \in B$, $l_{AB}\pathto l_B$ due to $A$ and $B$
        being strongly connected. By transitivity, $l_A \pathto l_B$.
        Symmetrically, for any $l_B \in B$, $l_B \pathto l_A$. But then $B
        \union \{l_A\}$ would be strongly connected, contradicting $B$
        maximality. Hence such a location $l_AB$ cannot exist and $A \intersect
        B = \emptyset$.
    \end{proof}
\end{lemma}
\begin{lemma}
    \label{lem:scc_exist}
    For every location $l\in L$, there exists a strongly connected component $A$
    such that $l\in A$.
    \begin{proof}
        Let $l_{k_0}\in L$ be an arbitrary location of a program $P$. The proof
        will be given in an inductive fashin. Starting with a set $A_0 =
        \{l_{k_0}\}$, by reflexivity $l \pathto l$. Hence, $A_0$ is strongly
        connected. 
        For $i \in \N$, if $A_i$ is maximal and $A_i$ is the SCC containing $l$.
        If not there exists another $l_{k_{i+1}} \notin A_i$, such that $A_{i+1}
        := A_i \union \{l_{k_{i+1}}\}$ is strongly connected. 
        Repeat the argument above until a maximal set is found. The induction
        ends, because the set of locations is finite.
    \end{proof}
\end{lemma}
\begin{definition}[Loop]
    A loop in a \gls{pip} $P$ is a sequence of pairwise different locations
    $(l_{k_0} \dots l_{k_n})$ with $l_{k_i} \rightarrow l_{k_{i+1}}$ for $i \in
    [0, n-1]$ and $l_{k_n} \rightarrow l_{k_0}$.
\end{definition}
\todo{examples: 1. loops, 2. two loopheads}
\begin{lemma}\label{lem:loop_path}
    Let $(l_{k_0} \dots l_{k_n})$ be a loop in the program $P$. For any two 
    locations in the loop $l_{k_i}, l_{k_j}$, $l_{k_i} \pathto l_{k_j}$ and
    $l_{k_j} \pathto l_{k_i}$.
    \todo{proof needed?}
\end{lemma}

\begin{lemma}
    Let $(l_{k_0} \dots l_{k_n})$ be a loop in the program $P$. Then all
    locations $l_{k_0} \dots l_{k_n}$ are contained in the same SCC.
    \begin{proof}
        Follows immediately from Lemma \ref{lem:scc_expand} and Lemma
        \ref{lem:loop_path} \todo{fix ref}
    \end{proof}
\end{lemma}

A \gls{pip} $\Prog$ induces a graph which we call $G_\Prog$ with vertices
$V(G_\Prog) = \Loc_\Prog$ and edges $E(G_\Prog) = \T_\Prog$. We define some
graph operations that will become useful during the thesis. Let $\G$ be the set
of graphs over vertices $\Loc$ and transitions $\T$.

Adding a transition and possibly new vertices(locations) therein to a graph is
denoted by the plus operator $+: \G \times \T \rightarrow \G$. Removing a
transitions from a graph, while preserving the vertices therein, is denoted by
the minus operator $- : \G \times \T \rightarrow \G$.

% Various languages exist to represent integer programs in a computer readable
% form; namely Koat2\cite{}, IntC, Some weird XML Onthology
% \cite{https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd}

For a \gls{pip} $\Prog$ the incoming transitions of a location are described by
the operation $\TPin : \Loc \rightarrow 2^\T_{\Prog}$, whereas the outgoing
transitions at a location are described by a function $\TPout : \Loc \rightarrow
2^{\TP}$. We define similar functions outgoing general transitions $\GTPout:
\Loc \rightarrow 2^\GT$. 
\begin{align*} 
    \TPout(\ell) &= \set{t}{t = (\ell, \_, \_, \_, \_) \in \T}\\ 
    \TPin(\ell) &= \set{t}{t = (\_, \_, \_, \_, \ell) \in \T}\\
    \GTPout(\ell) &= \set{g}{g \in \GTP\text{ and } \ell_g = \ell}
\end{align*}

% - CINT
% - Koat Format 
% For probabilistic: PIP 

A component $T \subset \T_\Prog$ is a subset of transitions of $\Prog$. All
locations in this component are denoted by a function $\Loc : 2^{\TP}
\rightarrow 2^{\Loc_\Prog}$ with 
\begin{equation*}
    \Loc(T) = \set{\ell, \ell'}{(\ell, \_, \_, \_, \ell') \in T}
\end{equation*}

% During this thesis we will transform programs. The goal is to find equivalent
% programs that are easier to analyze by Koat2. But what does equivalence mean?
% On non probabilistic programs one would expect, that while beeing structurally
% different, the outcome of the new program is the same as the old one.
% In addition the new program should take the same time as the old one. Since
% costs are represented as a variable, this is part of the outcome. But the
% runtime of a program is calculated by ranking-functions and they count the
% number of visits to a location. In order for the runtime to be the same, bounds
% shall remain the same. \todo{doesn't realy make sence!}

For a component $T \subset \T_\Prog$ the entry transitions are described by a
function $\TPin : 2^{\TP} \rightarrow 2^{\TP}$ and the exit transitions are
described by a function $\TPout : 2^{\TP} \rightarrow 2^{\TP}$ with 

% In probabilistic programs, a the run is non-deterministic and hence calculating
% the runtime is impossible. Instead we have expected runtime-bounds. So the new
% program should have the same expected runtime-bounds and the same expected
% costs, as the old program. Let's give a more formal definition. 

\begin{align*}
    \TPout(T) &= \Union_{\ell \in \Loc(T)} \TPin(\ell) \backslash T \\
    \TPin(T) &= \Union_{\ell \in \Loc(T)} \TPout(\ell) \backslash T \\
\end{align*}

% \section{Linear Ranking Funktions}
% Ranking functions are a widely use tool to prove termination and runtime-bounds of integer transition systems. The simplest variant of ranking functions are \gls{lrf}
% We seek a function $f(x_1,\dots,x_n) = a_1x_1 + \cdots + a_nx_n + a_0$ with the rationals as a co-domain, such that 
% \begin{enumerate} 
%     \item $f(\bar{x}) \leq 0$ for any valuation $\bar{x}$ that satisfies the loop constraints;
%     \item $f(\bar{x}) - f(\bar{x}') \geq 1$ for any transition leadtion from $\bar{x}$ to $\bar{x}'$
% \end{enumerate}
% \cite{benamram2017}\todo{plagiat}
% Intuition: The ranking function decreases for every walkable transition. If such a ranking function exists, the loop terminates. \todo{not sure about this, guess}

For a \gls{pip} $\Prog$ A loop (or cycle) is a finite sequence of locations $L =
\ell_0\dots\ell_n \in \Loc^n$ of length $n \in \N$ for which there exist
transitions $t_i = (\ell_i, \_, \_, \_, \ell_{i+1}) \in \T_\Prog$ for all $0
\leq i < n$ and a closing transition $t_n = (\ell_n, \_, \_, \_, \ell_0) \in
\T_\Prog$. Additionally we require the locations of a loop to be pairwise
different. The first location of the loop $\ell_0$ is called the \emph{loop
head}. A loop $L =\ell_0\dots\ell_n \in \Loc^n \in \Loc_\Prog^n$ induces a set
of components $T_L$ which we call the \emph{transition loops} of $L$ with
\begin{equation*} 
    T_L = \set{\{t_0,\dots,t_n\}}{t_i = (\ell_i, \_, \_, \_, \ell_{i+1}) \in \T_\Prog \text{ for } 0 \leq i < n \text{ and } t_n =
    (\ell_i, \_, \_, \_, \ell_0) \in \T_\Prog}. 
\end{equation*}

% \section{Lexicographic ranking functions}
% We expand the \gls{lrf} to a tuple of \gls{lrf}. Where whenever lexicograpically higher function decreases lower ones can increase again.

A component $T \subseteq \T_\Prog$ is \emph{strongly connected} when for every
two locations $\ell, \ell' \in V(T)$ there exists a path between the two using
only the transitions from $T$.

% Example for a tuple. 
% $$
% \langle f_1, f_2\rangle \text{s. th.}
% $$
% \section{Multiphase-ranking Functions}
% \section{Goal}
% Transform a program into an equivalent program. \todo{define equivalence of
% programs}
\begin{comment}
- Term Rewrite Systems (TRS)
- Transition Systems
    - A set of States S
    - A start location S_0 \in S
    - A set of transitions T \in S x C x S
- Integer Transition Systems (ITS)
Koat2 can work on integer programs with polynomial integer
arithmetic.\cite{Brockschmidt16} To represent states and invariants in such a
program, one needs polynomial constraints. As an extended concept Koat2 uses
boxes and we will use polyhedra for the partial evaluation. Since those concepts
are closely related we will introduce them together. 
\end{comment}