\setmathfont(Digits,Latin)[
UprightFont={*},
BoldFont={* Semibold},
ItalicFont={* Italic},
BoldItalicFont={* Semibold Italic} 
]{Source Serif Pro}

  AutoFakeSlant=0.15

  % AutoFakeSlant=0.15

  doi       = {10.1007/978-3-319-08587-6\_13},

  doi       = {10.1007/978-3-319-08587-6_13},

  url       = {https://doi.org/10.1007/978-3-319-08587-6\_13},

  url       = {https://doi.org/10.1007/978-3-319-08587-6_13},

  address   = {New York [u.a},

  address   = {New York},

  doi       = {10.1007/978-3-031-08166-8\_10},

  doi       = {10.1007/978-3-031-08166-8_10},

  url       = {https://doi.org/10.1007/978-3-031-08166-8\_10},

  url       = {https://doi.org/10.1007/978-3-031-08166-8_10},

  note   = {Available at \url{https://termination-portal.org/wiki/TPDB}; Version 11.0 (2019)},

  doi       = {10.1007/978-3-540-78800-3\_24},

  doi       = {10.1007/978-3-540-78800-3_24},

  url       = {https://doi.org/10.1007/978-3-540-78800-3\_24},

  url       = {https://doi.org/10.1007/978-3-540-78800-3_24},

  doi       = {10.1007/978-3-642-02658-4\_52},

  doi       = {10.1007/978-3-642-02658-4_52},

  url       = {https://doi.org/10.1007/978-3-642-02658-4\_52},

  url       = {https://doi.org/10.1007/978-3-642-02658-4_52},

  doi       = {10.1007/978-3-642-15769-1\_18},

  doi       = {10.1007/978-3-642-15769-1_18},

  url       = {https://doi.org/10.1007/978-3-642-15769-1\_18},

  url       = {https://doi.org/10.1007/978-3-642-15769-1_18},

  doi       = {10.1007/978-3-319-45641-6\_21},

  doi       = {10.1007/978-3-319-45641-6_21},

  url       = {https://doi.org/10.1007/978-3-319-45641-6\_21},

  url       = {https://doi.org/10.1007/978-3-319-45641-6_21},

variables. During a run of the program, those costs are added up. The runtime
runtime complexity of a program is a special case of cost-analysis where every
transition has costs equal to 1. Because the costs would be equally copied from
one transition to the unfolded transition, we conjecture that the
partial evaluation preserves worst-case expected costs similarly to the
worst-case expected runtime complexity. However, answering this question needs
additional research.

variables. During a run of the program, those costs are added up for every
transition in the run. The runtime runtime complexity of a program is a special
case of cost-analysis where every transition has costs equal to 1. Because the
costs would be equally copied from one transition to the unfolded transition, we
conjecture that the partial evaluation preserves worst-case expected costs
similarly to the worst-case expected runtime complexity. However, answering this
question needs additional research.

components during analysis of a program on which the control-flow-refinement via

components during analysis of a program on which the control-flow refinement via

transitions $T$ used for control-flow-refinement is generated by selecting the

transitions $T$ used for control-flow refinement is generated by selecting the

    % $\GTPn \leftarrow$ \set{\{\}}{\;

    $\GTPn \leftarrow \set{g \in \GTPn}{\text{no } t\in T \text{ s. th. } t \in g
    \text{ exits}}\lift$\;

$\ell_g$, then the version $\langle \ell_g, \texttt{true}$ and all transitions
in $g$ are unfolded by the first evaluation step for this entry transition
making $g$ whole again in the partial evaluation graph. If the $\langle \ell_g,
\texttt{true}$ is reachable trough the partial evaluation the version is
evaluated then at its corresponding step. If it is not reachable the invalid
general transition is removed at the end as part of the clean-up.

$\ell_g$, then the version $\langle \ell_g, \texttt{true}\rangle$ and all
transitions in $g$ are unfolded by the first evaluation step for this entry
transition making $g$ whole again in the partial evaluation graph. If the
$\langle \ell_g, \texttt{true}\rangle$ is reachable trough the partial
evaluation the version is evaluated then at its corresponding step. If it is not
reachable the invalid general transition is removed at the end as part of the
clean-up.

Both the Algorithm \ref{alg:pe} which applies control-flow-refinement via
partial evaluation on an entire \gls{pip} and the Algorithm \ref{alg:cfr_subscc}
which evaluates a set component of a program, where implemented. 

The Algorithm \ref{alg:pe} which applies control-flow refinement via partial
evaluation on a subset of transitions was implemented. A variant of the
implementation which refines an entire program is provided as well. 

The evaluation of a whole program is not used in \gls{koat}s analysis per-se due
to performance reasons, but made available through a new sub command. It might
be used by other tools in the future, that want to profit from partial
evaluation on probabilistic programs. 

The evaluation of a whole program is not used in \gls{koat}s analysis due to
performance reasons, but made available through a new sub command. It might be
used by other tools in the future, that want to profit from partial evaluation
on probabilistic programs. 

        functions. \cite{giesl2022lncs} No control-flow-refinement is used.

        functions. \cite{giesl2022lncs} No control-flow refinement is used.

        control-flow-refinement is used.

        control-flow refinement is used.

        that uses sub-\gls{scc} control-flow-refinement refinement but limits

        that uses sub-\gls{scc} control-flow refinement refinement but limits

        The control-flow-refinement is done by calling iRankFinder as a

        The control-flow refinement is done by calling iRankFinder as a

        activates sub-\gls{scc} control-flow-refinement with iRankFinder

        activates sub-\gls{scc} control-flow refinement with iRankFinder

        control-flow-refinement described in Algorithm \ref{alg:pe} with

        control-flow refinement described in Algorithm \ref{alg:pe} with

        control-flow-refinement described in Algorithm \ref{alg:pe} with

        control-flow refinement described in Algorithm \ref{alg:pe} with

The implementation for probabilistic programs was done on a 

    We define the lift $G\lift\in \PEG$ of a graph $G \in \G$ denoted as

    We define the lift $G\lift\in \PEG_\Prog$ of a graph $G \in \G$ denoted as

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

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

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

        Let $\varphi\in2^{\C_\PV}$, $s, s' \in \Sigma$, $s \models \varphi$ and $s'

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

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

    \begin{equation*}\begin{gathered} \unfold(\langle \ell,\varphi\rangle, t) =

    \begin{equation*}\begin{gathered} 
        \unfold(\langle \ell,\varphi\rangle, t) =

\begin{definition}[Unfolding a general transition]\label{def:unfold_g}
    \begin{equation*}
        \unfold(\langle \ell,\varphi\rangle, g) = \{ 
            \unfold(\langle\ell,\varphi\rangle, t) \mid t \in g
        \}
    \end{equation*}
\end{definition}
For an unfolded general transition $g' = \unfold(\langle\ell_g, \varphi\rangle,
g)$ for some general transition $g \in \GTP$ and a set of constraints $\varphi
\in 2^{\C_\Prog}$, all the probabilities add up to one, because they were copied
by the unfolding from the original transitions in $g$. Besides, we obtain a
location $\ell_{g'} = \langle \ell_g, \varphi\rangle$, and $\tau_{g'} = \tau_g
\land \varphi$ by construction.

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

    \evaluate_\Prog(G) = G + \Union_{
        \substack{
            g \in \GTPout(\ell)\\
            \langle \ell, \varphi\rangle \in V(G)
        }} \unfold(\langle \ell, \varphi \rangle,
    g)

\in \N$. Moreover, let $G^* = \evaluate_\Prog^*$ be the limit the evaluation
approaches with an increasing number of repetitions. 

\in \N$. Moreover, let $G^* = \evaluate_\Prog^*$ be the graph that is obtained
by an infinite number of repetitions of the evaluation.

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

    G_\Prog^* = \evaluate_\Prog^*(G_0) = \Union_{n=1}^\infty \evaluate_\Prog^n(G_0)

    $\ell_0$ is defined as the graph $G^*$.

    $\ell_0$ is defined as the graph $G_\Prog^*$.

    \textit{true}\rangle$ is evaluated over the transition $t_1$, resulting in a
    single new version $\langle \ell_1, \textit{true}\rangle$. The second
    evaluation step unfolds $\langle \ell_1, \textit{true}\rangle$ over $t_3$

    \texttt{true}\rangle$ is evaluated over the transition $t_1$, resulting in a
    single new version $\langle \ell_1, \texttt{true}\rangle$. The second
    evaluation step unfolds $\langle \ell_1, \texttt{true}\rangle$ over $t_3$

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

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

    Let $\Psi = \{\psi_1, \dots,\psi_n\}\subset \C$ be a finite set of

    Let $\Psi = \{\psi_1, \dots,\psi_n\}\subset \C$ be a finite non-empty set of

    also finite. The abstraction function
    $\alpha_\Psi : 2^{\C_\PV} \rightarrow \A_\Psi$ is defined as

    also finite. The abstraction function $\alpha_\Psi : 2^{\C_\PV} \rightarrow
    \A_\Psi$ is defined as

\begin{equation*}
    \unfold_\alpha(\langle \ell,\varphi\rangle, g) = \{ 
        \unfold_\alpha(\langle\ell,\varphi\rangle, t) \mid t \in g
    \}
\end{equation*}

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

    \evaluate_{\Prog,\alpha}(G) = G + \Union_{
        \substack{
            g \in \GTPout(\ell)\\
            \langle \ell, \varphi\rangle \in V(G)
        }} \unfold_\alpha(\langle \ell, \varphi \rangle, g)

    G_\alpha^* = \evaluate_{\Prog,\alpha}^*(G_0) =
    \lim_{n\rightarrow\infty}\evaluate_{\Prog,\alpha}^n(G_0)

    G_{\Prog,\alpha}^* = \evaluate_{\Prog,\alpha}^*(G_0) =
    \Union_{n=1}^\infty \evaluate_{\Prog,\alpha}^n(G_0)

        \unfold_{S}(\langle l,\varphi\rangle, t) = (\langle \ell,

        \unfold_{S}(\langle \ell,\varphi\rangle, t) = (\langle \ell,

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

    \unfold_S(\langle \ell,\varphi\rangle, g) = \{ 
        \unfold_S(\langle\ell,\varphi\rangle, t) \mid t \in g
    \}
\end{equation*}
\begin{equation*}
    \evaluate_{\Prog,S}(G) = G + \Union_{
        \substack{
            g \in \GTPout(\ell)\\
            \langle \ell, \varphi\rangle \in V(G)
        }} \unfold_S(\langle \ell, \varphi \rangle, g)

    G_{S}^* = \evaluate_{\Prog,S}^*(G_0) =
    \lim_{n\rightarrow\infty}\evaluate_{\Prog,S}^n(G_0)

    G_{\Prog,S}^* = \evaluate_{\Prog,S}^*(G_0) =
    \Union_{n=1}^\infty \evaluate_{\Prog,S}^n(G_0)

    Let $\Psi_{\ell_0},\dots,\Psi_{ell_n} \in (2^\C \union \{\bot\})$ be

    Let $\Psi_{\ell_0},\dots,\Psi_{\ell_n} \in (2^\C \union \{\bot\})$ be

    \begin{figure}[ht]
        \centering
        \input{figures/ch3_p3_full_pe_localized}
        \caption{Partial evaluation of $\Prog_3$ with a localised property based
        abstraction $S_{\bot,\Psi_{\ell_1},\bot}$.\label{fig:ex_localized_pba}}
    \end{figure}

    \begin{figure}[ht]
        \centering
        \input{figures/ch3_p3_full_pe_localized}
        \caption{Partial evaluation of $\Prog_3$ with a localised property based
        abstraction $S_{\bot,\Psi_{\ell_1},\bot}$.\label{fig:ex_localized_pba}}
    \end{figure}

    \rightarrow \C$ an evaluation step $\evaluate_{\Prog,S,T} : \G_\Prog
    \rightarrow \G_\Prog$ is defined as 
    \begin{align*}
        \evaluate_{\Prog,S}(G) = G 
        &+ \set{ \unfold_{S}(\langle \ell, \varphi \rangle, t)}{ \langle \ell,
        \varphi\rangle \in E(G) \text{, and } t \in \TPout(\ell) \cap T}\\
        &+ \set{
            (\langle\ell,\varphi\rangle,p,\tau,\eta,\langle\ell',\texttt{true}\rangle)}{
            \langle \ell, \varphi\rangle \in E(G) \text{, and } t \in
            \TPout(\ell) \backslash T}
    \end{align*}

    \rightarrow \C$ new unfolding functions $\unfold_{S,T} : \vers_\Prog \times
    \TP \rightarrow \VTP$, and $\unfold: \vers_\Prog \times \GTP \rightarrow 2^\VTP$
    are defined where
    \begin{equation*}
        \begin{gathered}
            \unfold_{S,T}(\langle \ell,\varphi\rangle, t) = \begin{cases}
                    (\langle\ell, \varphi\rangle, p, \tau\Land\varphi,
                    \eta,S(\langle \ell',\varphi'\rangle)) & \text{if } t \in T \\
                    (\langle\ell, \varphi\rangle, p, \tau\Land\varphi,
                    \eta,\langle\ell',\texttt{true}\rangle) & \text{if } t \not\in T
            \end{cases}
                \\ \text{for } t = (\ell, p, \tau, \eta,
            \ell') \in \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau,
            \eta), \\
        \end{gathered}
    \end{equation*}
    \begin{equation*}
        \unfold_{S,T}(\langle \ell,\varphi\rangle, g) = \{ 
            \unfold_{S,T}(\langle\ell,\varphi\rangle, t) \mid t \in g
        \},
    \end{equation*}
    \begin{equation*}
        \evaluate_{\Prog,S,T}(G) = G + \Union_{
            \substack{
                g \in \GTPout(\ell)\\
                \langle \ell, \varphi\rangle \in V(G)
            }} \unfold_{S,T}(\langle \ell, \varphi \rangle, g)
    \end{equation*}

    G_{S,T}^* = \evaluate_{\Prog,S}^*(G_0) =
    \lim_{n\rightarrow\infty}\evaluate_{\Prog,S}^n(G_0)

    G_{\Prog,S,T}^* = \evaluate_{\Prog,S,T}^*(G_0) =\Union_{n=1}^\infty 
    \evaluate_{\Prog,S,T}^n(G_0)

    \not\in\T$. 

    \not\in T$. 

    step. We obtain $G_3 = G_2 = G^*_{\Prog_3,S_{\bot,\Psi_{\ell_1},\bot}}$.

    step. We obtain $G_3 = G_2 = G^*_{\Prog_3,S_{\bot,\Psi_{\ell_1},\bot},T}$.

    Let $S$ be a localised abstraction function. The partial evaluation graph
    $G_{\Prog,S}^*$ is finite if every loop $L$ in $\Prog$ contains a location
    $\ell \in L$ such that $\set{S(\langle\ell,\varphi\rangle)}{\varphi \in
    2^{\C_\PV}}$ is finite.

    Let $S$ be a localised abstraction function and $T \subseteq \T_Prog$ The
    partial evaluation graph $G_{\Prog,S,T}^*$ is finite if every loop $L$ in
    $\Prog$ contains a location $\ell \in L$ such that
    $\set{S(\langle\ell,\varphi\rangle)}{\varphi \in 2^{\C_\PV}}$ is finite.

        Let $G_{\Prog,S}^*$ be the partial evaluation graph of a \gls{pip}

        Let $G_{\Prog,S,T}^*$ be the partial evaluation graph of a \gls{pip}

        $\evaluate_\Prog^*$ does not converge, there must exist a fresh version

        $\evaluate_\Prog^*$ is infinite, there must exist a fresh version

        $G_{\Prog,S}^*$ cannot be infinite.

        $G_{\Prog,S,T}^*$ cannot be infinite.

We will proceed with proving that the partial evaluation graph restricted to a
subset of transitions can be used for constructing an new program $\Prog'$ with
equal expected runtime complexity. All the results hold equally for partial
evaluation of the entire program and independently of the choice of the (global
or localised) abstraction function, as long as the localised evaluation function
asserts a finite partial evaluation graph by Lemma
\ref{lem:localized_pba_finite}.
\begin{lemma}[Soundness\label{lem:unfold_g_sound}]
    Let $G^*_{\Prog,S,T}$ be the evaluation graph of a \gls{pip} $\Prog$ with a
    localised abstraction function $S$ on a component $T \subseteq \TP$. The
    transitions of $E(G^*_{\Prog,S,T})$ can be split into finite pairwise
    disjunct subsets $g_0,\dots,g_n \subset E(G^*_{\Prog,\alpha}) \subset \VT$.
    For all $0 \leq i \leq n$ 
    \begin{enumerate}
        \item there exists a unique general transition $\bar{g}_i \in \GTP$ and
            some $\varphi \in 2^{\C_\PV}$ for which the following property holds:
            \begin{align*}
                g_i &= \set{t}{\bar{t} \in \bar{g}_i, t \in E(G^*_{\Prog,S,T})} \\
                    &= \set{(\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi
                    \land \tau_{g_i}, \eta, \langle\ell',\varphi'\rangle}{
                        (\ell_g, p, \tau_g, \eta, \ell') \in g'_i, \varphi' \in
                        2^{\C_\PV}}
            \end{align*}
        \item all transitions in $g_i$ have a common guard $\tau_{g_i}$ and
            source location $\ell_{g_i}$;
        \item the probabilities in $g_i$ add up to 1.
    \end{enumerate}
    \begin{proof}
        Let $t =(\langle \ell, \varphi\rangle, p, \tau, \eta, \_) \in
        E(G^*_{\Prog,S,T})$ be a transition in the partial evaluation graph
        $G^*_{\Prog,S,T}$ of a \gls{pip} $\Prog$ with a component $T \subset
        \TP$. There exists a unique general
        transition $g \in \GTP$ with $\bar{t} \in g$. Let $ g = \{ t'_1, \dots,
        t'_n \}$. We set $\bar{g} = g$. All $t'_i$ share a common guard $\tau_g$
        and source location $\ell_g = \ell$. 
        Let $1 \leq i \leq n$ an $t'_i = (\ell, p, \tau_g, \_, \_)$. By
        construction of $\evaluate_\Prog,S,T$ there was added either a
        transition $t_i = \unfold(\langle\ell,\varphi\rangle, t_i) =
        (\langle\ell,\varphi\rangle, p, \varphi \land \tau_g, \_, \_)$ if $t'_i
        \in T$ or $t_i = (\langle\ell,\varphi\rangle, p, \varphi \land \tau_g,
        \_, \_)$ if $t'_i \not\in T$. In any case, all $t'_i$ share a common
        guard $\tau_g' = \varphi \land \tau_g$ and the probabilities add up to
        1. 
    \end{proof}
\end{lemma}

evaluation graph $G^*_{\Prog,\alpha}$ by Lemma \ref{lem:unfold_g_sound}. 

evaluation graph $G^*_{\Prog,\alpha}$ where every general transition $g \in
\GT_{G^*_{\Prog,\alpha}}$ was added by the unfolding of a unique general
transition $g' \in \GT_Prog$. We call $\bar{g} = g'$, similar to Lemma
\ref{lem:original_transition}, the original transition of $g$.

    as $\Prog' = (\PV, \Loc_{\Prog'}, \GTPn, \langle l_0, \textit{true}\rangle)$

    as $\Prog' = (\PV, \Loc_{\Prog'}, \GTPn, \langle \ell_0, \texttt{true}\rangle)$

    \set{\unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t) }{ t \in g \text{
        and } t \in T} \union
    \set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land \tau_{g_i},
    \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g, \eta, \ell')
    \in g, \varphi' \in 2^{\C_\PV} \text{ and } t \not\in T}$. $g'$ is the
    general transition that contains all the unfolded and copied transitions for
    $t \in g$. For better readability we define a function
    $\texttt{eval}_{\Prog,S,T} : \GTP \rightarrow \GTPn$ where 
    \begin{align*}
        \texttt{eval}_{\Prog,S,T} (g) = &\set{\unfold_{\Prog,S}(\langle \ell,
        \varphi\rangle, t) }{ t \in g \cap t \in T} \union \\ 
        &\set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land
        \tau_{g_i}, \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g,
        \eta, \ell') \in g \backslash T, \varphi' \in 2^{\C_\PV}}.
    \end{align*}

    \unfold_{\Prog,S,T}(\langle\ell,\varphi\rangle,g)$
    % $
    % \set{\unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t) }{ t \in g \text{
    %     and } t \in T} \union
    % \set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land \tau_{g_i},
    % \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g, \eta, \ell')
    % \in g, \varphi' \in 2^{\C_\PV} \text{ and } t \not\in T}$. $g'$ is the
    % general transition that contains all the unfolded and copied transitions for
    % $t \in g$. For better readability we define a function
    % $\texttt{eval}_{\Prog,S,T} : \GTP \rightarrow \GTPn$ where 
    % \begin{align*}
    %     \texttt{eval}_{\Prog,S,T} (g) = &\set{\unfold_{\Prog,S}(\langle \ell,
    %     \varphi\rangle, t) }{ t \in g \cap t \in T} \union \\ 
    %     &\set{\langle\ell_{\bar{g}_i},\varphi\rangle,p,\varphi \land
    %     \tau_{g_i}, \eta, \langle\ell',\varphi'\rangle}{ t = (\ell_g, p, \tau_g,
    %     \eta, \ell') \in g \backslash T, \varphi' \in 2^{\C_\PV}}.
    % \end{align*}

            \texttt{eval}_{\Prog,S,T}(g)

            \texttt{unfold}_{S,T}(\langle\ell, \varphi\rangle, g)

        \texttt{eval}_{\Prog,S,T}(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in
        \T_\Prog',\\

        \texttt{unfold}_{S,T}(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in
        \TPn,\\

encountered symbols and their usage. \todo{update table}

encountered symbols and their usage.

        $s$ & assignments \\

        $s, \beta, \sigma$ & assignments \\

        $\psi, $ & constraints \\
        $\varphi, $ & formulas\\

        $\psi $ & constraints \\
        $\varphi $ & sets or conjunctions of constraints\\

        $f$ & finite prefixes \\

        $\varf$ & finite prefixes \\

        $G$ & graphs \\
        $L$ & sets of locations that form a loop \\
        $T$ & sets of transitions \\

    Let $\varphi_1, \varphi_2 \in \Phi$. If $\llbracket \varphi_1 \rrbracket

    Let $\varphi_1, \varphi_2 \in 2^\PC$. If $\llbracket \varphi_1 \rrbracket

undecidable\cite{kremer2016lncs}.

undecidable \cite{kremer2016lncs}.

We define a function $\texttt{lin} 2^\PC \rightarrow 2^\C$ that linearly
over-approximates polynomial constraints, that is $\llbracket \varphi\rrbracket
\subseteq \llbracket\texttt{lin}(\varphi) \rrbracket$. It is not important, how
the over-approximation works in details. An easy way of over-approximating
polynomial sets of constraints is to just drop all non-linear constraints.
However, one might take minima and maxima of the polynomials into account and
get arbitrarily precise. 

Octagons \cite{mine2001wcre, mine2007arxiv, mine2006hosc,truchet2010synacs} and

Octagons \cite{mine2001wcre, mine2006hosc,truchet2010synacs} and

            \caption{Formula $\varphi_1$}

            \caption{$\varphi_1$}

            \caption{Formula $\varphi_2$}

            \caption{$\varphi_2$}

            \caption{Formula $\varphi_3 = \varphi_1 \land \varphi_2$}

            \caption{$\varphi_3 = \varphi_1 \land \varphi_2$}

    \begin{align}

    \begin{align*}

    \end{align}

    \end{align*}

\subsection{Convex polyhedra}\label{ssec:polyhedra}

\subsection{Convex Polyhedra}\label{ssec:polyhedra}

\begin{definition}[Probability Measure\cite{billingsley2011}]\label{def:measure}

\begin{definition}[Probability Measure \cite{billingsley2011}]\label{def:measure}

\begin{definition}[Probability space\cite{billingsley2011}]\label{def:probability_space}

\begin{definition}[Probability space \cite{billingsley2011}]\label{def:probability_space}

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

\begin{definition}[Expected value \cite{billingsley2011,

\cite{kraaikamp2005modern}. Examples of the various probability distributions
are displayed in \fref{fig:distributions}.

\citetitle{kraaikamp2005modern} \cite{kraaikamp2005modern}. Examples of the
various probability distributions are displayed in \fref{fig:distributions}.

\subsection{Bernoulli Distribution}\label{ssec:bernoulli}

\subsection{Bernoulli Distribution \cite{kraaikamp2005modern}}\label{ssec:bernoulli}

    parameterized by $p \in [0,1]$ if its probability is given by $P(X=1) = p$
    and $P(X=0) = 1-p$.

    parameterized by $p \in [0,1]$ if its probability is given by $\mu(1) =
    P(X=1) = p$ and $\mu(0) = P(X=0) = 1-p$.

\subsection{Uniform Distribution}\label{ssec:uniform}

\subsection{Uniform Distribution \cite{kraaikamp2005modern}}\label{ssec:uniform}

\begin{definition}\label{def:uniform}

\begin{definition}[Uniform distribution]\label{def:uniform}

\subsection{Geometric Distribution}\label{ssec:geom}

\subsection{Geometric Distribution \cite{kraaikamp2005modern}}\label{ssec:geom}

\begin{definition}\label{def:geom}

\begin{definition}[Geometric distribution]\label{def:geom}

        P(X=k)&=(1-p)^{k-1}p & \text{for } k = 1, 2, \dots

        \mu(k) = P(X=k)&=(1-p)^{k-1}p & \text{for } k = 1, 2, \dots

\subsection{Hypergeometric Distribution}\label{def:hyper}

\subsection{Hypergeometric Distribution \cite{kraaikamp2005modern}}\label{def:hyper}

\begin{definition}[Hypergeometric Distribution]

\begin{definition}[Hypergeometric distribution]

        P(X=k) &= \frac{\binom{K}{k} \binom{N-K}{n-k}}{\binom{N}{n}} & \text{for

        \mu(k) = P(X=k) &= \frac{\binom{K}{k} \binom{N-K}{n-k}}{\binom{N}{n}} & \text{for

\begin{definition}[Binomial Distribution]\label{def:bino}

\begin{definition}[Binomial distribution \cite{kraaikamp2005modern}]\label{def:bino}

        P(X=k)&=\binom{n}{k} p^k (1-p)^{n-k} & \text{for } k = 0,\dots,n

        \mu(k) = P(X=k)&=\binom{n}{k} p^k (1-p)^{n-k} & \text{for } k = 0,\dots,n

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

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

\begin{definition}[Non-probabilistic over approximation of probabilistic

\begin{definition}[Non-probabilistic over-approximation of probabilistic

    $(\lfloor f\rceil,\tilde{\varf})$  with

    $(\lfloor f\rceil,\tilde{\varf}) \in \C \times \Z[A \uplus \{d_1,\dots,d_n\}]$  with

        \lfloor \varf \rceil = \LAnd_{i=1,\dots,m} \lfloor D_i \rceil_{d_i} \text{

        \lfloor \varf \rceil = \texttt{lin}(\LAnd_{i=1,\dots,m} \lfloor D_i
        \rceil_{d_i}) \text{

\begin{definition}[Markovian Scheduler\cite{meyer2021tacas}\label{def:mscheduler}]

\begin{definition}[Markovian scheduler\cite{meyer2021tacas}\label{def:mscheduler}]

    $\MDS_\Prog$, where \enquote{MD} stands for \enquote{Markovian
    deterministic}.

    $\MDS_\Prog$, where \enquote{MD} stands for \enquote{\underline{M}arkovian
    \underline{d}eterministic}.

    $\scheduler(fc) = (g, s')$ implies items \ref{itm:md1} to \ref{itm:md4} of

    $\scheduler(\varf\!c) = (g, s')$ implies items \ref{itm:md1} to \ref{itm:md4} of

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

    by $\HDS_\Prog$, where \enquote{HD} stands for \enquote{\underline{h}istory
    dependent \underline{d}eterministic}.

\begin{definition}[Admissible Run]\label{def:admissible}

\begin{definition}[Admissible run]\label{def:admissible}

    $\prSs(f) > 0$. A run $c_0c_1\dots \in \runs_\Prog$ is \textit{admissible}

    $\prSs(\varf{}) > 0$. A run $c_0c_1\dots \in \runs_\Prog$ is \textit{admissible}

runtime complexity and cost bounds.

runtime complexity bounds.

the minus operator $- : \G \times 2^\T \rightarrow \G$.

the minus operator $- : \G \times 2^\T \rightarrow \G$. Moreover, we write $G_1
\union G_2$ instead of $(V(G_1) \union V(G_2), E(G_1) \union E(G_2))$.

programs \cite{meyer2021tacas}. Unfortunately, by using iRankfinder
which is limited to non-probabilistic integer programs, the technique of
\gls{cfr} via partial evaluation remained out of reach for probabilistic
programs.

programs \cite{meyer2021tacas}. For probabilistic programs, \gls{koat} uses
probabilistic ranking functions, that work similarly to \gls{mprf}, but take
probability into accound. They fail for the same reasons as \gls{mprf} for
certain kinds of loops. Unfortunately, by using iRankFinder which is limited to
non-probabilistic integer programs, the technique of \gls{cfr} via partial
evaluation remained out of reach for probabilistic programs.

\gls{koat} with regard to non-probabilistic integer programs by reimplementing
the control flow refinement technique of iRankFinder \cite{irankfinder2018wst}

\gls{koat} with regard to non-prob\-a\-bilis\-tic integer programs by reimplementing
the control-flow refinement technique of iRankFinder \cite{irankfinder2018wst}

correctness, partial evaluation is made available for probabilistic programs for
the first time (to the best of our knowledge).

correctness, partial evaluation is made available for probabilistic programs.