\usepackage{cite}

}
@Article{johnson1975,
  author   = {Johnson, Donald B.},
  journal  = {SIAM Journal on Computing},
  title    = {Finding All the Elementary Circuits of a Directed Graph},
  year     = {1975},
  number   = {1},
  pages    = {77-84},
  volume   = {4},
  abstract = {An algorithm is presented which finds all the elementary circuits of a directed graph in time bounded by \$O((n + e)(c + 1))\$ and space bounded by \$O(n + e)\$, where there are n vertices, e edges and c elementary circuits in the graph. The algorithm resembles algorithms by Tiernan and Tarjan, but is faster because it considers each edge at most twice between any one circuit and the next in the output sequence.},
  doi      = {10.1137/0204007},
  eprint   = {https://doi.org/10.1137/0204007},
  url      = {https://doi.org/10.1137/0204007},

>>>>>>> 1 [LOQBLRZ6 ]
\section{Abstraction}\label{sec:abstraction}
======= 1 [QIVGMR6I WIP]

Finding loops in a program can be done with the algorithm described by
\citeauthor{johnson1975}\cite{johnson1975}. 
The algorithm is linear in the number of edges in the graph, specifically
$\mathcal{O}(n+e (c+1))$

Detecting all loops(cycles) in a graph is easily done by \gls{dfs} on the graph.
And the problem can instead be formulated as a hitting set problem. 

Detecting all loops(cycles) in a graph can be done easily done with an  
algorithm describe\gls{dfs} on
the graph. And the problem can instead be formulated as a hitting set problem. 

one symbol is replaced by another is denoted with $[\cdot\backslash{}\cdot]$.
For example $(x<y)[x\backslash{}1] = (1 < y)$. For a finite set $A =
{x_1,\dots,x_n}$, the process of $n$ consecutive substitutions
$[x_i\backslash{}y(i)]$ where the replacement expression $y$ varies only in some
index $i$ is denoted using a shortened notation: $[x_i\backslash{}y_i]_{x_i \in
A} = [x_1\backslash{}y(1)] \dots [x_n\backslash{}y(n)]$. For example
$[x_i\backslash{}i]_{x_i\in A} =
[x_0\backslash{}0]\dots[x_n\backslash{}n]\dots$, is the substution where every
variable is replaced by its index in $A = \{x_0, \dots, x_n\}$. The restriction
of a function $f: A \rightarrow B$ to a smaller domain $A' \subset A$ is denoted
by $f|A' : A' \rightarrow B$.

one symbol is replaced by another is denoted with $[\cdot/\cdot]$.
For example $(x<y)[x/1] = (1 < y)$. For a finite set $A =
\{x_1,\dots,x_n\}$, the $n$ consecutive substitutions $[x_i/y(i)]$
where the replacement expression $y$ varies only in some index $i$ is denoted
using a shortened notation: $[x_i/y_i]_{x_i \in A} =
[x_1/y(1)] \dots [x_n/y(n)]$. For example
$[x_i/i]_{x_i\in A} = [x_0/0]\dots[x_n/{}n]$, is
the substution where every variable is replaced by its index in $A = \{x_0,
\dots, x_n\}$. The restriction of a function $f: A \rightarrow B$ to a smaller
domain $A' \subseteq A$ is denoted by $f|A' : A' \rightarrow B$.

This section will define the foundations of various types of constraints that
are special cases of formulas of \gls{fo} logic. In the following
$\V$ denotes a finite set of variables $\V$. The set of quantifier-free formulas
of first-order logic over a variable set $A\subset\V$ is denoted with $\Phi_A$,
or simply $\Phi$, when $A=\V$. For foundations on FO-logic we'll refer to the
literature \cite{barwise1977}.

This section will define constraints that are special cases of formulas of
\gls{fo} logic. In the following $\V$ denotes a finite set of variables $\V$.
The set of quantifier-free formulas of first-order logic over a variable set
$A\subset\V$ is denoted with $\Phi_A$, or simply $\Phi$, when $A=\V$. For
foundations on FO-logic we'll refer to the literature \cite{barwise1977}.

Using the $\models$ relation and $\equiv$ relation from \gls{fo} logic, the
notion of satisfiability is defined.\cite{barwise1977}

% Let $\mathfrak{I} = ()$ be the
% structure of 
% \begin{definition}[Satisfiability\cite{barwise1977}]\label{def:satisfiability}
%     For a domain $A$ and a structure $\mathfrak{A} = (A, +, \cdot, 0, 1, \leq,
%     <, =)$ we say a variable assignment $\beta: \V \rightarrow A$
%     \textit{satisfies} the formula $\phi \in \Phi$ when $\mathfrak{A}, \beta
%     \models \psi$.

\begin{definition}[Satisfiability\cite{barwise1977}]\label{def:satisfiability}
    For a domain $A$ and a structure $\mathfrak{A} = (A, +, \cdot, 0, 1, \leq,
    <, =)$ we say a variable assignment $\beta: \V \rightarrow A$
    \textit{satisfies} the formula $\phi \in \Phi$ when $\mathfrak{A}, \beta
    \models \psi$.
    $\phi $ is \textit{satisfiable} in when an assignment $\beta: \V \rightarrow
    A$ exists such that $\mathfrak{A},\beta\models \phi$. When $\phi$ is
    satisfiable for any assignments, one writes $\mathfrak{A} \models \phi$.
\end{definition}

%     $\phi $ is \textit{satisfiable} in when an assignment $\beta: \V \rightarrow
%     A$ exists such that $\mathfrak{A},\beta\models \phi$. When $\phi$ is
%     satisfiable for any assignments, one writes $\mathfrak{A} \models \phi$.
% \end{definition}

    \rrbracket$ is defined as the set of all satisfying assignments or the
    \textit{solutions} of the formula $\varphi$.

    \rrbracket$ is defined as the set of all satisfying assignments of the
    formula $\varphi$.

        \Lin^{\leq}=\set{a_0 + \sum_{i=1}^{n} a_i v_i \leq 0}{a_i \in \R}.

        \Lin=\set{a_0 + \sum_{i=1}^{n} a_i v_i \leq 0}{a_i \in \R, v_i \in \V}.

    Analogously, the set of \textit{linear strict inequality} constraints is
    defined as the set
    \begin{align*}
        \Lin^{<}=\set{a_0 + \sum_{i=1}^{n} a_i v_i < 0}{a_i \in \R}.
    \end{align*}

    % Analogously, the set of \textit{linear strict inequality} constraints is
    % defined as the set
    % \begin{align*}
    %     \Lin^{<}=\set{a_0 + \sum_{i=1}^{n} a_i v_i < 0}{a_i \in \R}.
    % \end{align*}

    The union of strict and non-strict linear constraints is called
    \textit{mixed linear inequality} constraints denoted as $\Lin = \Lin^{\leq}
    \union \Lin^{<}$.

    % The union of strict and non-strict linear constraints is called
    % \textit{mixed linear inequality} constraints denoted as $\Lin = \Lin^{\leq}
    % \union \Lin^{<}$.

    The set of \textit{non-strict polynomial inequality} constraints is defined

    The set of \textit{non-strict polynomial inequality constraints} is defined

        \C^{\leq} = \set{e \leq 0}{e \in \Z[\V]},

        \C = \set{e \leq 0}{e \in \Z[\V]}.

    whereas the set of \textit{strict polynomial inequality} constraints is
    defined as the set 
    \begin{equation*}
        \C^< = \set{e < 0}{e \in \Z[\V]},
    \end{equation*}
    and the set of \textit{mixed polynomial inequality} constraints is the set
    $\C = \C^{\leq} \union \C^{<}$. 

    % whereas the set of \textit{strict polynomial inequality} constraints is
    % defined as the set 
    % \begin{equation*}
    %     \C^< = \set{e < 0}{e \in \Z[\V]},
    % \end{equation*}
    % and the set of \textit{mixed polynomial inequality} constraints is the set
    % $\C = \C^{\leq} \union \C^{<}$. 

    Strict and non-strict linear constraints are a subset of strict polynomial
    constraints and non-strict polynomial constraints respectively. For the most
    part we will just refer to \enquote{constraints} when the distinction
    between strict and non-strict or linear and polynomial constraints is
    unimportant.  

    Non-strict linear constraints are a subset of non-strict polynomial
    constraints. For the most part we will just refer to \enquote{constraints}
    when the distinction between linear and polynomial constraints is
    unimportant. 

Constraints are a subset of formulas in \gls{fo} logic, thus, their semantics
shall be defined accordingly.

Using the $\models$ relation and $\equiv$ relation from \gls{fo} logic, the
notion of satisfiability is defined.\cite{barwise1977} Constraints are a subset
of formulas in \gls{fo} logic, thus, their semantics shall be defined
accordingly. In this thesis we will only consider integer arithmetic. Let $\Zs
:= (\Z, +, \cdot, 0, 1, \leq, <, =)$ be the structure standard integer
arithmetic. For an assignment $\beta : \V \rightarrow \Z$ and a formula
$\varphi \in Phi$ we write $\beta \models \varphi$ instead of $\Zs, \beta
\models \varphi$.

A set of constraints $C \subseteq \C$ is satisfiable, when their conjunction is
satisfiable and we write $\mathfrak{A}, \beta \models C$ instead of
$\mathfrak{A} , \beta \models \LAnd_{\psi_i \in C} \psi_i$. In addition this
thesis will only consider integer arithmetic. Let $\Zs := (\Z, +, \cdot, 0, 1,
\leq, <, =)$ be the structure standard integer arithmetic. We write $\models
\psi$ and $\beta \models \psi$ instead of $\mathfrak{Z} \models \psi$ and
$\mathfrak{Z}, \beta \models \psi$ respectively.

A finite set of constraints $C \subseteq \C$ is satisfiable, when their
conjunction is satisfiable and we write $\beta \models C$ instead of $\beta
\models \LAnd_{\psi_i \in C} \psi_i$. 

    Two formulas, constraints, or set of constraints are considered
    \textit{equivalent}, denoted as $\varphi_1 \equiv \varphi_2$ when their
    solutions are equal.

    Two formulas, constraints, or set of constraints $\varphi_1$ and $\varphi_2$
    are considered \textit{equivalent}, denoted as $\varphi_1 \equiv \varphi_2$
    when $\llbracket \varphi_1 \rrbracket = \llbracket \varphi_2 \rrbracket$.

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

        $\beta \models \varphi_1 \Land \neg \varphi_2$. 

        an assignment $\beta: \V \rightarrow \Z$ exists such that $\beta \models
        \varphi_1 \Land \neg \varphi_2$. 

quantifier-free polynomial integer arithmetic (\texttt{QF\_PIA}). 

quantifier-free non-linear integer arithmetic (\texttt{QF\_NIA}). 

one would just existentially quantify the variable. However the new \gls{fo}

one would just existentially quantify the variable. However, the new \gls{fo}

$f[x_i\backslash{}s(x_i)]$. \todo{restrict to full assignments?}

$f[x_i/s(x_i)]$. \todo{restrict to full assignments?}

    u(x))|_{\PV'})[x'\backslash{}x]$. For any partial assignment $s' = u(s)|A$

    u(x))|_{\PV'})[x'/x]$. For any partial assignment $s' = u(s)|A$

            u(x))|_{A'})[x'\backslash{}x] \nonumber\\

            u(x))|_{A'})[x'/x] \nonumber\\

            u(x))|_{A'})[x'\backslash{}x][x\backslash{}s'(x)] \nonumber\\

            u(x))|_{A'})[x'/x][x/s'(x)] \nonumber\\

            u(x))|_{A'})[x'\backslash{}s'(x)] \label{eq:chaining_subst}\\

            u(x))|_{A'})[x'/s'(x)] \label{eq:chaining_subst}\\

            u(x)))[x'\backslash{}s'(x)]_{x\in A} \label{eq:dropping_projection}\\

            u(x)))[x'/s'(x)]_{x\in A} \label{eq:dropping_projection}\\

            u(x)))[x'\backslash{}u(s)(x)]_{x\in A}\nonumber\\

            u(x)))[x'/u(s)(x)]_{x\in A}\nonumber\\

            u(x)))[x'\backslash{}u(x)(s)]_{x\in A}\nonumber\\

            u(x)))[x'/u(x)(s)]_{x\in A}\nonumber\\

            (\varphi[x'\backslash{}u(x)(s)]_{x_\in A}) \Land (\LAnd_{x\in A}
            x'[x'\backslash{}u(x)(s)]_{x_\in A} = [x'\backslash{}u(x)(s)]_{x\in

            (\varphi[x'/u(x)(s)]_{x_\in A}) \Land (\LAnd_{x\in A}
            x'[x'/u(x)(s)]_{x_\in A} = [x'/u(x)(s)]_{x\in

            \varphi \Land \LAnd_{x\in A} x'[x'\backslash{}u(x)(s)] =

            \varphi \Land \LAnd_{x\in A} x'[x'/u(x)(s)] =

            \varphi[x\backslash{}s(x)]\Land \LAnd_{x\in A}
            u(x)[x\backslash{}s(x)] =

            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)] =

            \varphi[x\backslash{}s(x)]\Land \LAnd_{x\in A}
            u(x)[x\backslash{}s(x)][x\backslash{}s(x)] =
            u(x)[x\backslash{}s(x)]\label{eq:adding_model}\\

            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)][x/s(x)] =
            u(x)[x/s(x)]\label{eq:adding_model}\\

            (\varphi\Land \LAnd_{x\in A} u(x) = u(x))[x\backslash{}s(x)]

            (\varphi\Land \LAnd_{x\in A} u(x) = u(x))[x/s(x)]

            \varphi[x\backslash{}s(x)]\nonumber\\

            \varphi[x/s(x)]\nonumber\\

        necessary true. Applying the substitution $[x\backslash{}s(x)]$ a second

        necessary true. Applying the substitution $[x/s(x)]$ a second

        \tilde{f} = f[D_i\backslash{}d_i] \text{ and }

        \tilde{f} = f[D_i/d_i] \text{ and }

then after a small excursion to markov decision processes, the semantics are are

then after a small excursion to Markov decision processes, the semantics are are

\subsection{\gls{pip} as a Markov decision process}

\subsection{Probabilistic Integer Program as a Markov decision process}

    The set of all markovian schedulers for a program $\Prog$ is denoted by
    $\MDS^\Prog$, where \enquote{MD} stands for \enquote{markovian

    The set of all Markovian schedulers for a program $\Prog$ is denoted by
    $\MDS^\Prog$, where \enquote{MD} stands for \enquote{Markovian

computer science known to be undecidable. The so-called Halting Problem
is strongly related to the search for upper and lower runtime bounds, or the
runtime complexity of a program, is equally undecidable. Nevertheless, the
answers to those questions are very important in practice. For example a
compiler might want to warn the programmer about faulty code sections that were
not marked explicitly to run indefinitely, or the developer could be forced to
prove the efficiency of his program in critical scenarios. In an ever more
complex world, with ever more complex algorithms, the need for automatic tools
arised. Even though the question for runtime-complexity can not be answered in a
general case, many tools were developed to automatically analyze the complexity
of various programming paradigms as tight and fast as possible.

computer science known to be undecidable. The so-called Halting Problem is
strongly related to the search for upper and lower runtime complexity bounds, is
equally undecidable. Nevertheless, the answers to those questions are very
important in practice. For example a compiler might want to warn the programmer
about faulty code sections that were not marked explicitly to run indefinitely,
or the developer could be forced to prove the efficiency of his program in
critical scenarios. In an ever more complex world, with ever more complex
algorithms, the need for automatic tools arised. Even though the question for
runtime-complexity can not be answered in a general case, many tools were
developed to automatically analyze the complexity of various programming
paradigms as tight and fast as possible.

        \input{figures/ch1_classic}
        \caption{Classic integer program $\Prog_1$\label{fig:classic}}

        \input{figures/ch1_classic_c}
        \caption{Classic Integer Program $\Prog_1$\label{fig:classic_c}}

    \begin{subcaptionblock}[t]{0.5\textwidth}

    \begin{subcaptionblock}[t]{0.4\textwidth}

        \input{figures/ch1_classic_pe}
        \caption{(UNFINISHED) Partial evaluation of
        $\Prog_1$\label{fig:classic_pe}}

        \input{figures/ch1_classic_pe_c}
        \caption{Partial evaluation of $\Prog_1$\label{fig:classic_pe_c}}

    \caption{Program with hard to find runtime-complexity bounds using only
    \gls{mprf}.\cite{giesl2022arxiv}}

    \caption{Partial evaluation of a classic integer program with hard to find
    runtime-complexity bounds using only \gls{mprf}.\cite{giesl2022arxiv}}

% \begin{figure}
%     \centering
%     \begin{subcaptionblock}[t]{0.4\textwidth}
%         \centering
%         \input{figures/ch1_classic}
%         \caption{Classic integer program $\Prog_1$\label{fig:classic}}
%     \end{subcaptionblock}
%     \begin{subcaptionblock}[t]{0.5\textwidth}
%         \centering
%         \input{figures/ch1_classic_pe}
%         \caption{(UNFINISHED) Partial evaluation of
%         $\Prog_1$\label{fig:classic_pe}}
%     \end{subcaptionblock}
%     \caption{Program with hard to find runtime-complexity bounds using only
%     \gls{mprf}.\cite{giesl2022arxiv}}
% \end{figure}

program variables $x, y$ and two temporary variables $u,w$ where $u$ is used to
non-deterministically sample $x$ in the first transition $t_0$ and $w$ is used
to branch non-deterministically between $t_1$ and $t_2$. The program clearly
terminates, since both loops $t_1$ and $t_2,t_3$ decrement either $x$ or $y$ in
every iteration. However, the classical analysis using only \gls{mprf} fails to
find a finite runtime-complexity bounds for this program.\cite{giesl2022arxiv}.
With the help of \gls{cfr} on sub-\gls{scc} level, the program (see
\fref{fig:classic_pe}) can be transformed into an equivalent program where the
analysis with \gls{mprf} succeeds at finding a finite runtime-complexity bound.

program variables $x, y$ and one temporary variables $u$ which is used to
non-deterministically sample $x$ in the first transition $t_0$. The program
clearly terminates. The first loop increments $x$ up to 3 if $x$ is
positive to begin with. The second loop decrements $y$ while $y$ is positive. 
However, the classical analysis using only \gls{mprf} fails to find a finite
runtime-complexity bounds for this program\cite{giesl2022arxiv}. With the help
of \gls{cfr} on sub-\gls{scc} level, the program (see \fref{fig:classic_pe}) can
be transformed into an equivalent program where the analysis with \gls{mprf}
succeeds at finding a finite runtime-complexity bound.

        \input{figures/ch1_prob}
        \caption{Probabilistic integer program $\Prog_2$\label{fig:prob}}

        \input{figures/ch1_prob_c}
        \caption{Probabilistic integer program $\Prog_2$\label{fig:prob_c}}

    \begin{subcaptionblock}[t]{0.5\textwidth}

    \begin{subcaptionblock}[t]{0.4\textwidth}

        \input{figures/ch1_prob_pe}
        \caption{Partial evaluation of $\Prog_2$\label{fig:prob_pe}}

        \input{figures/ch1_prob_c}
        \caption{Partial evaluation of $\Prog_2$\label{fig:prob_pe_c}}

    \caption{Partial evaluation of a Probabilistic Integer Program with hard to
    find runtime-complexity bounds using only \gls{mprf}.}

\fref{fig:prob}. The variables $x$ and $y$ are now only decremented with 50\%
probability in every iteration. The program will probably always terminate,

\fref{fig:prob}. The variables $x$ and $y$ are now only in/-decremented with
50\% probability in every iteration. The program will probably always terminate,

\gls{koat} fails to find finite runtime an expected complexity bounds for this

\gls{koat} fails to find finite runtime and expected complexity bounds for this

\section{Related works}

\section{Related Work}

the whole program. Optionally to improve the analysis, Koat can resort to

the whole program. Optionally to improve the analysis, \gls{koat} can resort to

            {\LARGE\scshape Master Thesis}

            {\LARGE\scshape Master's Thesis}

            \color{rwth}\nth{1} Advisor		& Nils Lommen, MSc\\
            \color{rwth}\nth{2} Advisor		& Eleanore Meyer, MSc\\

            \color{rwth} Advisor		& Nils Lommen, MSc\\
            \color{rwth} Advisor		& Eleanore Meyer, MSc\\

    The \gls{koat}, the complexity analysis tool developed at RWTH University,
    was recently extended to the analysis probabilistic integer programs, with
    the goal to find tight expected runtime-complexity bounds. 
    At the time of writing \gls{koat} does control-flow-refinement via partial
    evaluation by calling the tool iRankFinder externally, making it slow in the
    process and hard to maintain. iRankFinder cannot handle probabilistic
    program, making it impossible to be used for their analysis.
    This thesis applies the techniques of partial evaluation to probabilistic
    programs. A partially evaluated probabilistic integer programs is proven to
    have the same expected runtime-complexity as its original, making this
    technique useful when searching tight expected runtime-complexity bounds on
    probabilistic integer program. 
    The evaluation is shown to work on a Sub-SCC level similar to the original
    the old control-flow-refinement. 
    The newly developed algorithms are implemented natively in \gls{koat} and
    integrated into the existing analysis algorithms using Sub-SCC evaluation.
    The native implementation turns out to be faster on classical integer
    programs, making it a good candidate to replace the old implementation in
    the future. Furthermore, the implementation is shown to improve the found
    expected runtime-bounds found for some probabilistic integer programs as
    well.

    \acrshort{KoAT} is an automatic complexity analysis tool for integer programs, which
    was recently extended to the analysis of probabilistic integer programs.
    Currently, \acrshort{koat} applies so-called control-flow-refinement via
    partial evaluation on classic programs by calling the tool iRankFinder
    externally. 
    In this thesis, we extend partial evaluation to probabilistic programs. A
    partially evaluated probabilistic integer program has the same expected
    runtime-complexity as the original program. However, the transformed program
    might be easier to analyse.
    The new algorithm is implemented natively in \acrshort{koat} and is
    integrated into the existing analysis algorithm modular and on-demand. Our
    evaluation shows that the native implementation is faster on classical
    programs. Futhermore, the new implementation infers tighter
    runtime complexity bounds for some probabilistic programs as well.

\maxtocdepth{subsection}

\maxtocdepth{section}