UprightFont={* Light},

UprightFont={*},

\usepackage[ngerman,english]{babel}
%
% Acronyms
\PassOptionsToPackage{acronym}{glossaries}
\usepackage{glossaries}

\PassOptionsToPackage{ngerman,english}{babel}
\RequirePackage{babel}

\usepackage{cite}

\RequirePackage{url}

\PassOptionsToPackage{backend=biber,style=numeric}{biblatex}

\PassOptionsToPackage{backend=biber,style=numeric,citestyle=numeric-comp,sorting=ynt,defernumbers=true,url=false}{biblatex}

\PassOptionsToPackage{pdfversion=2.0}{hyperref}

\PassOptionsToPackage{pdfversion=2.0,hidelinks}{hyperref}

% \RequirePackage{caption}

% Acronyms
% must be loaded after hyperref
\PassOptionsToPackage{acronym,nomain,automake,nonumberlist,toc}{glossaries}
\RequirePackage{glossaries}
\RequirePackage{glossary-longragged} 
% Captions

\urlstyle{same}

\newtheorem{apdxtheoreminner}{Theorem}
\newenvironment{apdxtheorem}[1]{%
  \renewcommand\theapdxtheoreminner{#1}%
  \apdxtheoreminner
}{\endapdxtheoreminner}

\newtheorem{apdxlemmainner}{Lemma}
\newenvironment{apdxlemma}[1]{%
  \renewcommand\theapdxlemmainner{#1}%
  \apdxlemmainner
}{\endapdxlemmainner}

% Acronyms with glossaries
\input{acronyms}
\makeglossaries

    \frontmatter

    \input{acronyms}
    \frontmatter

    \printacronyms
    \chapter{Appendix}\label{ch:appendix}
    \input{ch6_appendix}

% TeX root = ../main.tex
\begin{tikzpicture}[program]
    \node[state,initial]    (l0)                     {$l_0$};
    \node[state]            (l1)    [below=of l0]    {$l_1$};
    \node[state]            (l2)    [below left =of l1]    {$l_2$};
    \node[state]            (l3)    [below=of l2]    {$l_3$};
    \node[state]            (l4)    [below right=of l3]    {$l_4$};
    \node[state]            (l5)    [right=of l4]    {$l_5$};
    \node[state]            (l6)    [above right=of l5]    {$l_6$};
    \node[state]            (l7)    [above=of l6]    {$l_7$};
    \node[state]            (l8)    [above left=of l7]    {$l_8$};
    \node[state]            (l9)    [below right=of l2]    {$l_9$};
    \node[state]            (l10)    [right=of l9]    {$l_{10}$};
    % \path[->]    (l0)    edge node[swap]    {$\textit{true}$}  (l1)
    %              (l1)    edge node[swap]    {$x > 0$}          (l2)
    %                      edge node[swap]    {$x \leq 0$}       (l4)
    %              (l2)    edge node[swap]    {$y > 0$}          (l3)
    %                      edge node[swap]    {$\begin{aligned}
    %                                              y &\leq 0 \\
    %                                              x &:= x-1 \\
    %                                              z &:= z+2 \\
    %                                           \end{aligned}$}   (l1)
    %              (l3)    edge node[swap]    { \begin{aligned}%
    %                                              x &:= x+y \\
    %                                              y &:= y-1
    %                                           \end{aligned}}   (l3)
                                              ;
\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=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}

    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [right=3cm of l0] {$l_1$};
    \node[state] (l2) [right=3cm of l1] {$l_2$};

    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state] (l1) [right=4cm of l0] {$\ell_1$};
    \node[state] (l2) [right=4cm of l1] {$\ell_2$};

    \path[->]   (l0) edge node {$t_1:\textit{true}$} (l1)
                (l1) edge node {$t_3:x \leq 0$}      (l2)

    \path[->]   (l0) edge node {$t_1: \tau = \texttt{true}$} (l1)
                (l1) edge node {$t_3: \tau = x \leq 0$}      (l2)

                         x &> 0 \\
                         x &:= x - \textsc{Bern}(0.5)

                         \tau&= x > 0 \\
                         \eta(x)&= x - \textsc{Bern}(0.5)

    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [right=3cm of l0] {$l_1$};
    \node[state] (l2) [right=3cm of l1] {$l_2$};

    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state] (l1) [right=4cm of l0] {$\ell_1$};
    \node[state] (l2) [right=4cm of l1] {$\ell_2$};

    \path[->]   (l0) edge node {$t_1:\textit{true}$} (l1)
                (l1) edge node {$t_5:x \leq 0$}      (l2)

    \path[->]   (l0) edge node {$t_1:\tau = \texttt{true}$} (l1)
                (l1) edge node {$t_5:\tau = x \leq 0$}      (l2)

                     left] {$t_2:\begin{aligned} p&=0.5 \\ x &> 0 \\ x&:=

                     left] {$t_2:\begin{aligned} p&=0.5 \\ \tau&= x > 0 \\ \eta(x)&=

                     edge[in=35,out=80,looseness=15,draw=rot-75] node[above right] {$t_3:\begin{aligned}
                         p&=0.5 \\x &> 0 \\ x&:=
                     x+2\end{aligned}$} (l1)
                     edge[loop below] node  {$t_4:\begin{aligned} x &> 0 \\ x&:=
                     x-1\end{aligned}$} ()

                     edge[in=35,out=80,looseness=15,draw=rot-75] node[above
                     right] {$t_3:\begin{aligned} p&=0.5 \\\tau &= x > 0 \\
                     \eta(x)&= x+2\end{aligned}$} (l1)
                     edge[loop below] node  {$t_4:\begin{aligned} \tau&= x > 0
                     \\ \eta(x)&= x-1\end{aligned}$} ()

    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [right=3cm of l0] {$l_1$};
    \node[state] (l2) [right=3cm of l1] {$l_2$};

    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state] (l1) [right=4cm of l0] {$\ell_1$};
    \node[state] (l2) [right=4cm of l1] {$\ell_2$};

    \path[->]   (l0) edge node {$t_1:\textit{true}$} (l1)

    \path[->]   (l0) edge node {$t_1: \tau = \texttt{true}$} (l1)

                    x & > 0 \\
                    1 &\leq t \leq 3 \\
                    x &:= x - t

                    \tau&= x > 0  \Land 1 \leq t \leq 3 \\
                    \eta(x)&= x - t

                (l1) edge node {$t_3:x \leq 0$}      (l2)

                (l1) edge node {$t_3: \tau = x \leq 0$}      (l2)

    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [right=3cm of l0] {$l_1$};
    \node[state] (l2) [right=3cm of l1] {$l_2$};

    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state] (l1) [right=4cm of l0] {$\ell_1$};
    \node[state] (l2) [right=4cm of l1] {$\ell_2$};

    \path[->]   (l0) edge node {$t_1:\textit{true}$} (l1)
                (l1) edge node {$t_4:x \leq 0$}      (l2)
                     edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                     x+1\end{aligned}$} ()
                     edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                     x-1\end{aligned}$} ()

    \path[->]   (l0) edge node {$t_1:\tau = \texttt{true}$} (l1)
                (l1) edge node {$t_4:\tau = x \leq 0$}      (l2)
                     edge[loop above] node {$t_2:\begin{aligned} \tau&= x > 1 \\
                     \eta(x)&= x+1\end{aligned}$} ()
                     edge[loop below] node  {$t_3:\begin{aligned} \tau&= x > 0 \\
                     \eta(x)&= x-1\end{aligned}$} ()

% TeX root = ../main.tex
{
\RestyleAlgo{plain}
\SetAlgoNoLine
\LinesNotNumbered 
\begin{algorithm}[H]
    $x = u$\;
    \lIf{$1 \leq x \leq 3$}{ $x = x+1 \oplus_\frac{1}{2} x = x$}
    \lWhile{$1 \leq x \leq 3$}{ $x = x+1 \oplus_\frac{1}{2} x = x$ }
    \lWhile{$y \geq 0$}{ $y = y-1 \oplus_\frac{1}{2} y = y$ }
\end{algorithm}
}

% TeX root = ../main.tex
\begin{tikzpicture}[program,initial above,font=\scriptsize]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [below=2cm of l0] {$l_1$};
    \node[state] (l1a) at ($(l1) - (3,1.5)$) {$l_{1a}$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};
    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [out=140,in=120,looseness=2,draw=rot-75]
        node[below=0.3cm,pos=0.35] {$t_{1a}:\begin{aligned} \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1) edge [out=130,in=130,looseness=2,draw=rot-75] node[above,pos=0.4] {$t_{1b}:\begin{aligned} \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [out=150,in=210,looseness=10] node[swap]{$\begin{aligned}
            t_{1b}:& \\ \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [bend right=15] node[swap] {$t_{2b}: \begin{aligned}\tau &= y > 0 \\
        &\Land w = 1\end{aligned}$} (l2)
        (l1) edge[bend left =20] node {$\begin{aligned}t_{2a}:& \\ \tau =& y > 0 \\
        \Land& w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=20] node {$\begin{aligned}&t_3:\\ &\eta(y) = y - 1\end{aligned}$} (l1)
                % (l1) edge node {$t_4:x \leq 0$}      (l2)
                %      edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                %      x+1\end{aligned}$} ()
                %      edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                %      x-1\end{aligned}$} ()
                    ;
\end{tikzpicture}

\begin{algorithm}
    \SetNoline
    \LinesNotNumbered 

{
\RestyleAlgo{plain}
\SetAlgoNoLine
\LinesNotNumbered 
\begin{algorithm}[H]

    \lWhile{$2 \leq x \leq 3$}{
        $x = x+1 \oplus_\frac{1}{2} x = x$\;

    \lWhile{$1 \leq x \leq 3$}{
        $x = x+1 \oplus_\frac{1}{2} x = x$

        $y = y-1 \oplus_\frac{1}{2} y = y$\;

        $y = y-1 \oplus_\frac{1}{2} y = y$

}

% TeX root = ../main.tex
\begin{tikzpicture}[program,initial above,font=\scriptsize]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [below=2cm of l0] {$l_1$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};
    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [out=110,in=150,looseness=10,draw=rot-75]
        node[swap]{$t_{1a}:\begin{aligned} p&=0.5 \\ \tau&= 1 \leq x \leq 3
        \Land w = 0\end{aligned}$} (l1)
        (l1) edge [out=160,in=200,looseness=10,draw=rot-75]
        node[swap]{$ t_{1b}: \begin{aligned}p&=0.5 \\ \tau&= 1 \leq x \leq 3
        \Land w = 0 \\ \eta(x)&= x + 1\end{aligned}$} (l1)
        (l1) edge[bend left =30] node {$t_{2}:\begin{aligned}\tau =& y > 0
        \Land w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=30] node {$t_{3}:\begin{aligned} 
            p&=0.5 \\ \eta(y) &= y - \textsc{Bern}(0.5)
        \end{aligned}$} (l1)
        % (l2) edge[bend left=30,draw=rwth-75] node[swap] {$t_{3a}: p=0.5$} (l1)
                % (l1) edge node {$t_4:x \leq 0$}      (l2)
                %      edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                %      x+1\end{aligned}$} ()
                %      edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                %      x-1\end{aligned}$} ()
                    ;
\end{tikzpicture}

\begin{algorithm}
    \SetNoline
    \LinesNotNumbered 

{ 
\RestyleAlgo{plain}
\SetAlgoNoLine
\LinesNotNumbered 
\begin{algorithm}[H]

    \lIf {$1 \leq x \leq 3$}{$x = x + 1$\;}
    \lWhile{$2 \leq x \leq 3$}{ $x = x + 1$\; }
    \lWhile{$y \geq 0$}{ $y = y + 1$\; }

    \lIf{$1 \leq x \leq 3$}{$x = x + 1$}
    \lWhile{$2 \leq x \leq 3$}{ $x = x + 1$}
    \lWhile{$y \geq 0$}{ $y = y + 1$}

}

% TeX root = ../main.tex
\begin{tikzpicture}[program,initial above,font=\scriptsize]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [below=2cm of l0] {$l_1$};
    \node[state] (l1a) at ($(l1) - (3,1.5)$) {$l_{1a}$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};
    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [bend right=15] node[swap] {$t_{1a}:\begin{aligned} \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [out=150,in=210,looseness=10] node[swap]{$\begin{aligned}
            t_{1b}:& \\ \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [bend right=15] node[swap] {$t_{2b}: \begin{aligned}\tau &= y > 0 \\
        &\Land w = 1\end{aligned}$} (l2)
        (l1) edge[bend left =20] node {$\begin{aligned}t_{2a}:& \\ \tau =& y > 0 \\
        \Land& w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=20] node {$\begin{aligned}&t_3:\\ &\eta(y) = y - 1\end{aligned}$} (l1)
                % (l1) edge node {$t_4:x \leq 0$}      (l2)
                %      edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                %      x+1\end{aligned}$} ()
                %      edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                %      x-1\end{aligned}$} ()
                    ;
\end{tikzpicture}

\begin{algorithm}
    \SetNoline
    \LinesNotNumbered 

{
\RestyleAlgo{plain}
\SetAlgoNoLine
\LinesNotNumbered 
\begin{algorithm}[H]

    \lWhile{$1 \leq x \leq 3$}{ $x = x + 1$\; }
    \lWhile{$y \geq 0$}{ $y = y - 1$\; }

    \lWhile{$1 \leq x \leq 3$}{ $x = x + 1$}
    \lWhile{$y \geq 0$}{$y = y - 1$}

}

% TeX root = ../main.tex
\begin{tikzpicture}[program,initial above,font=\scriptsize]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [below=2cm of l0] {$l_1$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};
    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [out=150,in=210,looseness=10] node[swap]{$\begin{aligned}
            t_1:& \\\tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1)
        (l1) edge[bend left =30] node {$\begin{aligned}t_{2}:& \\ \tau =& y > 0 \\
        \Land& w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=30] node {$t_3: \eta(y) = y - 1$} (l1)
                % (l1) edge node {$t_4:x \leq 0$}      (l2)
                %      edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                %      x+1\end{aligned}$} ()
                %      edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                %      x-1\end{aligned}$} ()
                    ;
\end{tikzpicture}

\begin{apdxlemma}{\ref{lem:entailment}}\label{apdx:lem:entailment}
    $\varphi_1$ entails $\varphi_2$ if and only if $\varphi_1 \Land
    \neg\varphi_2$ is unsatisfiable.
    \begin{proof}
        \enquote{$\Rightarrow$} Let $\varphi_1$ entails $\varphi_2$, and assume
        an assignment $\beta: \V \rightarrow \Z$ exists such that $\beta \models
        \varphi_1 \Land \neg \varphi_2$. 
        \begin{align*}
            \Rightarrow &\beta \models \varphi_1 \\
            \Rightarrow & \beta \in \llbracket \varphi_1 \rrbracket \\
            \Rightarrow & \beta \in \llbracket \varphi_2 \rrbracket \\
            \Rightarrow & \beta \models \varphi_2 \\
            \Rightarrow & \beta \not\models \neg\varphi_2 \\
            \Rightarrow & \beta \not\models \varphi_1 \Land \neg\varphi_2 \lightning
        \end{align*}
        By contradiction $\varphi_1 \Land \neg\varphi_2$ is unsatisfiable.
        \enquote{$\Leftarrow$} Let $\varphi_1 \Land \neg\varphi_2$ is
        unsatisfiable and assume $\llbracket \varphi_1 \rrbracket \not\subseteq
        \llbracket \varphi_1 \rrbracket$. There exists an assignment 
        \begin{align*}
            & \beta \in \llbracket \varphi_1\rrbracket \\
            \Rightarrow&\beta \models \varphi_1 \\
        \end{align*}
        and 
        \begin{align*}
            &\beta \not\in\llbracket\varphi_2\rrbracket \\
            \Rightarrow& \beta \not\models \varphi_2 \\
            \Rightarrow& \beta \models \neg\varphi_2
        \end{align*}
        Combined $\beta \models \varphi_1 \Land\neg \varphi_2 \lightning$ 
        By contradiction $\varphi_1$ entails $\varphi_2$.
    \end{proof}
\end{apdxlemma}
\begin{apdxlemma}{\ref{lem:nonprop_update}}\label{apdx:lem:nonprop_update}
    Given an assignment $s\in\Sigma$, a formula $\varphi$ and an update $u: A
    \rightarrow \Z[\V]$. Without loss of generality $A' = \set{x'}{x \in A}$ is
    a set of fresh variables with $A' \cap \V = \emptyset$. We define
    $u(\varphi) := ((\varphi \Land \LAnd_{x\in A} x' = u(x))|_{A'})[x'/x]_{x\in
    A}$. For any partial assignment $s' = u(s)|_A$ and if $s \models \varphi$,
    then $s' \models u(\varphi)$.
    \begin{proof}
        \begin{align}
            s' &\models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x]_{x\in A} \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x]_{x\in A}[x/s'(x)]_{x\in A} \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/s'(x)]_{x\in A}\label{eq:chaining_subst}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/s'(x)]_{x\in A} \label{eq:dropping_projection}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/\bigl(\rho_u(s)\bigr)(x)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/\bigl(u(x)\bigr)(s)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models
            (\varphi[x'/\bigl(u(x)\bigr)(s)]_{x_\in A}) \Land (\LAnd_{x\in A}
            x'[x'/\bigl(u(x)\bigr)(s)]_{x_\in A} = u(x)[x'/\bigl(u(x)\bigr)(s)]_{x\in
            A}) \nonumber\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} x'[x'/\bigl(u(x)\bigr)(s)] =
            u(x) \label{eq:dropping_substitutions}\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} \bigl(u(x)\bigr)(s) = u(x)\nonumber\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)] =
            u(x)\label{eq:definition_of_update}\\
            \Leftarrow & \models
            \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}\\
            \Leftrightarrow & \models
            (\varphi\Land \LAnd_{x\in A} u(x) = u(x))[x/s(x)]
            \label{eq:dedup_substitution}\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\nonumber\\
            \Leftrightarrow s & \models \varphi\label{eq:assumption}
        \end{align}

        Equation \ref{eq:chaining_subst} holds, because the substitutions can be
        chained. Equation \ref{eq:dropping_projection} holds, because the
        projection removed no variables contained in the substitution. Hence they
        are just implicitly existentially quantified and not affected otherwise.
        In equation \ref{eq:dropping_substitutions} the substitutions can be
        removed, because $\varphi$ and $u(x)$ do not contain any affected
        variables, as they were freshly generated. In Equation
        \ref{eq:definition_of_update} the update is just replaced by it's
        definition. Equation \ref{eq:adding_model} holds because if $s$ is a
        model for the formula, the formula is satisfiable. The inverse is not
        necessary true. Applying the substitution $[x/s(x)]$ a second
        time, does nothing in Equation \ref{eq:dedup_substitution} because
        $s(x) \in \Z$ and specifically do not contain any variables $x\in A$.
        Afterwards, the substitution is moved to the outside. Equation
        \ref{eq:assumption} holds by assumption.
    \end{proof}
\end{apdxlemma}

projections of constraints and handling polyhedra we recurred \gls{apron} and
the \gls{ppl}\cite{bagnara2008socp}, which can be used as an abstract domain in
apron.

projections of constraints and handling polyhedra we recurred
\gls{apron}\cite{apron} and the \gls{ppl}\cite{bagnara2008socp}, which can be
used as an abstract domain in apron.

The Algorithm \ref{alg:cfr_pip} which applies control-flow-refinement via

Both the Algorithm \ref{alg:cfr_pip} which applies control-flow-refinement via

which evaluates a set of transitions in a program, where implemented natively in 
\gls{ocaml}.

which evaluates a set component of a program, where implemented. 

to performance reasons, but made available through a new sub command
\texttt{cfr}. It might be used by other tools in the future, that want to profit
from partial evaluation on probabilistic programs. 

to performance reasons, but made available through a new sub command. It might
be used by other tools in the future, that want to profit from partial
evaluation on probabilistic programs. 

\subsection{Loops}
\subsection{Sub-\gls{scc} evaluation}
% \begin{comment}
    % Base Algorithm 
    % fun find_loops_in(P)
    %     loop_heads = {}
    %     // Dijkstra
    %     on loop_back from l' -> l_h:
    %         loop_heads := loop_heads + l_h
    %     return loop_heads
    % end

    % fun heuristic(L: Loop)
    %     // same as original paper
    % end
    % fun partial_evaluation(Program P = (PV, L, GT, l_0))
    %     let lh := loop_heads(P)
    %     let properties := heuristic(P)
    %     let initial_state := (l_0, [])
    %     let P' := ({l_0}, l_0, {locations: P.l_0, {}) // todo
    %     for gt in GT: 
    %         let gt' = {}
    %         for t in gt: 
    %             (s', l_t') := evaluate(P, s, t)
    %             if l_t \in lh:
                    
    %             else : 
    %             gt' := gt' + 
    %         end
    %     end
    % Claims: 
    % Every path in P has an equivalent path in the evaluation graph EG
    % Every path in EG has an equivalent path in P'
    % SCC Algorithm:
    % similar to above but stops at SCC boundaries. 
% \end{comment}
% \section{Modules}
% \section{Command-Line Interface}
% The techniques described above were implemented natively in Koat2. They are
% available as part of the normal analysis via the flags \texttt{--cfr-native}.
% The old option for control-flow refinement \texttt{--cfr} was renamed to
% \texttt{--cfr-ir}, and can probably be removed in the future. 
% During normal analysis the control-flow refinement is done on every \gls{scc}
% and the bounds of the resulting scc is compared to the previous bounds. 
% A full program can be refined using the native control-flow refinement with a
% separate command \texttt{cfr}. For the new control-flow refinement the option is
% added to switch between the various method to select location for abstraction
% and the abstraction method itself (see \Sref{sec:abstraction}). An summary of
% the compatible options is given in \tref{tab:options}. 

\subsection{Selecting the Abstract domain}
In the implementation, the projection is computed using an abstract domain.
Thanks to the \gls{apron}\cite{apron} library, the new implementation is generic
over the specific abstract domain used. We decided to use the abstract domain of
polyhedra (see. \Sref{ssec:polyhedra}), since they are exact on linear
constraints. In practice only small components are partially evaluated, making
the performance disadvantage acceptable. \gls{apron} uses the
\gls{ppl}\cite{bagnara2008socp} under the hood for polyhedra. Other abstract
domains supported by \gls{apron} might be used in the future. In addition to the
projection operation, the library supports updates as-well, which is used when
possible. The \gls{ppl} ignores all non-linear constraints, over-approximating
the set of constraints in the process. In turn the projection is
over-approximated as well. One could decide to over-approximate non-linear
constraints manually, in order to achieve tighter projections. For example
quadratic polynomials have an easy to compute minimum and maximum, which could
be transformed into a single linear constraint. 

% As discussed in \Sref{sec:updateinvariants} the polyhedra computed during
% evaluation are tighter than the invariants computed during preprocessing. In
% order to update the invariants after the partial evaluation a new option
% \texttt{--update-invariants} is added and activated by default. 

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

% \begin{table}
%     \center
%     \begin{tabular}[ccc]
%         \hline
%         \begin{comment}
%         analysis --cfr=native,update-invariants,     --o
%                  --cfr=irankfinder,
%                  --cfr=off

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

%         prob-analysis --cfr=native

\subsection{Property-based abstraction}
We implemented the property based abstraction (recall
\Sref{sec:property_based_abstraction}) proposed by
\citeauthor{domenech2019arxiv}. The heuristic uses backwards-propagation as one
source of properties. Our implementation applies the backwards-propagation for
every loop a location marked for abstraction is on, possibly aggregating
properties from multiple loops.

%         cfr --native
%             --irankfinder
%         \end{comment}

The properties are projected onto the program variables, in order to reduce
their number, and because values for temporary variables do not propagate
throughout the program. The entailment checks of properties are done using
Z3 and Lemma \ref{lem:entailment}. Since a set of constraints is checked
against many properties, an incremental solver is used in order avoid
recomputing the model for the set of constraints every time.
Once a set of constraints is abstracted, it is replaced by the set of entailed
properties. 

%         \hline
%     \end{tabular}
%     \caption{}
% \end{table}

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

\gls{koat}s analysis goal is to find tight upper bounds for \gls{pip}. The
analysis techniques used such as \acrfull{mprf}, have their limits and cannot
always find tight bounds for every program, which motivates control-flow
refinement in order to find an equivalent program to the original one, that
opens the possibility for the analysis to find tighter runtime-complexity
bounds. 

\gls{koat}s analysis goal is to find tight upper bounds for \gls{pip} and
possibly non-probabilistic and non-deterministic integer programs that are a
specialization of the first. The analysis techniques used such as
\gls{mprf},\todo{more} have their limits and cannot always find tight bounds for
every program, which motivates control-flow refinement in order to find an
equivalent program to the original one, that opens the possibility for the
analysis to to find tighter bounds. 

Recall \ref{def:runtime_complexity}; the newly constructed refined program shall
have they have the same worst-case expected runtime complexity as the original
program which implies that runtime-complexity bounds found for the refined
program are also runtime-complexity bounds for the original one. Naturally the
control-flow refinement will add and replace transitions and locations, hence
the number runtime-complexity bounds and size-bounds of each transition won't
be preserved. However we will show, that each transition in the refined program
is a similar to a transition in the original program and hence every run in the
new program has a run of equal runtime-complexity and probability in the
original program and vice-versa.

Recall \ref{def:overallcomplexity}; the newly constructed refined program shall
have they have the same overall runtime complexity as the original program,
which implies that complexity bounds found for the refined program are also
complexity bounds for the original one. 
Naturally the control-flow refinement will add and replace transitions and
locations, hence the runtime and size complexity per each transition won't be
preserved. However we will show, that each transition in the refined program is
a copy of a transition in the original program, and that complexity of an
original transition is equal to the sum of its copies.

evaluation presented by \citeauthor{domenech2019arxiv}\cite{domenech2019arxiv}
for \acrlong{pip}. The partial evaluation will be constructed in a similar
way but explicitly taking probability and general transitions into account. 

evaluation technique presented by
\citeauthor{domenech2019arxiv}\cite{domenech2019arxiv} for \acrlong{pip}. The
partial evaluation will be constructed in a similar way but explicitly taking
probability and general transitions into account. 

possibly infinite evaluation tree is constructed that will finally be collapsed
into a finite evaluation graph by an abstraction layer. 

possibly infinite evaluation graph is constructed that will finally be collapsed
into a finite evaluation graph by the use of an abstraction layer. 
Afterwards we will show that the partial evaluation is sound for \gls{pip} and
prove that the expected runtime-complexity is preserved and thus also the
worst-case runtime-complexity of non-probabilistic programs.
\begin{example}
    \begin{figure}
        \centering
        \input{figures/ch1_prob}
        \caption{Representation of $\Prog_3$, a variataion of $\Prog_2$ from
        \fref{fig:prob_c}, as a transition graph, with non-deterministic
        branching.\label{fig:ex_prob}}
    \end{figure} 
    The examples in this chapter will follow through using a variation of the
    probabilistic program $\Prog_2$ from the introduction (\fref{fig:prob_c}),
    which we call $\Prog_3$. $\Prog_3$ is visually represented as a transition
    graph in \fref{fig:ex:prob}. The program uses a set of variables $\V =
    \{x,y,u,w\}$ and has the program variables $\PV_{\Prog_3} = \{x,y\}$. $u,w$
    are temporary variables whose values reassigned by the scheduler on every
    transition and whose values do not propagate throughout the program.

Afterwards we will show that the partial evaluation is sound for probabilistic
integer programs and prove that the overall expected runtime complexity
(\cref{def:past}) is equally preserved as the overall (worst-case) runtime
complexity (\cref{def:runtimebounds}).

    In transition $t_0$ the value of $x$ is set by non-deterministic sampling
    via the temporary variable $u$. At location $\ell_1$ the scheduler decides
    between one of the general transitions $g_1 = \{t_{1a}, t_{1b}\}$ or $g_2 =
    \{t_2\}$, and assigns the value for $w$ accordingly. 
    The program can alter between the loops non-deterministically after every
    iteration. Since both loops are independent of one another, the
    non-determinism doesn't change anything about the expected
    runtime-complexity of the program.
    On the general transition $g_1 = \{t_{1a}, t_{1b}\}$ at location $\ell_1$
    the program branches probabilistically, with a probability of $p=0.5$. On
    the transition $t_3$, the value with which $y$ is decremented is sampled
    probabilistically from a Bernoulli distribution, where both possible
    outcomes have the same probability $p=0.5$.
\end{example}

During a normal execution a program visits one location after another and
changes state with every transition. The configuration at a given point of the
execution  can be described by tuple of location and assignment. Simulating
every possible run of a program from every possible starting state is
impossible: First, the number of starting states is infinite; second the
program is not guaranteed to terminate and hence the simulation of a specific
run might not terminate either. 
For non-deterministic and probabilistic programs, the problem get's even more
complex, since the transition taken does not only depend on the current state
but also on the answer of the scheduler and some random event. 
Instead of simulating every single possible run, it would be nice to treat
\enquote{similar} states as one. Instead of simulating a single assignment, 
the set of all possible assignments after a step is described by a polyhedron. 
The resulting graph is called a \textit{partial evaluation graph}. It was
formalized for \gls{chc} by \citeauthor{gallagher2019eptcs}. In this thesis the
definitions are adapted to better fit the algorithm and the formalisms of
\Glspl{pip}. 

During a normal execution a program visits locations one after another and
changes its state with every transition. The configuration at a given point of
the execution can be described by tuples of locations and assignments.
Simulating every possible run of a program from every possible starting state is
impossible: First, the number of starting states is infinite; second the program
is not guaranteed to terminate and hence the simulation of a specific run might
not terminate either.
For non-deterministic and probabilistic programs, the problem gets even more
complex, since the transition taken do not only depend on the current state but
also on the answer of the scheduler and some random event. Instead of simulating
every single possible run, it would be nice to treat \emph{similar} states as
one. Instead of simulating a single assignment, the set of all possible
assignments after a step is described by a set of constraints. The resulting
graph is called a \emph{partial evaluation graph}. It was formalized for
\glspl{chc} by \citeauthor{gallagher2019eptcs}\cite{gallagher2019eptcs}. In this
thesis the definitions are adapted to better fit the algorithm and the formalism
of \Glspl{pip}. 

In order to guarantee termination, as will be elaborated further later on, a
finite set of abstracted values (not to be confused with abstract domains, such
as polyhedra etc.) is required. For now the set of abstracted values shall be a
finite set $\A \subset \C$.

% In order to guarantee termination of the refinement, as will be elaborated further later on, a
% finite set of abstracted values (not to be confused with abstract domains, such
% as polyhedra etc.) is required. For now the set of abstracted values shall be a
% finite set $\A \subset \C$.

Given a \gls{pip} $\Prog$ with locations $\Loc$, transitions $\T$ and general
transitions $\GT$, the versions are the vertices of the partial evaluation
graph. A version is composed of location from $\Loc$ and either an abstracted
value or a non-abstracted constraint. 

% Given a \gls{pip} $\Prog$ with locations $\Loc$, transitions $\T$ and general
% transitions $\GT$, the versions are the vertices of the partial evaluation
% graph. A version is composed of location from $\Loc$ and either an abstracted
% value or a non-abstracted constraint. 

    The set of \textit{constraint versions} is the set of tuples over the
    locations $L$ from $P$ and constraints $\C$. The set of \textit{abstract
    versions} is the set of tuples over the locations $L$ from $P$ and some
    finite abstraction space $A\subseteq\C$. Since the set of locations and the
    abstraction space are both finite, so are the abstract versions. The set of
    versions is the union of constraint and abstract versions. 

    The set of \textit{versions} is the set of tuples over the
    locations $\Loc_\Prog$ and constraints $\C$:

        \vers = (\Loc \times \C) \union (\Loc \times A)

        \vers_\Prog = (\Loc_\Prog \times \C).

For clarity sake, versions will be denoted with angles $\langle \cdot
\rangle$. Since elements of the abstraction space are constraints as well.
The set notation with curly braces is used for explicitly abstracted
constraints like so $\langle l, \{\psi_1, \dots\}\rangle$ and the formula
notation without brackets is used for non-abstracted values like so $\langle
l, \varphi\rangle$. An abstracted version can be lifted to a non-abstracted
version trivially.

% For clarity sake, versions will be denoted with angles $\langle \cdot
% \rangle$. Since elements of the abstraction space are constraints as well.
% The set notation with curly braces is used for explicitly abstracted
% constraints like so $\langle l, \{\psi_1, \dots\}\rangle$ and the formula
% notation without brackets is used for non-abstracted values like so $\langle
% l, \varphi\rangle$. An abstracted version can be lifted to a non-abstracted
% version trivially.

Every version describes a subset of configurations of the program $P$. We write 
$\llbracket \langle l, \varphi \rangle \rrbracket$ for the set of
configurations $\set{(l,\_,s)}{s \models \varphi}$. 

% Every version describes a subset of configurations of the program $P$. We write 
% $\llbracket \langle l, \varphi \rangle \rrbracket$ for the set of
% configurations $\set{(l,\_,s)}{s \models \varphi}$. 

The edges of the partial evaluation graph are transitions $\T_{PE}$ analogously
defined to Definition \ref{def:pip}, except that they connect versions and not
locations.

The versions are the edges/locations of the partial evaluation graph. The edges
of the partial evaluation graph are transitions $\T_{PE}$ analogously defined to
Definition \ref{def:pip}, except that they connect versions and not locations.

A \Gls{pip} $P$ can be lifted to a trivial partial evaluation graph by replacing
every location $l \in L$ by the trivial version $\langle l,
\textit{true}\rangle$. Obviously the lift of program is not useful for the
analysis, as it doesn't capture any interesting properties of the program,

A \Gls{pip} $P$ can be lifted to a trivial partial evaluation graph by
replacing every location $\ell \in \Loc_\Prog$ by the trivial version $\langle
\ell, \texttt{true}\rangle$. Obviously the lift of a program is not useful for
the analysis, as it doesn't capture any interesting properties of the program,

\langle l', \varphi'\rangle$ is computed by unfolding a transition $t \in \T$
from the original \gls{pip} that starts in the same location $l \in \Loc$ as the
version $v = \langle l, \varphi\rangle$. The resulting constraint $\phi'$
contains all states $s' \in \Sigma$ with $s' \models \varphi'$ reachable via the
transition from a state in the source version, i.e. $\prSs((l, s, \_)
\rightarrow (l',s',t)) > 0$. 

\langle l', \varphi'\rangle \in \vers_\Prog$ is computed by unfolding a
transition $t \in \T_\Prog$ from the original \gls{pip} that starts in the same
location $\ell \in \Loc$ as the source version $v = \langle \ell, \varphi\rangle
\in \vers_\Prog$. The resulting constraint $\varphi'$ contains all states $s'
\in \Sigma$ with $s' \models \varphi'$ wich are reachable via the transition $t$
from a state $s \models \varphi$ in the source version, i.e., $\prSs((\ell, s, \_)
\rightarrow (\ell',s',t)) > 0$. 

    An unfolding operation $\unfold : \C \times (\PV \rightarrow
    \Z[\V\union\D)]) \rightarrow \C$ of a formula $\varphi \in \C$ with an
    update $\eta: \PV\rightarrow\Z[\V \union \D]$ is defined as 

    An unfolding operation $\unfold : \Phi_\PV \times (\PV \rightarrow
    \Z[\V\union\D)]) \rightarrow \Phi_\PV$ of a formula $\varphi \in \Phi_\PV$
    with an update $\eta: \PV\rightarrow\Z[\V \union \D]$ is defined as 

        \unfold(\varphi, \eta) = \begin{cases}
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)|_{\PV} & \text{if }
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil) \text{ is
            SAT}\\ 
            \textit{false} & \text{otherwise}
        \end{cases}

        \unfold(\varphi, \eta) = \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)

    For any $\varphi\in2^\C$, assignments $s, s' \in \Sigma$ and probabilistic
    update $\eta : \PV \rightarrow \Z[\V\union\D]$, if $\models\varphi$ then

    For any $\varphi\in\Phi_\PV$, probabilistic update $\eta : \PV \rightarrow
    \Z[\V\union\D]$, if there exists an $s\in \Sigma$ with $s\models\varphi$
    then

        \item \label{itm:unfold1} $\models\unfold(\varphi, \eta)$. 
        \item \label{itm:unfold2} If additionally $s \models \varphi$ and $s' \in
            \support_s(\eta)$,
            then $s' \models \unfold(\varphi, \eta)$.

        \item \label{itm:unfold1} $\unfold(\varphi, \eta)$ is satisfiable.
        \item \label{itm:unfold2} If $s' \in \support_s(\eta)$ for some $s' \in
            \Sigma$, then $s' \models \unfold(\varphi, \eta)$.

        Let $\varphi\in2^\C$, $s, s' \in \Sigma$, $s \models \varphi$ and $s'

        Let $\varphi\in\Phi_\PV$, $s, s' \in \Sigma$, $s \models \varphi$ and $s'

         $\models\unfold(\varphi, \eta)$ follows directly from the existence of
         $s \models \varphi$ due to satisfiability and $s' \in \support_s(\eta)$
         since the support cannot be empty. 

        The satisfiability of $\unfold(\varphi, \eta)$ follows directly from the
        existence of $s \models \varphi$ due to satisfiability and $s' \in
        \support_s(\eta)$ since the support cannot be empty. 

\begin{example}
    Consider transition $t_3$ of $\Prog_3$ from \fref{fig:ex_prob}. $t_3$
    has an probabilistic update $\eta(y) = y - \textsc{Bern}(0.5)$ and
    implicitly $\eta(x) = x$. 
    Imagine a constraint $y > 0$, that is unfolded with the probabilistic update
    $\eta$. The update is approximated by $(\tilde{\eta},\lfloor\eta\rceil)$
    with
    \begin{align*}
        \tilde{\eta}(x) &= x' \\
        \tilde{\eta}(y) &= y' \\
        \lfloor\eta\rceil &= (x' = x \Land y' = y - d \Land 0 \leq d \leq 1)
    \end{align*}

    The unfolding computes the following new constraint.
    \begin{align*}
        \tilde{\eta}(\varphi \Land \lfloor\eta\rceil) &= \tilde{\eta}(x > 0 \Land
        x' = x \Land y' = y - d \Land 0 \leq d \leq 1) \\
        &= (y > 0 \Land x' = x \Land y' = y - d \Land 0 \leq d \leq 1 \Land x'' =
        x' \Land y'' = y')|_{\PV''}[x''/x]_{x\in\PV}\\
        &= (y'' \geq 0)[x''/x]_{x\in\PV'}\\
        &= (y \geq 0)
    \end{align*}
    Any satisfying assignment for $\varphi$ must assign $y$ a value larger than
    zero and after the update, the value of the assignment must be larger or
    equal to zero. Since $x$ is neither constrained before the update nor
    updated in any way, it remains unconstrained after the unfolding.
\end{example}

Using the unfolding, one can derive an unfolding operation $\unfold^*: \vers
\times \T \rightarrow 2^{\T_{PE}}$ that constructs a new transition between the
versions copying the guard $\tau$, update $\eta$, and probability $p$ from the
original transition. Since unsatisfiable versions cannot be reached they are
ignored and no transition is created. 

Using the unfolding, one can derive an unfolding operation $\unfold:
\vers_\Prog \times \T \rightarrow 2^{\T_{PE}}$ that constructs a new transition
between the versions copying the guard $\tau$, update $\eta$, and probability
$p$ from the original transition. 
% Since unsatisfiable versions cannot be
% reached they are ignored and no transition is created. 
% \begin{align*}
%     \unfold^*(\langle l,\varphi\rangle, t) = 
%     \begin{cases}
%         \{(\langle \ell, \varphi\rangle, p, \tau\Land\varphi, \eta,\langle \ell',\varphi'\rangle
%         \} & \text{if } \begin{aligned}[t]
%             &t = (\ell, p, \tau, \eta, \ell')\text {, and} \\
%             &\varphi' = \unfold(\varphi \land \tau, \eta) \text{ is SAT}
%         \end{aligned} \\
%         \emptyset & \text{ otherwise}
%     \end{cases}
% \end{align*}
\begin{align*}
    \unfold(\langle l,\varphi\rangle, t) = 
        \{(\langle \ell, \varphi\rangle, p, \tau\Land\varphi, \eta,\langle \ell',\varphi'\rangle
        \} \\ \text{ for } t = (\ell, p, \tau, \eta, \ell')\text { and } 
            \varphi' = \unfold(\varphi \land \tau, \eta)
\end{align*}

We define a function $\unfold_\T(T) : 2^{\T_{PE}} \rightarrow 2^{\T_{PE}}$ that
unfolds all target versions $\langle \ell, \varphi \rangle$ of the transitions
with each outgoing transitions $t \in \Tout(\ell)$. 

    \unfold^*(\langle l,\varphi\rangle, t) = 
    \begin{cases}
        \{(\langle l, \varphi\rangle, p, \tau, \eta,\langle l',\varphi'\rangle
        \} & \text{if } \begin{aligned}[t]
            &t = (l, p, \tau, \eta, l'), p \in [0,1], \tau \in 2^\C,\\
            &\eta: \PV \rightarrow \Z[\V\union\D]\text {, and} \\
            &\varphi' = \unfold(\varphi \land \tau, \eta) \text{ is SAT}
        \end{aligned} \\
        \{\} & \text{ otherwise}
    \end{cases}

    \unfold

\begin{lemma} [Existance, Similarity, Reachability of unfolded transitions]
    \label{lem:existance_and_similarity}
    Let $l \in \Loc_\Prog$, $t' \in \T_\Prog$, $s \in \Sigma$, and $\varphi$ be
    an \gls{fo}-formula over variables $\PV$. Moreover let $t = (l, p, \tau,
    \eta, l')$ with locations $l' \in \Loc_\Prog$, a probability $p \in
    [0,1]$ and an update $\eta: \PV \rightarrow \Z[\V\union\D]$.

\begin{lemma} [Existence, Similarity, Reachability of unfolded transitions]
    \label{lem:existence_and_similarity}
    Let $\ell \in \Loc_\Prog$, $t' \in \T_\Prog$, $s \in \Sigma$, and $\varphi$
    be an \gls{fo}-formula over variables $\PV$. Moreover, let $t = (\ell, p,
    \tau, \eta, \ell')$ with locations $\ell' \in \Loc_\Prog$, a probability $p
    \in [0,1]$ and an update $\eta: \PV \rightarrow \Z[\V\union\D]$.

    If $s|\PV \models \varphi \Land \tau$ and $l = l_1$ then:

    If $s|\PV \models \varphi \Land \tau$ and $\ell = \ell_1$ then:

                \unfold^*(\langle l, \varphi\rangle, t) = \{t^*\},

                \unfold^*(\langle \ell, \varphi\rangle, t) = \{t^*\},

                t^* = (\langle l, \varphi\rangle, p, \tau, \eta, \langle l',
                \varphi'\rangle) \text{ for some }\varphi' \in \C,

                t^* = (\langle \ell, \varphi\rangle, p, \tau, \eta, \langle \ell',
                \varphi'\rangle) \text{ for some }\varphi' \in \Phi,

        \ref{lem:existance_and_similarity}. 

        \ref{lem:existence_and_similarity}. 

        \ref{lem:existance_and_similarity} $t_i$ and $t'_i$ are similar. 

        \ref{lem:existence_and_similarity} $t_i$ and $t'_i$ are similar. 

                \uIf {$v' \not\in V(G$\label{alg:naive_line_inclusion}}{

                \uIf {$v' \not\in V(G)$\label{alg:naive_line_inclusion}}{

                    $G \leftarrow evaluate(\Prog, G, v')$\;

                    $G \leftarrow \FEvaluate{G, v'}$\;

<<<<<<< 1

                        $G \leftarrow evaluate(G, v')$\;

                        $G \leftarrow \FEvaluate{G, v'}$\;

    \ref{lem:existance_and_similarity} $t=(\langle l_n, \varphi_n\rangle, p,

    \ref{lem:existence_and_similarity} $t=(\langle l_n, \varphi_n\rangle, p,

    \ref{lem:existance_and_similarity} $s_{n+1} \models \varphi_{n+1}$. 

    \ref{lem:existence_and_similarity} $s_{n+1} \models \varphi_{n+1}$. 

For the sub-SCC level evaluation Algorithm \ref{alg:abstr_eval} is adapted to
stop the evaluation when leaving the component and instead of starting only from
the initial location of the program, the evaluation starts from every
entrytransition to the program. The exact algorithm is displayed in Algorithm
\ref{alg:eval_component}.
\begin{algorithm}
    \caption{Evaluate the component $S \subseteq \T_\Prog$ of a Program $\Prog$
    with abstraction $\alpha$.\label{alg:eval_component}}
    \KwData{ A \gls{pip} $\Prog$, component $S$, abstraction function $\alpha$,
    and abstraction oracle $S_\alpha$}
    \KwResult{A Graph $G$, and a set of pairwise disjunct general transitions
    $\GTG \subset \GT_\text{PE}$}
    $\ET \leftarrow \Tout(S)$\;
    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    $\GTG \leftarrow \emptyset$\;
    \Fn{\FEvaluate{$G$, $v$}}{
        $\langle l, \varphi\rangle \leftarrow v$\;
        \For{$g \in \GTout(l)$} {
            $g' \leftarrow \unfold^*(v, g)$\label{alg:abstr_line_unfold_g}\;
            \If {$g^* \neq \emptyset$ \label{alg:abstr_line_filteremptyg}}{
                $g^* \leftarrow \emptyset$\;
                \For{$t = (v, p, \tau, \eta, \langle l', \varphi\rangle) \in g$}{
                    \uIf {$g \in \ET$} {
                        $t \leftarrow (v, p, \tau, \eta, \langle l',
                        \texttt{true}\rangle)$\label{alg:abstr_line_exit}\;
                    }
                    \ElseIf {$S_\alpha$} {
                        $t \leftarrow (v, p, \tau, \eta, \langle l',
                        \alpha(\varphi)\rangle)$\label{alg:abstr_line_abstraction}\;
                    }
                    $g^* \leftarrow g^* + t$\label{alg:abstr_line_addtog}\;
                    \uIf {$v' \not\in V(G)$}{
                        $G \leftarrow G + t$\;
                        $G \leftarrow \FEvaluate{G, v'}$\;
                    }
                    \Else {
                        $G \leftarrow G + t$\label{alg:abstr_line_addt}\;
                    }
                }
                $\GTG \leftarrow \GTG + g^*$\;
            }
        }
        \Return {$G$}
    }
    $G \leftarrow \text{ graph of }\Prog \text{ lifted to a partial evaluation
    graph}$\;
    $G \leftarrow G - S$\;
    \For{$t = (\ell, p, \tau, \eta, \ell')\in \Tin(S)$} {
        $G \leftarrow \FEvaluate{$G, \langle\ell',\texttt{true}\rangle $}$ \;
    }
    \Return $G, \GTG$
    
\end{algorithm}
The partial evaluation starts at every entry transition $\T_in(S)$ to the
component. When unfolding an exit transition $t = (\ell, \_, \_, \_, \ell') \in
\Tout(S)$ from a version $\langle \ell, \varphi\rangle$, to $\unfold^*(\langle
\ell, \varphi\rangle, t) = \{(\langle\ell,\varphi\rangle, \_, \_, \_,
\langle\ell', \varphi'\rangle)\}$ the target version
$\langle\ell',\varphi'\rangle$ is replaced by the trivial overapproximation
$\langle\ell',\texttt{true}\rangle$. This target is always already contained in
the program, by construction and the algorithm always backtracks. 
Lets cosider an admissible finite prefix $f \in \fpath_\Prog$ with 
\begin{align*}
    f &= c_0c_1\dots{}c_k\dots{}c_m\dots{}c_n \\
      &=
      (\ell_0,t_\in,s_0)(\ell_1,t_1,s_1)\dots\underbrace{(\ell_k,t_k,s_k)\dots(\ell_m,t_m,s_m)}_{t_k,\dots,t_m
      \in S}\dots(\ell_n,t_n,s_n)
\end{align*}
with an infix $c_m\dots{}c_k$ going through the component.

By construction, up to the component the partial evaluation $\Prog'$ contains a
similar prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})
\in \fpath_{\Prog'}$. The component is entered via the transition
$t_k\in\Tin(S)$ which is was used as a starting point for the evaluation with
the trivial version $\langle\ell_{k-1}, \texttt{true}\rangle$ in Algorithm
\ref{alg:eval_component}. By the same argument as in Theorem
\ref{thm:correctness}, a similar prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})(\langle\ell_k,\varphi_k\rangle,t_k,s_k)\dots(\langle\ell_{m-1},\varphi_{m-1}\rangle,t_{m-1},s_{m-1})
\in \fpath_{\Prog'}$ through the component exists in $\Prog'$. The exit
transition $t_m$ must have been unfolded before backtracking and afterwards the
similar prefix trivially follows the lifted versions again, yielding a similar
finite prefix
$(\langle\ell_0,\texttt{true}\rangle,t_\in,s_0)(\langle\ell_1,\texttt{true}\rangle,t_1,s_1)\dots(\langle\ell_{k-1},\texttt{true}\rangle,t_{k-1},s_{k-1})(\langle\ell_k,\varphi_k\rangle,t_k,s_k)\dots(\langle\ell_{m-1},\varphi_{m-1}\rangle,t_{m-1},s_{m-1})(\langle\ell_m,\texttt{true}\rangle,t_m,s_m)\dots(\langle\ell_n,\texttt{true}\rangle,t_n,s_n)
\in \fpath_{\Prog'}$.

For any finite prefix visiting the component more than once, the similar finite
prefix of $\Prog'$ is found by making the argument above multiple times.
\section{Foo}

\subsection{Constructing the scheduler}

\subsection{Induction}

        $l$ & locations \\

        $\ell$ & locations \\

domain $A' \subseteq A$ is denoted by $f|A' : A' \rightarrow B$.

domain $A' \subseteq A$ is denoted by $\varf|_{A'} : A' \rightarrow B$.

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

\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 of the
    formula $\varphi$.
\end{definition}

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

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}.
Constraints are a subset of formulas in \gls{fo} logic, thus, there semantics
shall be defined accordingly using the $\models$ and $\equiv$ relation from
\gls{fo} logic.\cite{barwise1977}  
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$.

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

\begin{definition}[Entailment\cite{Domenech19}]

\begin{definition}[Entailment\cite{Domenech19}]\label{def:entailment}

\begin{lemma}

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

    \begin{proof}
        \enquote{$\Rightarrow$} Let $\varphi_1$ entails $\varphi_2$, and assume
        an assignment $\beta: \V \rightarrow \Z$ exists such that $\beta \models
        \varphi_1 \Land \neg \varphi_2$. 
        \begin{align*}
            \Rightarrow &\beta \models \varphi_1 \\
            \Rightarrow & \beta \in \llbracket \varphi_1 \rrbracket \\
            \Rightarrow & \beta \in \llbracket \varphi_2 \rrbracket \\
            \Rightarrow & \beta \models \varphi_2 \\
            \Rightarrow & \beta \not\models \neg\varphi_2 \\
            \Rightarrow & \beta \not\models \varphi_1 \Land \neg\varphi_2 \lightning
        \end{align*}
        By contradiction $\varphi_1 \Land \neg\varphi_2$ is unsatisfiable.

        \enquote{$\Leftarrow$} Let $\varphi_1 \Land \neg\varphi_2$ is
        unsatisfiable and assume $\llbracket \varphi_1 \rrbracket \not\subseteq
        \llbracket \varphi_1 \rrbracket$. There exists an assignment 
        \begin{align*}
            & \beta \in \llbracket \varphi_1\rrbracket \\
            \Rightarrow&\beta \models \varphi_1 \\
        \end{align*}
        and 
        \begin{align*}
            &\beta \not\in\llbracket\varphi_2\rrbracket \\
            \Rightarrow& \beta \not\models \varphi_2 \\
            \Rightarrow& \beta \models \neg\varphi_2
        \end{align*}
        Combined $\beta \models \varphi_1 \Land\neg \varphi_2 \lightning$ 
        By contradiction $\varphi_1$ entails $\varphi_2$.
    \end{proof}

    \proof{see Appendix on page \pageref{apdx:lem:entailment}.}

The inverse operation is to add new variables and trivial, since it only
requires to add the new variables to the set of used variables.

An update assigns a value to variable after the update using the values of

An update assigns a value to a variable after the update using the values of

Let $\Z[\V]$ be the set of integer polynomials over variables $\V$ and $\Sigma =
\set{s : A \rightarrow \Z}{A \subseteq \V}$ be the set of full integer
assignments.
For an integer polynomial $f\in\Z[\V]$ and a full assignment $s \in \Sigma$ we
write $f(s)$ for the value that is found by fully evaluating the polynomial
$f[x_i/s(x_i)]$. \todo{restrict to full assignments?}

Let $\Sigma = \{s : \V \rightarrow \Z\}$ be the set of full integer
assignments, that are assignments which assign a value to every variable
$v\in\V$. In contrast, partial assignments over a variable set $A \subseteq \V$
assign values only to a subset of variables, set set of partial assignments over
the variables $A\subseteq\V$ is denoted by $\Sigma_A = \{s: A \rightarrow \Z\}$.
For an integer polynomial $f\in\Z[A]$ over a variable set $A \subseteq \V$ and a
assignment $s \in \Sigma_A$ we write $\varf(s)$ for the value that is found by
evaluating the polynomial $\varf[x_i/s(x_i)]_{x\in A}$.

    An update is described by an update function $u : A \rightarrow \Z[\V]$ that
    maps every updated variable to a polynomial expression over $\V$. The value
    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.

    Let $A,B \subseteq \V$. An update is described by an update function $u : A
    \rightarrow \Z[B]$ that maps every updated variable to a polynomial
    expression over $B$. The value of a variable $x\in A$ \textit{after} the
    update for an assignment $s\in\Sigma_B$ is determined by
    $\bigl(u(x)\bigr)(s)$. Note, that $u(x) \in \Z[\V]$ is a polynomial and
    $\bigl(u(x)\bigr)(s) \in \Z$ is the evaluation of that polynomial.

full assignment $s : \V \rightarrow \Z$, we write $u(s) : A \rightarrow \Z$ for
the partial assignment found by assigning every updated variable to it's value
after the update. 

assignment $s \in \Sigma$, we define a function $\rho_u: \Sigma \rightarrow
\Sigma_A$. It computes the assignment after an update $u$ given an assignment
$s \in \Sigma$ before the update:

\begin{equation}
    u(s)(x) = \begin{cases} 
        u(x)(s) & \text{if } x \in A \\
        \text{undefined} & \text{otherwise}
    \end{cases}
\end{equation}

\begin{equation*}
    \bigl(\rho_u (s)\bigr)(x) = \bigl(u(x)\bigr)(s) \text{ for all } x\in A.
\end{equation*}

\begin{lemma}\label{lem:nonprop_update}
    Given a full assignment $s\in\Sigma$, a
    formula $\varphi$ and an update $u: A \rightarrow \Z[\V]$. Without loss of
    generality $A' = \set{x'}{x \in A}$ is a set of fresh temporary
    variables. We define $u(\varphi) := ((\varphi \Land \LAnd_{x\in A} x' =
    u(x))|_{\PV'})[x'/x]$. For any partial assignment $s' = u(s)|A$
    and if $s \models \varphi$, then $s' \models u(\varphi)$.

\begin{example}
    Consider the update $u : \{x\} \rightarrow \Z[\{x,y\}]$ with $u(x) = x\cdot
    y+1$. Let $s\in\Sigma_{\{x,y\}}$ assign $s(x) = 2$ and $s(y)=3$
    \textit{before} the update. \textit{After} the update
    $\bigl(\rho_u(s)\bigr)(x) = 2 \cdot 3 + 1 = 7$
\end{example}

    \begin{proof}
        \begin{align}
            s' &\models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x] \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x][x/s'(x)] \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/s'(x)] \label{eq:chaining_subst}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/s'(x)]_{x\in A} \label{eq:dropping_projection}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/u(s)(x)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/u(x)(s)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models
            (\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
            A}) \nonumber\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} x'[x'/u(x)(s)] =
            u(x) \label{eq:dropping_substitutions}\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} u(x)(s) = u(x)\nonumber\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)] =
            u(x)\label{eq:definition_of_update}\\
            \Leftarrow & \models
            \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}\\
            \Leftrightarrow & \models
            (\varphi\Land \LAnd_{x\in A} u(x) = u(x))[x/s(x)]
            \label{eq:dedup_substitution}\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\nonumber\\
            \Leftrightarrow s & \models \varphi\label{eq:assumption}
        \end{align}

\begin{lemma}\label{lem:nonprop_update}
    Let $A, B \subseteq \V$. Given an assignment $s\in\Sigma$, a formula
    $\varphi \in \Phi$ and an update $u: A \rightarrow \Z[B]$. Without loss of
    generality $A' = \set{x'}{x \in A} \subset \V$ is a set of fresh variables
    with $A' \cap (A \union B) = \emptyset$. We define $u(\varphi) := ((\varphi
    \Land \LAnd_{x\in A} x' = u(x))|_{A'})[x'/x]_{x\in A}$. For any partial
    assignment $s' = \rho_u(s)|_A$ and if $s \models \varphi$, then $s' \models
    u(\varphi)$.

        Equation \ref{eq:chaining_subst} holds, because the substitutions can be
        chained. Equation \ref{eq:dropping_projection} holds, because the
        projection removed no variables contained in the substitution. Hence they
        are just implicitly existentially quantified and not affected otherwise.
        In equation \ref{eq:dropping_substitutions} the substitutions can be
        removed, because $\varphi$ and $u(x)$ do not contain any affected
        variables, as they were freshly generated. In Equation
        \ref{eq:definition_of_update} the update is just replaced by it's
        definition. Equation \ref{eq:adding_model} holds because if $s$ is a
        model for the formula, the formula is satisfiable. The inverse is not
        necessary true. Applying the substitution $[x/s(x)]$ a second
        time, does nothing in Equation \ref{eq:dedup_substitution} because
        $s(x) \in \Z$ and specifically do not contain any variables $x\in A$.
        Afterwards, the substitution is moved to the outside. Equation
        \ref{eq:assumption} holds by assumption.
    \end{proof}

    \proof{see Appendix on page \pref{apdx:lem:nonprop_update}.}

$m$-dimensional space for variables $X \subset \V$ and $|X| = m$. Every

$m$-dimensional space for variables $X \subseteq \V$ and $|X| = m$. Every

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. 

The projection operation computes the projection of an \gls{fo} formula.
Geometrically, the projection is the set of assignments found by orthogonally
projecting every satisfying assignment onto the remaining dimensions.  

    formula $\text{proj}_X(\varphi) = x \geq -1 \land x \leq 1$.

    formula $\varphi|_X = x \geq -1 \land x \leq 1$.

Taking the definitions from \cite{bagnara2005convexpolyhedron} a set of linear
constraints exactly defines a polyhedron. Every linear non-strict inequality
constraint $\psi \in \Lin^{\leq}$ describes an closed affine half-space and every
linear strict inequality constraint $\psi \in \Lin^{\leq}$ describes an open
affine half-space in the euclidean space $\R^n$. 

Every linear non-strict inequality constraint describes an closed affine
half-space and every linear strict inequality constraint describes an open
affine half-space in the euclidean space $\R^n$. As discussed in
\Sref{sec:constraints} strictness of linear constraints and in turn openness of
half-spaces are not relevant to the integer domain.

\begin{definition}[Not necessarily closed
    Polyhedra\cite{bagnara2005convexpolyhedron}\label{def:polyhedra}]
    $\mathcal{P} \subseteq \R^n$ is a closed (convex) polyhedron if and only if
    it can be expressed by an intersection of a finite number of not necessarily
    closed affine half-spaces.

\begin{definition}[Convex Polyhedra\cite{bagnara2005convexpolyhedron}\label{def:polyhedra}]
    $\mathcal{H} \subseteq \N^n$ is a \emph{convex polyhedron} if and only if it
    can be expressed by an intersection of a finite number of affine
    half-spaces.

As discussed in \Sref{sec:constraints} strictness of linear constraints and in
turn openness of half-spaces are not relevant to the integer domain. Hence when
talking about integer arithmetic one refers only to polyhedra.
Polyhedra can exactly only represent linear constraints. Non-linear polynomial

Polyhedra can represent linear constraints exactly. Non-linear polynomial

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.

Polyhedra will be used to compute the projection of \gls{fo}-formulas, possibly
over-approximating the constraints in the process. 

    $\mathcal{P} \subseteq \R^n$ is an octagon if and only if it can be

    $\mathcal{O} \subseteq \R^n$ is an octagon if and only if it can be

\subsection{Intervals}\label{ssec:box}
For completeness sake, let's introduce a third abstract domain: the interval
domain. A closed interval $[a,b]$ with $a, b \in \R$ for a variable $v \in \V$
can be expressed as a pair of linear constraints of the form $a \leq v$ and $v
\leq b$.

\subsection{Boxes}\label{ssec:box}
For completeness' sake, let's introduce a third abstract domain of Boxes. A
closed interval $[a,b]$ with $a, b \in \R$ for a variable $v \in \V$ can be
expressed as a pair of linear constraints of the form $a \leq v$ and $v \leq b$.

    $\mathcal{P} \subseteq \R^n$ is a box if it can be expressed by a set of
    intervals.

    $\mathcal{B} \subseteq \R^n$ is a Box if it can be expressed by a cartesian
    product $I_1 \times \dots \times I_n$ of intervals $I_1,\dots,I_n$

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

polyhedron $\mathcal{H}$ one can find a box $\mathcal{B}$ that contains the
polyhedron $\mathcal{H}$. Boxes are computationally very efficient, although
rather imprecise for most applications.

\section{Probability Theory}
% 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. 

\section{Probability Theory}\label{sec:probability}

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. 

Imagine a probabilistic experiment 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. 

the intuitive property of random event: if you can measure two subsets of
outcomes (e.g. $A = \set{ \omega \in \Omega} {\text{ coin shows head}}$, and $B
= \set{\omega \in \Omega} {\text{coin shows tail}}$) so you can for both subsets
together ($A \union B = \set{\omega \in \Omega} {\text{coin shows head or

the intuitive property of a random event: if you can measure two subsets of
outcomes (e.g. $A = \set{ \omega \in \Omega} {\text{ coin shows head}}$ and $B
= \set{\omega \in \Omega} {\text{coin shows tail}}$) so you can for the union of
both subsets ($A \union B = \set{\omega \in \Omega} {\text{coin shows head or

the individual outcomes.

the individual outcomes, if $A$ and $B$ are disjoint.

        \item $A$ is closed under complement, i.e. $B \in A$ implies $B^C \in

        \item $A$ is closed under complement, i.e., $B \in A$ implies $B^C \in

        \item $A$ is closed under countable unions, i.e. $A_1, A_2 \dots, \in A$ 

        \item $A$ is closed under countable unions, i.e., $A_1, A_2 \dots \in A$ 

    A set function $\mu$ on a $\sigma$-algebra $\F$ is a probability

    A function $\mu: \F \rightarrow [0,1]$ on a $\sigma$-algebra $\F$ is a probability

In the following, we will encounter discrete random variables $X : \Omega
\rightarrow \bar{N}$ with countably (but possibly infinitely) many possible
results.

    : \Omega \rightarrow \R$ with $\set{\omega}{X(\omega) = x} \in \F$ for every
    $x \in \R$. 

    : \Omega \rightarrow \bar{\N}$ with $\set{\omega}{X(\omega) = x} \in \F$ for every
    $x \in \bar{N}$. 

In the following, we will encounter mostly discrete random variables $X : \Omega
\rightarrow \Z$ with countably (but possibly infinitely) many possible results.

    Let $X$ be a discrete random variable. The distribution is described by the
    probability measure $\mu: \Z \rightarrow \R$ with
    \begin{align}
        \mu(A) = P(\set{\omega \in \Omega}{X(\omega) \in A})

    Let $X$ be a discrete random variable. The probability of a single value is
    well defined by the distribution $\mu:F \rightarrow [0,1]$ as follows:
    \begin{align} 
        P(X=r) = \mu(\{r\}) = P(\set{\omega \in \Omega}{X(\omega) = r}) 

The probability of a single value is well defined by the distribution as
follows: 
\begin{align}
    P(X=r) = \mu(\{r\}) = P(\set{\omega \in \Omega}{X(\omega) = r})
\end{align}

    For a random variable with a distribution $\mu$, the support is smallest set

    For a random variable with distribution $\mu: $, the support is the smallest set

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, meyer20arxiv}]
    The expected value of a discrete random variable $X$ on a probability space
    $(\Omega, \F, P)$ is the weighted sum of all values X with respect to the
    measure $P$:
    \begin{equation*}
        \E(X) = \sum_{r \in \bar{\N}} r \cdot P(X = r)
    \end{equation*}
    If $\E(X)$ does not exist, then $\E(X) = \infty$.
\end{definition}

        \{0\} & p = 1 \\

        \{1\} & p = 1 \\

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

Let $\D$ be the set of (valid) probability distributions. $\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 $[\varf{}](s)(k)$.

we write $[x_i\backslash s(x_i)]$.
The resulting polynomial $f[x_i\backslash s(x_i)]$ describes a random variable
$[f](s)$ that takes a value at random depending only on the distributions $D_1,
\dots, D_m$ within. The random variable has the following probability
distribution: 

we write $[x_i\backslash s(x_i)]$. The resulting polynomial
$\varf{}[x_i\backslash s(x_i)]$ describes a random variable $[\varf{}](s)$ that
takes a value at random depending only on the distributions $D_1, \dots, D_m$
within. The random variable has the following probability distribution: 

    [f](s)(k) &= \sum_{\substack{d_i \in \Z \\ i = 0,\dots,m}} D_1(d_1)

    [\varf{}](s)(k) &= \sum_{d \in \Z^m} D_1(d_1)

        1, & \text{if } f[x_i \backslash s(x_i)][D_i\backslash d_i] = k \\

        1, & \text{if } \varf{}[x_i /s(x_i)]_{1\leq i\leq m}[D_i/d_i]_{1\leq i\leq m} = k \\

    & = P([f](s) = k) 

    & = P([\varf{}](s) = k) 

where $f[D_i\backslash d_i]$ is a syntactical substitution of every distribution
$D_i$ by an integer value $d_i \in \Z$ for all $i = 1,\dots,m$.

\begin{example}

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

    $s(x) = 2$. $[f](s)$ is the random variable described by the polynomial $f[x/2]

    $s(x) = 2$. $[\varf{}](s)$ is the random variable described by the polynomial $f[x/2]

        [f](s)(k) = \begin{cases}

        [\varf{}](s)(k) = \begin{cases}

\begin{definition}[Probabilistic update]

\begin{definition}[Probabilistic update]\ref{def:prob_update}

The value of a random variable can approximated by a constraint for the bounds
of the support of the probability distribution. For any probability distribution
$D \in \D$ and a variable $d \in \V$, we define 
\begin{equation*}
    \lfloor D \rceil_d = \begin{cases}
        \min (\support(D)) \leq d \leq \max (\support(D)) & \text{if}
        \min(\support(D)) \text{and} \max (\support(D)) \text{ exist}, \\
        \min (\support(D)) \leq d & \text{if} \min(\support(D))
        \text{ exists}, \\
        d \leq \max(\support(D))  & \text{if} \max(\support(D)) \text{ exists},\\
        \texttt{true} & \text{otherwise}.
    \end{cases}
\end{equation*}

    Let $f \in \Z[\V\union\D]$ be a probabilistic polynomial with probability
    distributions $D_1,\dots,D_n$ used within. Then the non-probabilistic
    over-approximation of a probabilistic polynomial is defined as the tuple
    $(\lfloor f\rceil,\tilde{f})$  with
    \begin{align*}
        \lfloor f \rceil = \LAnd_{i=1,\dots,m} \lfloor D_i \rceil \\
        \tilde{f} = f[D_i/d_i] \text{ and }

    Let $A\subset\V$ and $f \in \Z[A\union\D]$ be a probabilistic polynomial
    with probability distributions $D_1,\dots,D_n$ used within. Then the
    non-probabilistic over-approximation of a probabilistic polynomial is
    defined as the tuple
    $(\lfloor f\rceil,\tilde{\varf})$  with
    \begin{align*} 
        \lfloor \varf \rceil = \LAnd_{i=1,\dots,m} \lfloor D_i \rceil_{d_i} \text{
            and }
        \\ \tilde{f} = \varf{}[D_i/d_i] 

    with fresh variables $d_1,\dots,d_m \in (\V \backslash A)$. 

\begin{example}
    Consider the same probabilistic polynomial as in Example
    \ref{ex:prob_polynomial}: $f = x^2 + \textsc{Unif}(3,5)$. The distribution
    support of the uniform distribution is bounded in both directions. 
    \begin{align*}
        \min(\support(\textsc{Unif}(3,5))) &= 3 \\
        \max(\support(\textsc{Unif}(3,5))) &= 5 \\
    \end{align*}
    Hence a variable $d$ assigned from the distribution satisfies the constraint
    $\lfloor \varf\rceil = \lfloor \textsc{Unif}(3,5)\rceil_d = 3 \leq d \leq
    5$. The distribution in the probabilistic polynomial is replaced by the
    variable $d$. We get the new approximated polynomial $\tilde{\varf} = x^2 +
    d$.
\end{example}

    Let $A\subset\PV$ be a set of variables and $\eta: A \rightarrow \Z[\V\union

    Let $A,B\subseteq\V$ be a set of variables and $\eta: A \rightarrow \Z[B\union

    \tilde{\eta}) \in \C \times (\PV \rightarrow \Z[\V])$ where 

    \tilde{\eta}) \in \C \times (A \rightarrow \Z[\V])$ where 

        \lfloor\eta\rceil = \LAnd_{x\in\PV} x' = \tilde{\eta(x)} \Land

        \lfloor\eta\rceil = \LAnd_{x\in A} x' = \tilde{\eta(x)} \Land

        \tilde{\eta}(x) = x' \hspace{1cm} \text{for all } x\in\PV

        \tilde{\eta}(x) = x' \hspace{1cm} \text{for all } x\in A

    for some fresh temporary variables $x', d_i\in \TV$.

    Without loss of generality, the fresh variables introduced by the
    over-approximation of every probabilistic polynomials can be chosen to not
    appear in the other over-approximations.

        distributions within $[\eta(x)]$. 

        distributions within $\eta(x)$. 

              &= \sum_{\substack{a_i \in \Z \\ i = 0,\dots,m}} D_1(a_1)
    \cdot D_2(a_2) \cdots D_m(a_m) \cdot 

              &= \sum_{a \in \Z^m} D_1(a_1) \cdot D_2(a_2) \cdots D_m(a_m) \cdot 

                1, & \text{if } f[x_i \backslash s(x_i)][D_i\backslash a_i] =

                1, & \text{if } \varf{}[x_i/s(x_i)][D_i/a_i] =

        \begin{align*}
            \tilde{s} = \begin{cases}
                a_i & \text{for } x = d_i, i=1,\dots,m \\
            \end{cases}
        \end{align*}

        \begin{equation*}
            \tilde{s}(x) = a_i \text{ for } x = d_i, i=1,\dots,m \\
        \end{equation*}

        By construction $s = \tilde{s}|A$. Since $d_1,\dots,d_m$ are fresh

        By construction $s = \tilde{s}|_A$. Since $d_1,\dots,d_m$ are fresh

\section{Probabilistic integer programs}

\section{Probabilistic integer programs}\label{sec:pip}

over the years to formalize integer program. The one used in this thesis is the

over the years to formalize integer programs. The one used in this thesis is the

between those locations. A run of a program is a sequence of configurations,

between those locations. A run of a program is a sequence of configurations

contains a condition, called \textit{guard}, that must be true for the current
state to be taken. Whenever a transition is taken it can modifies the state with
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. 

contains a condition $\tau$, called \textit{guard}, that must be true for the
current state to be taken. Whenever a transition is taken it can modifies the
state with some \textit{update} $\eta$. An update assigns a new value to each
program variable depending on the previous state. Every integer program starts
at a unique location usually called $\ell_0$. Whenever no transition guard is
satisfied the program terminates. The arguments to the program is given by some
starting state $s_0$, assigning a value for every program variable.
We use a graphical representation of programs, as shown in
\fref{fig:ex_pip_nd}. Updates are assign a value to every program variable,
however for better readability, the updates that preserve the value of a program
variable are omitted.

    $l_1$ with the state $\sigma(x) = 3$ both transitions $t_2$ and $t_3$ are

    $\ell_1$ with the state $s(x) = 3$ both transitions $t_2$ and $t_3$ are

    At location $l_1$ with a variable assignment $\sigma(x) = 3$ three

    At location $\ell_1$ with a variable assignment $\sigma(x) = 3$ three

    selected, a coin is through to decide whether to take $t_2$ or $t_3$.

    selected, a coin is thrown to decide whether to take $t_2$ or $t_3$.

or probabilistic, which is called non-deterministic or probabilistic
sampling. Non-deterministic sampling occurs when on a transition a variable is
updated to an expression that contains unbound variables (variables that are not
assigned a value in the previous state). The unbound variables are sampled
arbitrarily from all the integers, but can be constraint by the guard, in which
case the transition is only taken if the non-deterministic sampling fulfills the
guard. If the sampled value fulfills no transition's guard it means the program

or probabilistic, which is called non-deterministic or probabilistic sampling.
Non-deterministic sampling occurs when on a transition a variable is updated to
an expression that contains unbound variables (variables that are not part of
the set of program variables). The unbound variables are sampled arbitrarily
from all the integers, but can be constraint by the guard, in which case the
transition is only taken if the non-deterministic sampling fulfills the guard.
If the sampled value fulfills no transition's guard it means the program

    Since the temporary variable $t$ is not bound in the state $\sigma: \PV

    Since the temporary variable $t$ is not bound in the state $s: \PV

    guard of $t_2$ and x is larger then zero, the program would terminate.

    guard of $t_2$ and x is larger than zero, the program would terminate.

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

\Sref{sec:probability}. Updates are expanded to integer polynomials over with
variables and distributions. The value of the indeterminate in the polynomial is
equal to the (possibly temporary) variable or sampled from the distribution with
the corresponding probability. 

of locations, $\T = \L \times [0,1] \times (\PV \rightarrow \Z[\V\union\D)

of locations, $\T = \Loc \times [0,1] \times (\PV \rightarrow \Z[\V\union\D])

    $(\PV, \Loc_\Prog, \GT_\Prog, l_0)$ is a probabilistic integer transition system where 

    $(\PV, \Loc_\Prog, \GT_\Prog, \ell_0)$ is a probabilistic integer transition
    system where 

        \item $\Loc_\Prog$ is a finite non-empty set of location,
        \item $\GT_\Prog$ is a finite set of general transitions, where a
            general transition $g \in \GT_\Prog$ is a finite non-empty set of
            transitions $t = (l, p, \tau, \eta, \kappa, l') \in \T_\Prog \subseteq
            \GT_\Prog$ with: 

        \item $\Loc_\Prog \subseteq \Loc$ is a finite non-empty set of location,
        \item $\GT_\Prog \subseteq \GT$ is a finite set of general transitions,
            where a general transition $g \in \GT_\Prog$ is a finite non-empty
            set of transitions $t = (\ell, p, \tau, \eta, \ell') \in \T_\Prog
            \subseteq \GT_\Prog$ with: 

                \item a source and target location $l,l' \in \Loc$,

                \item a source and target location $\ell,\ell' \in \Loc$,

                \item an update function $\eta : \PV \mapsto \Z[\V \cup D]$,

                \item an update function $\eta : \PV \rightarrow \Z[\V \cup \D]$,

            transitions share a common start location which we call $l_g$.
        \item $l_0 \in L$ is the start location of the program.

            transitions share a common start location which we call $\ell_g$.
        \item $\ell_0 \in \Loc$ is the start location of the program.

Before defining the semantics of a \gls{pip} a new special location $l_\bot$ is
introduced that will be used to indicate the termination of a program as well as
a virtual transition $t_\bot$ and general transition $g_\bot = \{t_\bot\}$ with
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

Before defining the semantics of a \gls{pip} a new special location $\ell_\bot$
is introduced that will be used to indicate the termination of a program as well
as a virtual transition $t_\bot$ and general transition $g_\bot = \{t_\bot\}$
with the same purpose. Instead of just \enquote{terminating} a program takes the
transition $g_\bot$ to the location $\ell_\bot$ if and only if no other general

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

$l_\bot$ the run loops indefinitely on the location $\ell_\bot$. In addition a
new transition $t_\text{in}$ is added for the start of the program. 

defined as $\confs_\Prog = \Loc_\Prog \union \{l_\bot\} \times \T_\Prog \union \{t_{\text{in}},
t_\bot\} \times \Sigma$.
Note that additionally to the location and state, the last transition taken to
the current location is remembered as well. This won't be relevant for the partial
evaluation but is important to define the probabilistic properties of a
\gls{pip}. 

defined as $\confs_\Prog = (\Loc_\Prog \union \{\ell_\bot\}) \times (\T_\Prog
\union \{t_{\text{in}}, t_\bot\}) \times \Sigma$. Note that additionally to the
location and state, the last transition taken to the current location is
remembered as well. This won't be relevant for the partial evaluation but is
important to define the probabilistic properties of a \gls{pip}. 

set of all runs is defined as $\runs_\Prog = \confs_\Prog^\omega$. In contrast a finite
prefix is a finite sequence of configurations. The set of all finite prefixes is
defined as $\fpath_\Prog = \confs_\Prog^*$. 

set of all runs is defined as $\runs_\Prog = \confs_\Prog^\omega$. In contrast a
finite prefix is a finite sequence of configurations. The set of all finite
prefixes is defined as $\fpath_\Prog = \confs_\Prog^*$. 

decisions and is not influenced by them. It is called a \textit{Markovian
scheduler}. 

decisions and is not influenced by them. It is called a \emph{Markovian
Scheduler}. 

    Markovian (memoryless) scheduler if for every configuration $c = (l,t,s) \in

    Markovian (memoryless) scheduler if for every configuration $c = (\ell,t,s) \in

        \item $l$ is the start location $l_g$ of the general transition $g$.

        \item $\ell$ is the start location $\ell_g$ of the general transition $g$.

        \item $g = g_\bot$ and $s' = s$, if $l=l_\bot$, $t=t_\bot$, or no $g'

        \item $g = g_\bot$ and $s' = s$, if $\ell=\ell_\bot$, $t=t_\bot$, or no $g'

    $\MDS^\Prog$, where \enquote{MD} stands for \enquote{Markovian

    $\MDS_Prog$, where \enquote{MD} stands for \enquote{Markovian

    $f\in\fpath$ and configuration $c=(l,t,s) \in \confs_\Prog$, $\scheduler(fc)

    $f\in\fpath_\Prog$ and configuration $c=(\ell,t,s) \in \confs_\Prog$, $\scheduler(fc)

    by $\HDS^\Prog$, where \enquote{HD} stands for \enquote{history dependent

    by $\HDS_\Prog$, where \enquote{HD} stands for \enquote{history dependent

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

The consequence is that when considering the worst-case expected reward it
doesn't matter if one looks at history dependent or Markovian schedulers. 

the outcomes of the probabilistic event are the runs on the program. Every

the outcomes of the probabilistic experiment are the runs on the program. Every

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$

terminating state $l_\bot$ it takes the special transition $g_\bot$ indicating

terminating state $\ell_\bot$ it takes the special transition $g_\bot$ indicating

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

Let $\scheduler \in \MDS_Prog$ be a scheduler and $s_0 \in \Sigma$ 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 $\ell_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]$

        1 & \text{ if } c = (l_0, s_0, t_\text{in}) \\

        1 & \text{ if } c = (\ell_0, s_0, t_\text{in}) \\

Lets say the program ran up to a configuration $c=(l,t,s)$. The scheduler

Lets say the program ran up to a configuration $c=(\ell,t,s)$. The scheduler

the configuration $c$ with $c' = (l', t', s')$ and $t' = (l, p, \tau, \eta, \_,
l') \in g$ depends on three things: First the transition $t \in g$ is taken with
the probability $p$, second the probability that each program variable
$x\in\PV$ is updated to the value $s'(x)$ by the probabilistic update - recall
definition \ref{def:prob_update}, third that the temporary variables are

the configuration $c$ with $c' = (\ell', t', s')$ and $t' = (\ell, p, \tau,
\eta, \_, \ell') \in g$ depends on three things: First the transition $t \in g$
is taken with the probability $p$, second the probability that each program
variable $x\in\PV$ is updated to the value $s'(x)$ by the probabilistic update -
recall definition \ref{def:prob_update}, third that the temporary variables are

probability measure $\prSs: \confs^2 \rightarrow [0,1]$. 

probability measure $\prSs: \confs_\Prog^2 \rightarrow [0,1]$. 

    $\prSs(f) > 0$. A run $c_0c_1\dots \in \runs$ is \textit{admissible} if and
    only if every finite prefix $c_0\dots c_n \in\fpath_\Prog$ is admissible.

    $\prSs(f) > 0$. A run $c_0c_1\dots \in \runs_\Prog$ is \textit{admissible}
    if and only if every finite prefix $c_0\dots c_n \in\fpath_\Prog$ is
    admissible.

    ending in the location $l_\bot$.

    ending in the location $\ell_\bot$.

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

program is in the terminal location $\ell_\bot$ and the following configuration
must again be in the terminal location $\ell_\bot$. A terminating run must end with

$c_\bot=(l_\bot,t_\bot,s)$ with some assignment $s\in\Sigma$.

$c_\bot=(\ell_\bot,t_\bot,s)$ with some assignment $s\in\Sigma$.

%     For a run $c_0c_1\dots{}\in \runs^\Prog$ the \textit{costs} of $\Cost :

%     For a run $c_0c_1\dots{}\in \runs_Prog$ the \textit{costs} of $\Cost :

        \Rt(\Prog)(c_0c_1\dots) = |\set{i}{c_i = (l_i, t_i, s_i) \text{ and } t_i \neq t_\bot}|

        \Rt_\Prog(c_0c_1\dots) = |\set{i}{c_i = (\ell_i, t_i, s_i) \text{ and } t_i \neq t_\bot}|

    For a scheduler $\scheduler$ and a start location $s_0 \in \Sigma$ the
    expected runtime complexity $\Rt_{\scheduler,s_0}(\Prog)$ of a program
    $\Prog$ is defined as the expected value of the runtime complexity. 

    For a scheduler $\scheduler \in MDS_\Prog$ and a start location $s_0 \in
    \Sigma$ the expected runtime complexity $\Rt_{\scheduler,s_0}(\Prog)$ of a
    \gls{pip} $\Prog$ is defined as the expected value of the runtime
    complexity. 

        \Rt_{\scheduler,s_0}(\Prog) = \ESs(\Rt(\Prog))

        \Rt_{\scheduler,s_0}(\Prog) = \ESs(\Rt_\Prog)

    $\scheduler$ and every initial state $s_0$, then $\Prog$ is called
    \gls{past}.

    $\scheduler \in \MDS_Prog$ and every initial state $s_0 \in \Sigma$, then
    $\Prog$ is called \gls{past}.

    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