\usepackage[ruled]{algorithm2e}

\usepackage[ruled,linesnumbered]{algorithm2e}

    finite abstraction space $A$. 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. 

    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. 

\end{definition}

    For clarity sake, versions will be denoted with angles $\langle \cdot
    \rangle$. The set notation with curly braces is used for non-abstracted
    constraints like so $\langle l, \{\psi_1, \dots\}\rangle$ and the list
    notation with brackets is used for abstracted values like so $\langle l,
    [\psi_1, \dots]\rangle$.
\end{definition}

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.

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

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

The next lemma shows, that unfolding a general transition creates a valid new
general transition in the partial evaluation graph.

    Either $unfold(\langle l, \varphi\rangle, g)=\emptyset$ or $unfold(\langle l,
    \varphi\rangle, g) = \{t_1, \dots{},t_n\}$ with probabilites adding up to 1. 

    For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g \in \GT$
    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 $t_i = (\_, p_i, \tau_g, \_,\_)$ for some $p_i \in [0,1]$ for all
    $i=1,\dots,n$ and $\sum_{i=1}^n p_i = 1$.

        \todo{proof}

        Let $g = \{t_1, \dots, t_n\} \in \GT$ with $t_i =
        (l,p_i,\tau_i,\eta_i,\_,\_)$. By Definition \ref{def:pip}, the
        probabilities of all transition in a general transition add up to 1.
        \begin{equation*}
            \sum_{i=1}^n p_i = 1,
        \end{equation*}
        and the share the same guard $\tau_g = t_i$ 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 \GT_\text{PE}$ and
        $i=1,\dots,n$. 
        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$.

The operation is overloaded a last time, with a function $\unfold^* :
\vers \rightarrow 2^{\T_{PE}}$ unfolding all outgoing general transitions in the

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

    \unfold^*(\langle l, \varphi\rangle) = \Union_{g \in \GT_{out}(l)}
    \unfold^*(\varphi, t)

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

\begin{lemma}\label{lem:unfold_v}
\end{lemma}

        A PIP $P$, Graph $G$, and source version $\langle l, \varphi\rangle$
    }
    \KwResult{A Graph $G$}

        A PIP $\Prog$, Graph $G$}
    \KwResult{A Graph $G$, and pairwise disjunct general transitions $\GT_G
    \subset \GT_\text{PE}$}

    \Fn{\FEvaluate{$G$, $v$, $t$}}{

    $\GT_G \leftarrow \emptyset$\;
    \Fn{\FEvaluate{$G$, $v$}}{

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

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

            $\GT_G \leftarrow \GT_G + g$\;

    \Return $G$

    \Return $G, \GT_G$

In the example above, it would be nice, if the infinitely path after $\langle
l_1, x > 1$ would be condensed to a single loop, looping over a single version

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

\textit{true}$. 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. 

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

    is called an \textit{abstraction function} if for every $\varphi\in\C$,

    is called an \textit{abstraction function} if for every $\varphi\subset\C$,

% 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^*$. 
% \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*}
% Since $\llbracket\varphi\rrbracket \subseteq \llbracket
% \alpha(\varphi)\rrbracket$, Lemma \ref{lem:unfold_t} to \ref{lem:unfold_g} hold
% equally for $\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. Just know that although necessary for the
algorithm to terminate, they are rather expensive and loose precision.
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.
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}.
\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 $\GT_G
    \subset \GT_\text{PE}$}
    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    $\GT_G \leftarrow \emptyset$\;
    \Fn{\FEvaluate{$G$, $v$}}{
        $N \leftarrow \unfold^*(v)$\label{alg:abstr_line_unfold_v}\;
        \For{$g \in N$}{
            $g' \leftarrow \emptyset$\;
            \For{$t = (v, p, \tau, \eta, \nu, \langle l', \varphi\rangle) \in g, $}{
                \If {$S_\alpha$} {
                    $t \leftarrow (v, p, \tau, \eta, \nu, \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 evaluate(G, v')$\;
                }
                \Else {
                    $G \leftarrow G + t$\;
                }
            }
            $\GT_G \leftarrow \GT_G + 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, \GT_G$
\end{algorithm}
The algorithm does a depth-first search on the original program $\P$ 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.
\begin{theorem}[Soundness\label{thm:soundness}]
    Let $\Loc_{\Prog'} = E(G)$, $\GT_{\Prog'} = \GT_G$ and $\Prog' = (\PV, E(G), GT_G,
    \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and $\GT_G$
    where found by the Algorithm \ref{alg:evaluate_abstr} on some input program
    $\Prog$.
    $\Prog'$ is a sound program.
    \begin{proof}
        Lemma \ref{lem:unfold_sound} asserts all general transitions found on line
        \ref{alg:abstr_line_unfold_v} 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 $\GT_G$.
        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}
\begin{theorem}
    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ as described in
    Theorem \ref{thm:soundness}, there exists a markovian scheduler
    $\scheduler': \confs' \rightarrow \GT' \union \{g'_\bot\}$, such that for
    all finite prefixes $f\in\fpath$ there exists a finite prefix $f'\in\fpath'$
    with 
    \begin{enumerate}
        \item $\Rt_{\scheduler,s_0}(f) = \Rt_{\scheduler',s_0}(f')$
        \item $\prSs,s_0(f) = \prSns,s_0 = (f')$
    \end{enumerate}
\end{theorem}
\begin{proof}
    The proof will be done in two steps, first a scheduler $\scheduler'$ is
    constructed that will select a similar transition in $\Prog'$ when possible.
    Then we will do an inductive construction over an arbitrary finite path
    using the the previously constructed scheduler. 
    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ we construct a
    markovian scheduler $\scheduler': \confs' \rightarrow \GT' \union \{g'_\bot\}$. 
    Note, that in this section primed items are items for $\Prog'$ and unprimed
    items denote items for $\Prog$. 
    % Also recall $\confs = \L \union \{l_\bot\}
    % \times \T \union \{t_\text{in}, t_\bot\}\times \Sigma$.
    Note that for any transition $t' \in \T'$ of the evaluated program, one can
    find a unique transition $t \in \T$ of the original program that was
    unfolded to $t'$, since every transition is created by exactly one unfold
    operation in on line \ref{alg:abstr_line_unfold_v} of Algorithm
    \ref{alg:evaluate_abstr}. 
    For all versions $\langle l, \varphi\rangle \in \vers$, let $(g, \tilde{s})
    = \scheduler((l, 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 $g\in\GT$ is unfolded to a new
    transition $g'\in\GT'$. Transitions that can not be taken from a state
    $s\models\varphi$ are filtered by a satisfiability check. This consideration
    is especially important because the (memoryless) scheduler selects the
    general transition independently of the fact that a configuration is
    reachable in first place. If this is the case, the new scheduler will select
    any arbitrary other transition. We will see that this doesn't matter, since
    a decision at an unreachable configuration has no impact on the equivalence
    of admissible runs. 
    We define $g' \in \GT'$ to be the general transition created by unfolding
    the general transition $g \in \GT$ or any other general transition 
    \begin{align} 
        \label{eq:schedulerconstruction1}
        \scheduler((l', t', s')) = 
        \begin{cases}
            (g'_\bot, s') & \text{if } l' = l'_\bot \text{ or } t' = t'_\bot\\
            (\unfold^*(\varphi, g), \tilde{s}) & \text{if } s\models\varphi
            \text{ and } g \neq g_\bot\\
            (g'^*, \tilde{s}^*) & \text{if } g'^* \in \unfold^*(\langle
            l,\varphi\rangle) \text{ and } \tilde{s}^* \models \tau_{g'^*}
            exists\\
            (g'_\bot, s') & \text{otherwise}
        \end{cases}
    \end{align}

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

    The scheduler newly constructed $\scheduler'$ is indeed a scheduler for
    $\Prog'$. We will show items \ref{itm:md1} to \ref{itm:md4} of Definition
    \ref{def:mscheduler}. Let $c' = (l', t', s)$. If $l' = l_\bot$ or $t' =
    t_\bot$, $\scheduler'(c') = (g'_\bot, s)$  follows immediately from the
    construction \ref{eq:schedulerconstruction1}. Next, let $l' \neq l'_\bot$
    and $t' \neq t'_\bot$. Assume $s\not\models\varphi$ the new scheduler
    selects a general transition fulfilling properties (1)-(3) automatically by
    construction. Note that all transitions starting in $l'$ must have been
    created by the unfolding $unfold(l')$ and hence considered by the scheduler
    for selection. 
    Finally assume $s\models\varphi$. If the original scheduler returned $(g,
    \tilde{s}) = \scheduler(c))$ and $g \neq g_\bot$, then $g' =
    \unfold^*(\varphi, g) = \Union_{t\in g} \neq \emptyset$ by lemma () and
    properties (1)-(3) are satisfied
    \begin{enumerate}
        \item $\tilde{s}'(x) = \tilde{s}(x) = s(x)$ for all $x\in\PV$ by
            Definition \ref{def:mscheduler} for $\scheduler$.
        \item $l = l_g$ by Definition \ref{def:mscheduler} for $\scheduler$ and 
            $l' = \langle l, \varphi \rangle = l'_g$ by construction of the
            unfolding (\todo{ref}).
        \item $s \models \tau_g$ by Defeinition \ref{def:mscheduler} and
            $\tau_{g'} = \tau_g$ by construction of the unfolding.
            $s\models\tau_{g'}$ holds.
    \end{enumerate}
    If the original scheduler returned the terminal transition $\scheduler(c)=
    (g_\bot, s)$, then so does the new scheduler $\scheduler(c') = (g'_\bot, s)$
    by construction. This is correct because by lemma (\ref{}). 
    We interject a small observation following from the above, that will be
    useful for the later induction. 
    \begin{lemma}[Corollary] 
        If $s \models \varphi$ then:
        \begin{enumerate}
            \item $(g_\bot, _) = \scheduler(c)$ if and only if $g'_\bot =
            \scheduler'(c')$.
            \item $(g, _) = \scheduler(c)$ and $(g',_) = \scheduler(c')$ with $g
                \neq g_\bot$ and $g' \neq g'_\bot$ then $g$ and $g'$ have the
                same probability $p$.
        \end{enumerate}
    \end{lemma}

\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) &= \Union_{g \in \Tout(l)}
    \unfold^*_\alpha(\langle l,\varphi\rangle, g)  \\
\end{align*}

    Given an admissible run $f^*= c_0\dots{}c_N\in \fpath$ of the original
    program $\Prog$ with $c_i = (l_i,s_i,t_i)$ for all $i = 0,1,\dots$ and a
    scheduler $\scheduler$ for the very same program. Let $\scheduler'$ be
    constructed as above.

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

    \textbf{Induction hypothesis.} We can find a prefix
    $f'_n=c'_0c'_1\cdots{}c_n \in \fpath'$ of length $n \leq N$ with 
    \begin{enumerate}
        \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 \C$, $t'_i \in \T'$, and $i = 1, \dots, n$ \label{itm:location_in_version}
        \item $s_i \models \varphi_i$ \label{itm:si_models_phi}
    \end{enumerate}

    Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are useful
    for using the properties of the scheduler but not important for the final
    result.  
    \textbf{Induction start n=0.}
    Since $f^*$ 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 added at first by the
    evaluation algorithm. $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 step.} 
    Assume the induction hypothesis holds for $n < N$ we will construct a prefix
    of length $n+1$ for which the induction hypothesis equally holds. 

In general, the abstraction can be arbitrary 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 omitten. Just know that altough necessary for the
construction to work, they are expensive and loose precision.

    Since the prefix $f$ is admissible, so is its prefix $f_i =
    c_0c_1\dots{}c_nc_{n+1}$ and by definition \todo{ref}
    \begin{equation*}
        \prSs(f) = \prSs(c_0) \cdot \prod_{i=1,\dots,n+1} \prSs(c_{i-1} \rightarrow
        c_i) > 0
    \end{equation*}

As stated above, it must be guaranteed that every infinite path is abstracted
often enough, so that it collapses onto itself\todo{rewrite}. The easiest way
would be to just abstract at every location. This however would result in a very
imprecise evaluation and be very expensive, since the abstraction is called after
every unfolding step.

    Let $\scheduler(c_n) = (g_{n+1},\tilde{s}_n)$ by definition \todo{ref}
    \begin{equation*}
        \prSs(c_n \rightarrow c_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s}_n)(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}_n(u),s_n(u)} > 0
    \end{equation*}

\todo{loop head abstraction}

    Set the state $s'_{n+1} = s_{n+1}$, and the transition $t'_{n+1} =
    \unfold(\varphi_i, t_i)$. $t_{n+1} \in g$ and by construction of the
    unfolding 
    Since $f'_n$ is an admissible path, $\langle l_n, \varphi_n \rangle$ is a valid
    location (version) in $\Prog'$, every version is unfolded by the evaluation
    algorithm immediately after being added to the new program in (\todo{ref}). As
    $g_i$ is selected by the scheduler, $g_{n+1}$ is a general transition with
    $l_{g_{n+1}} = l_n$. As such $g_{n+1}$ is unfolded by the algorithm in
    (\todo{ref}) and so is the transition $t_{n+1}$ as part of unfolding of the
    general transition $g_{n+1}$.
    With $g'_{n+1}=\text{unfold*}(\varphi_n, g_{i+1})$, define the next
    $\scheduler'_{n+1}$ as 
    \begin{equation*}
        \scheduler'_{n+1}(c) = \begin{cases}
            (g'_{n+1}, \tilde{s}_n) & \text{if } c = c'_n \\
            \scheduler'_n & \text{otherwise}
        \end{cases}
    \end{equation*}
    Select $t'_{n+1} = \text{unfold*}(\varphi_n, t_{n+1}) \in g'_{n+1}$
    Recall definition (\todo{ref}), by construction $t'_{n+1}=(\langle l_n,
    \varphi\rangle,p,\tau_i,\eta,\langle l_{n+1}, \varphi_{n+1}\rangle)$
    for some formula $\varphi_{n+1}$.
    \begin{equation*}
        \prSnns(c'_n \rightarrow c'_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s'}_n)(s'_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}(u),s(u)} > 0
    \end{equation*}
    By lemma (\todo{ref}) $s_{n+1} \models \varphi_{n+1}$, fulfilling (3) of the
    induction hypothesis. We fulfill (2) of the induction hypothesis, by
    constructing $c'_{n+1} = (\langle l_{n+1}, \varphi_n\rangle, s_{n+1},
    t'_{n+1})$. By setting $s'_{n+1} = s_{n+1}$ we get $\prSnns(c'_n\rightarrow
    c'_{n+1})= \prSs(c_n \rightarrow c_{n+1})$ and with the induction hypothesis
    \begin{equation*}
        \prSs(f_n) = \prSnns(f'_nc'_{n+1})
    \end{equation*}
    and fulfill (1) of the induction hypothesis.

\end{proof}

\begin{theorem}
    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ there exists a
    markovian scheduler $\scheduler': \confs' \rightarrow \GT' \union
    \{g'_\bot\}$, such that for all finite prefixes $f\in\fpath$ there exists a
    finite prefix $f'\in\fpath'$ with 
    \begin{enumerate}
        \item $\Rt_{\scheduler,s_0}(f) = \Rt_{\scheduler',s_0}(f')$
        \item $\prSs,s_0(f) = \prSns,s_0 = (f')$
    \end{enumerate}
\end{theorem}

\begin{proof}
    The proof will be done in two steps, first a scheduler $\scheduler'$ is
    constructed that will select a similar transition in $P'$ when possible.
    Then we will do an inductive construction over an arbitrary finite using the
    the previously constructed scheduler. 

    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ we construct a
    markovian scheduler $\scheduler': \confs' \rightarrow \GT' \union \{g'_\bot\}$. 
    Note, that in this section primed items are items for $\Prog'$ and unprimed
    items denote items for $\Prog$. Also recall $\confs = \L \union \{l_\bot\}
    \times \T \union \{t_\text{in}, t_\bot\}\times \Sigma$.
    Note that for any transition $t' \in \T'$ of the evaluated program, one can
    find a unique transition $t \in \T$ of the original program that was
    unfolded to $t'$, since every transition is created by exactly one unfold
    operation in (\todo{ref}) of the algorithm. 
    For all versions $\langle l, \varphi\rangle \in \vers$, let $(g, \tilde{s})
    = \scheduler((l, 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 $g\in\GT$ is unfolded to a new
    transition $g'\in\GT'$. Transitions that can not be taken from a state
    $s\models\varphi$ are filtered by a satisfiability check. This consideration
    is especially important because the (memoryless) scheduler selects the
    general transition independently of the fact that a configuration is
    reachable in first place. If this is the case, the new scheduler will select
    any arbitrary other transition. We will see that this doesn't matter, since
    a decision at an unreachable configuration has no impact on the equivalence
    of admissible runs. 
    We define $g' \in \GT'$ to be the general transition created by unfolding
    the general transition $g \in \GT$ or any other general transition 
    \begin{align} 
        \label{eq:schedulerconstruction1}
        \scheduler((l', t', s')) = 
        \begin{cases}
            (g'_\bot, s') & \text{if } l' = l'_\bot \text{ or } t' = t'_\bot\\
            (\unfold^*(\varphi, g), \tilde{s}) & \text{if } s\models\varphi
            \text{ and } g \neq g_\bot\\
            (g'^*, \tilde{s}^*) & \text{if } g'^* \in \unfold^*(\langle
            l,\varphi\rangle) \text{ and } \tilde{s}^* \models \tau_{g'^*}
            exists\\
            (g'_\bot, s') & \text{otherwise}
        \end{cases}
    \end{align}
    The scheduler newly constructed $\scheduler'$ is indeed a scheduler for
    $\Prog'$. We will show items \ref{itm:md1} to \ref{itm:md4} of Definition
    \ref{def:mscheduler}. Let $c' = (l', t', s)$. If $l' = l_\bot$ or $t' =
    t_\bot$, $\scheduler'(c') = (g'_\bot, s)$  follows immediately from the
    construction \ref{eq:schedulerconstruction1}. Next, let $l' \neq l'_\bot$
    and $t' \neq t'_\bot$. Assume $s\not\models\varphi$ the new scheduler
    selects a general transition fulfilling properties (1)-(3) automatically by
    construction. Note that all transitions starting in $l'$ must have been
    created by the unfolding $unfold(l')$ and hence considered by the scheduler
    for selection. 
    Finally assume $s\models\varphi$. If the original scheduler returned $(g,
    \tilde{s}) = \scheduler(c))$ and $g \neq g_\bot$, then $g' =
    \unfold^*(\varphi, g) = \Union_{t\in g} \neq \emptyset$ by lemma () and
    properties (1)-(3) are satisfied
    \begin{enumerate}
        \item $\tilde{s}'(x) = \tilde{s}(x) = s(x)$ for all $x\in\PV$ by
            Definition \ref{def:mscheduler} for $\scheduler$.
        \item $l = l_g$ by Definition \ref{def:mscheduler} for $\scheduler$ and 
            $l' = \langle l, \varphi \rangle = l'_g$ by construction of the
            unfolding (\todo{ref}).
        \item $s \models \tau_g$ by Defeinition \ref{def:mscheduler} and
            $\tau_{g'} = \tau_g$ by construction of the unfolding.
            $s\models\tau_{g'}$ holds.
    \end{enumerate}
    If the original scheduler returned the terminal transition $\scheduler(c)=
    (g_\bot, s)$, then so does the new scheduler $\scheduler(c') = (g'_\bot, s)$
    by construction. This is correct because by lemma (\ref{}). 
    We interject a small observation following from the above, that will be
    useful for the later induction. 
    \begin{lemma}[Corollary] 
        If $s \models \varphi$ then:
        \begin{enumerate}
            \item $(g_\bot, _) = \scheduler(c)$ if and only if $g'_\bot =
            \scheduler'(c')$.
            \item $(g, _) = \scheduler(c)$ and $(g',_) = \scheduler(c')$ with $g
                \neq g_\bot$ and $g' \neq g'_\bot$ then $g$ and $g'$ have the
                same probability $p$.
        \end{enumerate}
    \end{lemma}
    Given an admissible run $f^*= c_0\dots{}c_N\in \fpath$ of the original
    program $\Prog$ with $c_i = (l_i,s_i,t_i)$ for all $i = 0,1,\dots$ and a
    scheduler $\scheduler$ for the very same program. Let $\scheduler'$ be
    constructed as above.
    \textbf{Induction hypothesis.} We can find a prefix
    $f'_n=c'_0c'_1\cdots{}c_n \in \fpath'$ of length $n \leq N$ with 
    \begin{enumerate}
        \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 \C$, $t'_i \in \T'$, and $i = 1, \dots, n$ \label{itm:location_in_version}
        \item $s_i \models \varphi_i$ \label{itm:si_models_phi}
    \end{enumerate}
    Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are useful
    for using the properties of the scheduler but not important for the final
    result.  
    \textbf{Induction start n=0.}
    Since $f^*$ 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 added at first by the
    evaluation algorithm. $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 step.} 
    Assume the induction hypothesis holds for $n < N$ we will construct a prefix
    of length $n+1$ for which the induction hypothesis equally holds. 
    Since the prefix $f$ is admissible, so is its prefix $f_i =
    c_0c_1\dots{}c_nc_{n+1}$ and by definition \todo{ref}
    \begin{equation*}
        \prSs(f) = \prSs(c_0) \cdot \prod_{i=1,\dots,n+1} \prSs(c_{i-1} \rightarrow
        c_i) > 0
    \end{equation*}
    Let $\scheduler(c_n) = (g_{n+1},\tilde{s}_n)$ by definition \todo{ref}
    \begin{equation*}
        \prSs(c_n \rightarrow c_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s}_n)(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}_n(u),s_n(u)} > 0
    \end{equation*}
    Set the state $s'_{n+1} = s_{n+1}$, and the transition $t'_{n+1} =
    \unfold(\varphi_i, t_i)$. $t_{n+1} \in g$ and by construction of the
    unfolding 
    Since $f'_n$ is an admissible path, $\langle l_n, \varphi_n \rangle$ is a valid
    location (version) in $\Prog'$, every version is unfolded by the evaluation
    algorithm immediately after being added to the new program in (\todo{ref}). As
    $g_i$ is selected by the scheduler, $g_{n+1}$ is a general transition with
    $l_{g_{n+1}} = l_n$. As such $g_{n+1}$ is unfolded by the algorithm in
    (\todo{ref}) and so is the transition $t_{n+1}$ as part of unfolding of the
    general transition $g_{n+1}$.
    With $g'_{n+1}=\text{unfold*}(\varphi_n, g_{i+1})$, define the next
    $\scheduler'_{n+1}$ as 
    \begin{equation*}
        \scheduler'_{n+1}(c) = \begin{cases}
            (g'_{n+1}, \tilde{s}_n) & \text{if } c = c'_n \\
            \scheduler'_n & \text{otherwise}
        \end{cases}
    \end{equation*}
    Select $t'_{n+1} = \text{unfold*}(\varphi_n, t_{n+1}) \in g'_{n+1}$
    Recall definition (\todo{ref}), by construction $t'_{n+1}=(\langle l_n,
    \varphi\rangle,p,\tau_i,\eta,\langle l_{n+1}, \varphi_{n+1}\rangle)$
    for some formula $\varphi_{n+1}$.
    \begin{equation*}
        \prSnns(c'_n \rightarrow c'_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s'}_n)(s'_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}(u),s(u)} > 0
    \end{equation*}
    By lemma (\todo{ref}) $s_{n+1} \models \varphi_{n+1}$, fulfilling (3) of the
    induction hypothesis. We fulfill (2) of the induction hypothesis, by
    constructing $c'_{n+1} = (\langle l_{n+1}, \varphi_n\rangle, s_{n+1},
    t'_{n+1})$. By setting $s'_{n+1} = s_{n+1}$ we get $\prSnns(c'_n\rightarrow
    c'_{n+1})= \prSs(c_n \rightarrow c_{n+1})$ and with the induction hypothesis
    \begin{equation*}
        \prSs(f_n) = \prSnns(f'_nc'_{n+1})
    \end{equation*}
    and fulfill (1) of the induction hypothesis.
\end{proof}

Let $\PV \subset \V$ be a finite set of program variables. Let $\Loc$ be a set
of locations, $\T = \L \times [0,1] \times (\PV \rightarrow \Z[\V\union\D)
\times \R \times \Loc$ be the set of transitions over locations $\Loc$. Let $\GT
= 2^{\T}$ be set set of general transitions over $\Loc$. 

    $(\PV, \Loc, \GT, l_0)$ is a probabilistic integer transition system where 

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

        \item $\Loc$ is a finite non-empty set of location
        \item $\GT$ is a finite set of general transitions, where a general 
            transition $g \in \GT$ is a finite non-empty set of transitions 
            $t = (l, p, \tau, \eta, \nu, l')$ with: 

        \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, \nu, l') \in \T_\Prog \subseteq
            \GT_\Prog$ with: 

            Moreover, the probabilities of the 
            transitions must add up to $1$. We call $τ_g$ the guard of 
            the general transition $g$ and $l_g$ the start location

            Moreover, the probabilities of the transitions must add up to $1$.
            We call $τ_g$ the guard of the general transition $g$; and all
            transitions share a common start location which we call $l_g$. 

A state $s$ is a variable assignment for the variables of a program $s: \V
\rightarrow \Z$. \Sigma is the set of all states. The set of configuration is

A state $s$ is a full variable assignment for the variables of a program $s: \V
\rightarrow \Z$. $\Sigma$ is the set of all states. The set of configuration is

t_\bot\} \times \Sigma$. 

t_\bot\} \times \Sigma$.