\node[state,initial]    (l0)                           {$\langle l_0, \textit{true}\rangle$};

    \node[state,initial]    (l0)                           {$\langle \ell_0, \textit{true}\rangle$};

    \node[state]            (l2)    [below right=of l1]    {$\langle l_1, x > 1 \rangle$};
    \node[state]            (l2')   [below left=of l1]     {$\langle l_2, x \leq 0\rangle$};
    \node[state]            (l3)    [below right=of l2]    {$\langle l_1, x > 2 \rangle$};
    \node[state]            (l3')   [below left=of l2,gray]{$\langle l_2, \textit{false}\rangle$};

    \node[state]            (l2)    [below right=of l1]    {$\langle \ell_1, x > 1 \rangle$};
    \node[state]            (l2')   [below left=of l1]     {$\langle \ell_2, x \leq 0\rangle$};
    \node[state]            (l3)    [below right=of l2]    {$\langle \ell_1, x > 2 \rangle$};
    \node[state]            (l3')   [below left=of l2,gray]{$\langle \ell_2, \textit{false}\rangle$};

    \path[->]   (l0)      edge      node      {$\textit{true}$}    (l1)
                (l1)      edge      node[swap]{$x \leq 0$}         (l2')
                          edge      node      {$x > 0, x := x+1$ } (l2) 

    \path[->]   (l0)      edge      node      {$\tau = \textit{true}$}    (l1)
                (l1)      edge      node[swap]{$\tau = x \leq 0$}         (l2')
                          edge      node      {$\tau = x > 0; \eta(x) = x+1$ } (l2) 

                          edge      node[]    {$x > 0, x := x+1$ } (l3)

                          edge      node[]    {$\tau = x > 0; \eta(x) = x+1$ } (l3)

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

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

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

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

                                  x &> 0 \\ x &:= x+1

                                  \tau &= x > 0 \\ \eta(x)&= x+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 [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}

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

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

        (l0) edge node { $t_0: \eta(x) = u $ } (l1)

        (l0) edge node { $t_0: \eta_0(x) = u $ } (l1)

        node[swap]{$t_{1a}:\begin{aligned} p&=0.5 \\ \tau&= 1 \leq x \leq 3

        node[swap]{$t_{1a}:\begin{aligned} p&=0.5 \\ \tau_1&= 1 \leq x \leq 3

        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

        node[swap]{$ t_{1b}: \begin{aligned}p&=0.5 \\ \tau_1&= 1 \leq x \leq 3
        \Land w = 0 \\ \eta_{1b}(x)&= x + 1\end{aligned}$} (l1)
        (l1) edge[bend left =30] node {$t_{2}:\begin{aligned}\tau_2 =& y > 0

            p&=0.5 \\ \eta(y) &= y - \textsc{Bern}(0.5)

            p&=0.5 \\ \eta_3(y) &= y - \textsc{Bern}(0.5)

\begin{algorithm}
    \caption{Evaluate a Program $\Prog$ with abstraction
    $\alpha$.\label{alg:evaluate_abstr}}
    \KwData{ A PIP $\Prog$, abstraction function $\alpha$, and
    abstraction oracle $S_\alpha$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
    \subset \GT_\text{PE}$}

    \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$}{
                    \If {$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$}
    }
    $v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
    $G \leftarrow (\{v_0\}, \emptyset)$\;
    $G \leftarrow $\FEvaluate{$G$, $v_0$}\;
    \Return $G, \GTG$
\end{algorithm}

    graph in \fref{fig:ex:prob}. The program uses a set of variables $\V =

    graph in \fref{fig:ex_prob}. The program uses a set of variables $\V =

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

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

of the partial evaluation graph are transitions $\T_{PE}$ analogously defined to
Definition \ref{def:pip}, except that they connect versions and not locations.
% \begin{definition}[Partial Evaluation]
%     A graph $G = (\vers, \T_{PE})$ is a \textit{partial evaluation} of a
%     \gls{pip} $\Prog$ when for every admissible path $c_0c_1\dots{}c_n \in
%     \fpath$ of $\Prog$ with $c_i = (l_i, s_i, t_i)$ and $t_i = (l_{i-1}, \tau_i,
%     \eta_i, p_i, l_i)$ for all $i = 1, \dots, n$, there exists a path
%     $v_0'v_1'\dots{}v_n'$ in G with the following properties:
%     \begin{enumerate}
%         \item $v'_i = (\langle l_i, \varphi_i\rangle, t_i')$ with some $\varphi_i
%             \in \C$ and $t_i' \in \T_{PE}$,
%         \item $t'_i = (\langle l_{i-i}, \varphi_{i-1}\rangle, p_i, \tau_i, \eta_i, 
%             \langle l_i, \varphi_i\rangle)$, and
%         \item $s_i \models \varphi_i$
%     \end{enumerate}
% \end{definition}

of the partial evaluation graph are transitions $\VTP$ (\enquote{$\VT$} stands
for \enquote{version transitions}) analogously defined to Definition
\ref{def:pip}, except that they connect versions and not locations. The set of
all partial evaluation graphs for a program $\Prog$ is defined as $\G_\Prog =
2^{\vers_\Prog} \times 2^{\VTP}$.

A \Gls{pip} $P$ can be lifted to a trivial partial evaluation graph by

A \Gls{pip} $\Prog$ can be lifted to a trivial partial evaluation graph by

\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,
besides what is already known in the original program. In the following we will
present a construction for a partial evaluation graph using unfolding and
abstraction.

\ell, \texttt{true}\rangle \in \vers_\Prog$. Obviously, the lift of a program is
not useful for the analysis, as it doesn't capture any interesting properties of
the program, besides what is already known in the original program. In the
following we will present a construction for a partial evaluation graph using
unfolding and abstraction.

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

\in \Sigma$ with $s' \models \varphi'$ which 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$. 

\begin{definition}[Unfolding]

\begin{definition}[Unfolding]\label{def:unfold}

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

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

\begin{rem}
    By Lemma \ref{lem:unfold} $\unfold(\varphi)$ is satisfiable if $\varphi
    \land \tau$ is satisfiable. However in practice, the projection
    over-approximates the polynomial guards and updates during projection, hence
    the inverse doesn't hold. The satisfiability check marks unreachable
    versions as such explicitly.
\end{rem}

% The exactness is relaxed in order to work with abstract domains. Instead, the
% result of unfolding an abstract value equivalent to $c$ shall contain all values
% of the constraint unfolding but possibly more. 
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)$. 
\begin{align*}
    \unfold
\end{align*}
The following lemma proves that transitions are unfolded when the guard is
satisfiable from the given version and that the unfolded transition is
\enquote{similar} to the original transition.
\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 $\ell = \ell_1$ then:
    \begin{enumerate}
        \item\label{itm:t_exists} an unfolded transition $t^* \in
            \T_\mathrm{PE}$ exists with 
            \begin{equation*}
                \unfold^*(\langle \ell, \varphi\rangle, t) = \{t^*\},
            \end{equation*}
        \item\label{itm:t_similar} the unfolded transition $t^*$ is similar to
            the original transition:
            \begin{equation*}
                t^* = (\langle \ell, \varphi\rangle, p, \tau, \eta, \langle \ell',
                \varphi'\rangle) \text{ for some }\varphi' \in \Phi,
            \end{equation*}
        \item\label{itm:new_version_contains_reachable_states} for any
            \textit{reachable} state $s'$, that is there exists a scheduler
            $\scheduler \in \MDS$ and starting state $s_0$ and transitions $t'
            \in \T_\Prog$, for which $\prSs((l, t, s) \rightarrow (l', t', s'))
            > 0$, 
            \begin{equation*}
                s' \models \varphi'.
            \end{equation*}
    \end{enumerate}

    \begin{proof}
        Let $l \in \Loc_\Prog$, $t' \in \T_\Prog$, and $\varphi \in 2^\C$ If
        $s\models \varphi \Land \tau$ then by lemma \ref{lem:unfold}
        $\models\unfold(\varphi \Land \tau, \eta)$ and by construction the
        transition is unfolded to a single transition $t^* \T_\text{PE}$ with
        $\unfold^*(\langle l, \varphi\rangle, t) = \{t^*\}$.
        The similarity follows by construction, as the properties of the
        transition are only copied from the original transition. 
        Finally let $s_0\in\Sigma$ be any starting state, $\scheduler \MDS$ any
        scheduler, and $t \in \T_\Prog$ be any transition for which
        $\prSs((l,t,s) \rightarrow (l',t',s')) > 0$.
        In \Sref{ssec:probability_space} the probability measure $\prSs$ was
        defined to be non-zero only for transitions $t' \in g'$ where $g'$ was
        selected by the scheduler $\scheduler$. That implies that some $g' \in
        \GT$ with $t' \in g'$, and $\tilde{s}\in\Sigma$ must exist with $t' =
        (l, p, \tau, \eta, l')$ for some $p \in [0,1]$, $\tau \in C$, and $\eta
        : \PV \rightarrow \Z[\V \union \D]$. 
        By Definition \ref{def:mscheduler}, $\tilde{s} \models \tau_{g'} =
        \tau$, and $s|_\PV = \tilde{s}|_\PV$. It follows that $\tilde{s} \models
        \varphi$ as $\varphi$ can contain only program variables. Furthermore,
        \begin{align*}
            0 &< \prSs((l,t,s) \rightarrow (l',t',s')) \\
            &= p \cdot \prod_{x\in\PV} [\eta(x)](\tilde{s})(s'(x))\cdot \prod_{u \in
            \V\backslash\PV} \delta_{\tilde{s},s(u)} \\
            \Rightarrow 0 &< [\eta](\tilde{s})(s'(x)) \text{ for all } x \in \PV \\
            \Rightarrow s'& \in \support_{\tilde{s}}(\eta) \\
        \end{align*}

\begin{definition}[Unfolding a transition]\label{def:unfold_t}
    Using the unfolding operation from Definition \ref{def:unfold}, an unfolding
    operation $\unfold: \vers_\Prog \times \T_\Prog \rightarrow \VTP$ is defined
    that constructs a new transition between the versions. The update and
    probability from the original transition are simply copied, while the guard
    is extended with the constraint of the source version.
    \begin{equation*}\begin{gathered} \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') \in
        \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau, \eta)
    \end{gathered}\end{equation*}
\end{definition}

        Using lemma \ref{lem:unfold} one gets $s' \models \unfold(\varphi \Land
        \tau, \eta) = \varphi'$ completing the proof.
    \end{proof}
\end{lemma}

\begin{rem}
    The unfolding is undefined for transitions that do not start in the same
    location as the version. 
\end{rem}

The operation is overloaded again with a set function $\unfold_P^*: \vers \times
\GT \rightarrow 2^{\T_{PE}}$ unfolding all transitions in a general transition.

We define a function $\evaluate_\Prog(T) : \G_\Prog \rightarrow \G_\Prog $ that
unfolds all versions $\langle \ell, \varphi \rangle$ in the graph with each
outgoing transitions $t \in \Tout(\ell)$. 

    \unfold^*(\varphi, g) = \Union_{t \in g}\unfold^*(\varphi, t)

    \evaluate_\Prog(G) = G + \set{ \unfold(\langle \ell, \varphi \rangle, t)}{
        \langle \ell, \varphi\rangle \in E(G) \text{, and } t \in
        \Tout(\ell)}

\begin{lemma}[Existance, Similarity of unfolded general transitions\label{lem:existance_and_similarity_g}]
   
    Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
    \gls{fo}-formula over variables $\PV$. Moreover let $g = {t_1, \dots,t_n}
    \in \GTP$. If $s \models \varphi \Land \tau_g$ and $l = l_g$ then:
    \begin{enumerate}
        \item\label{itm:g_exists} the unfolded general transition $g' \in \GTPE$
            is not empty with some $t'_1, \dots, t'_n \in \T_\text{PE}$
            \begin{equation*}
                g' = \unfold^*(\langle l, \varphi\rangle, g) = \{t'_1, \dots,
                t'_n\} \neq \emptyset,
            \end{equation*}
        \item \label{itm:t_in_g_similar} $t_i \in g$ are similar to $t'_i \in
            g'$  for all $i=1, \dots, n$, that is for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
                \Z[\V\union\D]$, and $l_i \in \Loc_P$:
            \begin{equation*}
                 t_i' = (\langle l_g, \varphi\rangle, p_i, \tau_g, \eta_i,
                 \langle l_i,\varphi\rangle) \text{ when } t_i = (l_g, p_i, \tau_g, \eta_i, l_i)
            \end{equation*}
    \end{enumerate}
    \begin{proof}
        Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
        \gls{fo}-formula over variables $\PV$. Moreover let $g = {t_1,
        \dots,t_n} \in \GTP$. If $s \models \varphi \Land \tau_g$ and $l = l_g$
        then: Since all transitions $t_1, \dots t_n$ have the same guard
        $\tau_g$, the non-emptiness follows immediately from Lemma
        \ref{lem:existence_and_similarity}. 
        Let $g' = \{t'_1, \dots,t'_m\} = \unfold^*(\langle l_g, \varphi\rangle,
        g)$ for some $t'_1, \dots, t'_m \in \T_\mathrm{PE}$. Every $t'_i \in g'$
        was created by some unfolding $\unfold^*(\langle l_g, \varphi\rangle,
        t_i)$ where $t_i \in g$. This implies that $n =m$ and by Lemma
        \ref{lem:existence_and_similarity} $t_i$ and $t'_i$ are similar. 
    \end{proof}
\end{lemma}
\begin{lemma}[Soundness\label{lem:unfold_g_sound}]
    Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
    \gls{fo}-formula over variables $\PV$. Let $g \in \GTP$ and $g' =
    \unfold(\langle l, \varphi\rangle, g)$. If $g' \neq \emptyset$ then $g'$ is
    a sound general transition with $\tau_{g'} = \tau_g$, and starting location
    $l_{g'} = \langle l_g, \varphi\rangle$.
    \begin{proof}
        By construction $g'$ is only an non-empty set if one transition is
        unfolded and then all transitions are unfolded. Due to the similarity
        shown by lemma \ref{lem:existance_and_similarity_g} all unfolded
        transitions have probabilities adding up to 1, share the same guard
        $\tau_{g'} = \tau_{g}$, and the same starting location $l_{g'} = \langle
        l_g, \varphi\rangle$
    \end{proof}
\end{lemma}
% Lemma \ref{lem:existance_and_similarity_g} implies that if the transition is
% unfolded to a non-empty set, the unfolded set is a sound general transition,
% with a single guard $\tau_{g'}$ used by all transitions of all 
% \begin{lemma}\label{lem:unfold_g}
%     Let $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s, s'
%     \in \Sigma$ assignments, and let $\varphi \in \C$ be a constraint.
%     Furthermore let $g' \in \GT$ be the general transition containing $t'$. If
%     $s \in \llbracket\varphi\rrbracket$ and $\prSs((l,t,s) \rightarrow
%     (l',t',s')) > 0$ for any scheduler $\scheduler$ and starting state $s_0 \in
%     \Sigma$ then 
%     \begin{equation*}
%         \unfold(\varphi, t') \subseteq \unfold^*(\varphi, g') \neq \emptyset
%     \end{equation*}
%     \begin{proof}
%         Follows immediately from the existance asserted in Lemma
%         \ref{lem:existance_and_similarity}.
%     \end{proof}
% \end{lemma}
% \begin{lemma}[Soundness\label{lem:unfold_sound}]
%     For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g = \{t_1,
%     \dots{},t_n\} \in \GTP$ with guard $\tau_g$. Either $unfold(\langle l,
%     \varphi\rangle, g) = \emptyset$ or $unfold(\langle l, \varphi\rangle, g) =
%     \{t_1', \dots{},t_n'\}$ where for all $i=1,\dots{},n$:
    % \begin{enumerate}
    %     \item $\{t_i'\} = \unfold^*(\langle l, \varphi\rangle,t_i)$,
    %     \item $t_i' = (\langle l, \varphi\rangle, p_i, \tau_g, \eta_i,
    %         \kappa_i,\langle l',\varphi\rangle)$ when $t_i = (l, p_i, \tau_g, \eta_i,
    %         \kappa_i, l')$ for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
    %         \Z[\V\union\D]$, $\kappa_i\in\R$, and $l' \in \Loc_P$.
    % \end{enumerate}
    % This implies especially that the probabilities of transitions $t_1' \dots
    % t'_n$ add up to 1.

    % \begin{proof}
    %     Let $g = \{t_1, \dots, t_n\} \in \GTP$ with $t_i =
    %     (l_g,p_i,\tau_i,\eta_i,\kappa_i,l'_i)$. 

For a program $\Prog$ with a initial location $\ell_0$, the unfolding is
bootstrapped at the initial version $\langle \ell_0, \texttt{true}\rangle$ as
this version represents all valid starting configurations of the program. Let
$G_0 = (\{\langle \ell_0, \texttt{true}\rangle\}, \emptyset)$.

    %     By Definition \ref{def:pip} all transitions $t_1,\dots t_n$share the
    %     same guard $t_i = t_g$ for all $i=1,\dots,n$. All transitions are
    %     unfolded exactly once by construction. If $\models \varphi \Land
    %     \tau_g$, then by Lemma \ref{lem:supp_update_not_empty} and Lemma
    %     \ref{lem:prob_update} so is $ \models \tilde{\eta}(\varphi \Land \tau_g
    %     \lfloor\eta\rceil)$. Hence by Lemma \ref{lem:unfold} all $\models
    %     \unfold(\varphi \Land \tau_g, \eta_i)$ and $\unfold^*(\langle l,
    %     \varphi\rangle, t_i) = \{t_i'\}$ for some $t_i \in 2^{\T_\text{PE}}$ and
    %     $i=1,\dots,n$. And by Lemma \ref{lem:unfold_t_similar} they have the
    %     same probability, guard, update and cost.

Let $\evaluate^n$ be $n$ times concatenation of $\evaluate$ and $G_n$ be the
graph found by $n$ evaluation steps. 

    %     If $\not\models\varphi \Land\tau_g$, all
    %     $\not\models\unfold(\varphi\Land\tau_g, \eta_i)$ and $unfold(\langle
    %     l,\varphi\rangle,t_i) = \emptyset$ for all $i=1,\dots,n$.

\begin{equation*}
    G_n = \evaluate_\Prog^n(G_0) = \underbrace{\evaluate_\Prog \circ \cdots \circ
    \evaluate_\Prog}_{n
    \text{ times}}(T_0)
\end{equation*}

    %     The probabilities of all transition $t_1,\dots, t_n$ in the general
    %     transition $g$ add up to 1 and so do the probabilities of all
    %     transitions $t'_1,\dots,t'_n$, because the probabilities are just
    %     copied.
    % \end{proof}
% \end{lemma}

For any $V(G_n) \subseteq V(G_{n+1})$ and $E(G_n) \subseteq E(G_{n+1})$ for any
$n \in \N$. Let $G^* = \evaluate_\Prog^*$ be the limit the unfolding approaches
with an increasing number of repetitions. 

Let $\GT_\text{PE}$ be the set of general transitions over $\T_\text{PE}$. 
% The
% operation is overloaded a last time, with a function $\unfold^* : \vers
% \rightarrow 2^{\GT_\text{PE}}$ unfolding all outgoing general transitions in the
% \gls{pip} $\Prog$.

\begin{equation*}
    G^* = \evaluate_\Prog^*(G_0) = \lim_{n\rightarrow\infty}\evaluate_\Prog^n(G_0)
\end{equation*}

% \begin{align*}
%     \unfold^*(\langle l, \varphi\rangle) = \set{unfold^*(\langle l,
%     \varphi\rangle, g_i)}{g\in \GT_{out}(l)}
% \end{align*}

\begin{definition}[Evaluation Graph]
    The \emph{evaluation graph} of a program $\Prog$ with a starting location
    $\ell_0$ is defined as the graph $G^*$.
\end{definition}

Lets recap what was just constructed. A source constraint $\varphi\in\C$
describes a set of states. The unfolding computes a new (target) set of
constraint which describes a polyhedron that contains (at least) all states
reachable from the source constraint via a given transition. A version describes
a set of states at a given location. The overloaded unfolding create new
transitions between (possibly new versions), where every state reachable via an
original transition from a state in the source version, is contained in the
target version. The properties, such as probability, guard, update, and cost are
just copied, without alteration. 

In practice one can ignore unsatisfiable versions, since they cannot be reached
by the incoming transitions.

Next we will describe the evaluation algorithm, which uses the unfolding
operations to construct a (possibly infinite) evaluation graph. We will see,
that the unfolding must be adapted with an abstraction layer, to achieve finite
evaluation graphs and guarantee termination of the algorithm. The evaluation is
done recursively. The recursion starts at the start version $\langle l_0,
\textit{true}\rangle$. The evaluation unfolds all general transitions starting
at the same location as the version. It adds all created transitions to the
evaluation graph and proceeds with unfolding all newly encountered version. The
algorithm is displayed in Algorithm \ref{alg:naive_evaluation}
\begin{algorithm}
    \caption{Evaluate a Program $\Prog$.\label{alg:naive_evaluation}}
    \KwData{
        A PIP $\Prog$, Graph $G$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
    \subset \GT_\text{PE}$}
    \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)$\;
            \For{$t = (v, \tau, \eta, p, v') \in g'$}{
                \uIf {$v' \not\in V(G)$\label{alg:naive_line_inclusion}}{
                    $G \leftarrow G + t$\;
                    $G \leftarrow \FEvaluate{G, v'}$\;
                }
                \Else {
                    $G \leftarrow G + t$\;
                }
            }
            $\GTG \leftarrow \GTG + g'$\;
        }
        \Return {$G$}
    }
    $v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
    $G \leftarrow (\{v_0\}, \emptyset)$\;
    $G \leftarrow $\FEvaluate{$G$, $v_0$}\;
    \Return $G, \GTG$
\end{algorithm}
\begin{example}
    Consider the program shown in \fref{fig:ch3_inf_prog}. On the starting state
    $s_0 \in \Sigma$ with $s_0(x) = 0$, The run
    $(l_0,t_\text{in},s_0)(l_1,t_1,s_0)(l_1,t_1,s_1)(l_1,t_1,s_2)\dots$ with
    $s_i(x) = i$ for $i \in \N$ is clearly admissible and the program is stuck
    in this infinite loop on $l_1$. The evaluation would capture this behavior,
    and create the evaluation graph displayed in \fref{fig:ch3_inf_tree}. First
    the version $\langle l_0, \textit{true}\rangle$ would be evaluated over the
    transition $t_1$, resulting in a single new version $\langle l_1,
    \textit{true}\rangle$. The second unfolding steps, unfolds $\langle l_1,
    \textit{true}\rangle$ over $t_3$ to $\langle l_2, x\leq0\rangle$ and over
    $t_2$ to $\langle l_1, x>1\rangle$. $l_2$ has no outgoing transitions, and
    so the algorithm backtracks. $\langle l_1, x>1\rangle$ is unfolded to $\langle
    l_1, x>2$ over $t_2$ only since the guard of $t_3$ is not satisfiable.
    The new version is unfolded over and aver again, until end of time.

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

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

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

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

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

\end{example}

In the example above, it would be nice, if the infinite path after $\langle l_1,
x > 1\rangle$ would be condensed to a single loop, looping over a single version
$\langle l_1,x>1\rangle$ instead, but preserving the branch at $\langle l_1,
\textit{true}\rangle$. This can be achieved by abstraction. The exact
abstraction algorithm will be described in
\Sref{sec:property-based-abstraction}. For now we will define the general
properties of an abstraction. Even for always terminating programs, computing
the whole evaluation graph would be very inefficient, which motivates an
abstraction, reducing the final size of graph, while preserving the important
properties of the evaluation. 

    Consider the program shown in \fref{fig:ch3_inf_prog}. On the initial state
    $s_0 \in \Sigma$ with $s_0(x) = 0$, The run
    $(\ell_0,t_\text{in},s_0)(\ell_1,t_1,s_0)(\ell_1,t_1,s_1)(\ell_1,t_1,s_2)\dots$
    with $s_i(x) = i$ for $i \in \N$ is clearly admissible and the program is
    stuck in this infinite loop on $\ell_1$. The evaluation captures this
    behavior, and creates the evaluation graph displayed in
    \fref{fig:ch3_inf_tree}. First the version $\langle \ell_0,
    \textit{true}\rangle$ is evaluated over the transition $t_1$,
    resulting in a single new version $\langle \ell_1, \textit{true}\rangle$. The
    second unfolding steps, unfolds $\langle \ell_1,
    \textit{true}\rangle$ over $t_3$ to $\langle \ell_2, x\leq0\rangle$ and over
    $t_2$ to $\langle \ell_1, x>1\rangle$. $\ell_2$ has no outgoing transitions,
    hence no new transitions are added. 
    $\langle \ell_1, x>1\rangle$ is unfolded to $\langle \ell_1, x>2\rangle$
    over $t_2$ only since the guard of $t_3$ is not satisfiable from within $x >
    2$. The new version is unfolded over and aver again, until end of time.
\end{example}

Besides, we have to consider the fact, that constraints cannot be checked for
semantic equality easily. Thus checking, if a version is already present in the
graph, as done on line \ref{alg:naive_line_inclusion} of Algorithm
\ref{alg:naive_evaluation} is an expensive operation and should be avoided if
possible. Instead the check if a version is already present in the graph, will
be done with structural equality, which is fast and cheap. 

As one can see in example \ref{ex:infinite_evaluation}, the evaluation graph of
a program can be infinite, especially, when the program does not terminate on
every input. In order to find finite evaluation graphs, we need to add an
abstraction layer, which combines similar versions into one.

    Let the set $\A \subset \C$, be a \textit{finite} set where $\psi
    \in \mathcal{A}$ implies $\neg\psi \in \A$. It is called an
    \textit{abstraction space}. A function $\alpha: \C \rightarrow \A$
    is called an \textit{abstraction function} if for every $\varphi\subset\C$,
    $\llbracket \varphi \rrbracket \subseteq \llbracket \alpha(\varphi)\rrbracket$

    Let the set $\A \subset \C$, be a \textit{finite} set. It is called an
    \textit{abstraction space}. A function $\alpha: \Phi \rightarrow \A$ is
    called an \textit{abstraction function} if for every $\varphi\subset\Phi$,
    $\llbracket \varphi \rrbracket \subseteq \llbracket
    \alpha(\varphi)\rrbracket$

% The unfolding operation $\unfold^* : \T \rightarrow \T_\text{PE}$ is modified to
% abstract the unfolded constraint using an abstraction function $\alpha : 2^\C
% \rightarrow \A$. We get new unfolding operations $\unfold_\alpha^*$. 

In general, the abstraction can be arbitrary chosen, as long as the properties
above are satisfied. One possible abstraction, the so called property-based
abstraction, described in \Sref{sec:property_based_abstraction}. For now, the
exact details of abstraction will be omitted. 

% \begin{equation*}
%     \unfold^*_\alpha(\langle l,\varphi\rangle, t) = \begin{cases}
%         \{(\langle l, \varphi\rangle, p, \tau, \eta,\langle
%         l',\alpha(\varphi')\rangle \} & \text{if } t = (l, p, \tau, \eta, l') \\
%         & \text { and } \varphi' = \unfold(\varphi, t) \text{ is SAT} \\ \{\} &
%         \text{ otherwise}
%     \end{cases}
% \end{equation*}
% \begin{align*}
%     \unfold^*_\alpha(\langle l,\varphi\rangle, g) &= \Union_{t\in g}
%     \unfold^*_\alpha(\langle l,\varphi\rangle, t)  \\
%     \unfold^*_\alpha(\langle l,\varphi\rangle) &= \set{\unfold^*_\alpha(\langle
%     l,\varphi\rangle, g)}{g \in \GTout(l)}
% \end{align*}

The unfolding and evaluation are modified slightly to accommodate the
abstraction function $\alpha$.
\begin{equation*}
    \begin{gathered}
        \unfold_\alpha(\langle l,\varphi\rangle, t) = (\langle \ell,
        \varphi\rangle, p, \tau\Land\varphi, \eta,\langle \ell',
        \alpha(\varphi') \rangle) \\ \text{for } t = (\ell, p, \tau, \eta,
        \ell') \in \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau,
        \eta) \\
    \end{gathered}
\end{equation*}

% Since $\llbracket\varphi\rrbracket \subseteq \llbracket
% \alpha(\varphi)\rrbracket$, Lemma \ref{lem:unfold_t} to \ref{lem:unfold_g} hold
% equally for $\unfold_\alpha^*$.

\begin{equation*}
    \evaluate_{\Prog,\alpha}(G) = G + \set{ \unfold_\alpha(\langle
    \ell, \varphi \rangle, t)}{ \langle \ell, \varphi\rangle \in E(G)
    \text{, and } t \in \Tout(\ell)}
\end{equation*}
\begin{equation*}
    G_\alpha^* = \evaluate_{\Prog,\alpha}^*(G_0) = \lim_{n\rightarrow\infty}\evaluate_\Prog^n(G_0)
\end{equation*}

In general, the abstraction can be arbitrary chosen, as long as the properties
above are satisfied. One possible abstraction, the so called property-based
abstraction, described in \Sref{sec:property-based-abstraction}. For now, the
exact details of abstraction will be omitted. Just know that although necessary
for the algorithm to terminate, they are rather expensive and loose precision.

\begin{lemma}
    Let $\alpha: \Phi \rightarrow \A$ be an abstraction function over a finite
    abstraction space $\A\subset\C$. The partial evaluation graph $G_\alpha^*$
    exists and is finite.

When abstracting, instead of adding the transition to the graph and general
transition set directly, the target version is replaced by an abstracted
version. 
If one can guarantee that at every evaluation step of evaluating an infinite
path of $\Prog$ the algorithm eventually abstracts, the algorithm must at some
point encounter an abstracted version that is already contained in the graph, as
only finitely many abstracted versions exist. Hence at some point the algorithm
always backtracks.

    \begin{proof}
        The abstraction $\alpha$ can map to only finitely many values in the
        finite abstraction space $\A$. Every evaluation step adds only versions
        from a reduced and finite set of version $\Loc_\Prog \times \A \subset
        \vers_\Prog$. Hence the set of vertices of partial evaluation graph
        equally finite. A transition is added after a version $\langle \ell,
        \_\rangle$ for every outgoing transitions $t \in \Tout(\ell)$ only. 
        Since $\Tout(\ell) \subseteq \T_\Prog$ is finite, only finitely many
        transitions can exist between any two versions.
        The graph grows with every evaluation step, hence the limit exists and
        it must be reached in a finite number of evaluation steps.
    \end{proof}
\end{lemma}

This can be trivially achieved by abstracting every transition at every step.
However in practice, as we will see in \Sref{sec:loop_heads} one can select
fewer locations and save computation time and gain precision. Let $S_\alpha: ()
\rightarrow \{\textit{true}, \textit{false}\}$ be an oracle function that
decides if a transition should be abstracted or not. The algorithm using
abstraction is displayed as Algorithm \ref{alg:evaluate_abstr}.

For better readability, we write denote abstracted constraints with the set
notation. $\langle \ell, \{\psi_1, \dots, \psi_m\}\rangle$ 

\begin{algorithm}
    \caption{Evaluate a Program $\Prog$ with abstraction
    $\alpha$.\label{alg:evaluate_abstr}}
    \KwData{ A PIP $\Prog$, abstraction function $\alpha$, and
    abstraction oracle $S_\alpha$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GTG
    \subset \GT_\text{PE}$}

\begin{example}
    Consider program $\Prog_3$ from \fref{fig:ex_prob} again. We define
    $\psi_1,\psi_2,\psi_3 \in \C$ and an abstraction space $\A$ where 
    \begin{equation*}
        \begin{gathered}
        \psi_1 = 1 \leq x, \hspace{1cm} \neg\psi_1 = 1 > x\\
        \psi_2 = 2 \leq x, \hspace{1cm} \neg\psi_2 = 2 > x\\
        \psi_3 = x \leq 3, \hspace{1cm} \neg\psi_3 = x > 3\\
        \psi_4 = x \leq 4, \hspace{1cm} \neg\psi_4 = x > 4\\
        \psi_5 = y > 0,\hspace{1cm} \neg\psi_5 = y \leq 0\\
        \psi_6 = y \geq 0,\hspace{1cm} \neg\psi_6 = y < 0\\
        \A = \{\psi_1,\neg\psi_1,\dots,\psi_6,\neg\psi_6\}
        \end{gathered}
    \end{equation*}
    The abstraction function $alpha$ uses the abstraction space $\A$. The
    partial evaluation starts on the graph containing the single version
    $\langle \ell_0, \texttt{true}\rangle$ and 
    \begin{equation*}
        G_0 = (\{\langle \ell_0, \texttt{true}\rangle\}, \emptyset)
    \end{equation*}
    On the first evaluation step, the transition $t_0$ is unfolded, yielding a
    single new transition with a new version $\langle \ell_1,
    \texttt{true}\rangle$:
    \begin{align*}
        t_{0,1} &= (\langle \ell_0, \texttt{true}\rangle, 1, \tau_0, \eta_0, \langle
        \ell_1, \texttt{true}\rangle) \\
        G_1 &= G_0 + \{t_{0,1}\}
    \end{align*}
    On the second step the transitions $t_{1a}, t_{1b}$, and $t_2$ are unfolded
    from $\langle \ell_1, \texttt{true}\rangle$ yielding three new transitions
    $t_{1a,1}, t_{1b,1}$, and $t_{2,1}$:
    \begin{align*}
        t_{1a,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
        \eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3\}\rangle) \\
        t_{1b,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
        \eta_{1b},\langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{2,1} &= (\langle \ell_1, \texttt{true}\rangle, 1, \tau_2,
        \eta_{1b},\langle \ell_2, \{\psi_5\}\rangle) \\
        G_2 &= G_1 + \{t_{1a,1}, t_{1b,1},t_{2,1}\}
    \end{align*}
    On the third step of the evaluation the transitions $t_{1a}, t_{1b}$, and
    $t_2$ are unfolded again, but this time from versions $\langle \ell_1,
    \{\psi_1,\psi_3\}\rangle$ and $\langle \ell_1, \{\psi_2,\psi_4\}\rangle$,
    yielding new transitions $t_{1a,2}, t_{1b,2}$, $t_{2,2},t_{1a,3}, t_{1b,3}$,
    $t_{2,3}$:

    \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$}{
                    \If {$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$}
    }

    \begin{align*}
        t_{1a,2} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3\}\rangle) \\
        t_{1b,2} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1b}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{2,1} &= (\langle \ell_1, \{\psi_1,\psi_3\}\rangle, 1, \tau_2 \Land
        \psi_1 \Land \psi_3, \eta_2,\langle \ell_2,
        \{\psi_1,\psi_3,\psi_5\}\rangle)\\
        t_{1a,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 0.5, \tau_1 \Land
        \psi_2 \Land \psi_4, \eta_{1a}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{1b,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 0.5, \tau_1 \Land
        \psi_1 \Land \psi_3, \eta_{1b}, \langle \ell_1, \{\psi_2,\psi_4\}\rangle) \\
        t_{2,3} &= (\langle \ell_1, \{\psi_2,\psi_4\}\rangle, 1, \tau_2 \Land
        \psi_1 \Land \psi_3, \eta_2, \langle \ell_2, \{\psi_2,\psi_4,\psi_5\}\rangle) \\
        t_{3,1} &= (\langle \ell_2, \{\psi_5\}\rangle, 1, \tau_3 \Land
        \psi_5, \eta_{3}, \langle \ell_2, \{\psi_2,\psi_4,\psi_5\}\rangle) \\
        G_2 &= G_1 + \{t_{1a,2}, t_{1b,2},t_{2,2},t_{1a,3},
        t_{1b,3},t_{2,3},t_{3,1}\}
    \end{align*}
    Note that $t_{1a,2}$ and $t_{1b,2}$ transition to already existing versions
    $\langle \ell_1, \{\psi_1,\psi_3\}\rangle$ and $\langle \ell_1,
    \{\psi_2,\psi_4\}\rangle$.

    $v_0 \leftarrow \langle l_0, \textit{true}\rangle$\;
    $G \leftarrow (\{v_0\}, \emptyset)$\;
    $G \leftarrow $\FEvaluate{$G$, $v_0$}\;

    The remaining evaluation steps are omitted for briefness, but the final
    partial evaluation graph is shown in \fref{fig:ex_prob_fpe}.\todo{update
    figure}

    \Return $G, \GTG$
\end{algorithm}

    \begin{figure}
        \centering
        \input{figures/ch1_prob_fpe}
        \caption{Partial evaluation graph $G_{\Prog_3,\alpha}^*$ of $\Prog_3$
        from \fref{fig:ex_prob}.\label{fig:ex_prob_fpe}}
    \end{figure}
\end{example}

The algorithm does a depth-first search on the original program $\Prog$ and
backtracks whenever it unfolds and abstracts to an already known version. This
implies especially that every version is unfolded only once. As long as the
scheduler always abstracts eventually, the algorithm must backtrack eventually
for every infinite path on $\Prog$, that would otherwise result in an infinite
recursion.

We will proceed with proving, that the graph can be used for constructing an new
program $\Prog'$ with equal expected runtime-complexity.

From the partial evaluation graph a new program is constructed.
\begin{definition}[Partial evaluation]\label{def:partial_evaluation}
    Let $\Prog$ as defined by Definition \ref{def:pip} and $G$ and $\GTG$ be
    the results of Algorithm \ref{alg:evaluate_abstr} on $\Prog$.
    A new \gls{pip} is defined as $\Prog' = (\PV, \Loc_{\Prog'}, \GTPn,
    \langle l_0, \textit{true}\rangle)$ where $\Loc_{\Prog'} = E(G)$, and
    $\GTPn = \GTG$.

\begin{lemma}[Original transitions]\label{lem:original_transition}
    Let $G^*_{\Prog,\alpha}$ be the evaluation graph of a \gls{pip} $\Prog$ for
    any abstraction function $\alpha$. For every transition $t = (\langle \ell_1,
    \varphi_1\rangle, p, \tau, \eta, \langle \ell_2, \varphi_2\rangle) \in
    E(G^*_{\Prog,\alpha})$ one can find a unique transition denoted as
    $\bar{t}\in\T_\Prog$ for which 
    \begin{equation*}
        {\bar{t}} = (\ell, p, \tau', \eta, \ell_2)\textrm{, and }
        \llbracket\tau\rrbracket \subseteq \llbracket\tau'\rrbracket.
    \end{equation*}

    $\Prog'$ is called the \textit{partial evaluation} of $\Prog$.
\end{definition}

    \proof{Follows directly from construction of the unfolding.}
\end{lemma}

\begin{lemma}[Original transitions]
    Let $\Prog'$ be the partial evaluation of $\Prog$ as defined in Definition
    \ref{def:partial_evaluation}. 

In the following, $\bar{t}$ shall always denote the original transition found
with Lemma \ref{lem:original_transition}.

\begin{lemma}[Soundness\label{lem:unfold_g_sound}]
    Let $G^*_{\Prog,\alpha}$ be the evaluation graph of a \gls{pip} $\Prog$ with
    general transitions $\GTP$ and the abstraction function $\alpha$. The
    transitions of $E(G^*_{\Prog,\alpha})$ can be split into finite pairwise
    disjunct subsets $g_0,\dots,g_n \subset E(G^*_{\Prog,\alpha}) \subset \VT$.
    For all $0 \leq i \leq n$ 

        \item For every transition $t = (\langle l_1,
            \varphi_1\rangle, p, \tau, \eta, \langle l_2, \varphi_2\rangle) \in
            \T_{\Prog'}$ where $p \in [0,1]$, $\tau$ is an \gls{fo}-formula, and
            $\eta: \PV \rightarrow \Z[\V\union\D]$ one can find a unique
            transition denoted as $\bar{t}\in\T_\Prog$ for which 
            \begin{equation*}
                {\bar{t}} = (l, p, \tau, \eta, l_2)
            \end{equation*}
        \item For every general transition $g = \{t_1, \dots,t_n\} \in
            \GTPn$ one can find a unique general transition denoted as
            $\bar{g}\in\GT_Prog$ for which

        \item there exist a unique general transition $\bar{g_i} \in \GTP$ and
            some $\varphi \in \Psi$ for which the following property holds:

                \bar{g} = \{\bar{t_1}\dots\bar{t_n}\}

                g_i = \set{\unfold(\langle \ell_{g'_i}, \varphi \rangle,
                \bar{t})}{\bar{t} \in g'_i}

        \item all transitions in $g_i$ have a common guard $\tau_{g_i}$ and
            source location $\ell_{g_i}$;
        \item the probabilities in $g_i$ add up to 1.

        Any transition $t' = (\langle l_1, \varphi_1\rangle, p, \tau, \eta,
        \langle l_2, \varphi_2\rangle)\in\T_{\Prog'}$ must have been added in
        line \ref{alg:abstr_line_addt} in Algorithm \ref{alg:evaluate_abstr} and
        the transition was found by an unfolding of a general transition $g$ in
        line \ref{alg:abstr_line_unfold_g} and an unfolding of a transition $t
        \in g$. By Lemma \ref{lem:unfold_t_similar} follows $t = (l, p, \tau,
        \eta, l_2)$. We set $\bar{t'}=t$.
        A general transition $g'\in\GTPn$ must have been added in line
        \ref{alg:abstr_line_addtog} in Algorithm \ref{alg:evaluate_abstr} by an
        unfolding of a general transition $g$. And $g' \neq \emptyset$ due to
        the condition checked in \ref{alg:abstr_line_filteremptyg}. For all
        transitions $t'_i\in g'$ the same argument as above holds and we find
        $\bar{t_i} = t_i$ for all transitions, that must all exist due to Lemma
        \ref{lem:existance_and_similarity_g}. We set $\bar{g} = g$.

        \todo{proof}

\begin{theorem}[Soundness\label{thm:soundness}]
    Let $\Loc_{\Prog'} = E(G)$, $\GTPn = \GTG$ and $\Prog' = (\PV, E(G),
    \GTG, \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and
    $\GTG$ where found by the Algorithm \ref{alg:evaluate_abstr} on some input
    program $\Prog$. $\Prog'$ is a sound program.

Let $\GT_{G^*_{\Prog,\alpha}}$ be the set of general transitions in the partial
evaluation graph $G^*_{\Prog,\alpha}$ by Lemma \ref{lem:unfold_g_sound}. 

    \begin{proof}
        Lemma \ref{lem:unfold_g_sound} asserts all general transitions found on
        line \ref{alg:abstr_line_unfold_g} are sound general transitions. As the
        abstraction on line \ref{alg:abstr_line_abstraction} doesn't change
        anything about the transition except the target version, and the new
        transitions are all added to a new general transition $g'$ on line
        \ref{alg:abstr_line_addtog}, $g'$ is also a sound general transition,
        and they all end up in $\GTG$.

\begin{definition}[Partial evaluation]\label{def:partial_evaluation}
    Let $\Prog$ as defined by Definition \ref{def:pip} and $G^*_{\Prog,\alpha}$
    be the partial evaluation graph of $\Prog$ for some abstraction function
    $\alpha$. A new \gls{pip} is defined as $\Prog' = (\PV, \Loc_{\Prog'},
    \GTPn, \langle l_0, \textit{true}\rangle)$ where $\Loc_{\Prog'} =
    E(G^*_{\Prog,\alpha}) \subset \vers_\Prog$, and $\GTPn =
    \mathcal{G}\mathcal{T}_{G^*_{\Prog,\alpha}} \subset 2^\VTP$. $\Prog'$ is
    called the \textit{partial evaluation} of $\Prog$.
\end{definition}

        For a given version, every transition starting in the same location as
        the version is unfolded exactly once, and all created transitions start
        at the given version. Since additionally all version are unfolded only
        once, all generated general transitions must be pairwise disjunct. 
    \end{proof}
\end{theorem}

\section{Correctness}
This section will prove that the partial evaluation $\Prog'$ of a program
$\Prog$ has the same worst-case expected runtime-complexity as the original
program. Lemma \ref{lem:simurt} and \ref{lem:constrfleq} are precursors to
Theorem \ref{thm:correctness} which will shows that runtime-complexity bounds
for the partial evaluation are runtime-complexity bounds of the original
program, which demonstrates the correctness of the construction. 
Lemma \ref{lem:constrfgeq} and Theorem \ref{thm:thightness} will show that
worst-case expected runtime-complexity doesn't get worse with partial
evaluation.
The proof for correctness starts by defining a function that simulates a finite
prefix $f \in \fpath_\Prog$ in the partial evaluation $\Prog'$. Then we will
construct a new scheduler $\scheduler' \in \MDS_{\Prog'}$, that takes similar
decisions on $\Prog'$ as an original scheduler $\scheduler \in \MDS_\Prog$. When
using those schedulers, for any path $\varf \in \fpath_{\Prog}$ the simulation
of $f$ has equal probability and runtime-complexity. We will consider only
admissible finite prefixes, since non-admissible ones, do not count in the
expected runtime-complexity as they have a probability zero.

\subsection{Expected Runtime Complexity}
\todo{section introduction}

\begin{definition}
    For a \gls{pip} $\Prog$ and the partial evaluation $\Prog'$ of $\Prog$ as
    described in Definition \ref{def:partial_evaluation}, let $\simu:
    \fpath_\Prog \rightarrow \fpath_{\Prog'}$ be defined recursively. 
    \begin{equation*}
        \begin{gathered}
        \simu((\ell, t, s)) = (\langle \ell, \texttt{true}\rangle,
            \unfold_{\Prog,\alpha}(\langle \ell, \texttt{true}\rangle, t), s) \\
        \simu(\varf (\ell, t, s)) = \varf' (\langle \ell, \varphi\rangle,
            \unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t), s) \\ 
        \text{ where } \varf' = \simu(\varf) = \dots{}(\ell, \_, \_)
        \end{gathered}
    \end{equation*}
\end{definition}

\begin{lemma}\label{thm:constrfleq}
    For a \gls{pip} $\Prog$, a markovian scheduler $\scheduler \in \MDS$ of $\Prog$,
    and the evaluation $\Prog'$ as described in Theorem \ref{thm:soundness},
    there exists a markovian scheduler $\scheduler' \in \MDS$, such that for all
    finite prefixes $f\in\fpath_\Prog$ there exists a finite prefix
    $f'\in\fpath_{\Prog'}$ with 

\begin{lemma}\label{lem:simurt}
    Let $\Prog$ be a \gls{pip} and $\Prog'$ the partial evaluation $\Prog'$ of
    $\Prog$. 

        \item $\Rt_{\scheduler,s_0}(f) = \Rt_{\scheduler',s_0}(f')$
        \item $\prSs,s_0(f) = \prSns,s_0 = (f')$

        \item \label{itm:simurt_rt} For any admissible finite prefix $f \in
            \fpath_\Prog$ 
        \begin{equation*}
            \Rt_\Prog(\varf) = \Rt_{\Prog'}(\simu(\varf))
        \end{equation*}
    \item \label{itm:simurt_neq} For any two distinct admissible finite prefixes
        $f_1, f_2 \in \fpath_\Prog$
        \begin{equation*}
            \simu(f_1) \neq \simu(f_2)
        \end{equation*}

    \proof{Item \ref{itm:simurt_rt} follows by construction since only
    non-terminating transitions are selected in the simulation. Item
    \ref{itm:simurt_neq} follows by construction, since all distinguishing
    properties of $f_1$ and $f_2$ are copied into their respective simulations.
    }
\end{lemma}
\begin{lemma}\label{lem:constrfleq}
    For a \gls{pip} $\Prog$, and any initial state $s_0 \in \Sigma$, a Markovian
    scheduler $\scheduler \in \MDS_\Prog$ and the partial evaluation $\Prog'$ as
    described in Definition \ref{def:partial_evaluation}, there exists a
    Markovian scheduler $\scheduler' \in \MDS_{\Prog'}$, such that for all
    admissible finite prefixes $f\in\fpath_\Prog$ with $\prSs(\varf) > 0$
    there exists a finite prefix $\varf' = \simu(\varf)
    \in\fpath_{\Prog'}$ with 
    \begin{align*}
        \prSs(\varf) = \prSns(\varf')
    \end{align*}

    The proof is done in two steps. First a scheduler $\scheduler'$ is

    The proof is divided into two steps. First a scheduler $\scheduler'$ is

    Then using this scheduler, for a finite path $f$ an equivalent finite path
    is constructed by induction. 

    Then using this scheduler, the equal probability is shown by induction.

    For a \gls{pip} $\Prog$, a markovian scheduler $\scheduler \in \MDS$ of
    $\Prog$, and the evaluation $\Prog'$ we construct a markovian scheduler

    For a \gls{pip} $\Prog$, a Markovian scheduler $\scheduler \in \MDS$ of
    $\Prog$, and the evaluation $\Prog'$ we construct a Markovian scheduler

    Let $\langle l, \varphi\rangle \in \vers$, be a version on location $l \in
    \Loc_\Prog$ and formula $\varphi$. Let $t'\in\TPn$, $s' \in \Sigma$.
    Moreover let $(g, \tilde{s}) = \scheduler((l, \bar{t'}, s))$ be the decision
    taken by the original scheduler. 
    Recall Definition \ref{def:unfold_g}, for a given version $\langle l,
    \varphi\rangle$, not every general transition is unfolded to a new general
    transition. But in Lemma \ref{lem:existance_and_similarity_g} it was shown
    that an unfolded general transition $g'$ is non-empty if $s \models \varphi
    \land \tau_g$ and $l_g = l$. This consideration is especially important
    because the new (memoryless) scheduler must select a general transition
    independently of the fact that a configuration is reachable in first place. 

    The new scheduler is defined to map to the unfolded general transition of
    $g$. If it doesn't exist, any other general transition is selected, which
    satisfies the properties of a markovian scheduler. 

    At a configuration $(\langle \ell, \varphi \rangle, t', s') \in
    \confs_{\Prog'}$, if the original scheduler selects a general transition $g
    \in \GT_\Prog$ and $g \neq g_\bot$, as well as $t' \neq t_\bot$, the new
    scheduler is defined to select the general transition $g' =
    \set{unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t) }{ t \in g }$.
    The new scheduler selects the same assignment $\tilde{s}$ as $\scheduler$.
    However, remember that $\tau_g' = \varphi \Land \tau_g$ and $\varphi \in
    \Phi_\PV$. $s' \models \varphi$ is not guaranteed. $s' \not\models\varphi
    \Land \tau_g$ if and only if $s \not\models \varphi$. In that case the
    scheduler is defined to select any other transition while respecting the
    properties of a Markovian scheduler. In all other cases, for example if the
    original scheduler selects $g_\bot$, or when $t' = t_\bot$, the scheduler
    selects $g_\bot$ and keeps the assignment $s'$.

    In total the new scheduler is defined as follows:

    Formally, the scheduler is defined as follows:

        \scheduler'((l', t', s')) = 

        \scheduler'(\ell', t', s') =

            (\unfold^*(\langle l', \varphi\rangle, g), \tilde{s}) & 

            (g', \tilde{s}) & 

                &\text{if }l' = \langle l, \varphi \rangle \neq l_\bot, \varphi
                \in 2^\C, l \in \Loc_\Prog \\
                &\scheduler((l, \bar{t'}, s')) = (g, \tilde{s}), \text{ and }\\
                & s' \models \varphi

                &\text{if }\ell' = \langle \ell, \varphi \rangle \neq l_\bot, t'
                \neq t_\bot, s' \models \varphi, \\ 
                &\scheduler(\ell, \bar{t'}, s') = (g, \tilde{s}), g \neq g_\bot\text{, and}\\
                &g' = \set{\unfold_{\Prog,\alpha}(\langle \ell, \varphi\rangle, t) }{ t \in g }

            (g'^*, \tilde{s}^*) & \text{if } g'^* \in \GTout(\langle
            l,\varphi\rangle) \text{ and } \tilde{s}^* \models \tau_{g'^*}
            \text{ exists} \\

            (g'^*, \tilde{s}^*) & 
            \begin{aligned} 
                &\text{if }\ell' = \langle \ell, \varphi \rangle \neq \ell_\bot, t'
                \neq t_\bot, s' \models \varphi\text{, and}\\ 
                &g'^* \in \GTout(\langle \ell,\varphi\rangle) \text{ and }
                \tilde{s}^* \models \tau_{g'^*}
            \text{ exists}
            \end{aligned}\\

    The scheduler newly constructed $\scheduler'$ is indeed a scheduler for
    $\Prog'$. 

    Case 1, $s' \models \varphi$. Case 1.1, $\scheduler(\ell, \bar{t'},s')$
    selects $(g_\bot, s')$. In that case, $\scheduler(\ell', t', s') =
    (g_\bot, s')$ as well. This is correct because if no $(g, \tilde{s}) \in
    \GTout(\ell) \times \Sigma$ with $\tilde{s}|_\PV = s'$ and $\tilde{s}
    \models \tau_g$ exist, then so can't any $(g', \tilde{s'}) \in \GTout(\ell')
    \times \Sigma$, because all general transitions in $\GTout(\ell')$ have more
    restrictive guards than their original counterparts. 

    Case 1, $s' \models \varphi$. In case the original scheduler $\scheduler(l',
    \bar{t'},s') $ selects $(g_\bot, s')$, so does $\scheduler'$. This is
    correct, because $\scheduler(l, \bar{t'},s) = (g_\bot, s')$ implies by
    Definition \ref{def:mscheduler} that no transition $g\in\GTout(l)$ exists
    where $\tau_g$ can be satisfied and by Lemma
    \ref{lem:existance_and_similarity_g} no such transition can exist in
    $\GTout(l')$. If the original scheduler selects $\scheduler(l, \bar{t'},s) =
    (g, \tilde{s})$ with $g \neq g_\bot$ then by Definition \ref{def:mscheduler}
    $\tilde{s}\models \tau_g$. By $s\models \varphi$ and since $\varphi$
    contains only variables from $\PV$ so does $\tilde{s} \models \varphi$. By
    Lemma \ref{lem:existance_and_similarity_g} $\unfold(\langle l,
    \varphi\rangle) = g' \neq \emptyset$ and $\tilde{s} \models \tau_{g'} =
    \tau_{g}$.

    Case 1.2, $\scheduler(\ell, \bar{t'},s')$ selects $(g, s')$ with $g \neq
    g_\bot$. In that case $\scheduler(l, \bar{t'},s) = (g', \tilde{s})$ where
    $\tau_{g'} = \varphi \Land \tau_g$. Since $\tilde{s} \models \tau_g$ and
    $\tilde{s}|_\PV = s'$, it follows $\tilde{s} \models \varphi \Land \tau_g$. 

    Note, by construction the $\scheduler'$ selects a similar transition and and
    the same variable assignment $\scheduler$ whenever $s \models \varphi$. The
    proof is concluded with an induction using the constructed scheduler
    $\scheduler'$.

    \rem{In case unreachable transitions and versions are removed from the
    program, the original scheduler might select a general transition which has
    been removed in the partial evaluation. In that case the new scheduler can
    be adapted to make an arbitrary valid selection, as is already done for the
    case where $s' \not\models \varphi$.}
    Let $s_0 \in \Sigma$ be any initial state.

    \textbf{Induction hypothesis.} For any arbitrary run $f= c_0\dots{}c_n\in
    \fpath_\Prog$ of length $n \leq \N$ with with $c_i = (l_i,s_i,t_i)$ and all
    $i = 0,1,\dots$ one can find a prefix $f'_n=c'_0c'_1\cdots{}c_n \in
    \fpath_{\Prog'}$ with:

    \textbf{Claim:} For any admissible finite prefix $f_n= c_0\dots{}c_n\in
    \fpath_\Prog$ of length $n \leq \N$ with $\prSs(f_n) > 0$, $c_i =
    (\ell_i,s_i,t_i)$ and all $i = 0,1,\dots$ one can find a finite prefix
    $\varf'_n = \simu(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:

        \item $\prSs(c_0\dots{}c_n) = \prSns'(c'_0\dots{}c'_n)$
        \item  $c'_i = (\langle l_i, \varphi_i\rangle,t'_i,s_i)$ for some
            $\varphi_i \in 2^\C$, $t'_i \in \TPn$, and $i = 1, \dots, n$
            \label{itm:location_in_version}
        \item $s_i \models \varphi_i$ \label{itm:si_models_phi}

        \item $\prSs(\varf) = \prSns(\varf')$, and
        \item $s_n \models \varphi_n$ where $\varf'_n = \dots{}(\langle \_,
            \varphi_n\rangle, \_, s_n)$.\label{itm:si_models_phi}

    Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are required
    for the scheduler to select a similar general transition not important for
    the final result.  

    Item \ref{itm:si_models_phi} is required for the scheduler to select a
    similar general transition but not important for the final result.  

    \textbf{Induction start n=0.}
    Since $f = c_0$ is an admissible prefix, $c_0 = (l_0, t_\text{in},s_0)$. Set
    $f'_0=(\langle l_0,\textit{true}\rangle,s_0,t_\text{in})$. $\langle l_0,
    \textit{true}\rangle$ is a location in $\Prog'$ since it is the first
    location added to $\Prog'$ in line \ref{alg:abstr_line_addl0} of Algorithm
    \ref{alg:evaluate_abstr} and it is set as the start location of $\Prog'$ in
    Definition \ref{def:partial_evaluation}. $s_0 \models \textit{true}$
    trivially. $\prSs(c_0) = \prSs'(c'_0) = 1$ since both $c_0$ and $c'_0$ are
    valid starting configurations in $\Prog$ and $\Prog'$ respectively.

    \textbf{Induction start:} $n=0$.
    Since $f_0 = c_0$ is an admissible prefix, $c_0 = (\ell_0,
    t_\text{in},s_0)$. Set $\varf'_0= c'_0 = \simu(\varf) = (\langle
    \ell_0,\texttt{true}\rangle,s_0,t_\text{in})$. $\langle l_0,
    \texttt{true}\rangle$ is a location in $\Prog'$ by construction. $s_0
    \models \texttt{true}$ trivially. $\prSs(c_0) = \prSs'(c'_0) = 1$ since both
    $c_0$ and $c'_0$ are valid starting configurations in $\Prog$ and $\Prog'$
    respectively.

    Assume the induction hypothesis holds for $n \in \N$. Let $f = c_0\dots{}
    c_{n+1} \in \fpath_\Prog$ of length $n+1 \in \N$ be an admissible prefix,
    then so is $f^* = c_0\dots{}c_{n}$ of length $n$. By induction hypothesis a
    prefix $f'^* = c'_0\dots{}c'_{n}$ of equal length exists with 

    Assume the induction hypothesis holds for $n \in \N$. Let $f_{n+1} =
    c_0\dots{}c_{n+1} \in \fpath_\Prog$ of length $n+1 \in \N$ be an admissible
    prefix with probability $\prSs(f_{n+1})>0$, then $f_n = c_0\dots{}c_{n}$ of
    length $n$ is also admissible with $\prSs(f_n) > 0$. By induction hypothesis
    a finite prefix $\varf'_n = \simu(f_n) = c'_0\dots{}c'_{n} \in
    \fpath_{\Prog'}$ of equal length exists with 

        \item $\prSs(c_0\dots{}c_n) = \prSns'(c'_0\dots{}c'_n)$
        \item $c'_i = (\langle l_i, \varphi_i\rangle,s_i,t'_i)$ for some
            $\varphi_i \in 2^\C$, $t'_i \in \TPn$, and $i = 1, \dots, n$
        \item $s_i \models \varphi_i$ 

        \item $\prSs(f_n) = \prSns'(\varf'_n)$, and
        \item $s_n \models \varphi_n$ where $\varf'_n = \dots{}(\langle _,
            \varphi_n\rangle, \_, s_n)$.

    Let $c_i = (l_i,s_i,t_i)$ for all $i = 0, \dots,n+1$ and since $f$ is
    admissible, let $t_{n+1} = (l_n, p_{n+1},\tau_{n+1}, \eta_{n+1}, l_{n+1})$ with
    a probability $p \in [0,1]$, a guard $\tau_i \in 2^\C$, an update $\eta: \PV
    \rightarrow \Z[\V\union\D]$. Let $\{t'_{n+1}\} = \unfold^*(\langle l_n,
    \varphi_n\rangle)$, due similarity established in Lemma,
    \ref{lem:existence_and_similarity} $t=(\langle l_n, \varphi_n\rangle, p,
    \tau_{n+1}, \eta_{n+1}, \langle \varphi_{n+1}, l_{n+1}\rangle)$ for some
    $\varphi_{n+1} \in 2^\C$. Due to reachability by Lemma
    \ref{lem:existence_and_similarity} $s_{n+1} \models \varphi_{n+1}$. 
    Let $c'_{n+1} = (\langle l_{n+1}, \varphi_{n+1}, t_{n+1}, s_{n+1}$ be the
    last configuration of $f' = c'_0\dots{}c_nc_{n+1}$

    Moreover, let $c_i = (\ell_i,t_i,s_i)$ and $t_i = (\ell_{i-1}, p_i, \tau_i,
    \eta_i, \ell_i)$ for all $ 1 \leq i \leq n+1$. The simulation sets
    $t'_{n+1}$, location $\ell'_{n+1}$ and assignment $s'_{n+1}$ of the last
    configuration $c'_{n+1} = (\ell'_{n+1}, t'_{n+1}, s'_{n+1})$ on the extended
    finite prefix $\varf'_{n+1} =\simu(f_{n+1})= \simu(f_n)c'_{n+1}$ to 
    \begin{align*}
        t'_{n+1} &= (\langle \ell_n, \varphi_n\rangle, \varphi_n \Land
        \tau_{n+1}, \eta_{n+1}, \langle \ell_{n+1}, \varphi_{n+1}\rangle)\\
        &= \unfold(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in \T_\Prog',\\
        \ell'_{n+1} &= \langle \ell_{n+1}, \varphi_{n+1}\rangle, \text{ and} \\
        s'_{n+1} &= s_{n+1}
    \end{align*}

    Finally, let $\scheduler(c_n) = (g_{n+1},\tilde{s})$ where $g_{n+1} \neq
    g_\bot$ due to $f$ being admissible. By construction of the scheduler
    $\scheduler'$ a similar general transition is selected $\scheduler(c'_n) =
    (g'_{n+1},\tilde{s})@$ where $g'_{n+1} \neq g_\bot$ and with the same guard
    $\tau_g = \tau_{g'}$.

    Let $\scheduler(c_n) = (g_{n+1},\tilde{s})$ be the selection of the original
    scheduler where $g_{n+1} \neq g_\bot$ due to $f$ being admissible. By
    construction of the scheduler and since $s_n \models \varphi_n$, the new
    scheduler $\scheduler'$ selects a general transition $g'\in\GTPn$ with
    $t'_{n+1} \in g' \neq g_\bot$. 

    The last step on the finite prefix $\varf'_{n+1}$ has the same probability
    as the last step on the original finite prefix $f_{n+1}$. As a consequence,
    using the induction hypothesis, both prefixes have the same probability.

        \Leftrightarrow \prSs(f) &= \prSs(f^*) \cdot \prSs(c_n \rightarrow

        \Leftrightarrow \prSs(f_{n+1}) &= \prSs(f_n) \cdot \prSs(c_n \rightarrow

        &=  \prSs(f'^*) \cdot \prSs(c'_n \rightarrow c'_{n+1}) = \prSns(f')

        &=  \prSs(\varf'_n) \cdot \prSs(c'_n \rightarrow c'_{n+1}) =
        \prSns(\varf_{n+1})

    Finally, it follows that $s'_{n+1} \in \support_{\tilde{s}}(\eta_{n+1})$ and
    by Lemma \ref{lem:unfold}, $s'_{n+1} \models \varphi_{n+1}$. 
    \rem{
        At this point is becomes clear, why filtering unreachable transitions
        ans versions can be done in practice. The newly constructed prefix can
        never take those transitions, or else it would not be admissible. Hence
        the presence of non-reachable transitions and versions doesn't change
        anything for this proof.
    }

Lemma \ref{lem:constrfleq} implies that $\simu(\varf)\in\fpath_{\Prog'}$ is
admissible for any admissible finite prefix $f \in \fpath_\Prog$.

    For a pip $\Prog$, the evaluation $\Prog'$ as described in
    Definition \ref{def:partial_evaluation}, and a starting state $s_0

    For a \gls{pip} $\Prog$, the partial evaluation $\Prog'$ as described in
    Definition \ref{def:partial_evaluation}, and an initial state $s_0

        \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
        \sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\

        \sup_{\scheduler \in \MDS}(\ESs(\Rt_\Prog)) \leq
        \sup_{\scheduler' \in \MDS}(\ESns(\Rt_\Prog')) \\

        in Lemma \ref{lem:constrfleq}.

        in Lemma \ref{lem:constrfleq}. Recall Definition
        \ref{def:expected_value}.

        \todo{reference literature, probabilistic}

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

            \ESs(\Rt_{\Prog}) &= \sum_{i=1}^\infty i \cdot \PrSs(\Rt_\Prog=i) 
            = \sum_{i=1}^\infty \PrSs(\Rt_\Prog \leq i) 
            = \sum_{\substack{f \in \fpath_\Prog\\ \Rt_\Prog(f) \leq
            i}}^\infty \prSs(\varf) \\

            \sum_{\substack{f \in \fpath_\Prog\\ \Rt(f) \leq i}}^\infty \prSs(f)
            &\leq \sum_{\substack{f \in \fpath_{\Prog'}\\ \Rt(f) \leq i}}^\infty
            \prSns(f) \label{eq:sumsleq} \\
            \Leftrightarrow \ESs(\Rt(\Prog)) &\leq \ESns(\Rt(\Prog')) \label{eq:esleq}

            \sum_{\substack{f \in \fpath_\Prog\\ \Rt_\Prog(f) \leq i}}^\infty
            \prSs(f) &\leq \sum_{\substack{f \in \fpath_{\Prog'}\\ \Rt_\Prog(f)
            \leq i}}^\infty \prSns(f) \label{eq:sumsleq} \\
            \Leftrightarrow \ESs(\Rt_\Prog) &\leq \ESns(\Rt_{\Prog'})
            \label{eq:esleq}

        equal probability $f' \in \fpath_{\Prog'}$. The constructed paths must
        all be pairwise different, since it is also asserted, that every
        configuration of $f'$ shares the same state and (version) location as
        the original configuration. 
        Hence (at least) all constructed paths $f'$ contribute with equal
        probability to the sum on the right side of of (\ref{eq:sumsleq}). 

        equal probability $\varf' \in \fpath_{\Prog'}$. By Lemma
        \ref{lem:simurt} they are all pairwise different. Hence (at least) all
        constructed paths $\varf'$ contribute with equal probability to the sum
        on the right side of of (\ref{eq:sumsleq}). 

The following theorem shows, that the partial evaluation hasn't got worse
either. Note, that doesn't imply that a perfectly tight bound for the worst-case
expected runtime can be found.

The following theorem shows, that the partial evaluation hasn't gotten worse
either. Note, this doesn't imply that a perfectly tight bound for the worst-case
expected runtime can be found. Similarly to Lemma \ref{lem:constrfleq} we first
construct a new scheduler $\scheduler \in \HDS_\Prog$ and show that when using
this scheduler, a finite path of equal probability and runtime-complexity exists
in $\Prog$ for every finite path in $\Prog'$.
\begin{lemma}\label{lem:constrfgeq}
    For a \gls{pip} $\Prog$, the partial evaluation $\Prog'$ as described in
    Definition \ref{def:partial_evaluation} and a Markovian scheduler
    $\scheduler \in \MDS_{\Prog'}$, there exists a \emph{history dependent}
    scheduler $\scheduler' \in \HDS_{\Prog}$, such that for all finite prefixes
    $f\in\fpath_\Prog'$ there exists a finite prefix $f\in\fpath_{\Prog}$
    with 
    \begin{enumerate}
        \item $\Rt_{\Prog'}(\varf) = \Rt_{\Prog}(\varf')$
        \item $\prSns(\varf) = \prSs(\varf')$
    \end{enumerate}
\end{lemma}
\begin{rem}
    We require a history dependent scheduler instead of Markovian scheduler,
    because the Markovian $\scheduler$ can select general transitions $g_1$ and
    $g_2$ at version $\langle \ell, \varphi_1\rangle, \langle \ell,
    \varphi_2\rangle \in \Loc_\Prog'$, whereas the Markovian scheduler would be
    forced to always select the same transition $g \in \GT$ at location $\ell$.
    As we will see, this won't matter when considering the worst-case.
\end{rem}
\begin{proof}
    Again we start with the construction of the scheduler $\scheduler' \in
    \HDS_{\Prog'}$. It simulates the given history on the partial evaluation up
    to a configuration $c'_n \in \confs_{\Prog'}$ and then selects the original
    general transition $\bar{g} \in \GTPn$ to the general transition $g \in
    \GTP$ selected by the scheduler $\scheduler(c'_n) = (g, \tilde{s})$, and
    keeps the assignment $\tilde{s}$.
    Formally, the scheduler $\scheduler'$ is defined as follows:
    \begin{equation*}
        \scheduler'(\varf(\ell,t,s)) =
        \begin{cases}
            (\bar{g}, \tilde{s}) & \begin{aligned}
                &\text{if } \varf' = \simu(\varf(\ell,t,s)) = \dots c'_n, \\
                &\scheduler(c'_n) = (g, \tilde{s})\text{, and } g \neq g_\bot
            \end{aligned}\\
            (g_\bot, s) & \text{otherwise}
        \end{cases}
    \end{equation*}
    \textbf{Claim:} For any finite prefix $f \in \fpath_\Prog'$ there exists a
    finite prefix $\varf' \in \fpath_\Prog$ for which 
    \begin{enumerate}
        \item $\Rt_{\Prog'}(\varf) = \Rt_{\Prog}(\varf')$
        \item $\prSns(\varf) = \prSs(\varf')$
    \end{enumerate}

    \textbf{Induction start:} $n = 0$. 
\end{proof}

        \sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
        \sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\

        \sup_{\scheduler \in \MDS}(\ESs(\Rt_\Prog')) \leq
        \sup_{\scheduler' \in \HDS}(\ESns(\Rt_{\Prog})) \\

\begin{definition}[Expected Value\cite{billingsley2011, meyer20arxiv}]

\begin{definition}[Expected Value\cite{billingsley2011,
    meyer20arxiv}]\label{def:expected_value}

    \begin{equation*}
        \E(X) = \sum_{r \in \bar{\N}} r \cdot P(X = r)
    \end{equation*}

    \begin{align*}
        \E(X) &= \sum_{r \in \bar{\N}} r \cdot P(X = r)
        &= \sum_{r \in \bar{\N}} \cdot P(X \leq r)
    \end{align*}

For a \gls{pip} one can define a probability space $(\runs, \F, \PrSs)$, where

For a \gls{pip} one can define a probability space $(\runs_\Prog, \F, \PrSs)$, where

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

every set $\{r\} \in \F$ for $r \in \runs_\Prog$. The probability measure $\PrSs$

% The cost of a run (or total reward for the Markov decision process) is
% the sum of costs for every transition taken during a run. 
% \begin{definition}[Costs]
%     For a run $c_0c_1\dots{}\in \runs_Prog$ the \textit{costs} of $\Cost :
%     \runs \rightarrow \overline{\N}$ is a random variable with 
%     \begin{equation*}
%         \Cost(\Prog)(c_0c_1\dots) = |\set{\kappa_{t_i}}{c_i = (l_i, t_i, s_i) \text{
%             and } t_i \neq t_\bot}|
%     \end{equation*}
% \end{definition}
% \begin{definition}[Expected Costs]
%     For a scheduler $\scheduler$ and a start location $s_0 \in \Sigma$ the
%     expected costs $\Cost(\Prog)_{\scheduler,s_0}$ of a program $\Prog$ is
%     defined as the expected value of the random variable $\Cost(\Prog)$:
%     \begin{equation*}
%         \Cost_{\scheduler,s_0}(\Prog) = \ESs(\Cost(\Prog))
%     \end{equation*}
% \end{definition}
% \begin{example}
% \end{example}

during a run. 

during a finite prefix or run. For runs they can be seen as a random variable in
the probability space of a program.

    For a run $c_0c_1\dots{}\in \runs$ the runtime complexity $\Rt(\Prog) :
    \runs_\Prog
    \rightarrow \overline{\N}$ is is a random variable with:

    For a finite prefix $f \in \fpath_\Prog$ the runtime complexity $\Rt_\Prog
    : \fpath_\Prog \rightarrow \N$ is defined as 
    \begin{equation*}
        \Rt(\varf) = |\set{i}{ c_i = (\ell_i, t_i, s_i) \text{ and } t_i \neq
        t_\bot}| 
    \end{equation*}
    For a run $c_0c_1\dots{}\in \runs_\Prog$ the runtime complexity
    $\Rt_\Prog : \runs_\Prog \rightarrow \overline{\N}$ is is
    a random variable with:

    For a scheduler $\scheduler \in MDS_\Prog$ and a start location $s_0 \in

    For a scheduler $\scheduler \in \MDS_\Prog$ and a start location $s_0 \in

    for a given starting state $s_0 \in \Sigma$ 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

    for a given starting state $s_0 \in \Sigma$ and $\scheduler \in \MDS_\Prog$,
    the expected runtime depends on the initial variable $x$. The probability
    for decrementing $x$ once follows a geometric distribution. The runtime for

        \ESs(\Rt(\Prog)) = s_0(x) \cdot \frac{1}{p} = s_0(x) \cdot \frac{1}{0.5}

        \ESs(\Rt_\Prog) = s_0(x) \cdot \frac{1}{p} = s_0(x) \cdot \frac{1}{0.5}