The goal of \gls{koat}s analysis is to find tight upper bounds for \glspl{pip}.
The analysis techniques used, such as \acrfullpl{mprf} and \cite{lommen2022twn}, have
their limits and cannot always find tight bounds for every program. This
motivates control-flow refinement in order to find a program that is equivalent
to the original one, which opens the possibility for the analysis to find
tighter runtime complexity bounds.
Recall Definition \ref{def:runtime_complexity} -- the newly constructed refined
program shall have the same worst-case expected runtime complexity as the
original program. This implies that the runtime complexity bounds found for the
refined program are also runtime-complexity bounds for the original one.
Naturally, the control-flow refinement will add and replace transitions and
locations. We will show that each transition in the refined program is similar
to a transition in the original program and consequently every run in the new
program has a run of equal run~time complexity and probability in the original
program and vice-versa.
The control-flow refinement presented in this thesis adapts the partial
evaluation technique presented by \citeauthor{Domenech19} \cite{Domenech19} for
\glspl{pip}. The partial evaluation will be constructed in a similar way, but
explicitly taking probability and general transitions into account.
The construction is carried out in three steps. First, an unfolding operation is
presented. Second, an evaluation step is presented, which uses the unfolding.
Third, the evaluation step is repeated until a fix-point is found. The unfolding
and evaluation will be adapted multiple times in order to find finite partial
evaluation graphs, and to evaluate only the relevant parts of the program.
Afterwards, we will show that the partial evaluation is sound for \glspl{pip}
and prove that the expected runtime complexity is preserved and thus also the
worst-case runtime complexity of non-probabilistic programs.
\begin{example}
\begin{figure}
\centering
\input{figures/ch3_p3_program}
\caption{Representation of $\Prog_3$, a variation of $\Prog_2$ from
\fref{fig:prob_c}, as a transition graph, with non-deterministic
branching.\label{fig:ex_prob}}
\end{figure}
The examples in this chapter will follow through using a variation of the
probabilistic program $\Prog_2$ from the introduction (\fref{fig:prob_c} on
\pref{fig:prob_c}),
which we call $\Prog_3$. $\Prog_3$ is visually represented by a transition
graph in \fref{fig:ex_prob}. The program uses a set of variables $\V =
\{x,y,u,w\}$ and has the program variables $\PV_{\Prog_3} = \{x,y\}$. $u$,
and $w$ are temporary variables whose values are reassigned by the scheduler
on every transition and whose values do not propagate throughout the
program.
In transition $t_0$ the value of $x$ is set by non-deterministic sampling
via the temporary variable $u$. At location $\ell_1$ the scheduler decides
between one of the general transitions $g_1 = \{t_{1a}, t_{1b}\}$ or $g_2 =
\{t_2\}$, and assigns the value for $w$ accordingly. The program can
alternate between the loops non-deterministically after every iteration.
Since both loops are independent of one another, the non-determinism does
not change the expected runtime complexity of the program. On the general
transition $g_1 = \{t_{1a}, t_{1b}\}$ at location $\ell_1$ the program
branches probabilistically, with a probability of $p=0.5$. On the transition
$t_3$, the value with which $y$ is decremented is sampled probabilistically
from a Bernoulli distribution, where both possible outcomes have the same
probability $p=0.5$.
When entering any of the two loops at $t_{1a}$ or $t_{1b}$ the value of $x$
is unbounded due to the non-deterministic sampling of $x$ in $t_0$. Hence
\gls{koat} cannot find \gls{mprf} bounding the value of $x$ throughout the
execution and compute runtime bounds for those loops.
\end{example}
\section{Partial Evaluation of Probabilistic Programs}\label{sec:theory}\label{sec:partialevaluation}
During a normal execution, a program visits locations one after another and
changes its state with every transition. The configuration at a given point of
the execution can be described by tuples of locations and assignments.
Simulating every possible run of a program from every possible starting state is
impossible: first, the number of starting states is infinite, and second the
program is not guaranteed to terminate, hence the simulation of a specific run
might not terminate either.
For non-deterministic and probabilistic programs, the problem becomes even more
complex, since the transitions taken do not only depend on the current state but
also on the answer of the scheduler and some random event. Instead of simulating
every single possible run, it would be more efficient to treat \emph{similar}
states as one. Instead of simulating a single assignment, the set of all
possible assignments after a step is over-approximated by a set of constraints.
The resulting graph is called a \emph{partial evaluation graph}. It was
formalised for \glspl{chc} by \citeauthor{gallagher2019eptcs}
\cite{gallagher2019eptcs}. In this thesis, the definitions are adapted to better
fit the algorithm and the formalism of \Glspl{pip}.
\begin{definition}[Version]\label{def:version}
The set of \textit{versions} is the set of tuples over the
locations $\Loc_\Prog$ and constraints $\C$:
\begin{equation*}
\vers_\Prog = (\Loc_\Prog \times \C).
\end{equation*}
\end{definition}
The versions are the vertices/locations of the partial evaluation graph. The
edges of the partial evaluation graph are transitions $\VTP$ (\enquote{$\VT$}
stands for \enquote{version transitions}) analogously defined to Definition
\ref{def:pip}, except that they connect versions and not locations. The set of
all partial evaluation graphs for a program $\Prog$ is defined as $\PEG_\Prog =
2^{\vers_\Prog} \times 2^{\VTP}$.
A \Gls{pip} $\Prog$ can be lifted to a trivial partial evaluation graph by
replacing every location $\ell \in \Loc_\Prog$ by the trivial version $\langle
\ell, \texttt{true}\rangle \in \vers_\Prog$.
\begin{definition}
We define the lift $G\lift\in \PEG_\Prog$ of a graph $G \in \G$ denoted as
\begin{equation*}
G\lift = (\set{\langle\ell,\texttt{true}\rangle}{\ell \in V(G)},
\set{(\langle\ell,\texttt{true}\rangle,p,\tau,\eta,\langle\ell',
\texttt{true})}{t \in E(G)})
\end{equation*}
\end{definition}
\begin{example}\label{ex:lift}
The lift of the graph $G_{\Prog_3}$ of the program $\Prog_3$ is displayed in
\fref{fig:ex_lift}. It has the very same structure as the original program.
\begin{figure}[ht]
\centering
\input{figures/ch3_p3_lift}
\caption{Lift of the graph $G_{\Prog_3}$ of the program
$\Prog_3$.\label{fig:ex_lift}}
\end{figure}
\end{example}
Obviously, the lift of a program is not useful for the analysis, as it does not
capture any interesting properties of the program, besides what is already
known in the original program. In the following we will present a construction
for a partial evaluation graph using unfolding and abstraction.
The partial evaluation is done iteratively. On every step the next version $v' =
\langle l', \varphi'\rangle \in \vers_\Prog$ is computed by unfolding a
transition $t \in \T_\Prog$ from the original \gls{pip} that starts in the same
location $\ell \in \Loc$ as the source version $v = \langle \ell, \varphi\rangle
\in \vers_\Prog$. The resulting constraint $\varphi'$ contains all states $s'
\in \Sigma$ with $s' \models \varphi'$ which are reachable via the transition
$t$ from a state $s \models \varphi$ in the source version, i.e., $\prSs((\ell,
s, \_) \rightarrow (\ell',s',t)) > 0$.
The non-determinism is taken into account by the implicit existential
quantification of temporary variables in constraints. In contrast, the
probabilistic sampling is over-approximated with a non-probabilistic update
$\tilde{\eta}: \PV \rightarrow \Z[\V]$ and a constraint denoted as
$\lfloor\eta\rceil$. The probabilistic distributions in the probabilistic update
$\eta$ are replaced by fresh temporary variables that are then constrained by
$\lfloor\eta\rceil$.
\begin{definition}[Unfolding]\label{def:unfold}
An unfolding operation $\unfold : 2^{\C_\PV} \times (\PV \rightarrow
\Z[\V\union\D)]) \rightarrow 2^{\C_\PV}$ of a set of constraints $\varphi
\in 2^{\C_\PV}$ with an update $\eta: \PV\rightarrow\Z[\V \union \D]$ is
defined as
\begin{align*}
\unfold(\varphi, \eta) = \tilde{\eta}(\varphi \Land \lfloor\eta\rceil)
\end{align*}
\end{definition}
\begin{lemma}\label{lem:unfold}
For any $\varphi\in 2^{\C_\PV}$ and probabilistic update $\eta : \PV
\rightarrow \Z[\V\union\D]$, if there exists an $s\in \Sigma$ with
$s\models\varphi$ then
\begin{enumerate}
\item \label{itm:unfold1} $\unfold(\varphi, \eta)$ is satisfiable.
\item \label{itm:unfold2} If $s' \in \support_s(\eta)$ for some $s' \in
\Sigma$, then $s' \models \unfold(\varphi, \eta)$.
\end{enumerate}
\begin{proof}
Let $\varphi\in2^{\C_\PV}$, $s, s' \in \Sigma$, $s \models \varphi$ and $s'
\in \support_s(\eta)$. $s' \models \unfold(\varphi, \eta)$ follows from
Lemma \ref{lem:prob_update}.
The satisfiability of $\unfold(\varphi, \eta)$ follows directly from the
existence of $s \models \varphi$ due to satisfiability and $s' \in
\support_s(\eta)$ since the support cannot be empty.
\end{proof}
\end{lemma}
\begin{example}
Consider transition $t_3$ of $\Prog_3$ from \fref{fig:ex_prob}. $t_3$
has a probabilistic update $\eta(y) = y - \textsc{Bern}(0.5)$ and
implicitly $\eta(x) = x$.
Imagine a constraint $y > 0$ that is unfolded with the probabilistic update
$\eta$. The update is approximated by $(\tilde{\eta},\lfloor\eta\rceil)$
with
\begin{align*}
\tilde{\eta}(x) &= x' \\
\tilde{\eta}(y) &= y' \\
\lfloor\eta\rceil &= (x' = x \Land y' = y - d \Land 0 \leq d \leq 1)
\end{align*}
The unfolding computes the following new constraint.
\begin{align*}
\tilde{\eta}(\varphi \Land \lfloor\eta\rceil) &= \tilde{\eta}(x > 0 \Land
x' = x \Land y' = y - d \Land 0 \leq d \leq 1) \\
&\begin{aligned}
\;=(&y > 0 \Land x' = x \Land y' = y - d \Land 0 \leq d \leq 1 \\&\Land x'' =
x' \Land y'' = y')|_{\PV''}[x''/x]_{x\in\PV}\end{aligned}\\
&= (y'' \geq 0)[x''/x]_{x\in\PV'}\\
&= (y \geq 0)
\end{align*}
Any satisfying assignment for $\varphi$ must assign $y$ a value larger than
zero and after the update, the value of the assignment must be larger or
equal to zero. Since $x$ is neither constrained before the update nor
updated in any way, it remains unconstrained after the unfolding.
\end{example}
\begin{definition}[Unfolding a transition]\label{def:unfold_t}
Using the unfolding operation from Definition \ref{def:unfold}, an unfolding
operation $\unfold: \vers_\Prog \times \T_\Prog \rightarrow \VTP$ is defined
that constructs a new transition connecting both versions. The update and
probability from the original transition are simply copied, while the guard
is extended with the constraint of the source version.
\begin{equation*}\begin{gathered}
\unfold(\langle \ell,\varphi\rangle, t) =
(\langle \ell, \varphi\rangle, p, \tau\Land\varphi, \eta,\langle \ell',
\varphi' \rangle) \\ \text{for } t = (\ell, p, \tau, \eta, \ell') \in
\T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau, \eta)
\end{gathered}\end{equation*}
\end{definition}
\begin{rem}
The unfolding is undefined for transitions that do not start in the same
location as the version.
\end{rem}
\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.
We define a function $\evaluate_\Prog : \G_\Prog \rightarrow \G_\Prog $ that
unfolds all versions $\langle \ell, \varphi \rangle \in V(G)$ in the graph $G
\in \G_\Prog$ with each outgoing transition $t \in \TPout(\ell)$.
\begin{align*}
\evaluate_\Prog(G) = G + \Union_{
\substack{
g \in \GTPout(\ell)\\
\langle \ell, \varphi\rangle \in V(G)
}} \unfold(\langle \ell, \varphi \rangle,
g)
\end{align*}
For a program $\Prog$ with an initial location $\ell_0$, the unfolding is
bootstrapped at the initial version $\langle \ell_0, \texttt{true}\rangle$ as
this version represents all valid starting configurations of the program. Let
$G_0 = (\{\langle \ell_0, \texttt{true}\rangle\}, \emptyset)$.
Let $\evaluate^n$ be the $n$ times concatenation of $\evaluate$ and $G_n$ be the
graph found by $n$ evaluation steps.
\begin{equation*}
G_n = \evaluate_\Prog^n(G_0) = \underbrace{\evaluate_\Prog \circ \cdots \circ
\evaluate_\Prog}_{n
\text{ times}}(G_0)
\end{equation*}
For any $V(G_n) \subseteq V(G_{n+1})$ and $E(G_n) \subseteq E(G_{n+1})$ where $n
\in \N$. Moreover, let $G^* = \evaluate_\Prog^*$ be the graph that is obtained
by an infinite number of repetitions of the evaluation.
\begin{equation*}
G_\Prog^* = \evaluate_\Prog^*(G_0) = \Union_{n=1}^\infty \evaluate_\Prog^n(G_0)
\end{equation*}
\begin{definition}[Evaluation Graph]
The \emph{evaluation graph} of a program $\Prog$ with a starting location
$\ell_0$ is defined as the graph $G_\Prog^*$.
\end{definition}
In practice one can ignore unsatisfiable versions, since they cannot be reached
by the incoming transitions.
\begin{example}\label{ex:infinite_evaluation}
\begin{figure}
\centering
\begin{subcaptionblock}[t]{0.4\textwidth}
\input{figures/ch3_p4_program.tex}
\caption{A Program $\Prog_4$\label{fig:ch3_inf_prog}}
\end{subcaptionblock}
\begin{subcaptionblock}[t]{0.5\textwidth}
\input{figures/ch3_p4_tree.tex}
\caption{Extract of the infinite evaluation \\graph of $\Prog_4$\label{fig:ch3_inf_tree}}
\end{subcaptionblock}
\caption{A simple program $\Prog_4$ with an infinite evaluation
graph.\label{fig:ch3_inf}}
\end{figure}
Consider the program $\Prog_4$ shown in \fref{fig:ch3_inf_prog}. On the
initial state $s_0 \in \Sigma$ with $s_0(x) = 0$, the run
$(\ell_0,t_\text{in},s_0)(\ell_1,t_1,s_0)(\ell_1,t_2,s_1)(\ell_1,t_2,s_2)\dots$
with $s_i(x) = i$ for $i \in \N$ is clearly admissible and the program is
stuck in this infinite loop on $\ell_1$. The evaluation captures this
behaviour, and creates the infinite evaluation graph displayed in
\fref{fig:ch3_inf_tree}. First the version $\langle \ell_0,
\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$
to $\langle \ell_2, x\leq0\rangle$ and over $t_2$ to $\langle \ell_1,
x>1\rangle$. $\ell_2$ has no outgoing transitions. Thus, no new transitions
are added. $\langle \ell_1, x>1\rangle$ is unfolded to $\langle \ell_1,
x>2\rangle$ over $t_2$ only since the guard of $t_3$ is not satisfiable from
within $x > 2$. The new version is unfolded over and over again, until the
end of time.
\end{example}
As one can see in Example \ref{ex:infinite_evaluation}, the evaluation graph of
a program can be infinite, especially when the program does not terminate on
every input. In order to find finite evaluation graphs, we need to add an
abstraction layer, which combines similar versions into one.
\begin{definition}[Abstraction]\label{def:abstraction}
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$.
\end{definition}
In general, the abstraction can be arbitrarily chosen, as long as the properties
above are satisfied. One common abstraction method is the so-called
property-based abstraction \cite{Domenech19} which selects a subset of
properties from a finite set of properties that are all entailed by the
original constraint set.
\begin{definition}[Property based abstraction]
Let $\Psi = \{\psi_1, \dots,\psi_n\}\subset \C$ be a finite non-empty set of
properties. Let $\neg \Psi = \{\neg \psi_1, \dots, \neg \psi_n\}$. The
abstraction space of the property-based abstraction is defined as $\A_\Psi =
2^{\Psi \union \neg \Psi} \union \{\texttt{true},\texttt{false}\}$ which is
also finite. The abstraction function $\alpha_\Psi : 2^{\C_\PV} \rightarrow
\A_\Psi$ is defined as
\begin{equation*}
\alpha_\Psi(\varphi) = \set{\psi_i}{ \llbracket\varphi\rrbracket
\subseteq \llbracket \psi_i \rrbracket, \psi_i \in \A_\Psi}
\end{equation*}
\end{definition}
\begin{lemma}\label{lem:pba}
A property based abstraction function is a valid abstraction function. For
all $\varphi \in 2^{\C_\PV}$ and finite set of properties $\Psi \subset \C$,
the following holds.
\begin{equation*}
\llbracket \varphi\rrbracket \subseteq \llbracket\alpha_\Psi\rrbracket
\end{equation*}
\proof{see Appendix on \pref{apdx:lem:pba}.}
\end{lemma}
The unfolding and evaluation are modified slightly to accommodate for the
abstraction function $\alpha$.
\begin{equation*}
\begin{gathered}
\unfold_\alpha(\langle \ell,\varphi\rangle, t) = (\langle \ell,
\varphi\rangle, p, \tau\Land\varphi, \eta,\langle \ell',
\alpha(\varphi') \rangle) \\ \text{for } t = (\ell, p, \tau, \eta,
\ell') \in \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau,
\eta) \\
\end{gathered}
\end{equation*}
\begin{equation*}
\unfold_\alpha(\langle \ell,\varphi\rangle, g) = \{
\unfold_\alpha(\langle\ell,\varphi\rangle, t) \mid t \in g
\}
\end{equation*}
\begin{equation*}
\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)
\end{equation*}
\begin{equation*}
G_{\Prog,\alpha}^* = \evaluate_{\Prog,\alpha}^*(G_0) =
\Union_{n=1}^\infty \evaluate_{\Prog,\alpha}^n(G_0)
\end{equation*}
For better readability, we denote abstracted constraints with the set notation
using curly braces. We write $\langle \ell, \{\psi_1, \dots, \psi_m\}\rangle$
instead of $\langle \ell, \psi_1 \land \dots \land \psi_m\rangle$, in order to
highlight the condensing characteristic of the abstraction.
\begin{example}\label{ex:global_abstr}
Consider program $\Prog_3$ from \fref{fig:ex_prob} on \pref{fig:ex_prob}
again. We define $\psi_1,\psi_2,\psi_3 \in \C$ and an abstraction space
$\A_\Psi$ where
\begin{equation*}
\begin{gathered}
\begin{aligned}
\psi_1 &= 1 \leq x, \hspace{1cm} \neg\psi_1 = 1 > x,\\
\psi_2 &= 2 \leq x, \hspace{1cm} \neg\psi_2 = 2 > x,\\
\psi_3 &= x \leq 3, \hspace{1cm} \neg\psi_3 = x > 3,\\
\psi_4 &= x \leq 4, \hspace{1cm} \neg\psi_4 = x > 4,\\
\psi_5 &= y > 0,\hspace{1cm} \neg\psi_5 = y \leq 0,\\
\psi_6 &= y \geq 0,\hspace{1cm} \neg\psi_6 = y < 0, \text{ and}
\end{aligned}\\
\A_\Psi =
\{\psi_1,\neg\psi_1,\dots,\psi_6,\neg\psi_6,\texttt{true},\texttt{false}\}.
\end{gathered}
\end{equation*}
The property-based abstraction $\alpha_\Psi$ uses the abstraction space
$\A_\Psi$. The
partial evaluation starts on the graph containing the single version
$\langle \ell_0, \texttt{true}\rangle$ and
\begin{equation*}
G_0 = (\{\langle \ell_0, \texttt{true}\rangle\}, \emptyset)
\end{equation*}
On the first evaluation step, the transition $t_0$ is unfolded yielding a
single new transition with a new version $\langle \ell_1,
\texttt{true}\rangle$:
\begin{align*}
t_{0,1} &= (\langle \ell_0, \texttt{true}\rangle, 1, \tau_0, \eta_0, \langle
\ell_1, \texttt{true}\rangle) \\
G_1 &= G_0 + \{t_{0,1}\}
\end{align*}
On the second step the transitions, $t_{1a}, t_{1b}$, and $t_2$ are unfolded
from $\langle \ell_1, \texttt{true}\rangle$, yielding three new transitions,
$t_{1a,1}, t_{1b,1}$, and $t_{2,1}$:
\begin{align*}
t_{1a,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
\eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle) \\
t_{1b,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
\eta_{1b},\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
t_{2,1} &= (\langle \ell_1, \texttt{true}\rangle, 1, \tau_2,
\eta_{1b},\langle \ell_2, \{\psi_5\}\rangle) \\
G_2 &= G_1 + \{t_{1a,1}, t_{1b,1},t_{2,1}\}
\end{align*}
On the third step of the evaluation the transitions $t_{1a}, t_{1b}$, and
$t_2$ are unfolded again, but this time from versions $\langle \ell_1,
\{\psi_1,\psi_3\}\rangle$ and $\langle \ell_1, \{\psi_2,\psi_4\}\rangle$,
yielding new transitions $t_{1a,2}, t_{1b,2}$, $t_{2,2},t_{1a,3}, t_{1b,3}$,
$t_{2,3}$:
\begin{align*}
t_{1a,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1a}, \langle
\ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle) \\
t_{1b,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1b}, \langle
\ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
t_{2,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 1, \tau_2
\Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_2,\langle \ell_2,
\{\psi_1,\psi_3,\psi_4,\psi_5\}\rangle)\\
t_{1a,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1a}, \langle
\ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
t_{1b,3} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1b}, \langle
\ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
t_{2,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 1, \tau_2
\Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_2, \langle \ell_2,
\{\psi_1,\psi_2,\psi_4,\psi_5\}\rangle) \\
t_{3,1} &= (\langle \ell_2, \{\psi_5\}\rangle, 1, \tau_3 \Land \psi_5,
\eta_{3}, \langle \ell_1, \{\psi_6\}\rangle) \\
G_3 &= G_2 + \{t_{1a,2}, t_{1b,2},t_{2,2},t_{1a,3},
t_{1b,3},t_{2,3},t_{3,1}\}
\end{align*}
Note that $t_{1a,2}, t_{1b,2}, t_{1a,3}$, and $t_{1b,3}$ transition to
versions $\langle \ell_1,~\{\psi_1,~\psi_3,~\psi_4\}\rangle$ and
$\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle$ that already exist in the
previous graph $G_2$.
The remaining evaluation steps are omitted for briefness, but the final
partial evaluation graph is shown in \fref{fig:ex_prob_fpe}.
\begin{figure}[ht]
\centering
\input{figures/ch3_p3_full_pe}
\caption{Partial evaluation graph $G_{\Prog_3,\alpha_\Psi}^*$ of $\Prog_3$
from \fref{fig:ex_prob}.\label{fig:ex_prob_fpe}}
\end{figure}
\end{example}
\subsection{Localised abstraction}
Example \ref{ex:global_abstr} illustrates how a program becomes large very
quickly and that using the same abstraction function at every location captures
unnecessary properties that are not really important for the flow of a program.
We introduce a \emph{localised} abstraction function that can take the evaluation
history and the location at which the constraint is abstracted into account.
\begin{definition}[Localised abstraction]
A \emph{localised} abstraction function is a function $S : \vers_\Prog
\rightarrow \vers_\Prog$ that \emph{can} abstract the constraint of a
version, but is not required to do so. For any version $\langle
\ell,\varphi\rangle \in \vers_\Prog$ the abstraction is required to be of
the form $S (\langle \ell, \varphi' \rangle)$ with
$\llbracket\varphi\rrbracket \subseteq \llbracket \varphi'\rrbracket$.
\end{definition}
\begin{rem}
We have dropped the requirement for a finite abstraction space for now and
will reintroduce it in a slightly altered form later on, in order to still
guarantee a finite partial evaluation graph.
\end{rem}
The unfold operation is adapted to accommodate for the dynamic abstraction
function.
\begin{equation*}
\begin{gathered}
\unfold_{S}(\langle \ell,\varphi\rangle, t) = (\langle \ell,
\varphi\rangle, p, \tau\Land\varphi, \eta,S(\langle
\ell',\varphi'\rangle)) \\ \text{for } t = (\ell, p, \tau, \eta,
\ell') \in \T_\Prog \text{ and } \varphi' = \unfold(\varphi \land \tau,
\eta) \\
\end{gathered}
\end{equation*}
\begin{equation*}
\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)
\end{equation*}
\begin{equation*}
G_{\Prog,S}^* = \evaluate_{\Prog,S}^*(G_0) =
\Union_{n=1}^\infty \evaluate_{\Prog,S}^n(G_0)
\end{equation*}
The localised abstraction function allows us to select different abstraction
functions for every location. When using property-based abstraction, we can
select different properties for every location, or not abstract at all.
\begin{definition}[Localised property-based
abstraction]\label{def:localized_pba}
Let $\Psi_{\ell_0},\dots,\Psi_{\ell_n} \subseteq (2^\C \union \{\bot\})$ be
properties for the locations $\ell_0,\dots,\ell_n \in \Loc_\Prog$. $\bot$
indicates that the location shall not be abstracted at all. We define the
localised property-based abstraction function
$S_{\Psi_{\ell_0},\dots,\Psi_{\ell_n}} : \vers_\Prog \rightarrow \C$ with
\begin{equation*}
S_{\Psi_{\ell_0},\dots,\Psi_{\ell_n}}(\langle\ell,\varphi\rangle) =
\begin{cases}
\alpha_{\Psi_\ell}(\varphi) & \text{if } \Psi_\ell \neq \bot \\
\varphi & \text{otherwise}
\end{cases}
\end{equation*}
\end{definition}
\begin{example}\label{ex:localized_pba}
\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}
Let us return to our example program $\Prog_3$. Location $\ell_0$ and $\ell_2$
are good candidates to not abstract at all, since they are a linear part of
the program and no branching will occur there. Besides, we select the same
properties $\Psi_{\ell_1} = \psi_1,\dots,\psi_6$ as in Example
\ref{ex:global_abstr}.
The localised property-based abstraction function
$S_{\bot,\Psi_{\ell_1},\bot}$ is used in every evaluation step.
The evaluation starts again with the graph containing only the version
$\langle\ell_0,\texttt{true}\rangle$. We will skip the details of every
evaluation step, and just show the final evaluation graph in
\fref{fig:ex_localized_pba}. It looks very similar to before, but we saved
some entailment checks on location $\ell_2$, in return for which the
versions at $\ell_2$ are no longer collapsed.
One can clearly see the disadvantage of abstracting fewer locations. In
practice the abstraction is expensive and abstracting fewer locations can
speed up the partial evaluation. The real strength of localised abstraction
will be seen when only evaluating a subset of transitions of $\Prog_3$.
\end{example}
Clearly, a global abstraction function is a special case of a localised
abstraction function, where every location is abstracted with the same
abstraction function. How to select properties for the localised property-based
abstraction is discussed in \Cref{ch:implementation}.
The property-based abstraction crafted in Example \ref{ex:localized_pba} was
carefully crafted to guarantee a finite abstraction graph. In fact, we will see
that the localised abstraction function must abstract on at least one location
per loop in the original program. This is formalized by the Lemma
\ref{lem:localized_pba_finite}. But before that, we will adapt the evaluation one
last time. Instead of evaluating the entire program, the evaluation will unfold
only a subset of transitions $T \subseteq \T_\Prog$. This way the evaluation can
be focused on only the parts of the program where the classical analysis failed.
The subset is not required to be connected. How to select the transitions for
the best evaluation results is discussed in \Cref{ch:implementation}.
\begin{definition}[Evaluation of a subset of transitions]
Let $\Prog$ be a \gls{pip} and $T \subseteq \T_\Prog$ be a subset of
transitions of $\Prog$. For a localised abstraction $S : \vers_\Prog
\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*}
\end{definition}
The partial evaluation is bootstrapped with the lift of the program with the
subset of transitions $T$ removed.
\begin{equation*}
G_0 = (G_\Prog - T)\lift
\end{equation*}
The evaluation is then repeated on $G_0$ until a fix-point is found.
\begin{equation*}
G_{\Prog,S,T}^* = \evaluate_{\Prog,S,T}^*(G_0) =\Union_{n=1}^\infty
\evaluate_{\Prog,S,T}^n(G_0)
\end{equation*}
\begin{example}\label{ex:component_pe}
In this example the partial evaluation of $\Prog_3$ is restricted to the
subset of transitions $T = \{t_{1a}, t_{1b}\}$, because the two loops are
the only problematic transitions during analysis with \gls{mprf}s. In
addition, we reduce the number of properties. The evaluation uses the
localised property-based abstraction $S_{\bot,\Psi_{\ell_1},\bot}$ with
$\Psi_1 = \{\psi_1, \psi_2, \psi_3, \psi_4\}$ where:
\begin{align*}
\psi_1 = 1 \leq x, \hspace{1cm} \neg\psi_1 = 1 > x,\\
\psi_2 = 2 \leq x, \hspace{1cm} \neg\psi_2 = 2 > x,\\
\psi_3 = x \leq 3, \hspace{1cm} \neg\psi_3 = x > 3,\\
\psi_4 = x \leq 4, \hspace{1cm} \neg\psi_4 = x > 4,\\
\end{align*}
The program is lifted as shown in Example \ref{ex:lift} and
\fref{fig:ex_lift}, but with the transitions $t_{1a}$ and $t_{1b}$ removed.
The partial evaluation starts on this graph $G_0$ with
\begin{align*}
V(G_0) &= \{\langle\ell_0,\texttt{true}\rangle,\langle\ell_1,
\texttt{true}\rangle,\langle\ell_2,\texttt{true}\rangle\}\\
E(G_0) &= \{t_0,t_2,t_3\}
\end{align*}
The transitions $t_{1a}$ and $t_{1b}$ are unfolded already in the first
evaluation step. We find two new transitions by unfolding $t_{1a}, t_{1b} \in
\TPout(\ell_1) \cap T$ from $\langle\ell_1,\texttt{true}\rangle$
\begin{align*}
t_{1a,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
\eta_{1a}, \langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle) \\
t_{1b,1} &= (\langle \ell_1, \texttt{true}\rangle, 0.5, \tau_1,
\eta_{1b},\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle) \\
G_1 &= G_0 + \{t_{1a,1},t_{1b,1}\}
\end{align*}
Note that the transition $t_2$ is not in $T$. Instead of unfolding it, the
transition $t_2' = (\langle\ell_1,\texttt{true}\rangle,1,\tau_2,\eta_2,
\langle\ell_2,\texttt{true}\rangle)$ is added to the graph, which is already
contained in the lift of $t_2$. The same holds for $t_0$ and $t_3$.
In the second step the new versions $\langle \ell_1,
\{\psi_1,\psi_3,\psi_4\}\rangle$ and $\langle \ell_1,
\{\psi_1\psi_2,\psi_4\}\rangle$ are unfolded. We find new transitions:
\begin{align*}
t_{1a,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1a}, \langle
\ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle), \\
t_{1b,2} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_{1b}, \langle
\ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle), \\
t_{2,1} &= (\langle \ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle, 1, \tau_2
\Land \psi_1 \Land \psi_3 \Land \psi_4, \eta_2,\langle \ell_2,
\texttt{true}\rangle),\\
t_{1a,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1a}, \langle
\ell_1, \{\psi_1,\psi_3,\psi_4\}\rangle), \\
t_{1b,3} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 0.5,
\tau_1 \Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_{1b}, \langle
\ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle), \\
t_{2,2} &= (\langle \ell_1, \{\psi_1,\psi_2,\psi_4\}\rangle, 1, \tau_2
\Land \psi_1 \Land \psi_2 \Land \psi_4, \eta_2, \langle \ell_2,
\texttt{true}\rangle), \text{ and}\\
G_2 &= G_1+ \{t_{1a,2},t_{1b,2},t_{2,1},t_{1a,3},t_{1b,3},t_{2,2}\}
\end{align*}
Note that the transitions $t_{2,1}$ and $t_{2,2}$ are new transitions but
they transition to the trivial version instead of being unfolded due to $t_2
\not\in T$.
The evaluation ends here, since no new versions were added in the previous
step. We obtain $G_3 = G_2 = G^*_{\Prog_3,S_{\bot,\Psi_{\ell_1},\bot},T}$.
The full evaluation graph is displayed in \fref{fig:ex_component_pe}.
\begin{figure}[ht]
\centering
\input{figures/ch3_p3_component_pe}
\caption{Partial evaluation graph of $\Prog_3$ from \fref{fig:ex_prob}
on a subset of transitions $T = \{t_{1a},t_{1b}\}$ and with a localised
property-based abstraction
$S_{\bot,\Psi_{\ell_1},\bot}$.\label{fig:ex_component_pe}}
\end{figure}
\end{example}
\begin{rem}
In practice, versions that have no incoming transitions in $G_0$ are
removed, before the evaluation to avoid unnecessary unfoldings. Nonetheless,
if the version is reachable in the partial evaluation, it is
re-added by the evaluation and evaluated in a later step.
\end{rem}
The partial evaluation over the entire program is a special case of the partial
evaluation with a subset $T = \T_\Prog$. All the following lemmas and theorems
hold equally for a (global) abstraction and partial evaluations of the entire
program.
\begin{lemma}[Original transitions]\label{lem:original_transition}
Let $G^*_{\Prog,S,T}$ be the evaluation graph of a \gls{pip} $\Prog$ for any
localised abstraction function $S$. For every transition $t = (\langle
\ell_1, \varphi_1\rangle, p, \tau, \eta, \langle \ell_2, \varphi_2\rangle)
\in E(G^*_{\Prog,S,T})$ one can find a unique transition denoted as
$\bar{t}\in\T_\Prog$ for which
\begin{equation*}
{\bar{t}} = (\ell_1, p, \tau', \eta, \ell_2)\textrm{, and }
\llbracket\tau\rrbracket \subseteq \llbracket\tau'\rrbracket.
\end{equation*}
\proof{Follows directly from the construction of the unfolding and the
evaluation.}
\end{lemma}
In the following, $\bar{t}$ shall always denote the original transition found
with Lemma \ref{lem:original_transition}. In Example \ref{ex:global_abstr} and
\ref{ex:component_pe}, the localised property-based abstraction was carefully
crafted so that the evaluation graph is finite. As was already predicted, the
partial evaluation graph for a localised abstraction function is finite when
at least one location per loop in the original program is abstracted to a finite
abstraction space.
\begin{lemma}\label{lem:localized_pba_finite}
Let $S$ be a localised abstraction function and $T \subseteq \TP$ 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.
\begin{proof}
Let $G_{\Prog,S,T}^*$ be the partial evaluation graph of a \gls{pip}
$\Prog$ with a localised abstraction $S$, and let
$\set{S(\langle\ell,\varphi\rangle)}{\varphi \in 2^{\C_\PV}}$ for some
$\ell \in L$ on any loop $L$ of $\Prog$.
The proof will be done by contradiction. Assume the partial evaluation
graph $G_{\Prog,S,T}^*$ is infinite.
We can construct an infinite path $p = v_0v_1\dots = \langle\ell_0,
\_\rangle\langle\ell_1,\_\rangle\dots \in \vers_\Prog^\omega$, where all
versions on this path are pairwise different. Let $n \in \N$. Since
$\evaluate_\Prog^*$ is infinite, there must exist a fresh version
$v_n \in E(G_n) \backslash E(G_{n-1})$ that was added by unfolding or
copying a transition $t_n =(\ell_{n-1},\_, \_, \_,\ell_n)$ from a
version $v_{n-1} = \langle \ell_{n-1},\_\rangle \in E(G_{n-1})$.
$v_{n-1}$ must have been freshly added in $G_{n-1}$ or else $v_n$ would
have been part of $G_{n-1}$ already. By backwards induction we can
create a path $v_0v_1\dots{}v_n$ of $G_n$ for arbitrarily large $n \in N$
with pairwise different versions, which implies that there exists an
infinite path $p = v_0v_1\dots = \langle\ell_0
\_\rangle\langle\ell_1,\_\rangle\dots \in \vers_\Prog^\omega$ with
pairwise different versions in $G_{\Prog,S,T}^*$ as well.
Every version was added by unfolding or copying a transition $t_i
=(\ell_{i-1},\_, \_, \_,\ell_i) \in \T_\Prog$. Consequently, there must
exist an infinite path $p' = \ell_0\ell_1\dots \in \Loc_\Prog^\omega$
and since $\Prog$ is finite the path must contain a loop $L \in \Loc^*$
that appears an infinite number of times on $p'$.
By assumption there must exist a location $\ell^* \in L$ for which
$\set{S(\langle\ell,\varphi\rangle)}{\varphi \in 2^{\C_\PV}}$ is finite. At
the same time, versions $\langle\ell^*,\_\rangle$ must appear an infinite
number of times on $p$, and they can only be abstracted to finitely
many possible versions, which is a contradiction of the versions on $p$
being pairwise different.
$G_{\Prog,S,T}^*$ cannot be infinite.
\end{proof}
\end{lemma}
Let $\GT_{G^*_{\Prog,S,T}}$ be the set of general transitions in the partial
evaluation graph $G^*_{\Prog,S,T}$ where every general transition $g \in
\GT_{G^*_{\Prog,S,T}}$ was added by the unfolding of a unique general
transition $g' \in \GTP$. We call $\bar{g} = g'$, similar to Lemma
\ref{lem:original_transition}, the original transition of $g$.
\begin{definition}[Partial evaluation]\label{def:partial_evaluation}
Let $\Prog$ as defined by Definition \ref{def:pip} and $G^*_{\Prog,S,T}$ be
the partial evaluation graph of $\Prog$ for some localised abstraction
function $S$ and a component $T \subseteq \TP$. A new \gls{pip} is defined
as $\Prog' = (\PV, \Loc_{\Prog'}, \GTPn, \langle \ell_0, \texttt{true}\rangle)$
where $\Loc_{\Prog'} = E(G^*_{\Prog,S,T}) \subset \vers_\Prog$, and $\GTPn =
\mathcal{G}\mathcal{T}_{G^*_{\Prog,S,T}} \subset 2^\VTP$. $\Prog'$ is
called the \textit{partial evaluation} of $\Prog$.
\end{definition}
\section{Correctness}
This section will prove that the partial evaluation $\Prog'$ of a program
$\Prog$ has the same worst-case expected runtime complexity as the original
program. Lemma \ref{lem:simurt} and \ref{lem:constrfleq} are precursors to
Theorem \ref{thm:correctness}, which shows that any runtime-complexity bounds for
the partial evaluation are runtime-complexity bounds of the original program,
which demonstrates the correctness of the construction. Lemma
\ref{lem:constrfgeq} and Theorem \ref{thm:thightness} show that the worst-case
expected runtime-complexity does not worsen with partial evaluation either.
The proof for correctness starts by defining a function that simulates a finite
prefix $f \in \fpath_\Prog$ in the partial evaluation $\Prog'$. Then we will
construct a new scheduler $\scheduler' \in \MDS_{\Prog'}$, that takes similar
decisions on $\Prog'$ as an original scheduler $\scheduler \in \MDS_\Prog$. When
using those schedulers, for any path $\varf \in \fpath_{\Prog}$ the simulation
of $f$ has equal probability and runtime-complexity. We will consider only
admissible finite prefixes, since non-admissible ones do not count in the
expected runtime-complexity as they have a probability of zero.
\begin{definition}
For a \gls{pip} $\Prog$ and the partial evaluation $\Prog'$ of $\Prog$ as
described in Definition \ref{def:partial_evaluation} with localised
abstraction function $S$ and component $T$, let $\simu_{\Prog,S,T}:
\fpath_\Prog \rightarrow \fpath_{\Prog'}$ be defined recursively.
\begin{equation*}
\begin{gathered}
\simu_{\Prog,S,T}((\ell, t, s)) =
(\langle \ell, \texttt{true}\rangle,
\unfold_{\Prog,S}(\langle \ell, \texttt{true}\rangle, t), s) \\
\simu_{\Prog,S,T}(\varf (\ell, t, s)) =
\varf'(\langle \ell, \texttt{true}\rangle,
\unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t), s)\\
\text{ where } \varf' = \simu(\varf) =
\dots{}(\langle\ell,\varphi\rangle, \_, \_)
\end{gathered}
\end{equation*}
\end{definition}
\begin{lemma}\label{lem:simurt}
Let $\Prog$ be a \gls{pip} and $\Prog'$ the partial evaluation $\Prog'$ of
$\Prog$ with localised abstraction function $S$ and component $T$.
\begin{enumerate}
\item \label{itm:simurt_rt} For any admissible finite prefix $f \in
\fpath_\Prog$
\begin{equation*}
\Rt_\Prog(\varf) = \Rt_{\Prog'}(\simu_{\Prog,S,T}(\varf))
\end{equation*}
\item \label{itm:simurt_neq} For any two distinct admissible finite prefixes
$f_1, f_2 \in \fpath_\Prog$
\begin{equation*}
\simu_{\Prog,S,T}(\varff_1) \neq \simu_{\Prog,S,T}(\varff_2)
\end{equation*}
\end{enumerate}
\proof{Item \ref{itm:simurt_rt} follows by construction since only
non-terminating transitions are selected in the simulation. Item
\ref{itm:simurt_neq} follows by construction, since all distinguishing
properties of $f_1$ and $f_2$ are copied into their respective simulations.
}
\end{lemma}
\begin{lemma}\label{lem:constrfleq}
Let $\Prog$ be a \gls{pip}, $s_0 \in \Sigma$ an arbitrary initial state,
$\scheduler \in \MDS_\Prog$ a Markovian scheduler, and $\Prog'$ the partial
evaluation as described in Definition \ref{def:partial_evaluation} with a
localised abstraction function $S$ and the subset of transitions $T
\subseteq \TP$. There exists a Markovian scheduler $\scheduler' \in
\MDS_{\Prog'}$, such that for all admissible finite prefixes
$f\in\fpath_\Prog$ with $\prSs(\varf) > 0$ there exists a finite prefix
$\varf' =
\simu_{\Prog,S,T}(\varf)
\in\fpath_{\Prog'}$ with
\begin{align*}
\prSs(\varf) = \prSns(\varf')
\end{align*}
\end{lemma}
\begin{proof}
The proof is divided into two steps. First a scheduler $\scheduler'$ is
constructed that will select a similar transition in $\Prog'$ when possible.
Then using this scheduler, the equal probability is shown by induction.
For a \gls{pip} $\Prog$, a Markovian scheduler $\scheduler \in \MDS$ of
$\Prog$, and the evaluation $\Prog'$ we construct a Markovian scheduler
$\scheduler' \in \MDS$ for $\Prog'$.
At a configuration $(\langle \ell, \varphi \rangle, t', s') \in
\confs_{\Prog'}$, if the original scheduler selects a general transition $g
\in \GT_\Prog$ and $g \neq g_\bot$, as well as $t' \neq t_\bot$, the new
scheduler is defined to select the general transition $g' =
\unfold_{\Prog,S,T}(\langle\ell,\varphi\rangle,g)$
The new scheduler selects the same assignment $\tilde{s}$ as $\scheduler$.
However, remember that $\tau_g' = \varphi \Land \tau_g$ and $\varphi \in
2^{\C_\PV}$. $s' \models \varphi$ is not guaranteed. $s' \not\models\varphi
\Land \tau_g$ if and only if $s \not\models \varphi$. In that case, the
scheduler is defined to select any other transition while respecting the
properties of a Markovian scheduler. In all other cases, for example if the
original scheduler selects $g_\bot$, or when $t' = t_\bot$, the scheduler
selects $g_\bot$ and keeps the assignment $s'$.
Formally, the scheduler is defined as follows:
\begin{equation*}
\scheduler'(\ell', t', s') =
\begin{cases}
(g', \tilde{s}) &
\begin{aligned}
&\text{if }\ell' = \langle \ell, \varphi \rangle \neq l_\bot, t'
\neq t_\bot, s' \models \varphi, \\ &\scheduler(\ell, \bar{t'}, s')
= (g, \tilde{s}), g \neq g_\bot\text{, and}\\ &g' =
\texttt{unfold}_{S,T}(\langle\ell, \varphi\rangle, g)
\end{aligned} \\
(g'^*, \tilde{s}^*) &
\begin{aligned}
&\text{if }\ell' = \langle \ell, \varphi \rangle \neq \ell_\bot, t'
\neq t_\bot, s' \not\models \varphi\text{, and}\\
&g'^* \in \GTPout(\langle \ell,\varphi\rangle) \text{ and }
\tilde{s}^* \models \tau_{g'^*}
\text{ exists}
\end{aligned}\\
(g_\bot, s') & \text{otherwise}
\end{cases}
\end{equation*}
$\scheduler'$ is indeed a valid scheduler: Case 1, let $s' \models \varphi$.
Case 1.1, let $\scheduler(\ell, \bar{t'},s')$ selects $(g_\bot, s')$. In
that case, $\scheduler(\ell', t', s') = (g_\bot, s')$ as well. This is
correct because if no $(g, \tilde{s}) \in \GTPnout(\ell) \times \Sigma$ with
$\tilde{s}|_\PV = s'$ and $\tilde{s} \models \tau_g$ exist, then does no
$(g', \tilde{s'}) \in \GTPout(\ell') \times \Sigma$, because all general
transitions in $\GTPout(\ell')$ have more restrictive guards than their
original counterparts.
Case 1.2, $\scheduler(\ell, \bar{t'},s')$ selects $(g, s')$ with $g \neq
g_\bot$. In that case $\scheduler(l, \bar{t'},s) = (g', \tilde{s})$ where
$\tau_{g'} = \varphi \Land \tau_g$ by construction and $g'$ is part of the
evaluation graph. Since $\tilde{s} \models \tau_g$ and $\tilde{s}|_\PV =
s'$, it follows $\tilde{s} \models \varphi \Land \tau_g$.
Case 2, let $s' \not\models \varphi$. The properties of a scheduler (see
Definition \ref{def:mscheduler}) are satisfied by construction.
We conclude that the constructed scheduler $\scheduler'$ is a valid
Markovian scheduler for $\Prog'$.
\rem{If unreachable transitions and versions are removed from the
program, the original scheduler might select a general transition that has
been removed in the partial evaluation. In that case the new scheduler can
be adapted to make an arbitrary valid selection, as is already done for the
case where $s' \not\models \varphi$.}
Let $s_0 \in \Sigma$ be any initial state.
\textbf{Claim:} For any admissible finite prefix $f_n= c_0\dots{}c_n\in
\fpath_\Prog$ of length $n \leq \N$ with $\prSs(\varff_n) > 0$, $c_i =
(\ell_i,s_i,t_i)$ and all $i = 0,1,\dots$ one can find a finite prefix
$\varfpi{n} = \simu_{\Prog,S,T}(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:
\begin{enumerate}
\item $\prSs(\varf) = \prSns(\varf')$, and
\item $s_n \models \varphi_n$ where $\varfpi{n} = \dots{}(\langle \_,
\varphi_n\rangle, \_, s_n)$.\label{itm:si_models_phi}
\end{enumerate}
Item \ref{itm:si_models_phi} is required for the scheduler to select a
similar general transition but it is not important for the final result.
\textbf{Induction start:} $n=0$.
Since $f_0 = c_0$ is an admissible prefix, $c_0 = (\ell_0,
t_\text{in},s_0)$. Set $\varfpi{0} = c'_0 = \simu_{\Prog,S,T}(\varf) = (\langle
\ell_0,\texttt{true}\rangle,s_0,t_\text{in})$. $\langle \ell_0,
\texttt{true}\rangle$ is a location in $\Prog'$ by construction. $s_0
\models \texttt{true}$ trivially. $\prSs(c_0) = \prSs'(c'_0) = 1$ since both
$c_0$ and $c'_0$ are valid starting configurations in $\Prog$ and $\Prog'$
respectively.
\textbf{Induction step.}
Assume the induction hypothesis holds for $n \in \N$. Let $f_{n+1} =
c_0\dots{}c_{n+1} \in \fpath_\Prog$ of length $n+1 \in \N$ be an admissible
prefix with probability $\prSs(f_{n+1})>0$, then $f_n = c_0\dots{}c_{n}$ of
length $n$ is also admissible with $\prSs(f_n) > 0$. By induction hypothesis
a finite prefix $\varfpi{n} = \simu_{\Prog,S,T}(f_n) = c'_0\dots{}c'_{n} \in
\fpath_{\Prog'}$ of equal length exists with
\begin{enumerate}
\item $\prSs(f_n) = \prSns'(\varfpi{n})$, and
\item $s_n \models \varphi_n$ where $\varfpi{n} = \dots{}(\langle _,
\varphi_n\rangle, \_, s_n)$.
\end{enumerate}
Moreover, let $c_i = (\ell_i,t_i,s_i)$ and $t_i = (\ell_{i-1}, p_i, \tau_i,
\eta_i, \ell_i)$ for all $ 1 \leq i \leq n+1$. The simulation sets
$t'_{n+1}$, location $\ell'_{n+1}$ and assignment $s'_{n+1}$ of the last
configuration $c'_{n+1} = (\ell'_{n+1}, t'_{n+1}, s'_{n+1})$ on the extended
finite prefix $\varfpi{{}n+1} =\simu_{\Prog,S,T}(\varff_{n+1})= \simu_{\Prog,S,T}(\varff_n)c'_{n+1}$ to
\begin{align*}
t'_{n+1} &= (\langle \ell_n, \varphi_n\rangle, \varphi_n \Land
\tau_{n+1}, \eta_{n+1}, \langle \ell_{n+1}, \varphi_{n+1}\rangle)\\ &=
\texttt{unfold}_{S,T}(\langle \ell_n, \varphi_n\rangle, t_{n+1}) \in
\TPn,\\
\ell'_{n+1} &= \langle \ell_{n+1}, \varphi_{n+1}\rangle, \text{ and} \\
s'_{n+1} &= s_{n+1}
\end{align*}
Let $\scheduler(c_n) = (g_{n+1},\tilde{s})$ be the selection of the original
scheduler where $g_{n+1} \neq g_\bot$ due to $f$ being admissible. By
construction of the scheduler and since $s_n \models \varphi_n$, the new
scheduler $\scheduler'$ selects a general transition $g'\in\GTPn$ with
$t'_{n+1} \in g' \neq g_\bot$.
The last step on the finite prefix $\varfpi{n+1}$ has the same probability
as the last step on the original finite prefix $f_{n+1}$. As a consequence,
using the induction hypothesis, both prefixes have the same probability.
\begin{align*}
\prSs(c_n \rightarrow c_{n+1}) &= p \cdot
\prod_{x\in\PV}[\eta(x)](\tilde{s})(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
\delta_{\tilde{s}_n(u),s_n(u)} \\
&= \prSns(c'_n \rightarrow c'_{n+1}) \\
\Leftrightarrow \prSs(f_{n+1}) &= \prSs(f_n) \cdot \prSs(c_n \rightarrow
c_{n+1}) \\
&= \prSs(\varfpi{n}) \cdot \prSs(c'_n \rightarrow c'_{n+1}) =
\prSns(\varff_{n+1})
\end{align*}
Finally, it follows that $s'_{n+1} \in \support_{\tilde{s}}(\eta_{n+1})$ and
by Lemma \ref{lem:unfold}, $s'_{n+1} \models \varphi_{n+1}$.
\rem{
At this point it becomes clear why filtering unreachable transitions
and versions can be done in practice. The newly constructed prefix can
never take those transitions, or else it would not be admissible. Hence
the presence of non-reachable transitions and versions does not change
anything for this proof.
}
The induction hypothesis holds for $n+1$.
\end{proof}
Lemma \ref{lem:constrfleq} implies that
$\simu_{\Prog,S,T}(\varf)\in\fpath_{\Prog'}$ is admissible for any admissible
finite prefix $f \in \fpath_\Prog$.
\begin{theorem}\label{thm:correctness}
For a \gls{pip} $\Prog$, the partial evaluation $\Prog'$ of $\Prog$ as
described in Definition \ref{def:partial_evaluation}, and an initial state
$s_0 \in\Sigma$ the following holds:
\begin{equation*}
\sup_{\scheduler \in \MDS}(\ESs(\Rt_\Prog)) \leq
\sup_{\scheduler' \in \MDS}(\ESns(\Rt_\Prog')) \\
\end{equation*}
\begin{proof}
Let $\Prog$ be an arbitrary \gls{pip}, $\Prog'$ be its evaluation and
$s_0 \in \Sigma$ be any starting state. For any scheduler $\scheduler
\in \Pi_\text{MD}$ let $\scheduler' \in\Pi_\text{MD}$ be constructed as
in Lemma \ref{lem:constrfleq}. Recall Definition
\ref{def:expected_value}.
\begin{align*}
\ESs(\Rt_{\Prog}) &= \sum_{i=1}^\infty i \cdot \PrSs(\Rt_\Prog=i) =
\sum_{i=1}^\infty \PrSs(\Rt_\Prog \geq i) \\ &= \sum_{i=1}^\infty
\sum_{\substack{f \in \fpath_\Prog\\ |\varf| \leq i \\ \Rt_\Prog(f)
\leq i}} 1-\prSs(\varf) \\
\end{align*}
\begin{align}
\sum_{i=1}^\infty\sum_{\substack{f \in \fpath_\Prog\\ |\varf| \leq
i\\ \Rt_\Prog(\varf) \leq i}}^\infty 1- \prSs(\varf) &\leq
\sum_{i=1}^\infty\sum_{\substack{f \in
\fpath_{\Prog'}\\ |\varf| \leq i\\ \Rt_\Prog(\varf)
\leq i}}^\infty 1- \prSns(\varf) \label{eq:sumsleq} \\
\Leftrightarrow \ESs(\Rt_\Prog) &\leq \ESns(\Rt_{\Prog'})
\label{eq:esleq}
\end{align}
By Lemma \ref{lem:constrfleq}, for every finite prefix $f\in
\fpath_\Prog$ with non-zero probability, one can construct a path of
equal probability $\varf' \in \fpath_{\Prog'}$. By Lemma
\ref{lem:simurt} they are all pairwise different. Hence (at least) all
constructed paths $\varf'$ contribute with equal probability to the sum
on the right side of Equation \eqref{eq:sumsleq}.
Taking the supremum over all schedulers on both sides of Equation
\eqref{eq:esleq} does not change the relation, since we just found for
every scheduler of $\Prog$ a scheduler with equal or larger expected
runtime for $\Prog'$.
\begin{equation*}
\sup_{\scheduler \in \MDS}(\ESs(\Rt(\Prog))) \leq
\sup_{\scheduler' \in \MDS}(\ESns(\Rt(\Prog'))) \\
\end{equation*}
\end{proof}
\end{theorem}
The following Theorem \ref{thm:thightness} shows, that the partial evaluation
does not worsen the worst-case expected runtime complexity either. Note, this
does not imply that a perfectly tight bound for the worst-case expected runtime
can be found. Similar to Lemma \ref{lem:constrfleq} we first construct a new
scheduler $\scheduler \in \HDS_\Prog$ and show that when using this scheduler, a
finite path of equal probability and runtime-complexity exists in $\Prog$ for
every finite path in
$\Prog'$.
\begin{lemma}\label{lem:constrfgeq}
For a \gls{pip} $\Prog$, the partial evaluation $\Prog'$ as described in
Definition \ref{def:partial_evaluation} and a Markovian scheduler
$\scheduler \in \MDS_{\Prog'}$, there exists a \emph{history dependent}
scheduler $\scheduler' \in \HDS_{\Prog}$, such that for all finite prefixes
$f\in\fpath_\Prog'$ there exists a finite prefix $f\in\fpath_{\Prog}$
with
\begin{enumerate}
\item $\Rt_{\Prog'}(\varf) = \Rt_{\Prog}(\varf')$
\item $\prSns(\varf) = \prSs(\varf')$
\end{enumerate}
\end{lemma}
\begin{rem}
We require a history dependent scheduler instead of a Markovian scheduler,
because the Markovian $\scheduler$ can select general transitions $g_1, g_2
\in \GTPn$ with $g_1 \neq g_2$ at the version $\langle \ell,
\varphi_1\rangle$ and $\langle \ell, \varphi_2\rangle \in \Loc_\Prog'$,
whereas the Markovian scheduler would be forced to always select the same
transition $g \in \GTP$ at location $\ell$. As demonstrated in Lemma
\ref{lem:hdsvsmds} this does not matter when considering the worst-case.
\end{rem}
\begin{proof}
Again we start with the construction of the scheduler $\scheduler' \in
\HDS_{\Prog'}$. It simulates the given history on the partial evaluation up
to a configuration $c'_n \in \confs_{\Prog'}$ and then selects the original
general transition $\bar{g} \in \GTPn$ to the general transition $g \in
\GTP$ selected by the scheduler $\scheduler(c'_n) = (g, \tilde{s})$, and
keeps the assignment $\tilde{s}$.
Formally, the scheduler $\scheduler'$ is defined as follows:
\begin{equation*}
\scheduler'(\varf(\ell,t,s)) =
\begin{cases}
(\bar{g}, \tilde{s}) & \begin{aligned}
&\text{if } \varf' = \simu_{\Prog,S,T}(\varf(\ell,t,s)) = \dots
c'_n, \scheduler(c'_n) = (g, \tilde{s})\text{, and }\\ &g \neq
g_\bot,
\end{aligned}\\
(g^*, \tilde{s}^*) & \begin{aligned}
&\text{if } \simu_{\Prog,S,T}(\varf(\ell,t,s)) = \dots c'_n,
\scheduler(c'_n) = (g, \tilde{s}), \\ &g = g_\bot \text{, and }
g^* \in \GTPout(\ell), \text{ and } \tilde{s}^* \models
\tau_{g^*} \text { exists,}
\end{aligned}\\
(g_\bot, s) & \text{otherwise}
\end{cases}
\end{equation*}
\begin{rem}
Since all general transitions have more restrictive guards then their
originals, it is possible that a location $\ell$ a general transition
with a satisfiable guard exists in $\Prog$ whereas the guards of all
general transitions at a location $\langle \ell, \varphi\rangle$ cannot
be satisfied by the scheduler. In that case, the new scheduler selects
any one of the valid general transitions $g^*$ and a matching assignment
$\tilde{s}^*$. As before, this doesn't matter since those
configurations can never be reached by an admissible run.
\end{rem}
\textbf{Claim:} Let $s_0\in\Sigma$ be an initial state. For any finite
prefix $f = \dots (\langle\ell_n, \varphi_n\rangle, t_n, s_n) \in
\fpath_{\Prog'}$ with probability
$\prSs(\varf) > 0$ there exists a finite prefix $\varf' = \dots
(\ell_n,\bar{t}_n,s_n) \in \fpath_\Prog$ for which
\begin{enumerate}
\item $\Rt_{\Prog'}(\varf) = \Rt_{\Prog}(\varf')$
\item $\prSns(\varf) = \prSs(\varf')$
\end{enumerate}
\textbf{Induction start:} $n = 0$. Let $f_0 = c_0 = (\langle \ell_0,
\texttt{true}\rangle, t_\text{in}, s_0) \in \fpath_\Prog'$ which is the only
initial configuration with non-zero probability $\prSs(\varff_0) = 1$. We
set $\varfpi{0} = c'_0 = (\ell_0, t_\text{in}, s_0)$ which is by
construction the only valid starting configuration of $\Prog'$ with
$\prSns(c'_0) = 1$.
\textbf{Induction step.} Assume the induction hypothesis holds for $n \in
\N$. Let $f_{n+1} = c_0\dots{}c_nc_{n+1} \in \fpath_{\Prog'}$ of length $n+1
\in \N$ be an admissible prefix with probability $\prSs(\varff_{n+1})>0$,
then $f_n = c_0\dots{}c_{n}$ of length $n$ is also admissible with
$\prSs(\varff_n) > 0$. By induction hypothesis a finite prefix $\varfpi{n}
= c'_0\dots{}c'_{n} \in \fpath_{\Prog}$ of equal length and probability
exists. Additionally $c_n = (\langle\ell_n,\varphi\rangle, \_, s_n)$ and
$c'_n = (\ell_n, \_, s_n)$.
Let $c_{n+1} = (\langle \ell_{n+1}, \_ \rangle, t_{n+1}, s_{n+1}) \in
\confs_{\Prog'}$. We set $c'_{n+1} = (\ell_{n+1}, \bar{t}_{n+1}, s_{n+1})$
to be the last configuration of $\varfpi{{}n+1}=\varfpi{{}n}c'_{n+1}$.
Let $g\in\GTPn$, and $\tilde{s} \in \Sigma$ be the general transition and
assignment selected by the scheduler $\scheduler(c_{n+1}) = (g, \tilde{s})$.
\textbf{Case 1}: $g \neq g_\bot$. Then, the constructed scheduler selects
$\scheduler'(c'_{n+1}) = (\bar{g},\tilde{s})$ by construction and since the
guard $\tau_{\bar{g}}$ is less restrictive than the guard $\tau_g$, $\tilde{s}
\models \tau_{\bar{g}}$ and
\begin{equation*}
\prSs(c_n \rightarrow c_{n+1}) = p \cdot
\prod_{x\in\PV}[\eta(x)](\tilde{s})(s_{n+1}(x)) \cdot
\prod_{u\in\V\backslash\PV} \delta_{\tilde{s}_n(u),s_n(u)} = \prSns(c'_n
\rightarrow c'_{n+1})
\end{equation*}
\textbf{Case 2}: $g = g_\bot$. By construction of the unfolding the $s_n
\models \varphi_n$ and because $s_n \not\models \varphi \land \tau_g =
\varphi \land \tau_{\bar{g}}$ for any general transition $g \in
\GTPnout(\langle\ell_n, \varphi_n\rangle)$, there cannot be any general
transition $g' \in \GTPout$ for which $s_n \models \tau_{g'}$. The newly
constructed scheduler selects $\scheduler'(c'_{n+1}) = (g_\bot,s)$ as well.
By using the induction hypothesis we arrive at the following, concluding the
proof.
\begin{equation*}
\prSs(\varff_nc_{n+1}) = \prSns(\varfpi{n+1}c'_{n+1})
\end{equation*}
\end{proof}
\begin{theorem}\label{thm:thightness}
For a pip $\Prog$, the evaluation $\Prog'$ as described in
Definition \ref{def:partial_evaluation}, and a starting state $s_0
\in\Sigma$. The following holds:
\begin{equation*}
\sup_{\scheduler \in \MDS_{\Prog}}(\ESs(\Rt_{\Prog'})) \leq
\sup_{\scheduler' \in \MDS_{\Prog}}(\ESs(\Rt_{\Prog})) \\
\end{equation*}
\begin{proof}
Let $\Prog$ be an arbitrary \gls{pip}, $\Prog'$ be its evaluation and
$s_0 \in \Sigma$ be any initial state. For any scheduler $\scheduler \in
\MDS_{\Prog'}$ let $\scheduler' \in \HDS_\Prog$ be constructed as in
Lemma \ref{lem:constrfgeq}. Analogously to Theorem
\ref{thm:correctness}, the following relation holds:
\begin{equation*}
\sup_{\scheduler \in \MDS_\Prog}(\ESs(\Rt_\Prog)) \leq
\sup_{\scheduler \in \HDS_{\Prog}}(\ESs(\Rt_{\Prog'})) \\
\end{equation*}
By Lemma \ref{lem:hdsvsmds} the fact that we used a history-dependent
scheduler does not matter in the supremum and we optain the following
inequality, concluding our proof.
\begin{equation*}
\sup_{\scheduler \in \HDS_\Prog}(\ESs(\Rt_\Prog)) \leq
\sup_{\scheduler \in \HDS_{\Prog}}(\ESs(\Rt_{\Prog'})) \\
\end{equation*}
\end{proof}
\end{theorem}
Overall by Theorem \ref{thm:correctness} and Theorem \ref{thm:thightness}, we
conclude
\begin{align*}
\sup_{\scheduler \in \Pi_\text{HD}}(\ESs(\Rt(\Prog))) &= \sup_{\scheduler'
\in \Pi_\text{HD}}(\ESns(\Rt(\Prog'))) \\
\end{align*}
We have shown in Theorem \ref{thm:correctness}, that for any starting state, the
new program has a worst-case expected runtime at least as large as the original
program. Hence any bounds found for the partial evaluation are bounds for the
original program. Theorem \ref{thm:thightness} has shown additionally, that the
worst-case expected runtime do not worsen with a partial evaluation.