}
@InCollection{barwise1977,
  author    = {Jon Barwise},
  booktitle = {HANDBOOK OF MATHEMATICAL LOGIC},
  publisher = {Elsevier},
  title     = {An Introduction to First-Order Logic},
  year      = {1977},
  editor    = {Jon Barwise},
  pages     = {5-46},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {90},
  abstract  = {Publisher Summary
This chapter discusses the formulas that are certain finite strings of symbols. The “first” in the phrase “first-order logic” is to distinguish this form of logic from stronger logics, such as second-order or weak second-order logic, where certain extralogical notions (set or natural number) are taken as given in advance. The chapter provides information of what can and what cannot be expressed in first-order logic. Most of the examples are taken from the wealth of notions in modern algebra with which most mathematicians have at least a nodding acquaintance. The chapter also discusses many-sorted first-order logic, ω-logic, weak second-order logic, Infinitary logic, Logic with new quantifiers, and abstract model theory.},
  doi       = {https://doi.org/10.1016/S0049-237X(08)71097-8},
  file      = {:/home/paradyx/MA/literatur/introductiontofo.pdf:PDF},
  issn      = {0049-237X},
  url       = {https://www.sciencedirect.com/science/article/pii/S0049237X08710978},
}
@InProceedings{gurfinkel2010,
  author    = {Arie Gurfinkel and Sagar Chaki},
  booktitle = {Static Analysis - 17th International Symposium, {SAS} 2010, Perpignan, France, September 14-16, 2010. Proceedings},
  title     = {Boxes: {A} Symbolic Abstract Domain of Boxes},
  year      = {2010},
  editor    = {Radhia Cousot and Matthieu Martel},
  pages     = {287--303},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6337},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/sas/GurfinkelC10.bib},
  doi       = {10.1007/978-3-642-15769-1\_18},
  groups    = {Polyhedra, Octagons, Boxes},
  timestamp = {Mon, 03 Jan 2022 22:21:24 +0100},
  url       = {https://doi.org/10.1007/978-3-642-15769-1\_18},

% TeX root = ../main.tex
\begin{tikzpicture}[scale=0.5]
    \begin{axis}[
        axis lines = center,
        axis on top,
        xmin=-3.3,
        xmax=3.3,
        ymin=0,
        ymax=5.3,
        y=1cm,
        x=1cm,
        ytick={-0,...,5},
        xtick={-3,...,3},
        xlabel = x,
        ylabel = y,
        font=\tiny
    ]
        \addplot [ name path = A, thick ] {x + 4};
        \addplot [ name path = B, thick ] {x + 1};
        \addplot [ name path = C, thick ] {-x + 4};
        \addplot [ name path = D, thick ] {-x + 1};
        \addplot[name path=top,draw=none] {5.3};
        \addplot[name path=bottom,draw=none] {0};
        \addplot[pattern=north west lines,pattern color=blue!30] fill
        between[of=A and top];
        \addplot[pattern=north west lines,pattern color=blue!30] fill
        between[of=C and top];
        \addplot[pattern=north west lines,pattern color=blue!30] fill
        between[of=B and bottom];
        \addplot[pattern=north west lines,pattern color=blue!30] fill
        between[of=D and bottom];
        \addplot[only marks,mark=o] coordinates {
                    (0, 4) 
            (-1, 3) (0, 3) (1, 3)
            (-1, 2) (0, 2) (1, 2)
                    (0, 1) 
        };
        \addplot[fill=red,fill opacity=0.20] fill between [of=B and bottom,soft
        clip={domain=0:1.5}];
        \addplot[fill=red,fill opacity=0.20] fill between [of=D and bottom,soft
        clip={domain=-1.5:0}];
    \end{axis} 
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[scale=0.5]
    \begin{axis}[
        axis lines = center,
        axis on top,
        xmin=-3.3,
        xmax=3.3,
        ymin=-3.3,
        ymax=3.3,
        y=1cm,
        x=1cm,
        ytick={-3,...,3},
        xtick={-3,...,3},
        xlabel = x,
        ylabel = y,
        font=\tiny
    ]
        \addplot [
            % domain=-3:3,
            name path = A,
            thick,
            % pattern=north east lines,
        ] {0.5*x + 1};
        \addplot[name path=C,draw=none] {3.3};
        \addplot [
            % domain={-1.65:3},
            name path = B,
            thick,
            % pattern=north east lines,
        ] {0.5*x*x-2};
        \addplot[name path=D,draw=none] {-3.3};
        \addplot[pattern=north west lines,pattern color=blue!30] fill between[of=A and C];
        \addplot[pattern=north east lines,pattern color=red!30] fill between[of=B and D];
        \addplot[only marks,mark=o] coordinates {
                                                       (2,  2)
                                       (0,  1) (1,  1) (2,  1)        
                              (-1,  0) (0,  0) (1,  0)                
                              (-1, -1) (0, -1) (1, -1)                
        };
    \end{axis} 
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[scale=0.5]
    \begin{axis}[
        axis lines = center,
        axis on top,
        xmin=-3.3,
        xmax=3.3,
        ymin=-3.3,
        ymax=3.3,
        y=1cm,
        x=1cm,
        ytick={-3,...,3},
        xtick={-3,...,3},
        xlabel = x,
        ylabel = y,
        font=\tiny
    ]
        \addplot [
            % domain={-1.65:3},
            name path = B,
            thick,
            % pattern=north east lines,
        ] {0.5*x*x-2};
        \addplot[name path=D,draw=none] {-3.3};
        \addplot[pattern=north east lines,pattern color=red!30] fill between[of=B and D];
        \addplot[only marks,mark=o] coordinates {
            (-3,  3) (-2,  3) (-1,  3) (0,  3) (1,  3) (2,  3) (3,  3)
                     (-2,  2) (-1,  2) (0,  2) (1,  2) (2,  2)        
                     (-2,  1) (-1,  1) (0,  1) (1,  1) (2,  1)        
                     (-2,  1) (-1,  1) (0,  1) (1,  1) (2,  1)        
                              (-1,  0) (0,  0) (1,  0)                
                              (-1, -1) (0, -1) (1, -1)                
        };
    \end{axis} 
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[scale=0.5]
    \begin{axis}[
        axis lines = center,
        axis on top,
        xmin=-3.3,
        xmax=3.3,
        ymin=-3.3,
        ymax=3.3,
        y=1cm,
        x=1cm,
        ytick={-3,...,3},
        xtick={-3,...,3},
        xlabel = x,
        ylabel = y,
        font=\tiny
    ]
        \addplot [
            % domain=-3:3,
            name path = A,
            thick,
            % pattern=north east lines,
        ] {0.5*x + 1};
        \addplot[name path=C,draw=none] {3.3};
        \addplot[pattern=north west lines,pattern color=blue!30] fill between[of=A and C];
        \addplot[only marks,mark=o] coordinates {
                                                      (2,  2) (3,  2)
                                      (0,  1) (1,  1) (2,  1) (3,  1)
                    (-2, -0) (-1, -0) (0, -0) (1, -0) (2, -0) (3, -0)
            (-3,-1) (-2, -1) (-1, -1) (0, -1) (1, -1) (2, -1) (3, -1)
            (-3,-2) (-2, -2) (-1, -2) (0, -2) (1, -2) (2, -2) (3, -2)
            (-3,-3) (-2, -3) (-1, -3) (0, -3) (1, -3) (2, -3) (3, -3)
        };
        \addplot[only marks,mark=o,red!80] coordinates { (0, -2) };
    \end{axis} 
\end{tikzpicture}

        \addplot[mark=none,dashed] {4};

        \addplot[mark=none,dashed,domain={0:6}] {4};

        \addplot[mark=none,dashed] {-2*x + 12};

        \addplot[mark=none,dashed,domain={0:6}] {-2*x + 12};

        \addplot[mark=none,dashed] {x - 3};

        \addplot[mark=none,dashed,domain={0:6}] {x - 3};

        \addplot[mark=none,dashed] {1};

        \addplot[mark=none,dashed,domain={0:6}] {1};

        \addplot[mark=none,dashed] {-x + 3};

        \addplot[mark=none,dashed,domain={0:6}] {-x + 3};

        \addplot[mark=none,dashed] {4};

        \addplot[mark=none,dashed,domain={0:6}] {4};

        \addplot[mark=none,dashed] {-x + 8};

        \addplot[mark=none,dashed,domain={0:6}] {-x + 8};

        \addplot[mark=none,dashed] {x - 2};

        \addplot[mark=none,dashed,domain={0:6}] {x - 2};

        \addplot[mark=none,dashed] {1};

        \addplot[mark=none,dashed,domain={0:6}] {1};

\section{Partial evaluation on probabilistic programs}\label{sec:theory}

\section{Partial evaluation on probabilistic
programs}\label{sec:theory}\label{partialevaluation}

\begin{theorem}

\begin{lemma}\label{thm:constrfleq}

\end{theorem}

\end{lemma}

            \ESs(\Cost(\Prog)) &= \sum_{i=1}^\infty i \cdot P(\Rt(\Prog)=i) 
            = \sum_{i=1}^\infty P(\Cost(\Prog) \leq i) 

            \ESns(\Rt(\Prog')) &= \sum_{i=1}^\infty i \cdot P(\Rt(\Prog)=i) 
            = \sum_{i=1}^\infty P(\Rt(\Prog) \leq i) 

            \ESns(\Cost(\Prog')) &= \sum_{i=1}^\infty i \cdot P(\Rt(\Prog)=i) 
            = \sum_{i=1}^\infty P(\Cost(\Prog) \leq i) 
            = \sum_{\substack{f \in \fpath_\Prog\\ \Rt(f) \leq
            i}}^\infty \prSs(f) \\
            % & \leq \sum_{\substack{f \in \fpath_{\Prog}\\ \Rt(f) \leq i}}^\infty
            % \prSns(f) 
            % = \ESns(\Rt(\Prog'))

            \Leftrightarrow \ESs(\Cost(\Prog)) &\leq \ESns(\Cost(\Prog')) \label{eq:esleq}

            \Leftrightarrow \ESs(\Rt(\Prog)) &\leq \ESns(\Rt(\Prog')) \label{eq:esleq}

either than the original program. Note, that doesn't imply that a perfectly
tight bound for the worst-case expected runtime can be found.

either. Note, that doesn't imply that a perfectly tight bound for the worst-case
expected runtime can be found.

        in Lemma \ref{lem:constrfleq}.

        in Lemma \ref{lem:constrfleq}.\todo{lemma Rückrichtung fehlt}

\subsection{Expected Size bounds}

\section{Abstraction}\label{sec:abstraction}
In \Sref{sec:partialevaluation} the abstraction was represented by an oracle,
that decides if the location is abstracted and an abstraction function. It was
stated that Algorithm \ref{alg:evaluate_abstr} terminates if 
\begin{enumerate}
    \item the oracle eventually always decides to abstract, and 
    \item the abstraction has only a finite number of results.
\end{enumerate}
First, we will discuss some possibilities to select the locations for
abstraction, and then adapt the properties based abstraction developed by
\citeauthor{Domenech19}\cite{Domenech19} for probabilistic integer programs. 

\subsection{Property based abstraction}
\label{sec:propertybasedabstraction}

\begin{comment}
    pro: easy to implement
    contra: 
    - abstractions are expensive
    - abstractions loose precision
    open question:
    - how to select properties
\end{comment}
The naive approach would be to abstract at every location, as it also stated in
\cite{Domenech19}. The advantage is that the implementation is easy. The
evaluated program is small and the analysis thereof fast. The disadvantage is
that a lot of evaluated control-flow is lost to the abstraction. 
The property based abstraction abstraction presented in
\Sref{sec:propertybasedabstraction} requires $\Theta(n)$ calls to the
\gls{smt}-solver which is computationally expensive. 
The primary goal of the presented \gls{cfr} via partial evaluation is to
evaluate overlapping loops in order to find easier to analyse smaller loops.
In practice, the control-flow of a loop is mostly linear. Abstracting the linear
control-flow could lead to two linear sections merging together which would
otherwise-stay separated and thus make finding tight bounds harder in the
process. 
\subsection{Abstract Loop heads}\label{ssec:loopheads}
The second method proposed by \cite{Domenech19} is to abstract only on loop
heads. Termination is guaranteed since every infinite path in the evaluation
tree of a finite program must visit some loop (and in turn the head) an infinite
number of times. With only finitely many possible abstraction results, it is
guaranteed that at some point some version repeats and the evaluation
backtracks. 
The exact definition of a loop head is unclear. For sake of termination it is
sufficient that every loop contains at least one (but possibly arbitrary)
location marked for abstraction. The intuitive candidate is the head of the loop
since that's the location where most branching will probably occur in practice.
For this implementation a loop head is defined as follows.
\begin{definition}
    A \textit{loop head} of a loop is the first location of the loop encountered
    during a depth-first search starting at the start location $l_0$. 
\end{definition}

When selecting all loop heads for abstraction, multiple loop heads can end up on
a single loop, for when the loop is overlapping with another loop. 
\begin{figure}
    \input{figures/ch3_loopheads}
\end{figure}
(see examples \todo{} \todo{}). Detecting loops and loop-heads is further
discussed in \Sref{sec:findingloops}.
\todo{prove upper bound on program size}
% Since 
% In addition control-flow refinement was introduced to unroll loops in such a way
% that hidden branching is resolved. The heuristics presented by \cite{Domenech19}
% are focused on loops and the properties are selected for the loop heads.
% Constructing a heuristic, that is well suited for every location in the program
% is not obvious is left open for future work. 
\subsection{Property based abstraction}\label{sec:propertybasedabstraction}
\section{Sub-\gls{scc} level evaluation}

\subsection{Abstract everything}
\begin{comment}
    pro: easy to implement
    contra: 
    - abstractions are expensive
    - abstractions loose precision
    open question:
    - how to select properties
\end{comment}
The naive solution would be to just abstract at every location, as it also stated
in \cite{Domenech19}. The advantage is that the implementation is easy, and the
resulting program and analysis thereof quick. 
The disadvantage is that a lot of evaluated control-flow is lost to the
abstraction. Every abstraction requires $\Theta(n)$ calls to the SMT-solver
which is computationally expensive. 
In addition control-flow refinement was introduced to unroll loops in such a way
that hidden branching is resolved. The heuristics presented by \cite{Domenech19}
are focused on loops and the properties are selected for the loop heads.
Constructing a heuristic, that is well suited for every location in the program
is not obvious is left open for future work. 
\subsection{Abstract Loop heads}\label{ssec:loopheads}
The second method proposed by \cite{Domenech19} is to abstract only on loop
heads. Termination is guaranteed since every infinite path in the evaluation
tree of a finite program must visit some loop (and in turn the head) an infinite
number of times. With only finitely many abstraction candidates (versions), it
is guaranteed that at some point some version repeats and the evaluation
backtracks. 
The exact definition of a loop head is unclear. For sake of termination it is
sufficient that every loop contains at least one (but possibly arbitrary)
location marked for abstraction. The intuitive candidate is the head of the loop
since that's the location where most branching will probably occure in practice.
For this implementation a loop head is defined as follows.
\begin{definition}
    A \textit{loop head} are the entrance locations to a loop encountered during
    a depth-first search starting at the start location $l_0$. 
\end{definition}
A loop can have multiple loop heads, when it can be entered from different
locations, or when overlapping with other loops (see examples \todo{} \todo{}).
Detecting loops and loop-heads is further discussed in \Sref{sec:findingloops}.

\todo{prove upper bound on program size}

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

First, some basic notation is introduced. Let $\overline{\N} = \N \union
\{\infty\}$. $A^*$ is the set of finite words and $\A^\omega$ is the set of
infinite words over an alphabet $A$. The set of all integer polynomials over
some indeterminates $A$ is denoted by $\Z[A]$. A syntactical substitution where
one symbol is replaced by another is denoted with $[\cdot\backslash{}\cdot]$.
For example $(x<y)[x\backslash{}1] = (1 < y)$. For a finite set $A =
{x_1,\dots,x_n}$, the process of $n$ consecutive substitutions
$[x_i\backslash{}y(i)]$ where the replacement expression $y$ varies only in some
index $i$ is denoted using a shortened notation: $[x_i\backslash{}y_i]_{x_i \in
A} = [x_1\backslash{}y(1)] \dots [x_n\backslash{}y(n)]$. For example
$[x_i\backslash{}i]_{x_i\in A} =

variable is replaced by its index in $A = \{x_0, \dots, x_n\}$.

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

Let $\Zs := (\Z, +, \cdot, 0, 1, \leq, <, =)$ be the structure standard integer
arithmetic, and $\Rs := (\R, +, \cdot, 0, 1, \leq, <, =)$ the structure of
standard real arithmetic. In the following $\V$ denotes a finite set of
variables $\V$. 

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}.
Using the $\models$ relation and $\equiv$ relation from \gls{fo} logic, the
notion of satisfiability is defined.\cite{barwise1977}
\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}
\begin{definition}[Solutions\cite{Domenech19}]\label{def:solutions}
    Let $\varphi \in \Phi$ be an \gls{fo}-formula. $\llbracket \varphi
    \rrbracket$ is defined as the set of all satisfying assignments or the
    \textit{solutions} of the formula $\varphi$.
\end{definition}

\begin{definition}[Constraints]\label{def:constraints}

\begin{definition}[Constraints\cite{bagnara2005convexpolyhedron,
    meyer2021tacas,domenech2019arxiv}\label{def:constraints}]

    Strict and non-strict linear constraints are a subset of their polynomial
    counterpart. For the most part we will just refer to \enquote{constraints}
    when the exact type of constraint is unimportant.

    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.  

Constraints are a subset of formulas in \gls{fo} logic.Thus, their semantics
shall be defined accordingly using the $\models$ relation from \gls{fo} logic.
\begin{definition}[Satisfiability]\label{def:satisfiability}
    For a domain $A$ and a structure $\mathfrak{A} = (A, +, \cdot, 0, 1, \leq,
    <, =)$, a constraint $\psi \in \C$ is \textit{satisfiable} in when
    $\mathfrak{A} \models \psi$. We say a variable assignment $\beta: \V
    \rightarrow A$ \textit{satisfies} the constraint $\psi$ when $(\mathfrak{A},
    \beta) \models \psi$. 
\end{definition}

A set of constraints $C \subseteq \Lin$ is satisfiable, when their conjunction
is satisfiable and we write $\mathfrak{A} \models C$ instead of $\mathfrak{A}
\models \LAnd_{\psi_i \in C} \psi_i$. In addition whenever the structure is
evident from context, we write $\models \psi$ and $\beta \models \psi$ instead
of $\mathfrak{A} \models \psi$ and $(\mathfrak{A}, \beta) \models \psi$
respectively. 

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

\begin{definition}[Solutions]\label{def:solutions}
    Let $\varphi$ be an \gls{fo}-formula. $\llbracket \varphi \rrbracket$ is
    defined as the set of all satisfying assignments or the \textit{solutions}
    of the formula $\varphi$.
\end{definition}

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.

Let $\psi_1,\psi_2\in \C$ and $C \subseteq \C$, the following properties hold,

Let $\psi_1,\psi_2\in \C$ and $C \subseteq \C$. The following properties hold,

\begin{definition}[Equivalence]\label{def:equivalence}

\begin{definition}[Equivalence\cite{Domenech19}]\label{def:equivalence}

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

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

\begin{definition}[Entailment]
    Let $\varphi_1, \varphi_2$ be FO-formulas with variables $\V$. If
    $\llbracket \varphi_1 \rrbracket \subseteq \llbracket \varphi_2 \rrbracket$
    and we say that $\varphi_1$ \textit{entails} $\varphi_2$.

\begin{definition}[Entailment\cite{Domenech19}]
    Let $\varphi_1, \varphi_2 \in \Phi$. If $\llbracket \varphi_1 \rrbracket
    \subseteq \llbracket \varphi_2 \rrbracket$ and we say that $\varphi_1$
    \textit{entails} $\varphi_2$.

The problem of determining, if a set of constraints is satisfiable or finding

The problem of determining if a set of constraints is satisfiable or finding

researched. The theories relevant for this thesis the are the quantifier-free

researched. The theories relevant for this thesis are the quantifier-free

variables that are only relevant to the scope of a transition. In FO-logic one
would just existentially quantify the variable. However the new FO-formula
wouldn't be quantifier-free anymore. Instead a new formula is searched that has
just the same solutions when ignoring the values for the irrelevant variables.

variables that are only relevant to the scope of a transition. In \gls{fo} logic
one would just existentially quantify the variable. However the new \gls{fo}
formula wouldn't be quantifier-free anymore. Instead a new formula is searched
that has just the same solutions when ignoring the values for the irrelevant
variables.

    Let $X \subseteq V$ and $\varphi$ be a quantifier-free FO-formula over the
    variables $V$ and let $\beta|_X$ denote the restriction of the assignment
    $\beta$ to the smaller to domain $X$.
    The projection of $\varphi$ onto $X$ denoted as $\text{proj}_X(\varphi)$ is
    a quantifier-free FO-formula $\varphi'$ over the variables $X$, with
    $\llbracket \varphi' \rrbracket = \set{\beta|_X}{\sigma \in \llbracket
    \varphi \rrbracket}$. 

    Let $A \subseteq V$ and $\varphi \in \Phi$. The projection of $\varphi$ onto
    $A$ denoted as $\varphi|_A$ is a quantifier-free FO-formula $\varphi|_A\in
    \Phi_A$, with $\llbracket \varphi|_A \rrbracket = \set{\beta|_X}{\beta \in
    \llbracket \varphi \rrbracket}$. 

\section{Updates}

\section{Updates}\label{sec:update}

whereas for updates there exists a \textit{before} and an \textit{after}. 
In this section we will only consider integer arithmetic, although using real
arithmetic works analogously. 

whereas for updates there exists a \textit{before} and an \textit{after}.

\set{s : A \rightarrow \Z}{A \subseteq \V}$ be the set of integer assignments.

\set{s : A \rightarrow \Z}{A \subseteq \V}$ be the set of full integer
assignments.

    of a variable $x\in A$ \textit{after} the update is determined by $u(x)(s)$

    of a variable $x\in A$ \textit{after} the update is determined by $u(x)(s)$.
    Note, that $u(x)$ is a polynomial and $u(x)(s)$ is the evaluation of that
    polynomial.

\begin{lemma}[\label{lem:nonprop_update}]

\begin{lemma}\label{lem:nonprop_update}

    and if $s \models \varphi$, the then $s' \models u(\varphi)$.

    and if $s \models \varphi$, then $s' \models u(\varphi)$.

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

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

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

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

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

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

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

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

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

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

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

            \varphi \Land \LAnd_{x\in A} u(x)(s) = u(x)\nonumber\\

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

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

constraint partitions the space into one included and one excluded part. In case
of integer arithmetic the solutions are discrete points in this space. 

constraint partitions the space. One part is included and the other is excluded.
In case of integer arithmetic the solutions are discrete points in this space. 

An abstract domains is a representation of those sets of points. Usually they
over-approximate the sets in order to facilitate operations. Commonly used
abstract domains are Polyhedra\cite{bagnara2005convexpolyhedron}

An abstract domain is a representation of those sets of points. Usually a value
over-approximates the set of points in order to facilitate operations. Commonly
used abstract domains are Polyhedra\cite{bagnara2005convexpolyhedron}

the Interval domain\cite{}

the Interval domain (also called Boxes)\cite{gurfinkel2010}.

projection, upper, and lower bounds. There are many more but we will focus only
on the ones important for this thesis. They all 

projection, upper and lower bounds. There are many more but we will focus only
on the ones important for this thesis.

However, the intersection of two abstract values might include more values than
the solutions of the formula conjunction due to the approximative nature of
abstract domains. 

            \input{figures/ch1_example1_phi1}

            \input{figures/ch2_example1_phi1}

            \input{figures/ch1_example1_phi2}

            \input{figures/ch2_example1_phi2}

            \input{figures/ch1_example1_phi3}

            \input{figures/ch2_example1_phi3}

    clearly equal to the intersection of both sets of solutions. While
    $\varphi_1$ and $\varphi_2$ have infinitely many solutions, the conjunction
    $\varphi_3$ has not. 

    equal to the intersection of both sets of solutions. While $\varphi_1$ and
    $\varphi_2$ have infinitely many solutions, the conjunction $\varphi_3$ has
    not. 

The orthogonal projection computes the projection of an FO-formula, possibly
loosing some precision in the process. Geometrically, the projection can be seen
as set of solutions projected (casting a shadow) onto the remaining dimensions. 

The orthogonal projection computes the projection of an \gls{fo} formula.
Geometrically, the projection can be seen as set of solutions projected (casting
a shadow) onto the remaining dimensions. 

    \begin{figure}
        \centering
        \input{figures/ch2_projection}
        \caption{Projecting a 2D-formula onto the $x$-axis\label{fig:orthogonal_projection}}
    \end{figure}

    $x$-axis like shown in \fref{fig:ex2}. 
    \begin{figure}\label{fig:ex2}
        \centering
        \input{figures/ch1_example2}
        \caption{Projecting a
        2D-constraint.}
    \end{figure}

    $x$-axis like shown in \fref{fig:orthogonal_projection}. 

\begin{figure}

\begin{figure}[h]

\begin{definition}[Not necessarily closed Polyhedra]\label{def:polyhedra}

\begin{definition}[Not necessarily closed
    Polyhedra\cite{bagnara2005convexpolyhedron}\label{def:polyhedra}]

talking about integer arithmetic one refers only to polyhedra. 

talking about integer arithmetic one refers only to polyhedra.
Polyhedra can exactly only represent linear constraints. Non-linear polynomial
constraints are usually just removed, possibly leaving dimensions unbounded in
the process. There are certainly better linear over-approximations to polynomial
constraints, but finding these would go beyond the scope of this thesis.

\todo{more about tightness of operations} 
\todo{say something about
overapproximation of polynomial constraints}

Polyhedra will be used for the partial evaluation algorithm described in chapter
\ref{ch:theory}, since in practice the partial evaluation is called only on
small sub-programs and precision is more desirable than performance.

intervals (see \Sref{ssec:intervals} below and polyhedra. 

intervals (see \Sref{ssec:box}) and polyhedra (see
\Sref{ssec:polyhedra}).\cite{mine2006hosc}

\begin{definition}\label{def:octagons}

\begin{definition}[Octagons\cite{mine2006hosc,mine2001wcre}\label{def:octagons}]

    expressed by an a set of constraints of the form $\pm v_i \pm
    v_j \leq b$\cite{mine2001wcre}. 

    expressed by an a set of constraints of the form $\pm v_i \pm v_j \leq b$. 

specialization of polyhedra. Octagons are used in \gls{koat} during the

special case of polyhedra. Octagons are used in \gls{koat} during the

domain. An closed interval $[a,b]$ with $a, b \in \R$ for a variable $v \in \V$

domain. A closed interval $[a,b]$ with $a, b \in \R$ for a variable $v \in \V$

\begin{definition}[Box]\label{def:box}

\begin{definition}[Box\cite{gurfinkel2010}\label{def:box}]

polyhedron $P$ one can find a box $P'$ that contains the polyhedron
$P$.\todo{citation or proof} 
Whenever it's acceptable to arbitrarily widen the
polyhedron, one can work with boxes instead. Boxes are computationally very
efficient, although rather imprecise, for most applications.

polyhedron $P$ one can find a box $P'$ that contains the polyhedron $P$. Boxes
are computationally very efficient, although rather imprecise for most
applications.

\section{Probability}

\section{Probability Theory}

The field of probability and random variables is well studied. Only the core 

The field of probability and random variables is well studied. Only the core

definitions from \cite{billingsley2011}. For additional information we
will refer to the literature.\cite{kraaikamp2005modern, billingsley2011}

definitions from \citeauthor{billingsley2011}\cite{billingsley2011}. For
additional information we'll refer to the
literature.\cite{kraaikamp2005modern, billingsley2011}

Imagine probabilistic event with some possible outcomes $\Omega$. For example a 
coin-toss can have arbitrary many outcomes when taking the position on the table
into account, the fact that the coin might get lost in the process etc. 
A probability measure describes the probabilities of sets of random outcomes.
For example the coin-toss on the table has a sub-set of outcomes where the
coin's head is above. The probability measure would assign a probability close
to 50\% for a somewhat normal coin-toss. 

Imagine a probabilistic event with some possible outcomes $\Omega$. For example
a coin-toss can have arbitrary many outcomes when taking the position on the
table into account, the fact that the coin might get lost in the process etc. A
probability measure describes the probabilities of sets of random outcomes. For
example the coin-toss on the table has a sub-set of outcomes where the coin's
head is above. The probability measure would assign a probability close to 50\%
for a somewhat normal coin-toss. 

\begin{definition}[Probability Measure]\label{def:measure}
    A set function $\mu$ on a $\sigma$-field $\F$ is a probability

\begin{definition}[$\sigma$-Algebra\cite{billingsley2011}]
    Let $\Omega$ be an arbitrary set. A set $A \subset 2^\Omega$ is called a
    $\sigma$-algebra (also known as $\sigma$-field) when 
    \begin{enumerate}
        \item $\Omega \in A$,
        \item $A$ is closed under complement, i.e. $B \in A$ implies $B^C \in
            A$,
        \item $A$ is closed under countable unions, i.e. $A_1, A_2 \dots, \in A$ 
            implies $\Union_{n\in\N}A_n \in A$.
    \end{enumerate}
\end{definition}
\begin{definition}[Probability Measure\cite{billingsley2011}]\label{def:measure}
    A set function $\mu$ on a $\sigma$-algebra $\F$ is a probability

\begin{definition}[Probability space]\label{def:probability_space}
    A probability space is a triple $(\Omega,\F,P)$. Where the

\begin{definition}[Probability space\cite{billingsley2011}]\label{def:probability_space}
    A probability space is a triple $(\Omega,\F,P)$ where the

        \item $\F$ is the set of events that contains $\Omega$, is
            closed under complement, intersection and countable unions. Such a
            set is also called $\sigma$-field or $\sigma$-algebra.
            \begin{enumerate}
                \item $\Omega \in \F$ 
                \item For $A\subseteq\Omega$, if $A\in\F$ then so is
                    its complement $A^c\in\F$.
                \item For $A,B \subseteq \Omega$, if $A, B \in \F$,
                    then so is $A \cup B \in \F$.
                \item For $ A_1, A_2, \dots,A_n \subseteq \Omega$, if $A_i \in
                    \F$, then so is their union $\Union\limits_{i=1}^n
                    A_i \in \F$.
            \end{enumerate}

        \item $\F$ is a $\sigma$-algebra containing $\Omega$.

variables in formulas. Colloquially, a random variable maps the results of a
probabilistic event $\omega$ to a real value, or, the value of the random

variables in formulas. Informally, a random variable maps the results of a
probabilistic event $\omega$ to a real value, or the value of the random

\begin{definition}[Random variable]\label{def:random_variable}

\begin{definition}[Random variable\cite{billingsley2011}]\label{def:random_variable}

In the following, we will encounter discrete random variables $X : \Omega

In the following, we will encounter mostly discrete random variables $X : \Omega

underlying probability space. In case of discrete random variables the are
sufficient to fully describe them. The underlying probability space becomes
irrelevant at this point, as the specific events and their probabilities are not
important to the outcome of the random variable, as long as the probability of
the outcome is fully defined.

underlying probability space. In case of discrete random variables the
distribution is sufficient the random variable. The underlying probability space
becomes irrelevant at this point, as the specific events and their probabilities
are not important to the outcome of the random variable, as long as the
probability of the outcome is fully defined.

\begin{definition}[Distribution of a random variable]\label{def:distribution}
    Let $X$ be a discrete random variable. The distribution is describe by the

\begin{definition}[Distribution of a random variable\cite{billingsley2011}]\label{def:distribution}
    Let $X$ be a discrete random variable. The distribution is described by the

\begin{definition}[Support]
    For a random variable with a distribution $\mu$, the support is smallest
    Borel-set $S$ for which $\mu(S) = 1$. \todo{why borel set?} Discrete random
    variables have a countable support $S = \{S_1, S_2, \dots\}$.

\begin{definition}[Support\cite{billingsley2011}]
    For a random variable with a distribution $\mu$, the support is smallest set
    $S$ for which $\mu(S) = 1$. Discrete random variables have a countable
    support $S = \{S_1, S_2, \dots\}$.

The Bernoulli distribution is a distribution with two possible outcomes: $1$ and $0$. For
example decided by a coin-flip. 

The Bernoulli distribution is a distribution with two possible outcomes: $1$ and
$0$, for example decided by a coin-flip. 

The support of a hypergeometric distribution is as follows: \todo{elaborate}

The support of a hypergeometric distribution is as follows:

The binomial distribution similar to the geometric distribution except that the
number of successes of repeated independent Bernoulli events is counted. 
Or (\enquote{with putting back}). 

The binomial distribution is similar to the geometric distribution except that
the number of successes of repeated independent Bernoulli events is counted.

When considering a random variable one is usually interested the value to expect
in general. For example most possible outcomes of a binomial distribution are
very improbable. This is described by the expected value.
\begin{definition}[Expected Value\cite{billingsley2011}]
    The expected value of a random variable $X$ on a probability space $(\Omega,
    \F, P)$ is the integral of X with respect to the measure $P$:
    \begin{equation*}
        \E(X) = \int X dP = \int_\Omega X(\omega) P(d\omega)
    \end{equation*}
    This gets simplified for discrete random variables where every the integral can
    be replaced by a sum. (see Lemma 48 in \cite{meyer20arxiv})
    \begin{equation*}
        \E(X) = \sum_{r \in \bar{\R}_{\geq0}} r \cdot P(X = r)
    \end{equation*}
\end{definition}

$\Z[\V\union D]$, is the set of integer polynomials containing variables $\V$ or
distributions. They behave exactly like normal polynomials except that the
values of the distributions are sampled probabilistically instead of being given
as argument. As such we can define a function $[\cdot]: \Z[\V\union D]
\rightarrow \Sigma \rightarrow \Z \rightarrow [0,1]$ that returns the
probability that the polynomial $f \in \Z[\V \union D]$ with a state $s \in
\Sigma$ evaluates to a value $k\in\Z$ with a probability $[f](s)(k)$. 

$\Z[\V\union \D]$, is the set of integer polynomials containing variables $\V$
or probability distributions $\D$. They behave exactly like normal polynomials
except that the values of the distributions are sampled probabilistically
instead of being given as argument. As such we can define a function $[\cdot]:
\Z[\V\union \D] \rightarrow \Sigma \rightarrow \Z \rightarrow [0,1]$ that returns
the probability that the polynomial $f \in \Z[\V \union D]$ with a state $s \in
\Sigma$ evaluates to a value $k\in\Z$ with a probability $[f](s)(k)$.

\begin{align}

\begin{align*}

\end{align}

\end{align*}

    \begin{equation}

    \begin{equation*}

    \end{equation}

    \end{equation*}

The support of the update $\eta A \rightarrow \Z[\V\union \D]$ on an assignment

The support of the update $\eta : A \rightarrow \Z[\V\union \D]$ on an assignment

A probabilistic polynomial is a random variable, that evaluates to a random

A probabilistic polynomial is a random variable that evaluates to a random

        By Lemma \ref{lem:nonprop_update}, follows $s' \models

        By Lemma \ref{lem:nonprop_update} follows $s' \models

In general, an \textit{integer programs} is a program that only uses variables

In general, an \textit{integer program} is a program that only uses variables

contains conditions, called \textit{guard}, that must be true for the current

contains a condition, called \textit{guard}, that must be true for the current

some updates. An update assigns a new value to a program variable depending on
the previous state. Ever inter program starts at a unique location usually
called $l_0$. Whenever no transition guard is satisfied the program terminates. 

some \textit{update}. An update assigns a new value to a program variable
depending on the previous state. Every integer program starts at a unique
location usually called $l_0$. Whenever no transition guard is satisfied the
program terminates. 

Although similar, non-deterministic and probabilistic branching treated

Although similar, non-deterministic and probabilistic branching are treated

    resolved first 

    resolved first. Then if the general transition containing $t_2$ and $t_3$ is
    selected, a coin is through to decide whether to take $t_2$ or $t_3$.

or probabilistic, which is also called non-deterministic or probabilistic

or probabilistic, which is called non-deterministic or probabilistic

    Whenever temporary variable is sampled to a value not satisfying the

    Whenever a temporary variable is sampled to a value not satisfying the

Probabilistic sampling is done using probability distributions. Coincidentally,
only the probability distributions from \Sref{ssec:distributions} are supported.
Updates are restricted to integer polynomials with variables and additionally
distributions when probabilistic sampling is allowed. The value of the
indeterminate in the polynomial is equal to the (possibly temporary) variable or
sampled from the distribution with the corresponding probability. 

Probabilistic sampling is done using probability distributions (recall
\Sref{distributions}. Updates are restricted to integer polynomials with
variables and additionally distributions when probabilistic sampling is allowed.
The value of the indeterminate in the polynomial is equal to the (possibly
temporary) variable or sampled from the distribution with the corresponding
probability. 

\cite{meyer2021tacas}. First the formal definition for a probabilistic program
is given, then the semantics are introduced.

\cite{meyer2021tacas}. First the formal definition for a \acrfull{pip} is given,
then after a small excursion to markov decision processes, the semantics are are
defined.

        \item $\PV$ is a finite set of program variables
        \item $\Loc_\Prog$ is a finite non-empty set of location

        \item $\PV$ is a finite set of program variables,
        \item $\Loc_\Prog$ is a finite non-empty set of location,

                \item a source and target location $l,l' \in \Loc$.
                \item a probability $p \geq 0$, that the transition is taken
                    when the corresponding general transition $g$ is executed. 
                \item a guard $\tau \in C$

                \item a source and target location $l,l' \in \Loc$,
                \item a probability $p \geq 0$ that the transition is taken
                    when the corresponding general transition $g$ is executed,
                \item a guard $\tau \in C$,

                    g$ must share the same start location $l$, guard $τ$. 
                \item an associated cost $\kappa\in\R$

                    g$ must share the same start location and guard.

            We call $τ_g$ the guard of the general transition $g$; and all
            transitions share a common start location which we call $l_g$. 

            We call $τ_g$ the guard of the general transition $g$ and all
            transitions share a common start location which we call $l_g$.

the same purpose. Instead of just vaguely \enquote{terminating} a program takes
the transition $g_\bot$ to the location $l_\bot$ if and only if no other
transition is walkable. Since no normal transition leaves the location $l_\bot$
the run loops indefinitely on the location $l_\bot$ after termination. In
addition a new transition $t_\text{in}$ will be used for the start of the
program. 

the same purpose. Instead of just \enquote{terminating} a program takes the
transition $g_\bot$ to the location $l_\bot$ if and only if no other general
transitions guard is satisfied. Since no normal transition leaves the location
$l_\bot$ the run loops indefinitely on the location $l_\bot$. In addition a new
transition $t_\text{in}$ is added for the start of the program. 

\rightarrow \Z$. $\Sigma$ is the set of all states. The set of configuration is
defined as $\confs = L \union \{l_\bot\} \times \T \union \{t_{\text{in}},

\rightarrow \Z$. $\Sigma$ is the set of all states. The set of configurations is
defined as $\confs_\Prog = \Loc_\Prog \union \{l_\bot\} \times \T_\Prog \union \{t_{\text{in}},

the current location is captured as well. This won't be relevant for the partial

the current location is remembered as well. This won't be relevant for the partial

set of all runs is defined as $\runs = \confs^\omega$. In contrast a finite

set of all runs is defined as $\runs_\Prog = \confs_\Prog^\omega$. In contrast a finite

defined as $\fpath = \confs^*$. 

defined as $\fpath_\Prog = \confs_\Prog^*$. 

    \item \textit{decision epochs}, are points in time, at which a decision is

    \item \textit{decision epochs} are points in time at which a decision is

    \item \textit{states}, the decision process is in at a decision epoch;
    \item \textit{actions}, that are selected by the decision process;
    \item \textit{transition probabilities}, that describe the probabilities of

    \item \textit{states} the decision process is in at a decision epoch;
    \item \textit{actions} that are selected by the decision process;
    \item \textit{transition probabilities} that describe the probabilities of

    \item \textit{rewards}, that are accumulated over the whole decision process

    \item \textit{rewards} that are accumulated over the whole decision process

the program, are the states of the decision process. Non-deterministic sampling,
non-deterministic branching are similar to choosing an action, and the

the program are the states of the decision process. Non-deterministic sampling
and non-deterministic branching are similar to choosing an action, and the

The reward is usually the optimization goal, of the Markov decision process, and
the literature describes the properties of a given process with regard to the
highest achievable rewards. That is, one looks for a decision policy that
returns the highest accumulated rewards over a whole process.

The highest reward is the optimization goal, when taking decision in a Markov
decision process. One looks for a decision policy that returns the highest
accumulated rewards over a whole process. In literature\cite{puterman1994markov,
puterman1990markov}, the properties of a given process with regard to the
highest achievable rewards is researched extensively. 

complexity and runtime costs. If define runtime (or costs) as reward, we can
picture the Markov decision process as an adversary, finding the decision policy
with the longest runtime. 

complexity. If one defines runtime as reward, one can picture the policy for a
Markov decision process as an adversary. We call the policy \enquote{scheduler}.

    \item the states are the configurations $\confs$ of the program
    \item the actions are the selection of a general transition and full
        assignments that satisfy a guard of of the selected general transition,
        or the terminating transition.

    \item The states are the configurations $\confs_\Prog$ of the program.
    \item The actions are the selection of a general transition and full
        assignments that satisfy a guard of the selected general transition or
        the terminating transition.

        \Sref{ssec:probabilityspace}
    \item the reward is 1 for every non terminating transition

        \Sref{ssec:probabilityspace}.
    \item the reward is 1 for every non terminating transition.

    In general, at every decision epoch one can use a different decision rules,
    described by a policy. However, we will only consider stationary) policies,
    where the policy uses the same decision rule at every decision epoch. 

    In general, at every decision epoch one can use a different decision rule,
    described by a policy. However, we will only consider so-called stationary
    policies, where the policy uses the same decision rule at every decision
    epoch. 

The adversary that uses a stationary policy to decide the non-deterministic
sampling branching and branching deterministically for us, is called scheduler.

    A function $\scheduler : \confs \rightarrow (\GT \uplus \{g_\bot\})$ is a

    A function $\scheduler : \confs_\Prog \rightarrow (\GT_\Prog \uplus \{g_\bot\})$ is a

    \confs$, $\scheduler(c) = (g, s')$ implies:

    \confs_\Prog$, $\scheduler(c) = (g, s')$ implies:

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

    A function $\scheduler : \fpath \rightarrow (\GT \uplus \{g_\bot\})$ is a
    history dependent scheduler if for every finite prefix $f\in\fpath$ and
    configuration $c=(l,t,s) \in
    \confs$, $\scheduler(fc) = (g, s')$ implies: items \ref{itm:md1} to
    \ref{itm:md4} of Definition \ref{def:mscheduler}.

    A function $\scheduler : \fpath_\Prog \rightarrow (\GT_\Prog \uplus
    \{g_\bot\})$ is a history dependent scheduler if for every finite prefix
    $f\in\fpath$ and configuration $c=(l,t,s) \in \confs_\Prog$, $\scheduler(fc)
    = (g, s')$ implies: items \ref{itm:md1} to \ref{itm:md4} of Definition
    \ref{def:mscheduler} for the last configuration $c$.
    The set of all history dependent schedulers for a program $\Prog$ is denoted
    by $\HDS^\Prog$, where \enquote{HD} stands for \enquote{history dependent
    deterministic}.

every set ${r} \in \F$ for $r \in \runs$. The probability measure $\prSs$

every set $\{r\} \in \F$ for $r \in \runs$. The probability measure $\prSs$

\cite{meyer20arxiv}.

\citeauthor{meyer20arxiv}\cite{meyer20arxiv}.

transition. If no such transition is found of the program is already in the

transition. If no such transition is found or the program is already in the

Let $\scheduler$ be a scheduler and $s_0$ be an initial state. First, the
probability for a program to start at a configuration $c$ is 1 only for the
configuration that has the initial state $s_0$ at the start location $l_0$
coming from the initial transition $t_\text{in}$. All other configuration are
invalid starting configurations and get assigned a zero probability by the
probability measure $\prSs : \confs \rightarrow [0,1]$

Let $\scheduler \in \MDS^\Prog$ be a scheduler and $s_0$ be an initial state.
First, the probability for a program to start at a configuration $c$ is 1 only
for the configuration that has the initial state $s_0$ at the start location
$l_0$ coming from the initial transition $t_\text{in}$. All other configuration
are invalid starting configurations and get assigned a zero probability by the
probability measure $\prSs : \confs_\Prog \rightarrow [0,1]$

\begin{equation}

\begin{equation*}

\end{equation}

\end{equation*}

the probability $p$, second the probability that each program variables

the probability $p$, second the probability that each program variable

\begin{align}

\begin{align*}

\end{align}

\end{align*}

\begin{equation}

\begin{equation*}

\end{equation}

\end{equation*}

Naturally for all other configurations $c'$, such as configuration that are not

Naturally for all other configurations $c'$, such as configurations that are not

\begin{align}

\begin{align*}

\end{align}

\end{align*}

infinite runs $\PrSs : \runs \rightarrow [0,1]$ and the probability space
$(\runs, \F, \PrSs)$.

infinite runs $\PrSs : \runs_\Prog \rightarrow [0,1]$ and the probability space
$(\runs_\Prog, \F, \PrSs)$.

%     % Das ist falsch. Hier muss \tilde{s} betrachtet werden...

    An finite prefix $f \in \fpath$ is \textit{admissible} if and only if

    A finite prefix $f \in \fpath_\Prog$ is \textit{admissible} if and only if

    only if every finite prefix $c_0\dots c_n \in\fpath$ is admissible.

    only if every finite prefix $c_0\dots c_n \in\fpath_\Prog$ is admissible.

    An admissible run can very well have have a zero probability if the

    An admissible run can very well have a zero probability if the

Because by definition only the terminating transition $t_\bot$ is admissible
when the program is in the terminal location $l_\bot$ and the following
configuration must again be in the terminal location $l_\bot$. A terminating run
must end with infinitely many repetitions of a terminating configuration
$c_\bot=(l_\bot,t_\bot,s)$ for some assignment $s\in\Sigma$.

By definition only the terminating transition $t_\bot$ is admissible when the
program is in the terminal location $l_\bot$ and the following configuration
must again be in the terminal location $l_\bot$. A terminating run must end with
infinitely many repetitions of a terminating configuration
$c_\bot=(l_\bot,t_\bot,s)$ with some assignment $s\in\Sigma$.

    expected runtime complexity $\Rt{\scheduler,s_0}(\Prog)$ of a program

    expected runtime complexity $\Rt_{\scheduler,s_0}(\Prog)$ of a program

    \acrfull{past}

    \gls{past}.

The runtime complexity is a special case of the cost of a run, where every
transition has an associated cost of $\kappa_t=1$ for all $t \in \T$. Then 

\begin{example}
    Consider the program from example \ref{ex:prob_sampling} displayed in
    \fref{fig:ex_pip_probs}. It must take at least transitions $t_1$ and $t_3$
    hence any runtime less than $2$ is impossible. The variable $x$ is
    decremented by $1$ with a probability of $0.5$ on every transition $t_2$. So
    for a given starting state $s_0$ and $scheduler \in \MDS$, the expected
    runtime depends on the initial variable $x$. The probability for decrementing
    $x$ once follows a geometric distribution. The runtime for decrementing $x$
    until zero ($x$ times) is 
    \begin{equation*}
        \ESs(\Rt(\Prog)) = s_0(x) \cdot \frac{1}{p} = s_0(x) \cdot \frac{1}{0.5} = 2
        s_0(x).
    \end{equation*}
    The expected runtime doesn't depend on the scheduler and is finite for all
    values of $x$, hence the program is \gls{past}.
\end{example}

\begin{equation}
    \Rt_{\scheduler,s_0}(\Prog) = \Cost_{\scheduler, s_0}(\Prog)
\end{equation}

% The runtime complexity is a special case of the cost of a run, where every
% transition has an associated cost of $\kappa_t=1$ for all $t \in \T$. Then 

% \begin{equation}
%     \Rt_{\scheduler,s_0}(\Prog) = \Cost_{\scheduler, s_0}(\Prog)
% \end{equation}

runtime-complexity bounds. A bound is an expression that describes the upper

runtime complexity bounds. A bound is an expression that describes the upper

runtime complexity and cost bounds. A runtime bound is a bound on the 

runtime complexity and cost bounds.

\begin{definition}[Runtime complexity bounds]
    For $s_0\in\Sigma$ and a \gls{pip} $\Prog$, $\RB^1 \in \B$ is a runtime

\begin{definition}[Expected runtime complexity bounds]
    For $s_0\in\Sigma$ and a \gls{pip} $\Prog$, $\RB \in \B$ is a expected runtime

        \RB^1 \geq \sup \Rt(\Prog) = \sup \ESs(\Rt(\Prog)).

        \RB \geq \sup_{\scheduler\in\MDS}(\Rt_{\scheduler, s_0} = \sup_{\scheduler\in\MDS} (\ESs(\Rt(\Prog))).

    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}

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

\begin{comment}

computer science known to be undecidable. The so-called \textit{Halting Problem}

computer science known to be undecidable. The so-called Halting Problem

The tests are chosen to represent a large variety of commonly encountered
real-world programs, but also include known-to-be hard-to-solve problems in
order to challenge the competitors and improve their tools. Their collection of
test programs can be found in the \gls{tpdb} which is publicly
available\footnote{\url{https://github.com/TermCOMP/TPDB}}. During the latests
competition in 2022, eleven candidates lined up in twenty-eight
categories\cite{termcomp2022url}. 

% The tests are chosen to represent a large variety of commonly encountered
% real-world programs, but also include known-to-be hard-to-solve problems in
% order to challenge the competitors and improve their tools. Their collection of
% test programs can be found in the \gls{tpdb} which is publicly
% available\footnote{\url{https://github.com/TermCOMP/TPDB}}. During the latests
% competition in 2022, eleven candidates lined up in twenty-eight
% categories\cite{termcomp2022url}.

\subsection{\acrshort{aprove}, \acrshort{koat}, and \acrshort{loat}}
The \gls{aprove} is developed by \citeauthor{giesl2014ijcar} at RWTH
University\cite{giesl2014ijcar}. \Gls{aprove} is capable of analyzing real-world
programming languages like Java, C, Haskell, Prolog by transforming the given
program into an equivalent \gls{trs} and then analyzing the resulting \gls{trs}
with various different techniques and tools. Explaining every technique used in
\gls{aprove} would go beyond the scope of this thesis. It should only be
mentioned that during analysis parts of the \gls{trs} can be transformed further
into \gls{its} which opens the possibility for many more analysis techniques
typically not available for \gls{trs}. 

\section{Motivation}
\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}

The tools LoAT\cite{frohn2022ijcar} and KoAT\cite{brockschmidt2016acm} are also
developed at RWTH University and aim at the finding lower and respectively upper
runtime-complexity and size bounds on transition systems. At its core,
KoAT computes bounds for subprograms using \gls{mprf} or \gls{twn}, and then
putting the subprograms together generate upper runtime-complexity and size
bounds for the whole program. 
Optionally to improve the analysis, Koat can resort to partial evaluation 
as a control-flow refinement techniques\cite{giesl2022lncs}. 
At first \gls{koat} was aimed at linear integer programs, but it was recently
extended to probabilistic integer programs\cite{meyer2021tacas} and
non-linear arithmetic\todo{citation needed}. 

Consider the program $\Prog_1$ displayed in \fref{fig:classic}. It contains two
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.
This technique used for the transformation was first introduced by
\citeauthor{domenech2019arxiv}\cite{domenech2019arxiv} and is called \gls{cfr}
via partial evaluation and implemented in their analysis tool
iRankfinder\cite{irankfinder2018wst}. It achieves very similar results to
\gls{mprf} when used on the entire programs or whole \gls{scc}. Its real
strength comes from applying it to a sub-\gls{scc} level and refining
specifically the loops where \gls{mprf} fail to find size bounds. This technique
was presented by \citeauthor{giesl2022arxiv}\cite{giesl2022lncs,giesl2022arxiv}
and implemented in \gls{koat}\cite{giesl2014ijcar} the complexity analysis tool
developed by \citeauthor{giesl2014ijcar} at RWTH University. 

Underneath, \gls{koat} uses iRankFinder for the \gls{cfr}.
Recently, \gls{koat} was extended to probabilistic integer
programs\cite{meyer2021tacas,meyer20arxiv}. Unfortunately, by using iRankfinder
which is limited to non-probabilistic integer programs, the technique of
\gls{cfr} via partial evaluation remained out of reach for probabilistic
programs.
\begin{figure}
    \centering
    \begin{subcaptionblock}[t]{0.4\textwidth}
        \centering
        \input{figures/ch1_prob}
        \caption{Probabilistic integer program $\Prog_2$\label{fig:prob}}
    \end{subcaptionblock}
    \begin{subcaptionblock}[t]{0.5\textwidth}
        \centering
        \input{figures/ch1_prob_pe}
        \caption{Partial evaluation of $\Prog_2$\label{fig:prob_pe}}
    \end{subcaptionblock}
\end{figure}
Consider the very similar probabilistic integer program $\Prog_2$ displayed in
\fref{fig:prob}. The variables $x$ and $y$ are now only decremented with 50\%
probability in every iteration. The program will probably always terminate,
since a longer runtime gets increasingly unlikely. The current version of
\gls{koat} fails to find finite runtime an expected complexity bounds for this
program. It would be nice to transform $\Prog_2$ into an equivalent program like
the one shown in \fref{fig:prob_pe} similarly to the \gls{cfr} technique
presented by \citeauthor{giesl2022lncs}\cite{giesl2022lncs} and
\citeauthor{Domenech19}\cite{Domenech19}.
\section{Related works}
\subsection{\acrshort{aprove}, \acrshort{koat}, and \acrshort{loat}} The tools
LoAT\cite{frohn2022ijcar} and KoAT\cite{brockschmidt2016acm} are developed at
RWTH University and aim at the finding lower and respectively upper
runtime-complexity and size bounds on transition systems. At its core, KoAT
computes bounds for subprograms using \gls{mprf} or \gls{twn}, and then putting
the subprograms together generate upper runtime-complexity and size bounds for
the whole program. Optionally to improve the analysis, Koat can resort to
partial evaluation as a control-flow refinement techniques
on a sub-\gls{scc} level\cite{giesl2022lncs}.