}
@Article{puterman1990markov,
  author    = {Puterman, Martin L},
  journal   = {Handbooks in operations research and management science},
  title     = {Markov decision processes},
  year      = {1990},
  pages     = {331--434},
  volume    = {2},
  file      = {:/home/paradyx/MA/literatur/putermann1990markov.pdf:PDF},
  groups    = {Probability},
  publisher = {Elsevier},
}
@Book{puterman1994markov,
  author    = {Puterman},
  publisher = {John Wiley \& Sons, Inc},
  title     = {Markov Decision Processes: Discrete Stochastic Dynamic Programming},
  year      = {1994},
  edition   = {1},
  isbn      = {9780470316887},
  series    = {Wiley Series in Probability and Statistics},
  file      = {:/home/paradyx/MA/literatur/puterman1994markov.pdf:PDF},
  groups    = {Probability},
  keywords  = {Statistics},
  language  = {eng},

                          node[anchor=north] {$\begin{aligned}y &> 0\\ y&:= y-1\end{aligned}$}      (l1)

                          node[anchor=north] {$t:\begin{aligned}y &> 0\\ y&:= y-1\end{aligned}$}      (l1)

    \node[state]            (l3')   [below left=of l2]     {$\langle l_2, \textit{false}\rangle$};

    \node[state]            (l3')   [below left=of l2,gray]{$\langle l_2, \textit{false}\rangle$};

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

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

                (l2)      edge      node[swap]{$x \leq 0$}            (l3')

                (l2)      edge[gray]node[gray,swap]{$x \leq 0$}    (l3')

                (l3)      edge      (l4')

                (l3)      edge[gray]      (l4')

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

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

                              $\begin{aligned}

                              $t_2: \begin{aligned}

changes state with every transition. The configruation at a given point of the

changes state with every transition. The configuration at a given point of the

impossible: First, the number of starting states is infinte; second the

impossible: First, the number of starting states is infinite; second the

but also on the answer of some oracle, determining possibly the transition or the
value variables after the transition.
So, instead of simulating every single possible run, it would be nice to treat
\enquote{similar} states as one, for sake of execution. Instead of processing a
single assignment, the space of all possible assignments at a location is
described by a set of constraints. The resulting graph is called a
\textit{partial evaluation graph}. It was formalized for \gls{chc} by
\citeauthor{gallagher2019eptcs}. In this thesis the definitions are adapted to
better fit the algorithm and the formalisms of \Glspl{pip}. 

but also on the answer of the scheduler and some random event. 
Instead of simulating every single possible run, it would be nice to treat
\enquote{similar} states as one. Instead of simulating a single assignment, 
the set of all possible assignments after a step is described by a polyhedron. 
The resulting graph is called a \textit{partial evaluation graph}. It was
formalized for \gls{chc} by \citeauthor{gallagher2019eptcs}. In this thesis the
definitions are adapted to better fit the algorithm and the formalisms of
\Glspl{pip}. 
In order to guarantee termination, as will be elaborated further later on, a
finite set of abstracted values (not to be confused with abstract domains, such
as polyhedra etc.) is required. For now the set of abstracted values shall be a
finite set $\A \subset \C$.

Given \gls{pip} $P$ with locations $L$, transitions $T$ and general transitions
$G$. Versions are the vertices of the partial evaluation graph. They contain the
location at each step of the evaluation and a representation of the possible
assignments at each step of the evaluation. Versions can contain just
constraints, but in order to guarantee a finite graph later on, they can also
contain an value from an abstraction space (see \Sref{sec:abstraction_layer},
not to be confused with the abstract domains).

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. 

    \begin{equation}

    \begin{equation*}

    \end{equation}

    \end{equation*}

    For clarity sake, versions will be denoted with angles. 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$.

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

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

locations. 

locations.

    \gls{pip} $P$ when for every admissible path $c_0c_1\dots{}c_n \in \fpath$
    of P 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:

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

            \in \C$ and $t_i' \in E(G)$,

            \in \C$ and $t_i' \in \T_{PE}$,

The partial evaluation is done step-wise. On every step the next version
$v' = \langle l', \phi'\rangle$ is computed by unfolding a transition $t \in \T$

The partial evaluation is done iteratively. On every step the next version $v' =
\langle l', \varphi'\rangle$ is computed by unfolding a transition $t \in \T$

version $v = \langle l, \phi\rangle$. The resulting constraint $\phi'$ contains
all states $s' \in \Sigma$ with $s' \models \phi'$ reachable via the transition
from a state in the source version, i.e. $\prSs((l, s, \_) \rightarrow (l',s',t))
> 0$. 

version $v = \langle l, \varphi\rangle$. The resulting constraint $\phi'$
contains all states $s' \in \Sigma$ with $s' \models \varphi'$ reachable via the
transition from a state in the source version, i.e. $\prSs((l, s, \_)
\rightarrow (l',s',t)) > 0$. 

\begin{definition}[Non-probabilistic overapproximation\label{def:nonprobapprox}]
    Let $\eta: \PV \rightarrow \Z[\V\union D]$ be a probabilistic update
    function, with random distributions $D_1,\dots,D_n$ used within.  A
    \textit{non-probabilistic over-approximation} is a pair $(\lfloor\eta\rceil,
    \tilde{\eta}) \in \C \times (\PV \rightarrow \Z[\V])$ where 
    \begin{equation}
        \lfloor\eta\rceil = \LAnd_{x\in\PV} (x' = \eta(x)[D_i\backslash{}d_i])
        \land \LAnd_{i=1,\dots,n} \lfloor D_i \rceil \\
    \end{equation}
    \begin{equation}
        \tilde{\eta}(x) = x' \hspace{1cm} \text{for all } x\in\PV
    \end{equation}
    for some fresh temporary variables $x', d_i\in \TV$.

\begin{definition}[Unfolding]
    An unfolding operation $\unfold : \C \times (\PV \rightarrow
    \Z[\V\union\D)]) \rightarrow \C$ of a formula $\varphi \in \C$ with an
    update $\eta: \PV\rightarrow\Z[\V \union \D]$ is defined as 
    \begin{align*}
        \unfold(\varphi, \eta) = \begin{cases}
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)|_{\PV} & \text{if }
            \tilde{\eta}(\varphi \Land \lfloor\eta\rceil) \text{ is
            SAT}\\ 
            \textit{false} & \text{otherwise}
        \end{cases}
    \end{align*}

\begin{lemma}
    For any assignment $s,s'\in\Sigma$, and probabilistic update $\eta: \PV
    \rightarrow \Z[\V \union D]$ holds $s'(x_i) = k_i \in
    \text{supp}([\eta(x_i)](s))$ implies $s'\models \tilde{\eta}()$

\begin{lemma}[\label{lem:unfold}]
    For any assignment $s,s' \in\Sigma$, $\varphi\in\C$ and probabilistic update
    $\eta : \PV \rightarrow \Z[\V\union\D]$, if $s\models\varphi$, and $s'
    \in \support_s(\eta(s))$ then $s' \models \unfold(\varphi, \eta)$

    and values $k_i \in
    \text{supp}([\eta(x_i)](s))$, the assignment $s'(x_i)=k_i$ satisfies the
    non-probabilistic over-approximation \todo{todo}

    \begin{proof}
        Follows from Lemma \ref{lem:prob_update}.
    \end{proof}

\begin{definition}[Unfolding constraints]
    Let $\varphi \in \C$ be a constraint and $t = (\_, \tau, \eta, \_, \_) \in
    \T$. An unfolding of $\varphi$ via $t$ is defined as follows.
    \begin{align}
        \unfold(\varphi, t) = \begin{cases}
            \eta(\varphi \Land \tau \Land \lfloor\eta\rceil)|_{\PV} & \text{if }
            \tilde{\eta}(\varphi \Land \tau \Land \lfloor\eta\rceil) \text{ is
            SAT}\\ 
            \textit{false} & \text{otherwise}
        \end{cases}
    \end{align}
\end{definition}

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

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. 
Given an unfolding one can derive an unfolding operation $\unfold^*: \C \times
\T \rightarrow 2^{\T_{PE}}$ that constructs a new transition between the

Using the unfolding, one can derive an unfolding operation $\unfold^*: \vers
\times \T \rightarrow 2^{\T_{PE}}$ that constructs a new transition between the

ignored and no transition is created.  

ignored and no transition is created. 

\begin{align}
    \unfold^*(\varphi, (l, \tau, \eta, p, l')) = \begin{cases}
        \{(\langle l, \varphi\rangle, \tau, \eta, p, \langle l',
        \unfold(\varphi, t)\rangle \} & \unfold(\varphi, t) \text{ if is SAT} \\

\begin{align*}
    \unfold^*(\langle l,\varphi\rangle, t) = 
    \begin{cases}
        \{(\langle l, \varphi\rangle, p, \tau, \eta,\langle l',\varphi'\rangle
        \} & \text{if } t = (l, p, \tau, \eta, l') \\ &
        \text { and } \varphi' = \unfold(\varphi, t) \text{ is SAT} \\

\end{align}

\end{align*}
The following lemma proves that the new transition is similar enough to the
original transition.
\begin{lemma}\label{lem:unfold_t}
    L $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s,
    s' \in \Sigma$ assignments, and let $\varphi \in \C$. 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{enumerate}
        \item\label{itm:t_exists} $\unfold^*(\langle l, \varphi\rangle, t') =
            \{t^*\}$ for some $t^* \in \T_\text{PE}$, 
        \item\label{itm:t_equal} $t^* = (\langle l, \varphi\rangle, p, \tau,
            \eta, \langle l', \varphi'\rangle)$ for some $\varphi' \in \C$, and 
        \item\label{itm:smodelsphi}$s' \in \llbracket\varphi'\rrbracket$
    \end{enumerate}

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

    \begin{proof}
        Let $s_0\in\Sigma$ and $\scheduler$ be any scheduler 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 and $t' = (l,
        p, \tau, \eta, l')$ for some $p \in [0,1]$, $\tau \in C$, and $\eta :
        \PV \rightarrow \Z[\V \union \D]$. It remains to be shown that item
        \ref{itm:smodelsphi} $s' \models \varphi' = \unfold(\varphi \land \tau,
        t)$ holds, then \ref{itm:t_exists} and \ref{itm:t_equal} follow from
        construction. 
         
        By Definition \ref{def:mscheduler}, $\tilde{s} \models \tau_{g'} =
        \tau$, and $s = \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*}

        Using Lemma \ref{lem:unfold} we get $s' \models \unfold(\varphi \Land
        \tau,\eta)$, completing the proof.
    \end{proof}
\end{lemma}
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.

Again the operation is overloaded with a function $\unfold^* : \vers \rightarrow
2^{\T_{PE}}$ unfolding all outgoing general transitions in the \gls{pip} $P$.

\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 Lemma \ref{lem:unfold_t}.
    \end{proof}
\end{lemma}
\begin{lemma}[Soundness\label{lem:unfold_sound}]
    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. 
    \begin{proof}
        \todo{proof}
    \end{proof}
\end{lemma}
The operation is overloaded a last time, with a function $\unfold^* :
\vers \rightarrow 2^{\T_{PE}}$ unfolding all outgoing general transitions in the
\gls{pip} $\Prog$.

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

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

\begin{example}

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

\end{example}

\end{lemma}
Lets recap what we just constructed. A source constraint $\varphi\in\C$
describes a set of states. The unfolding computes a new (target) constraint
describing (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 unfoldings 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. 

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 the version. It adds all created
transitions to the evaluation graph and proceeds with unfolding all newly
encountered version. The algorithm is shown in Algorithm
\ref{alg:naive_evaluation}

    \caption{$evaluate(P, G, v)$}

    \caption{Evaluate a Program $\Prog$.\label{alg:naive_evaluation}}

    $N = \unfold^*(v)$\;
    \For{$t = (v, \tau, \eta, p, v') \in N $}{
        \If {$v' \not\in G$}{
            $G := G \union \{t\}$\;
            $G := evaluate(P, G, v')$\;
        }
        \Else {
            $G = G \union \{t\}$\;

    \SetKwFunction{FEvaluate}{evaluate}
    \SetKwProg{Fn}{Function}{:}{end}
    \Fn{\FEvaluate{$G$, $v$, $t$}}{
        $N \leftarrow \unfold^*(v)$\;
        \For{$g \in N$}{
            \For{$t = (v, \tau, \eta, p, v') \in g, $}{
                \uIf {$v' \not\in V(G$}{
                    $G \leftarrow G + t$\;
                    $G \leftarrow evaluate(P, G, v')$\;
                }
                \Else {
                    $G \leftarrow G + t$\;
                }
            }

        \Return {$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$

    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{subcaptiongroup}
            \subcaptionlistentry{Program}

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

            \subcaptionlistentry{Extract of the evaluation tree}

            \caption{A Program $\Prog$\label{fig:ch3_inf_prog}}
        \end{subcaptionblock}
        \begin{subcaptionblock}[t]{0.6\textwidth}

        \end{subcaptiongroup}
        % \subbottom[Program]{
        %     \input{figures/ch3_example1_program.tex}
        % }
        % \subbottom[Extract of the evaluation tree]{
        %     \input{figures/ch3_example1_tree.tex}
        % }
        \caption{Foo}
    \end{figure} \todo{ref}
    \begin{figure}
        \centering
        \begin{subcaptiongroup}
            \subcaptionlistentry{Program}
            \input{figures/ch3_example2_program.tex}
            \subcaptionlistentry{Extract of the evaluation tree}
            \input{figures/ch3_example2_tree.tex}
        \end{subcaptiongroup}
        % \subbottom[Program]{
        %     \input{figures/ch3_example2_program.tex}
        % }
        % \subbottom[Extract of the evaluation tree]{
        %     \input{figures/ch3_example2_tree.tex}
        % }
        % \caption{Foo}
    \end{figure} \todo{ref}

            \caption{Extract of the infinite evaluation graph of
            $\Prog$\label{fig:ch3_inf_tree}}
        \end{subcaptionblock}
        \caption{An simple example program with an infinite evaluation graph.\label{fig:ch3_inf}}
    \end{figure}

As already stated above, the evaluation tree is possibly infinite and computing
the whole evaluation tree would be very inefficient. For example versions can
repeat and it would be better to loop back to the already existing version
instead of continuing the evaluation. This by it self is unfortunaetly not
enough. 

Comparing set's of constraints for equality is hard \todo{citation} and hence
detecting repetitions impossible to do efficiently. One could recur to
structural equality instead, and just accept the impreciseness, but even then,
nothing guarantees that the infinite paths in the evaluation tree have repeating
versions. 
\begin{example}
    \todo{example of loop incrementing the bound by one in every step.}
\end{example}

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
$\langle l_1,x>1\rangle$ instead, but preserving the branch at $\langle l_1,
\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. 

Instead a version is abstracted to a less tight but easy to compare
representation. Choosing only a finite number of abstractions and guaranteeing
that every infinite path is abstracted at some point, will guarantee the
termination of the evaluation. 

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_evaluation_inclusion} of
\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. 

\section{Abstraction}\label{sec:abstraction}

\todo{definition}

    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\in\C$,
    $\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 : \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) &= \Union_{g \in \Tout(l)}
    \unfold^*_\alpha(\langle l,\varphi\rangle, g)  \\
\end{align*}
Since $\llbracket\varphi\rrbracket \subseteq \llbracket
\alpha(\varphi)\rrbracket$, Lemma \ref{lem:unfold_t} to \ref{lem:unfold_v} hold
equally for $\unfold_\alpha^*$.

\subsection{Constructing the scheduler}
\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. 

\subsection{Induction}
Given an admissible run $f^*= c_0c_1\dots \in \runs$ 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. 

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

\textbf{Induction hypothesis.} We can find an arbitrarily long prefix
$f'_n=c'_0c'_1\cdots{}c_n \in \fpath'$ of length $n \in \N$ and scheduler
$\scheduler'_n$ such that:
\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}

    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}

Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are only
required for the induction, but are unimportant for the final result. 

    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 start n=0.}
Since $f^*$ is an admissible run, $c_0 = (l_0, s_0,t_\text{in})$. Set
$f'_0=(\langle l_0,\textit{true}\rangle,s_0,t_\text{in})$. $\langle l_0,
\textit{true}$ 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 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}

\textbf{Induction step.} 
Assume the induction hypothesis holds for $n$ we will construct a prefix of
length $n+1$ for that the hypothesis equally holds. 

    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.  

Since the run 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*}

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

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

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

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

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

Select $t'_{n+1} = \text{unfold*}(\varphi_n, t_{n+1}) \in g'_{n+1}$

    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.

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

\end{proof}

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

\subsection{Induction}

\newcommand{\Rt}[0]{\mathcal{R}} %Runtime

\newcommand{\Cost}[0]{\mathcal{R}} % Costs
\newcommand{\Rt}[0]{\mathcal{R}^1} %Runtime

\newcommand{\A}[0]{\mathcal{A}} % Abstract values

\newcommand{\unfold}[0]{\text{unfold}}

\newcommand{\unfold}[0]{\mathrm{unfold}}

\newcommand{\Tin}[0]{\T_\text{in}}
\newcommand{\Tout}[0]{\T_\text{out}}

\newcommand{\Tin}[0]{\T_\mathrm{in}}
\newcommand{\Tout}[0]{\T_\mathrm{out}}

\newcommand{\support}[0]{\mathrm{supp}}

    Let $\varphi_1, \varphi_2$ be FO-formulas with variables $\V$. If $\varphi_1
    \models \varphi_2$, then $\llbracket \varphi_1 \rrbracket \subseteq
    \llbracket \varphi_2 \rrbracket$ and we say that $\varphi_1$
    \textit{entails} $\varphi_2$.

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

    $\varphi_1$ entails $\varphi_2$ if and only if $\varphi_1 \lor \neg
    \varphi_2$ is unsatisfiable.

    $\varphi_1$ entails $\varphi_2$ if and only if $\varphi_1 \Land
    \neg\varphi_2$ is unsatisfiable.

        Assume $\varphi_1$ entails $\varphi_2$. Let $\beta \models \varphi_1$ be
        any satisfying assignment of $\varphi_1$. From the assumption follows
        $\beta \models \varphi_2$ and in turn $\beta \not\models
        \neg\varphi_2$ by FO-semantics.
        Since every satisfying assignment of $\varphi_1$ cannot satisfy $\neg
        \varphi_2$ at the same time, $\varphi_1 \land \neg \varphi_2$ has no
        satisfying assignments.

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

Let $\varphi \in \C$ we write $u(\varphi)$ to denote the constraint 
\begin{equation}
    u(\varphi)(s) = \LAnd_{x_i\in A} x'_i = 
\end{equation}

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

\begin{lemma}[Update constraints]
    Let $s \in \Sigma$. If 

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

\subsection{Polynomials over distributions}

\subsection{Polynomials over distributions}\label{ssec:prob_update}

Under misuse of notation we write $f(s)$ to denote the unique value $v$ with
$f(s)(v) = 1$, when it exists. \todo{check if actually used}
The support of polynomial $f$ with an assignment $s$ is the set of values that
can be achieved with the polynomial by sampling the random distributions.

% Under misuse of notation we write $f(s)$ to denote the unique value $v$ with
% $f(s)(v) = 1$, when it exists. \todo{check if actually used}
% The support of polynomial $f$ with an assignment $s$ is the set of values that
% can be achieved with the polynomial by sampling the random distributions.

\begin{definition}[Probabilistic update]
    Similar to Definition \ref{def:update}, a probabilistic update is described
    by a function $\eta: A \rightarrow \Z[\V\union\D]$ that maps a probabilistic
    polynomial over $\V$ to every variable $x\in A$ and is undefined otherwise. 
    The value after the update is determined by evaluating the probabilistic
    polynomial.
\end{definition}
The support of the update $\eta A \rightarrow \Z[\V\union \D]$ on an assignment
$s \in \Sigma$ is the set $\support_s(\eta)=\set{s' \in \Sigma}
{[\eta(x)](s)(s') > 0 \text{ for all } x\in A }$.
\subsection{Non-probabilistic approximation}
A probabilistic polynomial is a random variable, that evaluates to a random
value. The random value can be approximated by a non-probabilistic polynomial
with fresh variables and a constraint, constraining the value of those newly
introduced variables. 
\begin{definition}[Non-probabilistic over approximation of probabilistic
    polynomials] 
    Let $f \in \Z[\V\union\D]$ be a probabilistic polynomial with probability
    distributions $D_1,\dots,D_n$ used within. Then the non-probabilistic
    over-approximation of a probabilistic polynomial is defined as the tuple
    $(\lfloor f\rceil,\tilde{f})$  with
    \begin{align*}
        \lfloor f \rceil = \LAnd_{i=1,\dots,m} \lfloor D_i \rceil \\
        \tilde{f} = f[D_i\backslash{}d_i] \text{ and }
    \end{align*}
\end{definition}
A probabilistic update can be over-approximated by using the non-probabilistic
over-approximation of all used probabilistic polynomials in the update. 
\begin{definition}[Non-probabilistic over-approximation\label{def:nonprobapprox}]
    Let $A\subset\PV$ be a set of variables and $\eta: A \rightarrow \Z[\V\union
    D]$ be a probabilistic update function. A \textit{non-probabilistic
    over-approximation} of the update $\eta$ is a pair $(\lfloor\eta\rceil,
    \tilde{\eta}) \in \C \times (\PV \rightarrow \Z[\V])$ where 
    \begin{align*}
        \lfloor\eta\rceil = \LAnd_{x\in\PV} x' = \tilde{\eta(x)} \Land
        \lfloor\eta(x)\rceil \\
        \tilde{\eta}(x) = x' \hspace{1cm} \text{for all } x\in\PV
    \end{align*}
    for some fresh temporary variables $x', d_i\in \TV$.
\end{definition}
\begin{lemma}\label{lem:prob_update}
    For any assignment $s,s'\in\Sigma$, $A \subset \V$, probabilistic update
    $\eta: A \rightarrow \Z[\V \union D]$, and formula $\varphi \in \C$, if $s'
    \in \support_s(\eta)$ and $s \models \varphi$ then $s' \models
    \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)$.

    \begin{proof}
        Assume $s' \in \support_s(\eta)$ and $s \models \varphi$. 
        We define a new assignment $\tilde{s} = s$ that will be expanded later
        on. For all $x \in
        A$ holds $[\eta(x)](s)(s'(x)) > 0$. Let $D_1,\dots,D_m \in \D$ be the
        distributions within $[\eta(x)]$. 
        \begin{align*}
            0 &< [\eta(x)](s)(s'(x)) \\
              &= \sum_{\substack{a_i \in \Z \\ i = 0,\dots,m}} D_1(a_1)
    \cdot D_2(a_2) \cdots D_m(a_m) \cdot 
            \begin{cases}
                1, & \text{if } f[x_i \backslash s(x_i)][D_i\backslash a_i] =
                s'(x) \\
                0, & \text{otherwise}
            \end{cases}
        \end{align*}
        There must exist $a_1,\dots, a_m\in \Z$ such that 
        \begin{equation*}
            0 < D_1(a_1) \cdot D_2(a_2) \cdots D_m(a_m)\text{ and }
            f[x_i \backslash s(x_i)][D_i\backslash a_i] = s'(x)
        \end{equation*}
        Without loss of generality, let $d_i$ for $i=1,\dots,m$ be new variables
        that are undefined by $\tilde{s}$. We expand the assignment $\tilde{s}$
        as follows:
        \begin{align*}
            \tilde{s} = \begin{cases}
                a_i & \text{for } x = d_i, i=1,\dots,m \\
            \end{cases}
        \end{align*}
        By construction $s = \tilde{s}|A$. Since $d_1,\dots,d_m$ are fresh
        variables, and $s \models \varphi$, so does $\tilde{s} \models \varphi$.
        Besides the following holds:
        \begin{align*}
            &D_i(a_i) > 0 \text{ for all } i=1,\dots,m \\
            \Leftrightarrow& s \models \lfloor D_i \rceil \text{ for all } i
            =1,\dots,m \\
            \Leftrightarrow& s\models \LAnd_{i=1,\dots,m} \lfloor D_i \rceil \\
            \Leftrightarrow& s\models \lfloor \eta(x) \rceil
        \end{align*}
        Since the above holds for all $x \in A$, 
        \begin{equation*}
            \tilde{s} \models \LAnd_{x \in A} \lfloor \eta(x) \rceil = \lfloor
            \eta \rceil
        \end{equation*}
        By Lemma \ref{lem:nonprop_update}, follows $s' \models
        \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)$
    \end{proof}
\end{lemma}
% \begin{lemma}
%     $s'\models\eta(varphi)$
%     $s'(x_i) = k_i \in
%     \text{supp}([\eta(x_i)](s))$ implies $s'\models \tilde{\eta}(\)$
    % and values $k_i \in
    % \text{supp}([\eta(x_i)](s))$, the assignment $s'(x_i)=k_i$ satisfies the
    % non-probabilistic over-approximation \todo{todo}
    % \begin{proof}
    % \end{proof}
% \end{lemma}

            $t = (l, p, \tau, \eta, l')$ with: 

            $t = (l, p, \tau, \eta, \nu, l')$ with: 

                \item an associated cost $\nu\in\R$

\subsection{Probability space of a program\label{ssec:probabilityspace}}

\subsection{\gls{pip} as a Markov decision process}
We will first introduce the Markov decision process in general and then apply
the concept to a run of a \gls{pip}. In general a Markov decision process
contains five parts:
\begin{enumerate}
    \item \textit{decision epochs}, are points in time, at which a decision is
        made;
    \item \textit{states}, the decision process is in at a decision epoch;
    \item \textit{actions}, that are selected by the decision process;
    \item \textit{transition probabilities}, that describe the probabilities of
        states transitioned into after a certain action was taken; and finally
    \item \textit{rewards}, that are accumulated over the whole decision process
        with every action.\cite{puterman1994markov}
\end{enumerate}

For a \gls{pip} one can define a probability space $(\runs, \F, \PrSs)$, where the
outcomes of the probabilistic event are the runs on the program. Every distinct
run is measurable hence the $\sigma$-algebra $\F$ is defined to contain every
set ${r} \in \F$ for $r \in \runs$. The probability measure $\prSs$ describes
the probability of the given run for a scheduler $\scheduler$ and the input
given to the program as the initial state $s_0$. Formally the probability space
is defined by a cylindrical construction expanding the length of finite prefixes
up to infinity. For the detailed construction we'll refer to \cite{meyer20arxiv}.

One can easily see the similarities to runs in a \gls{pip}. The steps of a
program are the decision epochs of the Markov decision process. The states of
the program, are the states of the decision process. Non-deterministic sampling,
non-deterministic branching are similar to choosing an action, and the
transition probabilities describe the probabilities of the probabilistic
branching and sampling. 
The reward is usually the optimization goal, of the Markov decision process, and
the literature describes the properties of a given process with regard to the
highest achievable rewards. That is, one looks for a decision policy that
returns the highest accumulated rewards over a whole process.
The goal of termination analysis is to find upper bounds for the runtime
complexity and runtime costs. If define runtime (or costs) as reward, we can
picture the Markov decision process as an adversary, finding the decision policy
with the longest runtime. 
Some side notes: 
\begin{enumerate}
    \item The decision epochs are the steps of the program. There are
        infinitely many. Hence this is a infinite horizon Markov decision
        process.
    \item the states are the configurations $\confs$ of the program
    \item the actions are the selection of a general transition and full
        assignments that satisfy a guard of of the selected general transition,
        or the terminating transition.
    \item the transition probability will be defined later in
        \Sref{ssec:probabilityspace}
    \item the reward is 1 for every non terminating transition
\end{enumerate}

On any given configuration a scheduler resolves the non-determinism first. The
probability measure will use the result of the scheduler instead of the previous
configuration. The scheduler keeps the values of all program variables from the
previous configuration. It selects a general transition $g$ and a variable
assignment $\tilde{s}$ satisfying the guard of the general transition. If no
such transition is found of the program is already in the terminating state
$l_\bot$ it takes the special transition $g_\bot$ indicating termination.

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

\begin{definition}[Scheduler]\label{def:scheduler} \cite{meyer20arxiv}

The adversary that uses a stationary policy to decide the non-deterministic
sampling branching and branching deterministically for us, is called scheduler.
We differentiate between two types of schedulers: First the scheduler that at a
given state always takes the same decision -- it has no memory of it's past
decisions and is not influenced by them. It is called a \textit{Markovian
scheduler}. 
\begin{definition}[Markovian Scheduler\cite{meyer20arxiv}\label{def:mscheduler}]

    scheduler if for every configuration $c = (l,t,s) \in \confs$,
    $\scheduler(c) = (g, s')$ implies:

    Markovian (memoryless) scheduler if for every configuration $c = (l,t,s) \in
    \confs$, $\scheduler(c) = (g, s')$ implies:

        \item \label{itm:scheduler1} $s'(x) = s(x)$ for all $x \in \PV$ 

        \item \label{itm:md1} $s'(x) = s(x)$ for all $x \in \PV$ 

        \item \label{itm:scheduler3} $s' \models \tau_g$ for the guard $\tau_g$ of the general
            transition $g$. 
        \item $g = g_\bot$ and $s' = s$, if $l=l_bot$, $t=t_\bot$, or no $g' \in
            \GT$ and $s'\in \Sigma$ satisfy \cref{itm:scheduler1} to
            \cref{itm:scheduler3}

        \item \label{itm:md3} $s' \models \tau_g$ for the guard $\tau_g$ of the
            general transition $g$. 
        \item $g = g_\bot$ and $s' = s$, if $l=l_\bot$, $t=t_\bot$, or no $g'
            \in \GT$ and $s'\in \Sigma$ satisfy \cref{itm:md1} to \cref{itm:md3}
            \label{itm:md4}

\begin{rem}
    Although the decision rule selecting the action (non-deterministic sampling
    and branching) is deterministic, the new state is not. After selecting the
    action the new state is determined by the probability distribution described
    by the \textit{transition probabilities}.
\end{rem}

The second type is a scheduler that remembers its past decisions. It is called
a history dependent scheduler. 
\begin{definition}[History dependent scheduler]
    A function $\scheduler : \fpath \rightarrow (\GT \uplus \{g_\bot\})$ is a
    history dependent scheduler if for every finite prefix $f\in\fpath$ and
    configuration $c=(l,t,s) \in
    \confs$, $\scheduler(fc) = (g, s')$ implies: items \ref{itm:md1} to
    \ref{itm:md4} of Definition \ref{def:mscheduler}.
\end{definition}
\subsection{Probability space of a program\label{ssec:probabilityspace}}
For a \gls{pip} one can define a probability space $(\runs, \F, \PrSs)$, where
the outcomes of the probabilistic event are the runs on the program. Every
distinct run is measurable hence the $\sigma$-algebra $\F$ is defined to contain
every set ${r} \in \F$ for $r \in \runs$. The probability measure $\prSs$
describes the probability of the given run for a scheduler $\scheduler$ and the
input given to the program as the initial state $s_0$. Formally the probability
space is defined by a cylindrical construction expanding the length of finite
prefixes up to infinity. For the detailed construction we'll refer to
\cite{meyer20arxiv}.
On any given configuration a Markovian scheduler resolves the non-determinism
first. The probability measure will use the result of the scheduler instead of
the previous configuration. The scheduler keeps the values of all program
variables from the previous configuration. It selects a general transition $g$
and a variable assignment $\tilde{s}$ satisfying the guard of the general
transition. If no such transition is found of the program is already in the
terminating state $l_\bot$ it takes the special transition $g_\bot$ indicating
termination.

the configuration $c$ with $c' = (l', t', s')$ and $t' = (l, p, \tau, \eta, l')
\in g$ depends on three things: First the transition $t \in g$ is taken with the
probability $p$, second the probability that each program variables $x\in\PV$ is
updated to the value $s'(x)$ by the probabilistic update - recall definition
\ref{def:polyindeterminates}, third that the temporary variables are sampled by
the scheduler equal to the target state. The result is the probability measure
$\prSs: \confs^2 \rightarrow [0,1]$. 

the configuration $c$ with $c' = (l', t', s')$ and $t' = (l, p, \tau, \eta, \_,
l') \in g$ depends on three things: First the transition $t \in g$ is taken with
the probability $p$, second the probability that each program variables
$x\in\PV$ is updated to the value $s'(x)$ by the probabilistic update - recall
definition \ref{def:prob_update}, third that the temporary variables are
sampled by the scheduler equal to the target state. The result is the
probability measure $\prSs: \confs^2 \rightarrow [0,1]$. 

\subsection{Bounds}
The whole goal of \gls{koat}'s analysis is to find bounds. A bound is an
expression that describes the upper limit of a property of the program.

\subsection{Costs and Runtime-complexity}
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}[Bounds\cite{meyer2021tacas}]\label{def:bounds}
    The set of bounds $\B$ is the smallest set with $\PV \union \R_{\geq 0}
    \subseteq \B$, and where $b_1,b_2 \in \B$ and $v\in \R_{\geq 1}$ imply $b_1 +
    b_2, b_1 \cdot b_2 \in \B$ and $v^{b_1} \in \B$.

\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{\nu_{t_i}}{c_i = (l_i, t_i, s_i) \text{
            and } t_i \neq t_\bot}|
    \end{equation*}

During analysis of classical integer programs, one is especially interested in
runtime and size bounds. A runtime bound is an upper bound on the number of
visits to a transition in the program over all admissible runs, whereas a size
bound describes the highest value of a program variable observed at a
transition over all admissible runs. Because the values observed in a run are
highly dependent on the decisions made by the scheduler $\scheduler$, the bounds 
we take the supremum over all $\scheduler$. One can also picture the scheduler 
as an adversary that always takes the worst decision possible for runtime and
size-bounds.

\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}
The runtime complexity is the number of non-terminating transitions visited
during a run. 

\begin{definition}[Runtime and Size Bounds\cite{meyer2021tacas}\label{def:runtimebounds}]
    $\RB: \T \rightarrow \B$ is a runtime bound and $\SB: \T \times \V
    \rightarrow \B$ is a size bound if for all transitions $t\in\T$, all
    variables $x\in\V$, all schedulers $\scheduler$, and all states $s_0 \in
    \Sigma$, we have
    \begin{align*}
        &|s_0|(\RB(t)) \geq \sup \set{ |\set{i}{t_i =
        t}|}{f=(\_,t_0,\_)\dots(\_,t_n,\_), \prSs(f) > 0} \\
        &|s_0|(\SB(t, x)) \geq \sup \set{ |s(x)| }{f=\dots(\_,t,s), \prSs(f) >
        0}.
    \end{align*}

\begin{definition}[Runtime complexity]
    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:
    \begin{equation*}
        \Rt(\Prog)(c_0c_1\dots) = |\set{i}{c_i = (l_i, t_i, s_i) \text{ and } t_i \neq t_\bot}|
    \end{equation*}

In probabilistic programs not only the worst case is of interest, but also the
probable case. For example a program might run indefinitely in the worst case
but the worst-case has a probability approaching zero. The expected bounds are
defined using the expected value of random variables in the probability space
$(\runs, \F, \PrSs)$ defined in \Sref{ssec:probabilityspace}. Moreover, recall
definition \ref{def:expected_value}.

\begin{definition}[Expected runtime complexity, \acrshort{past}]
    For a scheduler $\scheduler$ and a start location $s_0 \in \Sigma$ the
    expected runtime complexity $\Rt{\scheduler,s_0}(\Prog)$ of a program
    $\Prog$ is defined as the expected value of the runtime complexity. 

\begin{definition}[Expected Runtime Complexity, \acrshort{past}
    \cite{meyer2021tacas}\label{def:past}]
    For $g \in \GT$ its runtime is the random variable $\Rt(g)$ where $R: \GT
    \rightarrow \runs \rightarrow \overline{\N}$ with \begin{equation}
    \Rt(g)((\_,t_0,\_)(\_,t_i,\_)\dots) = |\set{i}{t_i \in g}|. \end{equation}
    For a scheduler $\scheduler$ and starting state $s_0\in\Sigma$, the expected
    runtime complexity of $g\in\GT$ is $\E_{\scheduler,s_0}(\Rt(g))$ and the
    expected runtime complexity of $\Prog$ is $\sum_{g\in\GT}\E_{\scheduler,
    s_0}(\Rt(g)))$.

    \begin{equation*}
        \Rt_{\scheduler,s_0}(\Prog) = \ESs(\Rt(\Prog))
    \end{equation*}

The expected size bound is defined similarly 
\begin{definition}[Expected Size
    Complexity\cite{meyer2021tacas}\label{def:expectedcomplexity}]
    The set of general result variables is $\GRV = \set{(g,l,x)}{g\in\GT,
    x\in\PV, (\_,\_,\_,\_,l) \in g}$. The size of $\alpha = (g,l,x) \in \GRV$ is
    the random variable $\S(\alpha)$ where $\S : \GRV \rightarrow (\runs
    \rightarrow \overline{N})$ with
    \begin{equation}
        \S(g,l,x)((l_0,t_0,s_0)(l_1,t_1,s_1)\dots) = \sup \set{|s_i(x)|}{l_i =
        l, t_i \in g}.
    \end{equation}
    For a scheduler $\scheduler$ and starting state $s_0$, the expected size
    complexity of $\alpha \in \GRV$ is $\E_{\scheduler,s_0}(\S(\alpha))$.
\end{definition}

The runtime complexity is a special case of the cost of a run, where every
transition has an associated cost of $\nu_t=1$ for all $t \in \T$. Then 
\begin{equation}
    \Rt_{\scheduler,s_0}(\Prog) = \Cost_{\scheduler, s_0}(\Prog)
\end{equation}
\subsection{Bounds}
The primary goal of \gls{koat}'s analysis is to find bounds for the
runtime-complexity bounds. A bound is an expression that describes the upper
bound of the costs or runtime complexity the program.

\begin{definition}[Expected Runtime and Size
    Bounds\cite{meyer2021tacas}\label{def:expectedbounds}]\phantom{ }
    \begin{itemize}
        \item $\RBe : \GT \rightarrow \B$ is an expected runtime bound if for
            all $g\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
            have $|s_0|(\RBe(g)) \geq \ESs(\Rt(g))$.
        \item $\SBe : \GRV \rightarrow \B$ is an expected size bound if for
            all $\alpha\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
            have $|s_0|(\SBe(g)) \geq \ESs(\S(g))$.
    \end{itemize}

\begin{definition}[Bounds\cite{meyer2021tacas}]\label{def:bounds}
    The set of bounds $\B$ is the smallest set with $\PV \union \R_{\geq 0}
    \subseteq \B$, and where $b_1,b_2 \in \B$ and $v\in \R_{\geq 1}$ imply $b_1 +
    b_2, b_1 \cdot b_2 \in \B$ and $v^{b_1} \in \B$.

\begin{example}

During analysis of classical integer programs, one is especially interested in
runtime complexity and cost bounds. A runtime bound is a bound on the 

\end{example}

% visits to a transition in the program over all admissible runs, whereas a size
% bound describes the highest value of a program variable observed at a
% transition over all admissible runs. Because the values observed in a run are
% highly dependent on the decisions made by the scheduler $\scheduler$, the bounds 
% we take the supremum over all $\scheduler$. One can also picture the scheduler 
% as an adversary that always takes the worst decision possible for runtime and
% size-bounds.

\begin{definition}[Total worst-case runtime complexity \label{def:wc_rt_complexity}]
    For a \gls{pip} $\Prog$, the overall worst-case runtime complexity $\Rt_\Prog :
    \runs \rightarrow \overline{\N}$ is defined as the \textit{random variable}

\begin{definition}[Runtime complexity bounds]
    For $s_0\in\Sigma$ and a \gls{pip} $\Prog$, $\RB^1 \in \B$ is a runtime
    bound for $s_0$, if
    \begin{equation*}
        \RB^1 \geq \sup \Rt(\Prog) = \sup \ESs(\Rt(\Prog)).
    \end{equation*}
    Analogously, $\RB \in \B$ is a cost bound for $s_0$ if 

        \Rt_\Prog(\vartheta)= \sum_{g\in\GT}\Rt(g)(\vartheta)

        \RB \geq \sup \Cost(\Prog) = \sup \ESs(\Rt(\Prog))

The following holds for any $\vartheta = (\_,t_0,\_)(\_,t_1,\_)\dots \in \runs$:
\begin{align}
    \Rt_P(\vartheta) &= \sum_{g\in\GT}\Rt(g)(\vartheta) & \text{by Definition
    \ref{def:wc_rt_complexity}} \\
    &= \sum_{g\in\GT} |\set{i}{t_i \in g}| & \text{by Definition \ref{def:past}}
    \\
    &= | \set{i}{t_i \in g, g\in\GT} & \text{for all } g \neq g', g\intersect{}g' = \emptyset 
\end{align}

\subsection{Non-probabilistic integer programs}
A non-probabilistic program is a probabilistic program where every general
transition contains only a single transition with probability $p = 1$. In that
case for a scheduler $\scheduler$ and a starting state $s_0$ there is only a
single run $c_0c_1\dots$ with probability $\PrSs(c_0c_1\dots) = 1$ and the
expected runtime defines the runtime of the program.
\begin{equation*}
    \ESs(\Rt) = \Rt(c_0c_1\dots)
\end{equation*}
% In probabilistic programs not only the worst case is of interest, but also the
% probable case. For example a program might run indefinitely in the worst case
% but the worst-case has a probability approaching zero. The expected bounds are
% defined using the expected value of random variables in the probability space
% $(\runs, \F, \PrSs)$ defined in \Sref{ssec:probabilityspace}. Moreover, recall
% definition \ref{def:expected_value}.
% \begin{definition}[Expected Runtime Complexity, \acrshort{past}
%     \cite{meyer2021tacas}\label{def:past}]
%     For $g \in \GT$ its runtime is the random variable $\Rt(g)$ where $R: \GT
%     \rightarrow \runs \rightarrow \overline{\N}$ with 
%     \begin{equation}
%         \Rt(g)((\_,t_0,\_)(\_,t_i,\_)\dots) = |\set{i}{t_i \in g}|. 
%     \end{equation}
%     For a scheduler $\scheduler$ and starting state $s_0\in\Sigma$, the expected
%     runtime complexity of $g\in\GT$ is $\E_{\scheduler,s_0}(\Rt(g))$ and the
%     expected runtime complexity of $\Prog$ is $\sum_{g\in\GT}\E_{\scheduler,
%     s_0}(\Rt(g)))$.
%     If $\Prog$'s expected runtime complexity is finite for every scheduler
%     $\scheduler$ and every initial state $s_0$, then $\Prog$ is called
%     \acrfull{past}
% \end{definition}
% The expected size bound is defined similarly 
% \begin{definition}[Expected Size
%     Complexity\cite{meyer2021tacas}\label{def:expectedcomplexity}]
%     The set of general result variables is $\GRV = \set{(g,l,x)}{g\in\GT,
%     x\in\PV, (\_,\_,\_,\_,l) \in g}$. The size of $\alpha = (g,l,x) \in \GRV$ is
%     the random variable $\S(\alpha)$ where $\S : \GRV \rightarrow (\runs
%     \rightarrow \overline{N})$ with
%     \begin{equation}
%         \S(g,l,x)((l_0,t_0,s_0)(l_1,t_1,s_1)\dots) = \sup \set{|s_i(x)|}{l_i =
%         l, t_i \in g}.
%     \end{equation}
%     For a scheduler $\scheduler$ and starting state $s_0$, the expected size
%     complexity of $\alpha \in \GRV$ is $\E_{\scheduler,s_0}(\S(\alpha))$.
% \end{definition}
% \begin{definition}[Expected Runtime and Size
%     Bounds\cite{meyer2021tacas}\label{def:expectedbounds}]\phantom{ }
%     \begin{itemize}
%         \item $\RBe : \GT \rightarrow \B$ is an expected runtime bound if for
%             all $g\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
%             have $|s_0|(\RBe(g)) \geq \ESs(\Rt(g))$.
%         \item $\SBe : \GRV \rightarrow \B$ is an expected size bound if for
%             all $\alpha\in\GT$, all schedulers $\scheduler$, and all $s_0 \Sigma$, we
%             have $|s_0|(\SBe(g)) \geq \ESs(\S(g))$.
%     \end{itemize}
% \end{definition}

\begin{rem}
    $t_\bot \in g_\bot \not\in \GT$, hence terminating runs have a finite
    overall runtime complexity.
\end{rem}

% \begin{example}

The worst-case total runtime complexity, for an initial state $s_0\in\Sigma$ and
all scheduler $\scheduler$, is the supremum over all admissible runs:
\begin{align}
    \sup \set{\Rt_\Prog (\vartheta)}{\vartheta \in \runs, \PrSs(\vartheta) > 0}
\end{align}

% \end{example}

The expected total runtime complexity is the expected value of the random
variable $\ESs(\Rt_\Prog)$

% \begin{definition}[Total worst-case runtime complexity \label{def:wc_rt_complexity}]
%     For a \gls{pip} $\Prog$, the overall worst-case runtime complexity $\Rt_\Prog :
%     \runs \rightarrow \overline{\N}$ is defined as the \textit{random variable}
%     \begin{equation}
%         \Rt_\Prog(\vartheta)= \sum_{g\in\GT}\Rt(g)(\vartheta)
%     \end{equation}
% \end{definition}

\subsection{Costs}
It is useful to add the notion of costs to a transition to reflect variable
complexity of transitions. The accumulative costs of a run are the sum of costs
for each transition taken. Accumulative costs can simulated by an additional
program variable $\mathbf{c} \in \PV$ that is updated only by polynomials of the
form $\eta(\mathbf{c}) = \mathbf{c} + c_t$, where $c_t \in
\Z$ is the cost associated with the transition $t\in\T$.

% The following holds for any $\vartheta = (\_,t_0,\_)(\_,t_1,\_)\dots \in \runs$:
% \begin{align}
%     \Rt_P(\vartheta) &= \sum_{g\in\GT}\Rt(g)(\vartheta) & \text{by Definition
%     \ref{def:wc_rt_complexity}} \\
%     &= \sum_{g\in\GT} |\set{i}{t_i \in g}| & \text{by Definition \ref{def:past}}
%     \\
%     &= | \set{i}{t_i \in g, g\in\GT} & \text{for all } g \neq g', g\intersect{}g' = \emptyset 
% \end{align}

For a given size bound $\SB$ for the \gls{pip} $\Prog$ and a starting assignment
$s_0$, the cost bound is defined as $|s_0|(\SB(t_\bot,\mathbf{c}))$, and given
an expected size bound $\SBe$, the expected cost bound is defined as
$|s_0|\SBe(t_\bot, mathbf{c})$.

% \begin{rem}
%     $t_\bot \in g_\bot \not\in \GT$, hence terminating runs have a finite
%     overall runtime complexity.
% \end{rem}
% The worst-case total runtime complexity, for an initial state $s_0\in\Sigma$ and
% all scheduler $\scheduler$, is the supremum over all admissible runs:
% \begin{align}
%     \sup \set{\Rt_\Prog (\vartheta)}{\vartheta \in \runs, \PrSs(\vartheta) > 0}
% \end{align}
% The expected total runtime complexity is the expected value of the random
% variable $\ESs(\Rt_\Prog)$

% \subsection{Costs}
% It is useful to add the notion of costs to a transition to reflect variable
% complexity of transitions. The accumulative costs of a run are the sum of costs
% for each transition taken. Accumulative costs can simulated by an additional
% program variable $\mathbf{c} \in \PV$ that is updated only by polynomials of the
% form $\eta(\mathbf{c}) = \mathbf{c} + c_t$, where $c_t \in
% \Z$ is the cost associated with the transition $t\in\T$.
% For a given size bound $\SB$ for the \gls{pip} $\Prog$ and a starting assignment
% $s_0$, the cost bound is defined as $|s_0|(\SB(t_\bot,\mathbf{c}))$, and given
% an expected size bound $\SBe$, the expected cost bound is defined as
% $|s_0|\SBe(t_\bot, mathbf{c})$.

the plus operator $+: \G, \T \rightarrow \G$ 

the plus operator $+: \G \times \T \rightarrow \G$ 

\section{Linear Ranking Funktions}

% \section{Linear Ranking Funktions}