\theoremstyle{plain}
\newtheorem{theorem}{Theorem} % Needs proof, and is central to this thesis.
\newtheorem{lemma}{Lemma} % Needs proof, and works towards a theorem

\theoremstyle{remark}
\newtheorem*{rem}{Remark} % Trivial stuff.

\renewcommand{\L}{\mathcal{L}} % Set of polynomial constraints

\renewcommand{\L}{\mathcal{L}} % Set of linear constraints

\newcommand{\N}[0]{\mathbb{N}} % natural numbers

\newcommand{\pathto}[0]{\overset{*}{\rightarrow}}
\newcommand{\npathto}[1]{\overset{#1}{\rightarrow}}

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. 

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

integer arithmetic. Let $\PV$ be a finite set of program variables and $\TV$ be
a finite set of temporary variables. Together they form the set of variables $\V
:= \PV \union \TV$. 

integer arithmetic. Let $V$ be a finite set of variables. 

Constraints are a subset of FO formulas and thus the semantics according to the
semantics of FO-formulas. 

Constraints are a subset of FO-formulas and thus the semantics are defined
accordingly. 

    A constraint $c \in \C$ is \textit{satisfiable} when the formula $\varphi=
    c$ is satisfiable in $\Zs$ or $\Zs \models c$. We say a variable assignment

    A constraint $c \in \C$ is \textit{satisfiable} when the formula $c$ is
    satisfiable in $\Zs$ or $\Zs \models c$. We say a variable assignment

    \beta) \models \LAnd{c_i \in \C} c_i$. 

    \beta) \models \LAnd_{c_i \in \C} c_i$. 

\models \LAnd_{c_i \in C} c_i$ and $(\Zs, \beta)\models \LAnd {c_i \in C} c_i$,
respectively. Furthermore, we use conjunctions and sets of constraints
interchangeably. 

\models \LAnd_{c_i \in C} c_i$ and $(\Zs, \beta)\models \LAnd_{c_i \in C} c_i$,
respectively.
\begin{definition}[Solutions]
    Let $\varphi$ be an FO-formula. $\llbracket \varphi \rrbracket$ is defined
    as the set of all satisfying assignments or the \textit{solutions} of the
    formula $\varphi$.
    Correspondingly, $\llbracket c \rrbracket$ and $\llbracket C \rrbracket$ are
    the solutions of the constraint $c \in \C$ and the set of constraints $C
    \subset \C$, respectively.
\end{definition}
The following properties hold. Hence, we use conjunctions and sets of
constraints interchangeably.
\begin{align*}
    \llbracket c_1 \Land c_2 \rrbracket &= \llbracket c_1 \rrbracket \intersect
    \llbracket c_2 \rrbracket \\
    \llbracket C \rrbracket &= \llbracket \LAnd_{c_i \in C} c_i \rrbracket \\
        &=  \Intersect_{c_i \in C} \llbracket c_i \rrbracket
\end{align*}
\begin{definition}[Equivalence]
    Two formulas, constraints, or set of constraints are considered equivalent,
    when there solutions are equal. We write $\varphi_1 \equiv \varphi_2$.
\end{definition}

<, \leq, \geq$ can be transformed into equivalent constraints $e' < 0 \in \C$. 

<, \leq, \geq$ can be transformed into equivalent constraints $e' < 0 \in \C$: 

Hence, we will use the all operators above, wherever it improves readability, 

Hence, we will use the all operators above, whenever it improves readability, 

% Solutions
The we define $\llbracket c \rrbracket$ as the set of all satisfying assignments
of the constraint $c$ and $\llbracket C \rrbracket$ as the set of all satisfying
assignments for $C$. The following holds:
\begin{equation*}
    \llbracket C \rrbracket = \Intersect_{c_i \in C} \llbracket c_i \rrbracket
\end{equation*}

Example: $X < 0 \Land Y \leq X$ entails $Y \leq 1$.

Example: $X < 1 \Land Y \leq X$ entails $Y \leq 0$.

Since we are talking about probabilistic programs, we will need tools to
represent probabilities throughout the program. For example a variable in a
probabilistic program can take a random value. That means that the value
assigned to a variable is not deterministic but chosen at random from a given
distribution. 
The field of probability and random variables is well studied. We will only
introduce the core concepts needed to understand this thesis and follow the

% Since we are talking about probabilistic programs, we will need tools to
% represent probabilities throughout the program. For example a variable in a
% probabilistic program can take a random value. That means that the value
% assigned to a variable is not deterministic but chosen at random from a given
% distribution. 
The field of probability and random variables is well studied. Only the core 
concepts needed to understand this thesis will be introduced, following the

will refere to the literature. 

will refer to the literature. 

        \item $P$ assignes a probability to every event and satisfies the

        \item $P$ assigns a probability to every event and satisfies the

            \todo{Refere to a definition of a $\sigma$-algebra.}

            \todo{Refer to a definition of a $\sigma$-algebra.}

For random program variables in this thesis, $\Omega$ will be the set of
integers and $\mathcal{F}$ the maximal $\sigma$-field in $\Omega$, the powerset
$2^\Omega$. However since the program variables are chosen at random, a
specific path over a given program can also be considered a random event in the
probability space and hence be considered as a ransom variable. In this case
$\Omega$ is the set of all runs $\mathcal{Runs}$. The exact definition will be
introduced later on in \Sref{}.

% For random program variables in this thesis, $\Omega$ will be the set of
% integers and $\mathcal{F}$ the maximal $\sigma$-field in $\Omega$, the power-set
% $2^\Omega$. However since the program variables are chosen at random, a specific
% path over a given program can also be considered a random event in the
% probability space and hence be considered as a ransom variable. In this case
% $\Omega$ is the set of all runs $\mathcal{Runs}$. The exact definition will be
% introduced later on in \Sref{}.

The general concept of random variables is not to be confused with program
variables (that can take random values). Random variables assign a probability
to an event of a probability space. 

The concept of random variables is not to be confused with program
variables or variables in formulas. Random variables assign a probability
to an event of a probability space, whereas variables in formulas can be bound
to a value by an assignment or existentially quantified. 

    A random variable on a probability space $(\Omega, \F, \P)$ is a 

    A random variable on a probability space $(\Omega, \F, \P)$ 

\todo{remark: the following relations do not consider the satisfiability but
only the mere existence of transitions.}
For the following let $P=(\V, L, GT, l_0)$ be \gls{pip}.
\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, \nu, l)$. 
\end{definition}
\begin{definition}[Path relations]
    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. 

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

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