Computing Expected Runtimes for Constant Probability Programs

TL;DR

This paper introduces constant probability programs, providing a decision procedure for their almost sure termination and an algorithm to compute their exact expected runtimes efficiently.

Contribution

It defines CP programs and offers a novel, straightforward method to determine their termination behavior and expected runtime, extending classical probability theory results.

Findings

Decidable almost sure termination for CP programs

Efficient computation of expected runtimes for CP programs

Asymptotically tight bounds on expected runtimes

Abstract

We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almost sure termination of programs in this class. Moreover, asymptotically tight bounds on their expected runtime can always be computed easily. Based on this, we present an algorithm to infer the exact expected runtime of any CP program.

Equations

$$f(\vec{x})={\sum }_{1\le j\le n}{p}_{{\vec{c}}_j}(\vec{x})\cdot f(\vec{x}+{\vec{c}}_j)+p^{\prime }(\vec{x})\cdot f(\vec{d})+1\text{for all x with a∙x>b}.$$

$${\mathcal{L}}^{\mathcal{P}}(f)(\vec{x})=\{\begin{array}{ll}{\sum }_{1\le j\le n}{p}_{{\vec{c}}_j}(\vec{x})\cdot f(\vec{x}+{\vec{c}}_j)+p^{\prime }(\vec{x})\cdot f(\vec{d})+1,& \text{if }\vec{a}\bullet \vec{x}>b\\ f(\vec{x}),& \text{if }\vec{a}\bullet \vec{x}\le b\end{array}$$

$$\{\begin{array}{ll}\frac{6}{11}\cdot f(t+1,h)+\frac{1}{22}\cdot {\sum }_{1\le j\le 10}f(t+1,h+j)+1,& \text{if t−h>−1}\\ f(t,h),& \text{if t−h≤−1}\end{array}$$

$$-\frac{1}{{\mu }_{{\mathcal{P}}^{rdw}}}\cdot {rdw}_{\mathcal{P}}({\vec{x}}_0)\le r{t}_{{\vec{x}}_0}^{\mathcal{P}}\le -\frac{1}{{\mu }_{{\mathcal{P}}^{rdw}}}\cdot {rdw}_{\mathcal{P}}({\vec{x}}_0)+\frac{1-k_{\mathcal{P}}}{{\mu }_{{\mathcal{P}}^{rdw}}}.$$

$$f(x)={\sum }_{-k\le j\le m}{p}_j\cdot f(x+j)+p^{\prime }\cdot f(d)+1\text{for all x>0},$$

$$f(x)=0\text{for all x≤0}.$$

$$f(x)={\sum }_{-k\le j\le m}{p}_j\cdot f(x+j)+1\text{for all x>0}.$$

$$f(x)=\frac{6}{11}\cdot f(x+1)+\frac{1}{11}\cdot f(x)+\frac{1}{22}\cdot f(x-1)+\frac{7}{22}\cdot f(x-2)+1\text{ for all x>0}.$$

$$\begin{array}[]{r@{\;\;}c@{\;\;}l}0&=&p_{m}\cdot f(x+m)+\ldots+p_{1}\cdot f(x+1)+(p_{0}-1)\cdot f(x)\;+\\ &&p_{-1}\cdot f(x-1)+\ldots+p_{-k}\cdot f(x-k)+1\hskip 59.75095pt\text{for all $\displaystyle x>0$.}\end{array}$$

$$C_{const}=\frac{1}{p^{\prime }},\text{if p′>0 and }{C}_{lin}=-\frac{1}{{\mu }_{\mathcal{P}}},\text{if p′=0.}$$

$${\chi }_{\mathcal{P}}(\lambda )=p_m\cdot {\lambda }^{k+m}+\dots +p_1\cdot {\lambda }^{k+1}+(p_0-1)\cdot {\lambda }^k+p_{-1}\cdot {\lambda }^{k-1}+\dots +p_{-k}$$

$${\lambda }_j^x\cdot x^u\text{ for all 1≤j≤c and all 0≤u≤vj−1}$$

$$f(x)=C(x)+{\sum }_{1\le j\le c}{\sum }_{0\le u\le v_j-1}{a}_{j,u}\cdot {\lambda }_j^x\cdot x^u\text{for all x>−k,}$$

$${\chi }_{{\mathcal{P}}_{race}^{mod}}(\lambda )=\frac{6}{11}\cdot {\lambda }^3-\frac{10}{11}\cdot {\lambda }^2+\frac{1}{22}\cdot \lambda +\frac{7}{22}.$$

$$\begin{array}[]{r@{\;\;}c@{\;\;}l}f(x)&=&C_{lin}\cdot x+a_{1}\cdot 1^{x}+a_{2}\cdot(-\tfrac{1}{2})^{x}\!+a_{3}\cdot(\tfrac{7}{6})^{x}\\ &=&\tfrac{22}{3}\cdot x+a_{1}+a_{2}\cdot(-\tfrac{1}{2})^{x}\!+a_{3}\cdot(\tfrac{7}{6})^{x}\hskip 31.2982pt\text{for $\displaystyle x>-2$}.\end{array}$$

$$r{t}_x^{\mathcal{P}}=C(x)+{\sum }_{1\le j\le c,|{\lambda }_j|\le 1}{\sum }_{0\le u\le v_j-1}{a}_{j,u}\cdot {\lambda }_j^x\cdot x^u\text{for x>0},$$

$$0=C(x)+{\sum }_{1\le j\le c,|{\lambda }_j|\le 1}{\sum }_{0\le u\le v_j-1}{a}_{j,u}\cdot {\lambda }_j^x\cdot x^u\text{for −k+1≤x≤0}$$

$$r{t}_x^{{\mathcal{P}}_{race}^{mod}}=\frac{22}{3}\cdot x+a_1+a_2\cdot (-\frac{1}{2}{)}^x\text{for x>0, cf. lx@crefcreftype refnumallSolutionsTortoise.}$$

$$0$$

$$\displaystyle rt^{\mathcal{P}}_{x}\!=\!\left\{\begin{array}[]{lll}C(x)&+\sum_{1\leq j\leq s,\;|\lambda_{j}|\leq 1}\;\;\;\sum_{0\leq u\leq v_{j}-1}a_{j,u}\cdot\lambda_{j}^{x}\cdot x^{u}\\ &+\sum_{s+1\leq j\leq s+t,\;|\lambda_{j}|\leq 1}\;\sum_{0\leq u\leq v_{j}-1}\left(b_{j,u}\!\cdot\!\mathrm{Re}(\lambda_{j}^{x})+b_{j,u}^{\prime}\!\cdot\!\mathrm{Im}(\lambda_{j}^{x})\right)\cdot x^{u},&\text{for $\displaystyle x>0$}\\ 0,&&\text{for $\displaystyle x\leq 0$}\end{array}\right.$$

$$\displaystyle\begin{array}[]{rl}rt^{\mathcal{P}_{race}}_{(t,h)}=&0.049\cdot{0.65}^{(t-h+1)}\;\cdot\sin\left(2.8\cdot(t-h+1)\right)-0.35\cdot{0.65}^{(t-h+1)}\!\cdot\cos\left(2.8\cdot(t-h+1)\right)\\ &+0.15\cdot{0.66}^{(t-h+1)}\!\cdot\sin\left(2.2\cdot(t-h+1)\right)-0.35\cdot{0.66}^{(t-h+1)}\!\cdot\cos\left(2.2\cdot(t-h+1)\right)\\ &+0.3\cdot{0.7}^{(t-h+1)}\!\cdot\sin\left(1.5\cdot(t-h+1)\right)-0.39\cdot{0.7}^{(t-h+1)}\!\cdot\cos\left(1.5\,(t-h+1)\right)\\ &+0.62\cdot{0.75}^{(t-h+1)}\!\cdot\sin\left(0.83\cdot(t-h+1)\right)-0.49\cdot{0.75}^{(t-h+1)}\!\cdot\cos\left(0.83\cdot(t-h+1)\right)\\ &+\tfrac{2}{3}\cdot(t-h)\;+\;2.3\\ \end{array}$$

$$r{t}_x^{\mathcal{P}}=8+a_1\cdot (2-\sqrt{2}{)}^x\text{for x>0}.$$

$$r{t}_x^{\mathcal{P}}=8-8\cdot (2-\sqrt{2}{)}^x,$$

$$f(x)=\frac{30}{13}\cdot x+a_1+a_2\cdot (\frac{-1+\sqrt{3}i}{5}{)}^x+a_3\cdot (\frac{-1-\sqrt{3}i}{5}{)}^x\text{for x>−3}$$

$$r{t}_x^{\mathcal{P}}=\frac{30}{13}\cdot x+\frac{180}{169}-\frac{180}{169}\cdot {\left(\frac{2}{5}\right)}^x\cdot \cos \left(\frac{2\pi }{3}\cdot x\right)+\frac{4}{169}\cdot \sqrt{3}\cdot {\left(\frac{2}{5}\right)}^x\cdot \sin \left(\frac{2\pi }{3}\cdot x\right).$$

$$f(x)=\frac{175}{12}\cdot x+a_{1,0}+a_{2,0}\cdot (-\frac{1}{5}{)}^x+a_{2,1}\cdot x\cdot (-\frac{1}{5}{)}^x\text{for x>−3}.$$

$$0$$

$$r{t}_x^{\mathcal{P}}=\frac{175}{12}x+\frac{175}{36}-\frac{175}{36}\cdot (-\frac{1}{5}{)}^x-\frac{35}{12}\cdot x\cdot (-\frac{1}{5}{)}^x.$$

$$r{t}_x^{\mathcal{P}}=\{\begin{array}{ll}2\cdot x,& \text{ if }x>0\\ 0,& \text{ if }x\le 0\end{array}$$

Full text

1 Introduction

Probabilistic programs are used to describe randomized algorithms and probabil-distributions, with applications in many areas. For example, consider the well-known program which models the race between a tortoise and a hare (see, e.g.,[11, 24, 30]). As long as the tortoise (variable $\displaystyle t$) is not behind the hare (variable $\displaystyle h$),

it does one step in each iteration. With probability $\displaystyle\tfrac{1}{2}$, the hare stays at its position and with probability $\displaystyle\tfrac{1}{2}$ it does a random number of steps uniformly chosen between $\displaystyle 0$ and $\displaystyle 10$. The race ends whenthe hare is in front of the tortoise. Here, the hare wins with probability 1 and thetechnique of [30] infers the upper bound $\displaystyle\tfrac{2}{3}\cdot\max(t-h+9,0)$ on the expected num-ber of loop iterations. Thus, the program is positively almost surely terminating.

Sect. 2 recapitulates preliminaries on probabilistic programs and on the connection between their expected runtime and their corresponding recurrence equation. Then we show in Sect. 3 and 4 that classical results on random walk theory directly yield a very simple decision procedure for (positive) almost sure termination of CP programs like the tortoise and hare example. In this way, we also obtain asymptotically tight bounds on the expected runtime of any CP program. Based on these bounds, in Sect. 5 we develop the first algorithm to compute closed forms for the exact expected runtime of such programs. In Sect. 6, we present its implementation in our tool KoAT [10] and discuss related and future work. We refer to the appendix for a collection of examples to illustrate the application of our algorithm and for all proofs.

2 Expected Runtimes of Probabilistic Programs

Example 1 (Tortoise and Hare)

The   pro-

gram $\displaystyle\mathcal{P}_{race}$ on the right formulates the race of the tortoise and the hare as a CP program. In the loop guard, we use the scalar product $\displaystyle(1,-1)\bullet(t,h)$ which stands for $\displaystyle t-h$. Exactly one of the instructions with numbers in brackets $\displaystyle[\ldots]$ is executed in each loop iteration and the number indicates the probability that the corresponding instruction is chosen.

We now define the kind of probabilistic programs considered in this paper.

Definition 1 (Probabilistic Program)

A   pro-

gram has the form on the right, where $\displaystyle\vec{x}=(x_{1},\ldots,x_{r})$ for some $\displaystyle r\geq 1$ is a tuple of pairwise different program variables, $\displaystyle\vec{a},\vec{c}_{1},\ldots,\vec{c}_{n}\in\mathbb{Z}^{r}$ are tuples of integers, the $\displaystyle\vec{c}_{j}$ are pairwise distinct, $\displaystyle b\!\in\!\mathbb{Z}$, $\displaystyle\bullet$ is the scalar product (i.e., $\displaystyle(a_{1},\ldots,a_{r})\bullet(x_{1},\ldots,x_{r})=a_{1}\cdot x_{1}+\ldots+a_{r}\cdot x_{r}$), and $\displaystyle\vec{d}\in\mathbb{Z}^{r}$ with $\displaystyle\vec{a}\bullet\vec{d}\leq b$. We require $\displaystyle p_{\vec{c}_{1}}(\vec{x}),\ldots,p_{\vec{c}_{n}}(\vec{x}),p^{\prime}(\vec{x})\in\mathbb{R}_{\geq 0}=\{r\in\mathbb{R}\mid r\geq 0\}$ and $\displaystyle\sum\nolimits_{1\leq j\leq n}p_{\vec{c}_{j}}(\vec{x})+p^{\prime}(\vec{x})=1$ for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$. It is a program with direct termination if there is an $\displaystyle\vec{x}\in\mathbb{Z}^{r}$ with $\displaystyle\vec{a}\bullet\vec{x}>b$ and $\displaystyle p^{\prime}(\vec{x})>0$. If all probabilities are constant, i.e., if there are $\displaystyle p_{\vec{c}_{1}},\ldots,p_{\vec{c}_{n}},p^{\prime}\in\mathbb{R}_{\geq 0}$ such that $\displaystyle p_{\vec{c}_{j}}(\vec{x})=p_{\vec{c}_{j}}$ and $\displaystyle p^{\prime}(\vec{x})=p^{\prime}$ for all $\displaystyle 1\leq j\leq n$ and all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$, we call it a constant probability (CP) program.

Such a program means that the integer variables $\displaystyle\vec{x}$ are changed to $\displaystyle\vec{x}+\vec{c}_{j}$ with probability $\displaystyle p_{\vec{c}_{j}}(\vec{x})$. For inputs $\displaystyle\vec{x}$ with $\displaystyle\vec{a}\bullet\vec{x}\leq b$ the program terminates immediately. Note that the program in Ex. 1 has no direct termination (i.e., $\displaystyle p^{\prime}(\vec{x})=0$ for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$). Since the values of the program variables only depend on their values in the previous loop iteration, our programs correspond to Markov Chains [32] and they are related to random walks [21, 33, 17], cf. the appendix for details.

Clearly, in general termination is undecidable and closed forms for the runtimes of programs are not computable. Thus, decidability results can only be obtained for suitably restricted forms of programs. Our class nevertheless includes many examples that are often regarded in the literature on probabilistic programs. So while other approaches are concerned with incomplete techniques to analyze termination and complexity, we investigate classes of probabilistic programs where one can decide the termination behavior, always find complexity bounds, and even compute the expected runtime exactly. Our decision procedure could be integrated into general tools for termination and complexity analysis of probabilistic programs: As soon as one has to investigate a sub-program that falls into our class, one can use the decision procedure to compute its exact runtime. Our contributions provide a starting point for such results and the considered class of programs can be extended further in future work.

In probability theory (see, e.g., [2]), given a set $\displaystyle\Omega$ of possible events, the goal is to measure the probability that events are in certain subsets of $\displaystyle\Omega$. To this end, one regards a set $\displaystyle\mathfrak{F}$ of subsets of $\displaystyle\Omega$, such that $\displaystyle\mathfrak{F}$ contains the full set $\displaystyle\Omega$ and is closed under complement and countable unions. Such a set $\displaystyle\mathfrak{F}$ is called a $\displaystyle\sigma$-field, and a pair of $\displaystyle\Omega$ and a corresponding $\displaystyle\sigma$-field $\displaystyle\mathfrak{F}$ is called a measurable space.

A probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ extends a measurable space $\displaystyle(\Omega,\mathfrak{F})$ by a *probabil-*ity measure $\displaystyle\mathbb{P}$ which maps every set from $\displaystyle\mathfrak{F}$ to a number between 0 and 1, with$\displaystyle\mathbb{P}(\Omega)=1$, $\displaystyle\mathbb{P}(\varnothing)=0$, and $\displaystyle\mathbb{P}(\biguplus\nolimits_{j\geq 0}A_{j})=\sum\nolimits_{j\geq 0}\mathbb{P}(A_{j})$ for any pairwise disjoint sets $\displaystyle A_{0},A_{1},\ldots\in\mathfrak{F}$. So $\displaystyle\mathbb{P}(A)$ is the probability that an event from $\displaystyle\Omega$ is in the subset $\displaystyle A$. In our setting, we use the probability space $\displaystyle((\mathbb{Z}^{r})^{\omega},\mathfrak{F}^{\mathbb{Z}^{r}},\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}})$ arising from the standard cylinder-set construction of MDP theory, cf. App. 0.B. Here, $\displaystyle(\mathbb{Z}^{r})^{\omega}$corresponds to all infinite sequences of program states and $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}$ is the probability measure induced by the program $\displaystyle\mathcal{P}$ when starting in the state $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$. For example, if $\displaystyle A\subseteq(\mathbb{Z}^{2})^{\omega}$ consists of all infinite sequences starting with $\displaystyle(5,1)$, $\displaystyle(6,1)$,$\displaystyle(7,6)$, then $\displaystyle\mathbb{P}_{(5,1)}^{\mathcal{P}_{race}}(A)=\tfrac{6}{11}\,\cdot\,\tfrac{1}{22}=\tfrac{3}{121}$. So, if one starts with $\displaystyle(5,1)$, then $\displaystyle\tfrac{3}{121}$ is the probability that the next two states are $\displaystyle(6,1)$ and $\displaystyle(7,6)$. Once a state is reached that violates the loop guard, then the probability to remain in this state is 1. Hence, if $\displaystyle B$ contains all infinite sequences starting with $\displaystyle(7,8)$, $\displaystyle(7,8)$, then $\displaystyle\mathbb{P}_{(7,8)}^{\mathcal{P}_{race}}(B)=1$. In the following, for any set of numbers $\displaystyle M$ let $\displaystyle\overline{M}=M\cup\{\infty\}$.

Definition 2 (Termination Time)

For a program $\displaystyle\mathcal{P}$ as in Def. 1, its termination time is the random variable $\displaystyle T^{\mathcal{P}}:(\mathbb{Z}^{r})^{\omega}\to\overline{\mathbb{N}}$ that maps every infinite sequence $\displaystyle\langle\vec{z}_{0},\vec{z}_{1},\ldots\rangle$ to the first index $\displaystyle j$ where $\displaystyle\vec{z}_{j}$ violates $\displaystyle\mathcal{P}$’s loop guard.

Thus, $\displaystyle T^{\mathcal{P}_{race}}(\langle(5,1),(6,1),(7,8),(7,8),\ldots\rangle)=2$ and $\displaystyle T^{\mathcal{P}_{race}}(\langle(5,1),(6,1),(5,6),\linebreak(8,6),(9,6),\ldots\rangle)=\infty$ (i.e., this sequence always satisfies $\displaystyle\mathcal{P}_{race}$’s loop guard as the $\displaystyle j$th entry is $\displaystyle(5+j,6)$ for $\displaystyle j\geq 3$). Now we can define the different notions of termination and the expected runtime of a probabilistic program. As usual, for any random variable $\displaystyle X$ on a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$, $\displaystyle\mathbb{P}(X=j)$ stands for $\displaystyle\mathbb{P}(X^{-1}(\{j\}))$. So $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}=j)$ is the probability that a sequence has termination time $\displaystyle j$. Similarly, $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}<\infty)=\sum\nolimits_{j\in\mathbb{N}}\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}=j)$. The expected value $\displaystyle\mathbb{E}(X)$ of a random variable $\displaystyle X:\Omega\to\overline{\mathbb{N}}$ for a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ is the weighted average under the probability measure $\displaystyle\mathbb{P}$, i.e., $\displaystyle\mathbb{E}(X)=\sum\nolimits_{j\in\overline{\mathbb{N}}}\;j\cdot\mathbb{P}(X=j)$, where $\displaystyle\infty\cdot 0=0$ and $\displaystyle\infty\cdot u=\infty$ for all $\displaystyle u\in\mathbb{N}_{>0}$.

Definition 3 (Termination and Expected Runtime)

A program $\displaystyle\mathcal{P}$ as in Def. 1 is almost surely terminating (AST) if $\displaystyle\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}(T^{\mathcal{P}}\!\!<\infty)=1$ for any initial value $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$. For any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, its expected runtime $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}$ (i.e., the expected number of loop iterations) is defined as the expected value of the random variable $\displaystyle T^{\mathcal{P}}$ under the probability measure $\displaystyle\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}$, i.e., $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=\mathbb{E}^{\mathcal{P}}_{\vec{x}_{0}}\left(T^{\mathcal{P}}\right)=\linebreak\sum\nolimits_{j\in\mathbb{N}}\;j\cdot\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\!\!=\!j)$ if $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\!\!<\!\infty)=1$, and $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}\!=\mathbb{E}^{\mathcal{P}}_{\vec{x}_{0}}\left(T^{\mathcal{P}}\right)=\infty$ otherwise.

The program $\displaystyle\mathcal{P}$ is positively almost surely terminating (PAST) if for any initial value $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, the expected runtime of $\displaystyle\mathcal{P}$ is finite, i.e., if $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=\mathbb{E}^{\mathcal{P}}_{\vec{x}_{0}}\left(T^{\mathcal{P}}\right)<\infty$.

Example 2 (Expected Runtime for $\displaystyle\mathcal{P}_{race}$)

By the observations in Sect. 4 we will infer that $\displaystyle\tfrac{2}{3}\cdot(t-h+1)\leq rt_{(t,h)}^{\mathcal{P}_{race}}\leq\tfrac{2}{3}\cdot(t-h+1)+\tfrac{16}{3}$ holds whenever $\displaystyle t-h>-1$, cf. Ex. 7. So the expected number of steps until termination is finite (and linear in the input variables) and thus, $\displaystyle\mathcal{P}_{race}$ is PAST. The algorithm in Sect. 5 will even be able to compute $\displaystyle rt_{(t,h)}^{\mathcal{P}_{race}}$ exactly, cf. LABEL:ExactExpected_Runtime_of_Tortoise_and_Hare.

If the initial values $\displaystyle\vec{x}_{0}$ violate the loop guard, then the runtime is trivially 0.

Corollary 1 (Expected Runtime for Violating Initial Values)

For any program $\displaystyle\mathcal{P}$ as in Def. 1 and any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$ with $\displaystyle\vec{a}\bullet\vec{x}_{0}\leq b$, we have $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}=0$.

To obtain our results, we use an alternative, well-known characterization of the expected runtime, cf. e.g., [25, 4, 34, 26, 27, 16, 9, 24, 32]. To this end, we search for the smallest (or “least”) solution of the recurrence equation that describes the runtime of the program as 1 plus the sum of the runtimes in the next loop iteration, multiplied with the corresponding probabilities. Here, functions are compared pointwise, i.e., for $\displaystyle f,g:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq_{0}}}$ we have $\displaystyle f\leq g$ if $\displaystyle f(\vec{x})\leq g(\vec{x})$ holds for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$. So we search for the smallest function $\displaystyle f:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq 0}}$ that satisfies

[TABLE]

Equivalently, we can search for the least fixpoint of the “expected runtime trans-former” $\displaystyle\mathcal{L}^{\mathcal{P}}$ which transforms the left-hand side of (1) into its right-hand side.

Definition 4 ($\displaystyle\mathcal{L}^{\mathcal{P}}$, cf. [32])

For $\displaystyle\mathcal{P}$ as in Def. 1, we define the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}\!:(\mathbb{Z}^{r}\!\to\overline{\mathbb{R}_{\geq 0}})\to(\mathbb{Z}^{r}\!\to\overline{\mathbb{R}_{\geq 0}})$, where for any $\displaystyle f\!:\mathbb{Z}^{r}\!\to\overline{\mathbb{R}_{\geq 0}}$:

[TABLE]

Example 3 (Expected Runtime Transformer for $\displaystyle\mathcal{P}_{race}$)

For $\displaystyle\mathcal{P}_{race}$ from Ex. 1, $\displaystyle\mathcal{L}^{\mathcal{P}_{race}}$ maps any function $\displaystyle f:\mathbb{Z}^{2}\to\overline{\mathbb{R}_{\geq 0}}$ to $\displaystyle\mathcal{L}^{\mathcal{P}_{race}}(f)$, where $\displaystyle\mathcal{L}^{\mathcal{P}_{race}}(f)(t,h)=$

[TABLE]

Thm. 2.1 recapitulates that the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{P}}$ indeed yields an equivalent characterization of the expected runtime. In the following, let $\displaystyle\mathfrak{0}:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq 0}}$ be the function with $\displaystyle\mathfrak{0}(\vec{x})=0$ for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$.

Theorem 2.1 (Connection Between Expected Runtime and Least Fixpoint of

$\displaystyle\mathcal{L}^{\mathcal{P}}$, cf. [32])

For any $\displaystyle\mathcal{P}$ as in Def. 1, the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ is continuous. Thus, it has a least fixpoint $\displaystyle\mathrm{lfp}(\mathcal{L}^{P}):\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq_{0}}}$ with $\displaystyle\mathrm{lfp}(\mathcal{L}^{\mathcal{P}})=\sup\{\mathfrak{0},\mathcal{L}^{\mathcal{P}}(\mathfrak{0}),(\mathcal{L}^{\mathcal{P}})^{2}(\mathfrak{0}),\ldots\}$. Moreover, the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{P}}$ is the expected runtime of $\displaystyle\mathcal{P}$, i.e., for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, we have $\displaystyle\mathrm{lfp}(\mathcal{L}^{\mathcal{P}})(\vec{x}_{0})=rt^{\mathcal{P}}_{\vec{x}_{0}}$.

So the expected runtime $\displaystyle rt^{\mathcal{P}_{race}}_{(t,h)}$ can also be characterized as the smallest function $\displaystyle f\!:\mathbb{Z}^{2}\!\to\overline{\mathbb{R}_{\geq 0}}$ satisfying $\displaystyle f(t,h)\!=\!\eqref{rhs of ert example}$, i.e., as the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{P}_{race}}$.

3 Expected Runtime of Programs with Direct Termination

We start with stating a decidability result for the case where for all $\displaystyle\vec{x}$ with $\displaystyle\vec{a}\bullet\vec{x}>b$, the probability $\displaystyle p^{\prime}(\vec{x})$ for direct termination is at least $\displaystyle p^{\prime}$ for some $\displaystyle p^{\prime}>0$. Intuitively, these programs have a termination time whose distribution is closely related to the geometric distribution with parameter $\displaystyle p^{\prime}$ (which has expected value $\displaystyle\tfrac{1}{p^{\prime}}$). By using the alternative characterization of $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}$ from Thm. 2.1, one obtains that such programs are always PAST and their expected runtime is indeed bounded by the constant $\displaystyle\tfrac{1}{p^{\prime}}$. This result will be used in Sect. 5 when computing the exact expected runtime of such programs. The more involved case where $\displaystyle p^{\prime}(\vec{x})=0$ is considered in Sect. 4.

Theorem 3.1 (PAST and Expected Runtime for Programs With Direct Termination)

Let $\displaystyle\mathcal{P}$ be a program as in Def. 1 where there is a $\displaystyle p^{\prime}>0$ such that $\displaystyle p^{\prime}(\vec{x})\geq p^{\prime}$ for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$ with $\displaystyle\vec{a}\bullet\vec{x}>b$. Then $\displaystyle\mathcal{P}$ is PAST and its expected runtime is at most $\displaystyle\tfrac{1}{p^{\prime}}$, i.e., $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}\leq\tfrac{1}{p^{\prime}}$ if $\displaystyle\vec{a}\bullet\vec{x}_{0}>b$, and $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}=0$ if $\displaystyle\vec{a}\bullet\vec{x}_{0}\leq b$.

Example 4 (Ex. 1

with Direct Termination)

Consider the variant $\displaystyle\mathcal{P}_{direct}$ of $\displaystyle\mathcal{P}_{race}$ on the right, where in each iteration, the hare either does nothing with probability $\displaystyle\tfrac{9}{10}$ or one directly reaches a configuration where the hare is ahead of the tortoise. By Thm. 3.1 the program is PAST and its expected runtime is at most $\displaystyle\tfrac{1}{\frac{1}{10}}=10$, i.e., independent of the initial state it takes at most 10 loop iterations on average. In Sect. 5 it will turn out that 10 is indeed the exact expected runtime, cf. Ex. 13.

4 Expected Runtimes of Constant Probability Programs

Now we present a very simple decision procedure for termination of CP programs (Sect. 4.2) and show how to infer their asymptotic expected runtimes (Sect. 4.3). This will be needed for the computation of exact expected runtimes in Sect. 5.

4.1 Reduction to Random Walk Programs

As a first step, we show that we can restrict ourselves to random walk programs, i.e., programs with a single program variable $\displaystyle x$ and the loop condition $\displaystyle x>0$.

Definition 5 (Random Walk Program). A CP program $\displaystyle\mathcal{P}$ is called a random walk program if there exist $\displaystyle m,k\in\mathbb{N}$ and $\displaystyle d\in\mathbb{Z}$ with $\displaystyle d\leq 0$ such that $\displaystyle\mathcal{P}\!$ has the form on the right. Here, we require that $\displaystyle m>0$ implies $\displaystyle p_{m}>0$ and that $\displaystyle k>0$ implies $\displaystyle p_{-k}>0$.

Def. 6 shows how to transform any CP program as in Def. 1 into a random walk program. The idea is to replace the tuple $\displaystyle\vec{x}$ by a single variable $\displaystyle x$ that stands for $\displaystyle\vec{a}\bullet\vec{x}-b$. Thus, the loop condition $\displaystyle\vec{a}\bullet\vec{x}>b$ now becomes $\displaystyle x>0$. Moreover, a change from $\displaystyle\vec{x}$ to $\displaystyle\vec{x}+\vec{c}_{j}$ now becomes a change from $\displaystyle x$ to $\displaystyle x+\vec{a}\bullet\vec{c}_{j}$.

Definition 6 (Transforming CP Programs to Random Walk Programs). Let $\displaystyle\mathcal{P}$ be the CP program on the left with $\displaystyle\vec{x}=(x_{1},\ldots,x_{r})$ and $\displaystyle\vec{a}\bullet\vec{d}\leq b$. Let $\displaystyle\mathit{rdw}_{\mathcal{P}}$ denote the affine map $\displaystyle\mathit{rdw}_{\mathcal{P}}\!:\mathbb{Z}^{r}\!\!\to\mathbb{Z}$ with $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z})=\vec{a}\bullet\vec{z}-b$ for

all $\displaystyle\vec{z}\in\mathbb{Z}^{r}$. Thus, $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{d})\leq 0$. Let $\displaystyle k_{\mathcal{P}},m_{\mathcal{P}}\in\mathbb{N}$ be minimal such that   $\displaystyle-k_{\mathcal{P}}\leq\vec{a}\bullet\vec{c}_{j}\leq m_{\mathcal{P}}$   holds

for all $\displaystyle 1\leq j\leq n$. For all $\displaystyle-k_{\mathcal{P}}\leq j\leq m_{\mathcal{P}}$, we define $\displaystyle p^{\mathit{rdw}}_{j}=\sum\nolimits_{1\leq u\leq n,\;\vec{a}\bullet\vec{c}_{u}=j}p_{\vec{c}_{u}}$. This results in the random walk program $\displaystyle\mathcal{P}^{\mathit{rdw}}$ on the right.

Example 5 (Transforming $\displaystyle\mathcal{P}_{race}$)

For the program $\displaystyle\mathcal{P}_{race}$

of Ex. 1, the mapping $\displaystyle\mathit{rdw}_{\mathcal{P}_{race}}:\mathbb{Z}^{2}\to\mathbb{Z}$ is $\displaystyle\mathit{rdw}_{\mathcal{P}_{race}}(t,h)=(1,-1)\bullet(t,h)+1=t-h+1$. Hence we obtain the random walk program $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ on the right, where $\displaystyle x=\mathit{rdw}_{\mathcal{P}_{race}}(t,h)$ represents the distance between the tortoise and the hare.

Approaches based on supermartingales (e.g., [5, 11, 14, 18, 13, 1]) use mappings similar to $\displaystyle\mathit{rdw}_{\mathcal{P}}$ in order to infer a real-valued term which over-approximates the expected runtime. However, in the following (non-trivial) theorem we show that our transformation is not only an over- or under-approximation, but the termination behavior and the expected runtime of $\displaystyle\mathcal{P}$ and $\displaystyle\mathcal{P}^{\mathit{rdw}}$ are identical.

Theorem 4.1 (Transformation Preserves Termination & Expected Runtime)

Let $\displaystyle\mathcal{P}$ be a CP program as in Def. 1. Then the termination times $\displaystyle T^{\mathcal{P}}\!$ and $\displaystyle T^{\mathcal{P}^{\mathit{rdw}}}\!\!\!\!$ are identically distributed w.r.t. $\displaystyle\mathit{rdw}_{\mathcal{P}}$, i.e., for all $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$ with $\displaystyle x_{0}=\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})$ and all $\displaystyle j\!\in\!\overline{\mathbb{N}}$ we have $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\!\!\!=\!j)=\mathbb{P}^{\mathcal{P}^{\mathit{rdw}}}_{x_{0}}(T^{\mathcal{P}^{\mathit{rdw}}}\!\!\!=\!j)$. So in particular, $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\!\!<\!\!\infty)\!=\mathbb{P}^{\mathcal{P}^{\mathit{rdw}}}_{x_{0}}(T^{\mathcal{P}^{\mathit{rdw}}}\!\!\!<\!\!\infty)$ and $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}\!=\!\mathbb{E}^{\mathcal{P}}_{\vec{x}_{0}}(T^{\mathcal{P}})\!=\!\mathbb{E}^{\mathcal{P}^{\mathit{rdw}}}_{x_{0}}(T^{\mathcal{P}^{\mathit{rdw}}})\!=\!rt_{x_{0}}^{\mathcal{P}^{\mathit{rdw}}}$. Thus, the expected runtimes of $\displaystyle\mathcal{P}$ on the input $\displaystyle\vec{x}_{0}$ and of $\displaystyle\mathcal{P}^{\mathit{rdw}}$ on $\displaystyle x_{0}$ coincide.

The following definition identifies pathological programs that can be disregarded.

Definition 7 (Trivial Program)

Let $\displaystyle\mathcal{P}$ be a CP pro-

gram as in Def. 1. We call $\displaystyle\mathcal{P}$ trivial if $\displaystyle\vec{a}=\vec{0}=(0,0,\ldots,0)$ or if $\displaystyle\mathcal{P}^{\mathit{rdw}}$ is the program on the right.

Note that a random walk program $\displaystyle\mathcal{P}$ is trivial iff it has the form $\displaystyle\texttt{while}(x\!>\!0)\{x=x\;\;[1];\}$, since $\displaystyle\mathcal{P}\!=\!\mathcal{P}^{\mathit{rdw}}$ holds for random walk programs $\displaystyle\mathcal{P}$. From now on, we will exclude trivial programs $\displaystyle\mathcal{P}$ as their termination behavior is obvious: for inputs $\displaystyle\vec{x}_{0}$ that satisfy the loop condition $\displaystyle\vec{a}\bullet\vec{x}_{0}>b$, the program never terminates (i.e., $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=\infty$) and for inputs $\displaystyle\vec{x}_{0}$ with $\displaystyle\vec{a}\bullet\vec{x}_{0}\leq b$ we have $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=0$. Note that if $\displaystyle\vec{a}=\vec{0}$, then the termination behavior just depends on $\displaystyle b$: if $\displaystyle b<0$, then $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=\infty$ for all $\displaystyle\vec{x}_{0}$ and if $\displaystyle b\geq 0$, then $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=0$ for all $\displaystyle\vec{x}_{0}$.

4.2 Deciding Termination

We now present a simple decision procedure for (P)AST of random walk programs $\displaystyle\mathcal{P}$. By the results of Sect. 4.1, this also yields a decision procedure for arbitrary CP programs. If $\displaystyle p^{\prime}>0$, then Thm. 3.1 already shows that $\displaystyle\mathcal{P}$ is PAST and its expected runtime is bounded by the constant $\displaystyle\tfrac{1}{p^{\prime}}$. Thus, in the rest of Sect. 4 we regard random walk programs without direct termination, i.e., $\displaystyle p^{\prime}=0$.

Def. 8 introduces the drift of a random walk program, i.e., the expected value of the change of the program variable in one loop iteration, cf. [5].

Definition 8 (Drift)

Let $\displaystyle\mathcal{P}$ be a random walk program $\displaystyle\mathcal{P}$ as in Def. 5. Then its drift is $\displaystyle\mu_{\mathcal{P}}=\sum\nolimits_{-k\leq j\leq m}j\cdot p_{j}$.

Thm. 4.2 shows that to decide (P)AST, one just has to compute the drift.

Theorem 4.2 (Decision Procedure for (P)AST of Random Walk Programs)

Let $\displaystyle\mathcal{P}$ be a non-trivial random walk program without direct termination.

1. $\displaystyle\bullet$

If $\displaystyle\mu_{\mathcal{P}}>0$, then the program is not AST. 2. $\displaystyle\bullet$

If $\displaystyle\mu_{\mathcal{P}}=0$, then the program is AST but not PAST. 3. $\displaystyle\bullet$

If $\displaystyle\mu_{\mathcal{P}}<0$, then the program is PAST.

Example 6 ($\displaystyle\mathcal{P}_{race}$ is PAST)

The drift of $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ in Ex. 5 is $\displaystyle\mu_{\mathcal{P}^{\mathit{rdw}}_{race}}=1\cdot\tfrac{6}{11}+\tfrac{1}{22}\cdot\sum\nolimits_{-9\leq j\leq 0}j=-\tfrac{3}{2}<0$. So on average the distance $\displaystyle x$ between the tortoise and the hare decreases in each loop iteration. Hence by Thm. 4.2, $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ is PAST and the following Cor. 2 implies that $\displaystyle\mathcal{P}_{race}$ is PAST as well.

Corollary 2 (Decision Procedure for (P)AST of CP programs)

For a non-trivial CP program $\displaystyle\mathcal{P}$, $\displaystyle\mathcal{P}$ is (P)AST iff $\displaystyle\mathcal{P}^{\mathit{rdw}}$ is (P)AST. Hence, Thm. 4.1 and 4.2 yield a decision procedure for AST and PAST of CP programs.

In the appendix, we show that Thm. 4.2 follows from classical results on random walks [33]. Alternatively, Thm. 4.2 could also be proved by combining several recent results on probabilistic programs: The approach of [28] could be used to show that $\displaystyle\mu_{\mathcal{P}}=0$ implies AST. Moreover, one could prove that $\displaystyle\mu_{\mathcal{P}}<0$ implies PAST by showing that $\displaystyle x$ is a ranking supermartingale of the program [5, 11, 14, 18]. That the program is not PAST if $\displaystyle\mu_{\mathcal{P}}\geq 0$ and not AST if $\displaystyle\mu_{\mathcal{P}}>0$ could be proved by showing that $\displaystyle-x$ is a $\displaystyle\mu_{\mathcal{P}}$-repulsing supermartingale [13].

While the proof of Thm. 4.2 is based on known results, the formulation of Thm. 4.2 shows that there is an extremely simple decision procedure for (P)AST of CP programs, i.e., checking the sign of the drift is much simpler than applying existing (general) techniques for termination analysis of probabilistic programs.

4.3 Computing Asymptotic Expected Runtimes

It turns out that for random walk programs (and thus by Thm. 4.1, also for CP programs), one can not only decide termination, but one can also infer tight bounds on the expected runtime. Thm. 4.3 shows that the computation of the bounds is again very simple.

Theorem 4.3 (Bounds on the Expected Runtime of CP

Programs)

Let $\displaystyle\mathcal{P}$ be a non-trivial CP program as in Def. 1 without direct termination which is PAST (i.e., $\displaystyle\mu_{\mathcal{P}^{\mathit{rdw}}}<0$). Moreover, let $\displaystyle k_{\mathcal{P}}$ be obtained according to the transformation from Def. 6. If $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})\leq 0$, then $\displaystyle rt_{\vec{x}_{0}}^{\mathcal{P}}=0$. If $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})>0$, then $\displaystyle\mathcal{P}$’s expected runtime is asymptotically linear and we have

[TABLE]

Example 7 (Bounds on the Runtime of $\displaystyle\mathcal{P}_{race}$)

In Ex. 6 we saw that the program $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ from Ex. 5 is PAST as it has the drift $\displaystyle\mu_{\mathcal{P}^{\mathit{rdw}}_{race}}=-\tfrac{3}{2}<0$. Note that here $\displaystyle k=9$. Hence by Thm. 4.3 we get that whenever $\displaystyle\mathit{rdw}_{\mathcal{P}_{race}}(t,h)=t-h+1$ is positive, the expected runtime $\displaystyle rt^{\mathcal{P}_{race}}_{(t,h)}$ is between $\displaystyle-\tfrac{1}{\mu_{\mathcal{P}^{\mathit{rdw}}_{race}}}\cdot\mathit{rdw}_{\mathcal{P}_{race}}(t,h)=\tfrac{2}{3}\cdot(t-h+1)$ and $\displaystyle-\tfrac{1}{\mu_{\mathcal{P}^{\mathit{rdw}}_{race}}}\cdot\mathit{rdw}_{\mathcal{P}_{race}}(t,h)+\tfrac{1-k}{\mu_{\mathcal{P}^{\mathit{rdw}}_{race}}}=\tfrac{2}{3}\cdot(t-h+1)+\tfrac{16}{3}$.The same upper bound $\displaystyle\tfrac{2}{3}\cdot(t-h+1)+\tfrac{16}{3}$ was inferred in [30] by an incomplete technique based on several inference rules and linear programming solvers. In contrast, Thm. 4.3 allows us to read off such bounds directly from the program.

Our proof of Thm. 4.3 in the appendix again uses the connection to random walks and shows that the classical Lemma of Wald [21, Lemma 10.2(9)] directly yields both the upper and the lower bound for the expected runtime. Alternatively, the upper bound in Thm. 4.3 could also be proved by considering that $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})+(1-k_{\mathcal{P}})$ is a ranking supermartingale [5, 11, 14, 18, 1] whose expected decrease in each loop iteration is $\displaystyle\mu_{\mathcal{P}}$. The lower bound could also be inferred by considering the difference-bounded submartingale $\displaystyle-\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})$ [20, 8].

5 Computing Exact Expected Runtimes

While Thm. 3.1 and 4.3 state how to deduce the asymptotic expected runtime, we now show that based on these results one can compute the runtime of CP programs exactly. In general, whenever it is possible, then inferring the exact runtimes of programs is preferable to asymptotic runtimes which ignore the “coefficients” of the runtime.

Again, we first consider random walk programs and generalize our technique to CP programs using Thm. 4.1 afterwards. Throughout Sect. 5, for any random walk program $\displaystyle\mathcal{P}$ as in Def. 5, we require that $\displaystyle\mathcal{P}$ is PAST, i.e., that $\displaystyle p^{\prime}>0$ (cf. Thm. 3.1) or that the drift $\displaystyle\mu_{\mathcal{P}}$ is negative if $\displaystyle p^{\prime}=0$ (cf. Thm. 4.2). Note that whenever $\displaystyle k=0$ and $\displaystyle\mathcal{P}$ is PAST, then $\displaystyle p^{\prime}>0$.111If $\displaystyle p^{\prime}=0$ and $\displaystyle k=0$ then $\displaystyle\mu_{\mathcal{P}}\geq 0$.

To compute $\displaystyle\mathcal{P}$’s expected runtime exactly, we use its characterization as the least fixpoint of the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ (cf. Thm. 2.1), i.e., $\displaystyle rt^{\mathcal{P}}_{x}$ is the smallest function $\displaystyle f:\mathbb{Z}\to\overline{\mathbb{R}_{\geq 0}}$ satisfying the constraint

[TABLE]

cf. 1. Since $\displaystyle\mathcal{P}$ is PAST, $\displaystyle f$ never returns $\displaystyle\infty$, i.e., $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$. Note that the smallest function $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ that satisfies (3) also satisfies

[TABLE]

Therefore, as $\displaystyle d\leq 0$, the constraint (3) can be simplified to

[TABLE]

In Sect. 5.1 we recapitulate how to compute all solutions of such inhomogeneous recurrence equations (cf., e.g., [15, Ch. 2]). However, to compute $\displaystyle rt^{\mathcal{P}}_{x}$, the challenge is to find the smallest solution $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ of the equation (5). Therefore, in Sect. 5.2 we will exploit the knowledge gained in Thm. 3.1 and 4.3 to show that there is only a single function $\displaystyle f$ that satisfies both (4) and (5) and is bounded by a constant (if $\displaystyle p^{\prime}>0$, cf. Thm. 3.1) resp. by a linear function (if $\displaystyle p^{\prime}=0$, cf. Thm. 4.3). This observation then allows us to compute $\displaystyle rt^{\mathcal{P}}_{x}$ exactly. So the crucial prerequisites for this result are Thm. 2.1 (which characterizes the expected runtime as the smallest solution of the equation (5)), Thm. 4.2 (which allows the restriction to negative drift if $\displaystyle p^{\prime}=0$), and in particular Thm. 3.1 and 4.3 (since LABEL:sec:smallestsolution will show that the results of Thm. 3.1 and 4.3 on the asymptotic runtime can be translated into suitable conditions on the solutions of (5)).

5.1 Finding All Solutions of the Recurrence Equation

Example 8 (Modification of $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$)

To illustrate our ap-

proach, we use a modified version of $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ from Ex. 5 to ease readability. In Sect. 6, we will consider the original program $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ resp. $\displaystyle\mathcal{P}_{race}$ from Ex. 5 resp. Ex. 1 again and show its exact expected runtime inferred by the implementation of our approach. In the modified program $\displaystyle\mathcal{P}^{mod}_{race}$ on the right, the distance between the tortoise and the hare still increases with probability $\displaystyle\tfrac{6}{11}$, but the probability of decreasing by more than two is distributed to the cases where it stays the same and where it decreases by two. We have $\displaystyle p^{\prime}=0$ and the drift is $\displaystyle\mu_{\mathcal{P}^{mod}_{race}}=1\cdot\tfrac{6}{11}+0\cdot\tfrac{1}{11}-1\cdot\tfrac{1}{22}-2\cdot\tfrac{7}{22}=-\tfrac{3}{22}<0$. So by Thm. 4.2, $\displaystyle\mathcal{P}^{mod}_{race}$ is PAST. By Thm. 2.1, $\displaystyle rt^{\mathcal{P}^{mod}_{race}}_{x}$ is the smallest function $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ satisfying

[TABLE]

Instead of searching for the smallest $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ satisfying (5), we first calculate the set of all functions $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ that satisfy (5), i.e., we also consider functions returning negative or complex numbers. Clearly, 5 is equivalent to

[TABLE]

The set of solutions on $\displaystyle\mathbb{Z}\to\mathbb{C}$ of this linear, inhomogeneous recurrence equation is an affine space which can be written as an arbitrary particular solution of the inhomogeneous equation plus any linear combination of $\displaystyle k+m$ linearly independent solutions of the corresponding homogeneous recurrence equation.

We start with computing a solution to the inhomogeneous equation 7. To this end, we use the bounds for $\displaystyle rt^{\mathcal{P}}_{x}$ from Thm. 3.1 and 4.3 (where we take the upper bound $\displaystyle\tfrac{1}{p^{\prime}}$ if $\displaystyle p^{\prime}>0$ and the lower bound $\displaystyle-\tfrac{1}{\mu_{\mathcal{P}}}\cdot x$ if $\displaystyle p^{\prime}=0$). So we define

[TABLE]

One easily shows that if $\displaystyle p^{\prime}>0$, then $\displaystyle f(x)=C_{const}$ is a solution of the inhomogeneous recurrence equation 7 and if $\displaystyle p^{\prime}=0$, then $\displaystyle f(x)=C_{lin}\cdot x$ solves 7.

Example 9 (Ex. 8 cont.)

In the program $\displaystyle\mathcal{P}^{mod}_{race}$ of Ex. 8, we have $\displaystyle p^{\prime}=0$ and $\displaystyle\mu_{\mathcal{P}^{mod}_{race}}=-\tfrac{3}{22}$. Hence $\displaystyle C_{lin}=\tfrac{22}{3}$ and $\displaystyle C_{lin}\cdot x$ is a solution of 6.

After having determined one particular solution of the inhomogeneous recurrence equation 7, now we compute the solutions of the homogeneous recurrence equation which results from 7 by replacing the add-on “+ 1” with 0. To this end, we consider the corresponding characteristic polynomial $\displaystyle\chi_{\mathcal{P}}$:222If $\displaystyle m=0$ then $\displaystyle\chi_{\mathcal{P}}(\lambda)=(p_{0}-1)\cdot\lambda^{k}+p_{-1}\cdot\lambda^{k-1}+\ldots+p_{-k}$, and if $\displaystyle k=0$ then $\displaystyle\chi_{\mathcal{P}}(\lambda)=p_{m}\cdot\lambda^{m}+\ldots+p_{1}\cdot\lambda+(p_{0}-1)$. Note that $\displaystyle p_{0}\neq 1$ since $\displaystyle\mathcal{P}$ is PAST and in Def. 5 we required that $\displaystyle m>0$ implies $\displaystyle p_{m}>0$ and $\displaystyle k>0$ implies $\displaystyle p_{-k}>0$. Hence, the characteristic polynomial has exactly the degree $\displaystyle k+m$, even if $\displaystyle m=0$ or $\displaystyle k=0$.

[TABLE]

Let $\displaystyle\lambda_{1},\ldots,\lambda_{c}$ denote the pairwise different (possibly complex) roots of the characteristic polynomial $\displaystyle\chi_{\mathcal{P}}$. For all $\displaystyle 1\leq j\leq c$, let $\displaystyle v_{j}\in\mathbb{N}\setminus\{0\}$ be the multiplicity of the root $\displaystyle\lambda_{j}$. Thus, we have $\displaystyle v_{1}+\ldots+v_{c}=k+m$.

Then we obtain the following $\displaystyle k+m$ linearly independent solutions of the homogeneous recurrence equation resulting from (7):

[TABLE]

So $\displaystyle f\!:\!\mathbb{Z}\!\to\!\mathbb{C}$ is a solution of 5 (resp. (7)) iff there exist coefficients $\displaystyle a_{j,u}\!\in\!\mathbb{C}$ with

[TABLE]

where $\displaystyle C(x)=C_{const}=\tfrac{1}{p^{\prime}}$ if $\displaystyle p^{\prime}>0$ and $\displaystyle C(x)=C_{lin}\cdot x=-\tfrac{1}{\mu_{\mathcal{P}}}\cdot x$ if $\displaystyle p^{\prime}=0$. The reason for requiring (9) for all $\displaystyle x>-k$ is that $\displaystyle-k+1$ is the smallest argument where $\displaystyle f$’s value is taken into account in 5.

Example 10 (Ex. 9 cont.)

The characteristic polynomial for the program $\displaystyle\mathcal{P}^{mod}_{race}$ of Ex. 8 has the degree $\displaystyle k+m=2+1=3$ and is given by

[TABLE]

Its roots are $\displaystyle\lambda_{1}=1$, $\displaystyle\lambda_{2}=-\tfrac{1}{2}$, and $\displaystyle\lambda_{3}=\tfrac{7}{6}$. So here, all roots are real numbers and they all have the multiplicity $\displaystyle 1$. Hence, three linearly independent solutions of the homogeneous part of 6 are the functions $\displaystyle 1^{x}=1$, $\displaystyle(-\tfrac{1}{2})^{x}$, and $\displaystyle(\tfrac{7}{6})^{x}$. Therefore, a function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ satisfies 6 iff there are $\displaystyle a_{1},a_{2},a_{3}\in\mathbb{C}$ such that

[TABLE]

5.2 Finding the Smallest Solution of the Recurrence Equation

In Sect. 5.1, we recapitulated the standard approach for solving inhomogeneous recurrence equations which shows that any function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ that satisfies the constraint (5) is of the form (9). Now we will present a novel technique to compute $\displaystyle rt^{\mathcal{P}}_{x}$, i.e., the smallest non-negative solution $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ of 5. By Thm. 3.1 and 4.3, this function $\displaystyle f$ is bounded by a constant (if $\displaystyle p^{\prime}>0$) resp. linear (if $\displaystyle p^{\prime}=0$). So, when representing $\displaystyle f$ in the form (9), we must have $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$. The following lemma shows how many roots with absolute value less or equal to 1 there are (i.e., these are the only roots that we have to consider). It is proved using Rouché’s Theorem which allows us to infer the number of roots whose absolute value is below a certain bound. Note that $\displaystyle 1$ is a root of the characteristic polynomial iff $\displaystyle p^{\prime}=0$, since $\displaystyle\sum\nolimits_{-k\leq j\leq m}p_{j}=1-p^{\prime}$.

Lemma 1 (Number of Roots With Absolute Value $\displaystyle\leq 1$)

Let $\displaystyle\mathcal{P}$ be a random walk program as in Def. 5 that is PAST. Then the characteristic polynomial $\displaystyle\chi_{\mathcal{P}}$ has $\displaystyle k$ roots $\displaystyle\lambda\in\mathbb{C}$ (counted with multiplicity) with $\displaystyle|\lambda|\leq 1$.

Example 11 (Ex. 10 cont.)

In $\displaystyle\mathcal{P}^{mod}_{race}$ of Ex. 8 we have $\displaystyle k=2$. So by LABEL:Numberof_Roots_Lemma, $\displaystyle\chi_{\mathcal{P}}$ has exactly two roots with absolute value $\displaystyle\leq 1$. Indeed, the roots of $\displaystyle\chi_{\mathcal{P}}$ are $\displaystyle\lambda_{1}=1$, $\displaystyle\lambda_{2}=-\tfrac{1}{2}$, and $\displaystyle\lambda_{3}=\tfrac{7}{6}$, cf. Ex. 10. So $\displaystyle|\lambda_{3}|>1$, but $\displaystyle|\lambda_{1}|\leq 1$ and $\displaystyle|\lambda_{2}|\leq 1$.

Based on Lemma 1, the following lemma shows that when imposing the restriction that $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$, then there is only a single function of the form (9) that also satisfies the constraint (4). Hence, this must be the function that we are searching for, because the desired smallest solution $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ of (5) also satisfies (4).

Lemma 2 (Unique Solution of (4) and (5) when

Disregarding Roots With Absolute Value $\displaystyle>1$)

Let $\displaystyle\mathcal{P}$ be a random walk program as in Def. 5 that is PAST. Then there is exactly one function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ which satisfies both (4) and (5) (thus, it has the form (9)) and has $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$.

The main theorem of Sect. 5 now shows how to compute the expected runtime exactly. By Thm. 3.1 and 4.3 on the bounds for the expected runtime and by Lemma 2, we no longer have to search for the smallest function that satisfies (4) and (5), but we just search for any solution of (4) and (5) which has $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$ (because there is just a single such solution). So one only has to determine the values of the remaining $\displaystyle k$ coefficients $\displaystyle a_{j,u}$ for $\displaystyle|\lambda_{j}|\leq 1$, which can be done by exploiting that $\displaystyle f(x)$ has to satisfy both (4) for all $\displaystyle x\leq 0$ and it has to be of the form (9) for all $\displaystyle x>-k$. In other words, the function in (9) must be 0 for $\displaystyle-k+1\leq x\leq 0$.

Theorem 5.1 (Exact Expected Runtime for Random Walk Programs)

Let $\displaystyle\mathcal{P}$ be a random walk program as in Def. 5 that is PAST and let $\displaystyle\lambda_{1},\ldots,\lambda_{c}$ be the roots of its characteristic polynomial with multiplicities $\displaystyle v_{1},\ldots,v_{c}$. Moreover, let $\displaystyle C(x)=C_{const}=\tfrac{1}{p^{\prime}}$ if $\displaystyle p^{\prime}>0$ and $\displaystyle C(x)=C_{lin}\cdot x=-\tfrac{1}{\mu_{\mathcal{P}}}\cdot x$ if $\displaystyle p^{\prime}=0$. Then the expected runtime of $\displaystyle\mathcal{P}$ is $\displaystyle rt^{\mathcal{P}}_{x}=0$ for $\displaystyle x\leq 0$ and

[TABLE]

where the coefficients $\displaystyle a_{j,u}$ are the unique solution of the $\displaystyle k$ linear equations:

[TABLE]

So in the special case where $\displaystyle k=0$, we have $\displaystyle rt^{\mathcal{P}}_{x}=C(x)=C_{const}=\tfrac{1}{p^{\prime}}$ for $\displaystyle x>0$.

Thus for $\displaystyle x>0$, the expected runtime $\displaystyle rt^{\mathcal{P}}_{x}$ can be computed by summing up the bound $\displaystyle C(x)$ and an add-on $\displaystyle\sum\nolimits_{1\leq j\leq c,\;|\lambda_{j}|\leq 1}\;\sum\nolimits_{0\leq u\leq v_{j}-1}\ldots\;$ Since $\displaystyle C(x)$ is an upper bound for $\displaystyle rt^{\mathcal{P}}_{x}$ if $\displaystyle p^{\prime}>0$ and a lower bound for $\displaystyle rt^{\mathcal{P}}_{x}$ if $\displaystyle p^{\prime}=0$, this add-on is non-positive if $\displaystyle p^{\prime}>0$ and non-negative if $\displaystyle p^{\prime}=0$.

Example 12 (Ex. 11 cont.)

By Thm. 5.1, the expected runtime of the program $\displaystyle\mathcal{P}^{mod}_{race}$ from Ex. 8 is $\displaystyle rt^{\mathcal{P}^{mod}_{race}}_{x}=0$ for $\displaystyle x\leq 0$ and

[TABLE]

The coefficients $\displaystyle a_{1}$ and $\displaystyle a_{2}$ are the unique solution of the $\displaystyle k=2$ linear equations

[TABLE]

So $\displaystyle a_{1}=\tfrac{22}{9}$, $\displaystyle a_{2}=-\tfrac{22}{9}$, and hence $\displaystyle rt^{\mathcal{P}^{mod}_{race}}_{x}\;=\;\tfrac{22}{3}\cdot x+\tfrac{22}{9}-\tfrac{22}{9}\cdot(-\tfrac{1}{2})^{x}$ for $\displaystyle x>0$.

By Thm. 4.1, we can lift Thm. 5.1 to arbitrary CP programs $\displaystyle\mathcal{P}$ immediately.

Corollary 3 (Exact Expected Runtime for CP Programs)

For any CP program, its expected runtime can be computed exactly.

Note that irrespective of the degree of the characteristic polynomial, its roots can always be approximated numerically with any chosen precision. Thus, “exact computation” of the expected runtime in the corollary above means that a closed form for $\displaystyle rt^{\mathcal{P}}_{\vec{x}}$ can also be computed with any desired precision.

Example 13 (Exact Expected Runtime of $\displaystyle\mathcal{P}_{direct}$)

Reconsi-

der the program $\displaystyle\mathcal{P}_{direct}$ of Ex. 4 with the probability $\displaystyle p^{\prime}=\tfrac{1}{10}$ for direct termination. $\displaystyle\mathcal{P}_{direct}$ is PAST and its expected runtime is at most $\displaystyle\tfrac{1}{p^{\prime}}=10$, cf. Ex. 4. The random walk program $\displaystyle\mathcal{P}_{direct}^{\mathit{rdw}}$ on the right is obtained by the transformation of Def. 0Univariate Transformation. As $\displaystyle k=0$, by Thm. 5.1 we obtain $\displaystyle rt^{\mathcal{P}_{direct}^{\mathit{rdw}}}_{x}=\tfrac{1}{p^{\prime}}=10$ for $\displaystyle x>0$.By Thm. 4.1, this implies $\displaystyle rt^{\mathcal{P}_{direct}}_{(t,h)}=rt^{\mathcal{P}_{direct}^{\mathit{rdw}}}_{\mathit{rdw}_{\mathcal{P}_{direct}}(t,h)}=10$ if $\displaystyle\mathit{rdw}_{\mathcal{P}_{direct}}(t,h)=t-h+1>0$, i.e., 10 is indeed the exact expected runtime of $\displaystyle\mathcal{P}_{direct}$.

Note that Thm. 5.1 and 3 imply that for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, the expected runtime $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}$ of a CP program $\displaystyle\mathcal{P}$ that is PAST and has only rational probabilities $\displaystyle p_{\vec{c}_{1}},\ldots,p_{\vec{c}_{n}},p^{\prime}\in\mathbb{Q}$ is always an algebraic number. Thus, one could also compute a closed form for the exact expected runtime $\displaystyle rt^{\mathcal{P}}_{\vec{x}}$ using a representation with algebraic numbers instead of numerical approximations.

Nevertheless, Thm. 5.1 may yield a representation of $\displaystyle rt^{\mathcal{P}}_{x}$ which contains complex numbers $\displaystyle a_{j,u}$ and $\displaystyle\lambda_{j}$, although $\displaystyle rt^{\mathcal{P}}_{x}$ is always real. However, one can easily obtain a more intuitive representation of $\displaystyle rt^{\mathcal{P}}_{x}$ without complex numbers:

Since the characteristic polynomial $\displaystyle\chi_{\mathcal{P}}$ only has real coefficients, whenever $\displaystyle\chi_{\mathcal{P}}$ has a complex root $\displaystyle\lambda$ of multiplicity $\displaystyle v$, its conjugate $\displaystyle\overline{\lambda}$ is also a root of $\displaystyle\chi_{\mathcal{P}}$ with the same multiplicity $\displaystyle v$. So the pairwise different roots $\displaystyle\lambda_{1},\ldots,\lambda_{c}$ can be distinguished into pairwise different real roots $\displaystyle\lambda_{1},\ldots,\lambda_{s}$, and into pairwise different non-real complex roots $\displaystyle\lambda_{s+1},\overline{\lambda_{s+1}},\ldots,\lambda_{s+t},\overline{\lambda_{s+t}}$, where $\displaystyle c=s+2\cdot t$.

For any coefficients $\displaystyle a_{j,u},a_{j,u}^{\prime}\in\mathbb{C}$ with $\displaystyle j\in\{s+1,\ldots,s+t\}$ and $\displaystyle u\in\{0,\ldots,v_{j}-1\}$ let $\displaystyle b_{j,u}=2\cdot\mathrm{Re}(a_{j,u})\in\mathbb{R}$ and $\displaystyle b_{j,u}^{\prime}=-2\cdot\mathrm{Im}(a_{j,u})\in\mathbb{R}$. Then $\displaystyle a_{j,u}\cdot\lambda_{j}^{x}+a_{j,u}^{\prime}\cdot\overline{\lambda_{j}}^{x}\;=\;b_{j,u}\cdot\mathrm{Re}(\lambda_{j}^{x})+b_{j,u}^{\prime}\cdot\mathrm{Im}(\lambda_{j}^{x})$. Hence, by Thm. 5.1 we get the following representation of the expected runtime which only uses real numbers:

[TABLE]

To compute $\displaystyle\mathrm{Re}(\lambda_{j}^{x})$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})$, take the polar representation of the non-real roots $\displaystyle\lambda_{j}=w_{j}\cdot e^{\theta_{j}\cdot i}$. Then $\displaystyle\mathrm{Re}(\lambda_{j}^{x})=w^{x}_{j}\cdot\cos(\theta_{j}\cdot x)$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})=w^{x}_{j}\cdot\sin(\theta_{j}\cdot x)$.

Therefore, we obtain the following algorithm to deduce the exact expected runtime automatically.

6 Conclusion, Implementation, and Related Work

We presented decision procedures for termination and complexity of classes of probabilistic programs. They are based on the connection between the expected runtime of a program and the smallest solution of its corresponding recurrence equation, cf. Sect. 2. For our notion of probabilistic programs, if the probability for leaving the loop directly is at least $\displaystyle p^{\prime}$ for some $\displaystyle p^{\prime}>0$, then the program is always PAST and its expected runtime is asymptotically constant, cf. Sect. 3. In Sect. 4 we showed that a very simple decision procedure for AST and PAST of CP programs can be obtained by classical results from random walk theory and that the expected runtime is asymptotically linear if the program is PAST. Based on these results, in Sect. 5 we presented our algorithm to automatically infer a closed form for the exact expected runtime of CP programs (i.e., with arbitrarily high precision). All proofs and a collection of examples to demonstrate our algorithm can be found in the appendix.

Implementation.

We implemented Sect. 5.2 in our tool KoAT [10], which was already one of the leading tools for complexity analysis of (non-probabilistic) integer programs. The implementation is written in OCaml and uses the Python libraries MpMath [22] and SymPy [29] for solving linear equations and for finding the roots of the characteristic polynomial. In addition to the closed form for the exact expected runtime, our implementation can also compute the concrete number of expected loop iterations if the user specifies the initial values of the variables. For further details, a set of benchmarks, and to download our implementation, we refer to https://aprove-developers.github.io/recurrence/.

Example 14 (Computing the Exact Expected Runtime of $\displaystyle\mathcal{P}_{race}$ Automatically)

For the tortoise and hare program $\displaystyle\mathcal{P}_{race}$ from Ex. 1, our implementation in KoAT computes the following expected runtime within 0.49 s on an Intel Core i7-6500 with 8 GB memory (when selecting a precision of 2 decimal places):

[TABLE]

So when starting in a state with $\displaystyle t=1000$ and $\displaystyle h=0$, according to our implementation the number of expected loop iterations is $\displaystyle rt^{\mathcal{P}_{race}}_{(1000,0)}=670$.

Related Work.

Many techniques to analyze (P)AST have been developed, which mostly rely on ranking supermartingales, e.g., [5, 11, 18, 28, 1, 30, 14, 13, 20]. Indeed, several of these works (e.g., [5, 18, 1, 20]) present complete criteria for (P)AST, although (P)AST is undecidable. However, the corresponding automation of these techniques is of course incomplete. In [14] it is shown that for affine probabilistic programs, a superclass of our CP programs, the existence of a linear ranking supermartingale is decidable. However, the existence of a linear ranking supermartingale is sufficient but not necessary for PAST or an at most linear expected runtime.

Classes of programs where termination is decidable have already been studied for deterministic programs. In [35] it was shown that for a class of linear loop programs over the reals, the halting problem is decidable. This result was transferred to the rationals [6] and under certain conditions to integer programs [6, 31, 19]. Termination analysis for probabilistic programs is substantially harder than for non-probabilistic ones [23]. Nevertheless, there is some previous work on classes of probabilistic programs where termination is decidable and asymptotic bounds on the expected runtime are computable. For instance, in [7] it was shown that AST is decidable for certain stochastic games and [12] presents an automatic approach for inferring asymptotic upper bounds on the expected runtime by considering uni- and bivariate recurrence equations.

However, our algorithm is the first which computes a general formula (i.e., a closed form) for the exact expected runtime of arbitrary CP programs. To our knowledge, up to now such a formula was only known for the very restricted special case of bounded simple random walks (cf. [17]), i.e., programs of the

form on the right for some $\displaystyle 1\geq p\geq 0$ and some $\displaystyle b\in\mathbb{Z}$. Note that due to the two boundary conditions $\displaystyle x>0$ and $\displaystyle b>x$, the resulting recurrence equation for the expected runtime of the program only has a single solution $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ that also satisfies $\displaystyle f(0)=0$ and $\displaystyle f(b)=0$. Hence, standard techniques for solving recurrence equations suffice to compute this solution. In contrast, we developed an algorithm to compute the exact expected runtime of unbounded arbitrary CP programs where the loop condition only has one boundary condition $\displaystyle x>0$, i.e., $\displaystyle x$ can grow infinitely large. For that reason, here the challenge is to find an algorithm which computes the smallest solution $\displaystyle f:\mathbb{Z}\to\mathbb{R}_{\geq 0}$ of the resulting recurrence equation. We showed that this can be done using the information on the asymptotic bounds of the expected runtime from Sect. 3 and 4.

Future Work.

There are several directions for future work. In Sect. 4.1 we reduced CP programs to random walk programs. In future work, we will consider more advanced reductions in order to extend the class of probabilistic programs where termination and complexity are decidable. Moreover, we want to develop techniques to automatically over- or under-approximate the runtime of a program $\displaystyle\mathcal{P}$ by the runtimes of corresponding CP programs $\displaystyle\mathcal{P}_{1}$ and $\displaystyle\mathcal{P}_{2}$ such that $\displaystyle rt^{\mathcal{P}_{1}}_{\vec{x}}\leq rt^{\mathcal{P}}_{\vec{x}}\leq rt^{\mathcal{P}_{2}}_{\vec{x}}$ holds for all $\displaystyle\vec{x}\in\mathbb{Z}^{r}$. Furthermore, we will integrate the easy inference of runtime bounds for CP programs into existing techniques for analyzing more general probabilistic programs.

Acknowledgments

We would like to thank Nicos Georgiou and Vladislav Vysotskiy for drawing our attention to Wald’s Lemma and to the work of Frank Spitzer on random walks, and Benjamin Lucien Kaminski and Christoph Matheja for many helpful discussions. Furthermore, we thank Tom Küspert who helped with the implementation of our technique in our tool KoAT.

Appendix 0.A Case Studies

In this section, we demonstrate our approach for the computation of the exact expected runtime on further examples.

Example 15 (Example with Direct Termination and Non-Constant Exact Runtime)

As an example with $\displaystyle p^{\prime}>0$ where the exact expected runtime is not constant, consider the following program $\displaystyle\mathcal{P}$.

[TABLE]

The characteristic polynomial is $\displaystyle\chi_{\mathcal{P}}(\lambda)=\tfrac{1}{8}\cdot\lambda^{2}-\tfrac{1}{2}\cdot\lambda+\tfrac{1}{4}$. It has the $\displaystyle k+m=1+1=2$ roots $\displaystyle 2\pm\sqrt{2}$. So the only root with absolute value $\displaystyle\leq 1$ is $\displaystyle 2-\sqrt{2}$. By Thm. 5.1 we obtain $\displaystyle rt^{\mathcal{P}}_{x}=0$ for $\displaystyle x\leq 0$ and

[TABLE]

Here, $\displaystyle a_{1}$ is the unique solution of the linear equation $\displaystyle 0=8+a_{1}\cdot(2-\sqrt{2})^{0}\cdot 0^{0}=8+a_{1}$, i.e., $\displaystyle a_{1}=-8$. So for $\displaystyle x>0$ we have

[TABLE]

i.e., here the negative add-on $\displaystyle-8\cdot(2-\sqrt{2})^{x}$ is added to the upper bound 8.

Example 16 (Example with Complex Roots)

To show that complex roots are indeed possible, we apply Sect. 5.2 to the following program $\displaystyle\mathcal{P}$, where $\displaystyle p^{\prime}=0$ and $\displaystyle\mu_{\mathcal{P}}=-\tfrac{13}{30}$. Thus, $\displaystyle C_{lin}=\tfrac{30}{13}$ and $\displaystyle C(x)=\tfrac{30}{13}\cdot x$.

[TABLE]

The characteristic polynomial $\displaystyle\chi_{\mathcal{P}}(\lambda)$ has the roots 1, 3, and the two complex roots $\displaystyle\tfrac{-1\pm\sqrt{3}\,i}{5}$. Hence, the $\displaystyle k=3$ roots with absolute value $\displaystyle\leq 1$ are $\displaystyle 1$ and $\displaystyle\tfrac{-1\pm\sqrt{3}\,i}{5}$. By Thm. 5.1 we obtain the following general solution:

[TABLE]

The coefficients $\displaystyle a_{1},a_{2},a_{3}$ are determined by the three linear equations $\displaystyle 0=f(x)$ for $\displaystyle-2\leq x\leq 0$, cf. 11. They have the unique solution $\displaystyle a_{1}=\tfrac{180}{169}$, $\displaystyle a_{2}=-{\tfrac{90}{169}}-{\tfrac{2}{169}}\cdot\sqrt{3}\,i$, and $\displaystyle a_{3}=-{\tfrac{90}{169}}+{\tfrac{2}{169}}\cdot\sqrt{3}\,i$. Thus, $\displaystyle b_{2}=2\cdot\mathrm{Re}(a_{2})=-\tfrac{180}{169}$, and $\displaystyle b^{\prime}_{2}=-2\cdot\mathrm{Im}(a_{2})=\tfrac{4}{169}\cdot\sqrt{3}$. The polar representation of $\displaystyle\lambda=\tfrac{-1+\sqrt{3}\,i}{5}$ is $\displaystyle\tfrac{2}{5}\cdot e^{\tfrac{2\pi}{3}\cdot i}$. Hence, $\displaystyle\mathrm{Re}(\lambda^{x})=(\tfrac{2}{5})^{x}\cdot\cos(\tfrac{2\pi}{3}\cdot x)$ and $\displaystyle\mathrm{Im}(\lambda^{x})=(\tfrac{2}{5})^{x}\cdot\sin(\tfrac{2\pi}{3}\cdot x)$. Thus, we get $\displaystyle rt^{\mathcal{P}}_{x}=0$ for $\displaystyle x\leq 0$ and for $\displaystyle x>0$ we have

[TABLE]

Example 17 (Example with Root of Higher Multiplicity)

As an example where the characteristic polynomial has a root with multiplicity greater than 1, consider the following program $\displaystyle\mathcal{P}$.

[TABLE]

We use the approach of Sect. 5.2 to infer the exact expected runtime. Step 1 is not necessary, since we already have a random walk program.

We have $\displaystyle p^{\prime}=0$, $\displaystyle\mu_{\mathcal{P}}=-\tfrac{12}{175}$, and thus, $\displaystyle C_{lin}=\tfrac{175}{12}$. 2. 3.

The characteristic polynomial has the degree $\displaystyle k+m=3+1=4$ and is given by $\displaystyle\chi_{\mathcal{P}}(\lambda)=\tfrac{5}{21}\cdot\lambda^{4}-\tfrac{3}{7}\cdot\lambda^{3}+\tfrac{3}{35}\cdot\lambda^{2}+\tfrac{7}{75}\cdot\lambda+\tfrac{2}{175}$. It has the roots $\displaystyle\lambda_{1}=1$ with multiplicity $\displaystyle 1$, $\displaystyle\lambda_{2}=\tfrac{6}{5}$ with multiplicity $\displaystyle 1$, and $\displaystyle\lambda_{3}=-\tfrac{1}{5}$ with multiplicity $\displaystyle 2$. Hence, the three roots with absolute value $\displaystyle\leq 1$ are $\displaystyle 1$ and $\displaystyle-\tfrac{1}{5}$ with multiplicity 2. As proved in Lemma 1 we have $\displaystyle 1+2=3=k$ such roots counted with multiplicity. 3. 4.

By Thm. 5.1, the general solution is

[TABLE]

The coefficients $\displaystyle a_{1,0}$, $\displaystyle a_{2,0}$, and $\displaystyle a_{2,1}$ are determined by the following linear equations, cf. 11:

[TABLE]

They have the unique solution $\displaystyle a_{1,0}=\tfrac{175}{36}$, $\displaystyle a_{2,0}=-\tfrac{175}{36}$, and $\displaystyle a_{2,1}=-\tfrac{35}{12}$. Hence, $\displaystyle rt^{\mathcal{P}}_{x}=0$ for $\displaystyle x\leq 0$ and for $\displaystyle x>0$ we have

[TABLE]

Example 18 (Negative Binomial Loop from [28, Sect. 5.1])

Consider the following program $\displaystyle\mathcal{P}$ from [28, Sect. 5.1].

[TABLE]

The drift of this program is $\displaystyle\mu_{\mathcal{P}}=-\tfrac{1}{2}<0$ and by Thm. 4.2 we can conclude that the negative binomial loop is positive almost surely terminating. Furthermore, as $\displaystyle k=1$ and $\displaystyle m=0$ we obtain that the expected runtime $\displaystyle rt^{\mathcal{P}}_{x}$ of this program satisfies $\displaystyle 2\cdot x\leq rt^{\mathcal{P}}_{x}\leq 2\cdot x$ for all $\displaystyle x>0$ by Thm. 4.3, i.e.,

[TABLE]

So with our approach, the expected runtime of this example can be determined with clearly less effort than with the technique presented in [28]. On the other hand, the reasoning of [28] can be applied to arbitrary probabilistic programs which may even include non-determinism.

Example 19 (Symmetric Random Walk)

Consider the following program $\displaystyle\mathcal{P}$.

[TABLE]

One easily calculates the drift $\displaystyle\mu_{\mathcal{P}}=\tfrac{1}{2}-\tfrac{1}{2}=0$. So by Thm. 4.2 we immediately obtain the well-known result that this program is almost surely terminating but not positive almost surely terminating, i.e., the expected runtime is infinite.

Example 20 (Example with Irrational Runtime from [14, Ex. 5.1])

Consider the following program $\displaystyle\mathcal{P}$ which was presented in [14, Ex. 5.1] to show that expected runtimes can be irrational.

[TABLE]

Its drift is $\displaystyle\mu_{\mathcal{P}}=\tfrac{1}{2}\cdot 1+\tfrac{1}{2}\cdot(-2)=-\tfrac{1}{2}<0$, so by Thm. 4.2 this program is indeed PAST. As $\displaystyle k=2$, we obtain the following bounds on the expected runtime by Thm. 4.3 for any positive initial value $\displaystyle x>0$:

[TABLE]

The characteristic polynomial of this program is $\displaystyle\chi_{\mathcal{P}}(x)=\tfrac{1}{2}\cdot x^{3}-x^{2}+\tfrac{1}{2}$. It has the three roots $\displaystyle 1$, $\displaystyle\tfrac{1+\sqrt{5}}{2}$, and $\displaystyle\tfrac{1-\sqrt{5}}{2}$. So the $\displaystyle k=2$ roots of absolute value $\displaystyle\leq 1$ are $\displaystyle 1$ and $\displaystyle\tfrac{1-\sqrt{5}}{2}$. By Thm. 5.1, the general solution is

[TABLE]

The coefficients $\displaystyle a_{1}$ and $\displaystyle a_{2}$ are determined by the following equations:

[TABLE]

They have the unique solution $\displaystyle a_{1}=3-\sqrt{5}$ and $\displaystyle a_{2}=\sqrt{5}-3$. Hence, we infer the following exact expected runtime for $\displaystyle x>0$:

[TABLE]

So in particular, $\displaystyle rt^{\mathcal{P}}_{1}=1+\sqrt{5}$. The expected runtime obtained in [14, Ex. 5.1] is slightly different (they obtain $\displaystyle 2\cdot(5+\sqrt{5})$), because [14] counts the number of executed statements whereas we count loop iterations.

Example 21 (Example from [30, Sect. 3.1])

Consider the following program $\displaystyle\mathcal{P}$. It was used in [30, Sect. 3.1] to show how one can infer the expected runtime of a probabilistic program by solving a recurrence equation. However, the authors of [30] conclude that recurrence equations are not well suited for runtime analyses, while our paper shows that for CP programs, an automated runtime analysis based on recurrence equations is feasible.

[TABLE]

Its drift is $\displaystyle\mu_{\mathcal{P}}=\tfrac{1}{4}\cdot 1+\tfrac{3}{4}\cdot(-1)=-\tfrac{1}{2}<0$, so by Thm. 4.2 this program is indeed PAST. By Thm. 4.3, we can infer the following bounds on the expected runtime for any positive initial value $\displaystyle x>0$:

[TABLE]

Hence, in this example we can directly conclude that for any $\displaystyle x>0$ the expected runtime is $\displaystyle rt^{\mathcal{P}}_{x}=2\cdot x$, without having to solve the corresponding recurrence equation with Thm. 5.1 resp. Sect. 5.2.

Appendix 0.B Proofs for Sect. 2

We begin with introducing some auxiliary definitions that will be needed in the proofs. To define the run of a program, we use the “Kronecker-Delta” where for any $\displaystyle\vec{y},\vec{z}\in\mathbb{Z}^{r}$ with $\displaystyle\vec{y}\neq\vec{z}$ we have $\displaystyle\delta_{\vec{y},\vec{z}}=0$ and $\displaystyle\delta_{\vec{y},\vec{y}}=1$.

Definition 9 (Run of a Program)

For any program $\displaystyle\mathcal{P}$ as in Def. 1, a run is an infinite sequence $\displaystyle\left\langle\vec{z}_{0},\vec{z}_{1},\vec{z}_{2},\ldots\right\rangle\in(\mathbb{Z}^{r})^{\omega}$ and a prefix run is a finite sequence $\displaystyle\left\langle\vec{z}_{0},\vec{z}_{1},\ldots,\vec{z}_{j}\right\rangle\in(\mathbb{Z}^{r})^{j+1}$ for some $\displaystyle j\in\mathbb{N}$. For a prefix run $\displaystyle\pi$, its cylinder set $\displaystyle\mathit{Cyl}^{\mathbb{Z}^{r}}(\pi)\subseteq(\mathbb{Z}^{r})^{\omega}$ consists of all runs with prefix $\displaystyle\pi$.

For any initial value $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$ of the program variables, we define a function $\displaystyle pr^{\mathcal{P}}_{\vec{x}_{0}}$ that maps any prefix run $\displaystyle\pi$ to its probability (i.e., $\displaystyle 0\leq pr^{\mathcal{P}}_{\vec{x}_{0}}(\pi)\leq 1$). Thus, for any prefix run $\displaystyle\left\langle\vec{z}_{0},\vec{z}_{1},\ldots,\vec{z}_{j}\right\rangle$, let $\displaystyle pr^{\mathcal{P}}_{\vec{x}_{0}}(\left\langle\vec{z}_{0}\right\rangle)=\delta_{\vec{x}_{0},\vec{z}_{0}}$ and if $\displaystyle j\geq 1$, we define:

[TABLE]

Example 22 (Run in $\displaystyle\mathcal{P}_{race}$)

For $\displaystyle\mathcal{P}_{race}$ from Ex. 1 and a start configuration where the tortoise is 10 steps ahead of the hare (e.g., $\displaystyle\vec{x}_{0}=(11,1)$), the prefix run $\displaystyle\left\langle(11,1),(12,1),(13,6)\right\rangle$ has the probability $\displaystyle pr^{\mathcal{P}_{race}}_{(11,1)}\left(\left\langle(11,1),(12,1),(13,6)\right\rangle\right)=\delta_{(11,1),(11,1)}\,\cdot\,p_{(12,1)-(11,1)}(11,1)\,\cdot\,p_{(13,6)-(12,1)}(12,1)=p_{(1,0)}(11,1)\,\cdot\,p_{(1,5)}(12,1)=\tfrac{6}{11}\,\cdot\,\tfrac{1}{22}=\tfrac{3}{121}$. So we take into account whether the prefix run starts with $\displaystyle\vec{x}_{0}=(11,1)$ and multiply the probability to get from $\displaystyle\vec{x}=(11,1)$ to $\displaystyle\vec{x}=(12,1)$ with the probability to get from $\displaystyle\vec{x}=(12,1)$ to $\displaystyle\vec{x}=(13,6)$.

In our setting, we regard a measurable space $\displaystyle(\Omega,\mathfrak{F})$ where $\displaystyle\Omega$ is the set of runs $\displaystyle(\mathbb{Z}^{r})^{\omega}$ and we want to measure the probability that a run starts with a certain sequence $\displaystyle\pi$ of numbers. So we regard the smallest $\displaystyle\sigma$-field $\displaystyle\mathfrak{F}^{\mathbb{Z}^{r}}$ that contains all cylinder sets $\displaystyle Cyl^{\mathbb{Z}^{r}}(\pi)$ for all prefix runs $\displaystyle\pi$. Moreover, we consider the probability space $\displaystyle((\mathbb{Z}^{r})^{\omega},\mathfrak{F}^{\mathbb{Z}^{r}},\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}})$. Here, the probability measure $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}$ for a program $\displaystyle\mathcal{P}$ is defined such that the probability that a run is in $\displaystyle Cyl^{\mathbb{Z}^{r}}(\pi)$ is the probability $\displaystyle pr^{\mathcal{P}}_{\vec{x}_{0}}(\pi)$ of the prefix run $\displaystyle\pi$.

Definition 10 (Probability Measure for a Program)

For any program $\displaystyle\mathcal{P}$ as in Def. 1 and any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, let $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}:\mathfrak{F}^{\mathbb{Z}^{r}}\to[0,1]$ be the unique probability measure such that we have $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(Cyl^{\mathbb{Z}^{r}}(\pi))=pr_{\vec{x}_{0}}^{\mathcal{P}}(\pi)$ for any prefix run $\displaystyle\pi$.

Example 23 (Probability Measure for $\displaystyle\mathcal{P}_{race}$)

$\displaystyle Cyl^{\mathbb{Z}^{2}}(\langle(11,1),(12,1),(13,6)\rangle)$ consists of all runs that start with $\displaystyle(11,1)$, $\displaystyle(12,1)$, $\displaystyle(13,6)$. If the initial value is $\displaystyle\vec{x}_{0}=(11,1)$, then the probability that a run is in $\displaystyle Cyl^{\mathbb{Z}^{2}}(\left\langle(11,1),(12,1),(13,6)\right\rangle)$ is

[TABLE]

Now we introduce a stochastic process $\displaystyle\mathbf{X}^{\mathbb{Z}^{r}}$ (i.e., a family of random variables $\displaystyle X_{j}^{\mathbb{Z}^{r}}$) which corresponds to the values of the program variables during a run.

Definition 11 (Stochastic Process $\displaystyle\mathbf{X}^{\mathbb{Z}^{r}}$)

For $\displaystyle r\!\geq\!1$, let $\displaystyle\mathbf{X}^{\mathbb{Z}^{r}}\!\!=\!(X^{\mathbb{Z}^{r}}_{j})_{j\in\mathbb{N}}$ where $\displaystyle X^{\mathbb{Z}^{r}}_{j}\!\!:(\mathbb{Z}^{r})^{\omega}\!\!\to\mathbb{Z}^{r}$ is defined as $\displaystyle X^{\mathbb{Z}^{r}}_{j}\!(\left\langle\vec{z}_{0},\ldots,\vec{z}_{j},\ldots\right\rangle)=\vec{z}_{j}$, i.e., when applied to a run, $\displaystyle\!X^{\mathbb{Z}^{r}}_{j}\!\!\!$ returns the values of the program variables after the $\displaystyle j$-th loop iteration.

So $\displaystyle X^{\mathbb{Z}^{2}}_{0}(\left\langle(11,1),(12,1),\ldots\right\rangle)=(11,1)$ and $\displaystyle X^{\mathbb{Z}^{2}}_{1}(\left\langle(11,1),(12,1),\ldots\right\rangle)=(12,1)$.

Using $\displaystyle\mathbf{X}^{\mathbb{Z}^{r}}$, the termination time of a program (cf. Def. 2) can also be defined as $\displaystyle T^{\mathcal{P}}(\pi)=\inf\{j\in\mathbb{N}\mid\vec{a}\bullet X^{\mathbb{Z}^{r}}_{j}(\pi)\leq b\}$ for any $\displaystyle\pi\in(\mathbb{Z}^{r})^{\omega}$. As shown in Def. 3, the termination time is needed to define the expected runtime of a program. We first prove that if the initial values $\displaystyle\vec{x}_{0}$ violate the loop guard, then the expected runtime is trivially 0.

See 1

Proof

We have $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(X_{0}^{\mathbb{Z}^{r}}=\vec{x}_{0})=\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}((X_{0}^{\mathbb{Z}^{r}})^{-1}(\{\vec{x}_{0}\}))=\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}(\mathit{Cyl}^{\mathbb{Z}^{r}}(\vec{x}_{0}))=pr^{\mathcal{P}}_{\vec{x}_{0}}(\vec{x}_{0})=\delta_{\vec{x}_{0},\vec{x}_{0}}=1$. Thus, for $\displaystyle\vec{x}_{0}$ with $\displaystyle\vec{a}\bullet\vec{x}_{0}\leq b$, we obtain $\displaystyle\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}(T^{\mathcal{P}}=0)=\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}(\vec{a}\bullet X_{0}^{\mathbb{Z}^{r}}\leq b)\leq\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}(X_{0}^{\mathbb{Z}^{r}}=\vec{x}_{0})=1$ and hence $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}=\mathbb{E}^{\mathcal{P}}_{\vec{x}_{0}}\left(T^{\mathcal{P}}\right)=0$. ∎

To prove Thm. 2.1 we show how to translate any probabilistic program into a Markov Decision Process (MDP) and then reuse existing corresponding results for MDPs [32]. In this section we recapitulate the needed concepts for MDPs and after the introduction of any concept, we show how it is related to the corresponding notions for probabilistic programs.

We consider infinite time horizon MDPs, where we restrict ourselves to deterministic MDPs without final states, i.e., to Discrete Time Markov Chains (DTMCs). So there is one unique action for every state of the MDP.

Definition 12 (Discrete Time Markov Chain)

A Discrete Time Markov Chain (DTMC) without final states $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ consists of the following components:

• $\displaystyle\bullet$

$\displaystyle\mathcal{S}$ is a set of states.

• $\displaystyle\bullet$

$\displaystyle P:\mathcal{S}\times\mathcal{S}\to[0,1]$ is a transition probability function such that for all states $\displaystyle s\in\mathcal{S}$ we have $\displaystyle\sum\nolimits_{s^{\prime}\in\mathcal{S}}\;P(s,s^{\prime})=1$.

• $\displaystyle\bullet$

$\displaystyle rew:\mathcal{S}\to\mathbb{R}$ is the reward function.

Def. 13 shows how to translate any probabilistic program $\displaystyle\mathcal{P}$ to a corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$. This is possible for our notion of probabilistic programs, because the values of the program variables only depend on their values in the previous loop iteration. To ease notation, let the probabilities $\displaystyle p_{\vec{c}}(\vec{x})$ be constant zero for all $\displaystyle\vec{c}\in\mathbb{Z}^{r}\setminus\{\vec{c}_{1},\ldots,\vec{c}_{n}\}$.

Definition 13 (Translating Probabilistic Programs to DTMCs)

Let $\displaystyle\mathcal{P}$ be a program as in Def. 1. Its corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}=(\mathcal{S},P,rew)$ is given by

• $\displaystyle\bullet$

$\displaystyle\mathcal{S}=\mathbb{Z}^{r}$

• $\displaystyle\bullet$

For states satisfying the loop guard, the probability function $\displaystyle P$ is induced by the probabilities $\displaystyle p_{\vec{c}_{j}}$, and for states that do not satisfy the loop guard, the probability to remain in the state is 1:

[TABLE]

• $\displaystyle\bullet$

The reward function is given by $\displaystyle rew(s)=\begin{cases}1,&\text{if }\vec{a}\bullet s>b\\ 0,&\text{if }\vec{a}\bullet s\leq b\end{cases}$

For a DTMC $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ and each initial state $\displaystyle\vec{x}_{0}\in\mathcal{S}$, we examine a stochastic process $\displaystyle\mathbf{X}^{\mathcal{S}}$ using a probability measure $\displaystyle\mathbb{P}^{\mathcal{M}}_{\vec{x}_{0}}$ for the measurable space $\displaystyle(\mathcal{S}^{\omega},\mathfrak{F}^{\mathcal{S}})$. The definitions of $\displaystyle\mathfrak{F}^{\mathcal{S}}$, $\displaystyle\mathbb{P}^{\mathcal{M}}_{\vec{x}_{0}}$, and $\displaystyle\mathbf{X}^{\mathcal{S}}$ are generalizations of the corresponding definitions from Sect. 2 to arbitrary state spaces.

Moreover, instead of (prefix) runs we now regard histories resp. sample paths and instead of the probability $\displaystyle pr^{\mathcal{P}}_{\vec{x}_{0}}$ of a run with the initial variable assignment $\displaystyle\vec{x}_{0}$ we regard the probability $\displaystyle pr^{\mathcal{M}}_{x_{0}}$ of a sample path with the initial state $\displaystyle x_{0}$.

Definition 14 (Probability Measure for a DTMC)

Let $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ be a DTMC.

• $\displaystyle\bullet$

A sample path is an infinite sequence $\displaystyle\left\langle s_{0},s_{1},s_{2},\ldots\right\rangle\in\mathcal{S}^{\omega}$ and a history is a finite sequence $\displaystyle\left\langle s_{0},s_{1},\ldots,s_{j}\right\rangle\in\mathcal{S}^{j+1}$ for some $\displaystyle j\in\mathbb{N}$. The cylinder set $\displaystyle Cyl^{\mathcal{S}}(\pi)$ of a history $\displaystyle\pi$ consists of all sample paths with prefix $\displaystyle\pi$.

• $\displaystyle\bullet$

For any $\displaystyle x_{0}\in\mathcal{S}$, $\displaystyle pr^{\mathcal{M}}_{x_{0}}:\bigcup\nolimits_{j\in\mathbb{N}}\;\mathcal{S}^{j+1}\to[0,1]$ is the function that maps any history $\displaystyle\left\langle s_{0},\ldots,s_{j}\right\rangle$ to its probability if $\displaystyle x_{0}$ is the initial state. Thus, let $\displaystyle pr^{\mathcal{M}}_{x_{0}}(\left\langle s_{0}\right\rangle)=\delta_{x_{0},s_{0}}$ and if $\displaystyle j\geq 1$, we define:

[TABLE]

• $\displaystyle\bullet$

The (canonical) measurable space for a DTMC is $\displaystyle(\mathcal{S}^{\omega},\mathfrak{F}^{\mathcal{S}})$, where $\displaystyle\mathfrak{F}^{\mathcal{S}}$ is the smallest $\displaystyle\sigma$-field containing all cylinder sets $\displaystyle Cyl^{\mathcal{S}}(\pi)$ for all histories $\displaystyle\pi$.

• $\displaystyle\bullet$

For any $\displaystyle x_{0}\in\mathcal{S}$, the probability measure $\displaystyle pr^{\mathcal{M}}_{x_{0}}:\mathfrak{F}^{\mathcal{S}}\to[0,1]$ for the DTMC $\displaystyle\mathcal{M}$ and the initial state $\displaystyle x_{0}$ is the unique probability measure such that for any history $\displaystyle\pi$ we have $\displaystyle\mathbb{P}^{\mathcal{M}}_{x_{0}}(Cyl^{\mathcal{S}}(\pi))=pr^{\mathcal{M}}_{x_{0}}(\pi)$.

• $\displaystyle\bullet$

The stochastic process $\displaystyle\mathbf{X}^{\mathcal{S}}=(X^{\mathcal{S}}_{j})_{j\in\mathbb{N}}$ is defined as $\displaystyle X^{\mathcal{S}}_{j}:\mathcal{S}^{\omega}\to\mathcal{S}$, where $\displaystyle X^{\mathcal{S}}_{j}(s_{0},\ldots,s_{j},\ldots)=s_{j}$.

The following corollary shows that for any probabilistic program $\displaystyle\mathcal{P}$, the probability spaces for $\displaystyle\mathcal{P}$ and for its corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$ are the same.

Corollary 4 ($\displaystyle\mathcal{P}$ and $\displaystyle\mathcal{M}_{\mathcal{P}}$ Have the Same Probability Measure)

For any program $\displaystyle\mathcal{P}$ as in Def. 1 and its corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$, the corresponding probability spaces are the same. So in particular, we have $\displaystyle\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}=\mathbb{P}^{\mathcal{M}_{\mathcal{P}}}_{\vec{x}_{0}}$ for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$.

Proof

By Def. 13 and 14, the measurable space for $\displaystyle\mathcal{M}_{\mathcal{P}}$ is $\displaystyle((\mathbb{Z}^{r})^{\omega},\mathfrak{F}^{\mathbb{Z}^{r}})$, which is also the measurable space for $\displaystyle\mathcal{P}$. Moreover, Def. 14 implies $\displaystyle pr_{\vec{x}_{0}}^{\mathcal{P}}=pr_{\vec{x}_{0}}^{\mathcal{M}_{\mathcal{P}}}$ and thus, $\displaystyle\mathbb{P}^{\mathcal{P}}_{\vec{x}_{0}}=\mathbb{P}^{\mathcal{M}_{\mathcal{P}}}_{\vec{x}_{0}}$ for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$. ∎

For DTMCs, one is interested in the expected total reward. For a DTMC $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ and the stochastic process $\displaystyle\mathbf{X}^{\mathcal{S}}$, the expected total reward maps any initial state $\displaystyle s_{0}\in\mathcal{S}$ to the expected value of $\displaystyle\sum\nolimits_{j\in\mathbb{N}}\;rew(X^{\mathcal{S}}_{j})$ under the probability measure $\displaystyle\mathbb{P}^{\mathcal{M}}_{s_{0}}$ (if this expected value exists). Note that if $\displaystyle rew(s)\geq 0$ for all $\displaystyle s\in\mathcal{S}$, then the sum $\displaystyle\sum\nolimits_{j\in\mathbb{N}}rew(X^{\mathcal{S}}_{j}):\mathcal{S}^{\omega}\to\overline{\mathbb{R}_{\geq 0}}$ is a non-negative333The non-negativity of $\displaystyle rew$ ensures that the infinite sum of all $\displaystyle rew(X^{\mathcal{S}}_{j})$ is a value in $\displaystyle\overline{\mathbb{R}_{\geq 0}}$. In contrast, if we have positive and negative rewards, then the infinite sum might diverge and neither converge to $\displaystyle-\infty$ nor to $\displaystyle\infty$. random variable. Hence, its expected value under the probability measure $\displaystyle\mathbb{P}_{s_{0}}^{\mathcal{M}}$ is well defined. In particular, this holds for the DTMCs $\displaystyle\mathcal{M}_{\mathcal{P}}$ corresponding to programs $\displaystyle\mathcal{P}$, because for any run $\displaystyle\pi=\left\langle\vec{z}_{0},\vec{z}_{1},\ldots\right\rangle\in(\mathbb{Z}^{r})^{\omega}$, $\displaystyle rew(X^{\mathbb{Z}^{r}}_{j}(\pi))=rew(\vec{z}_{j})$ is 1 if the $\displaystyle j$-th tuple $\displaystyle\vec{z}_{j}$ in the run does not violate the loop condition $\displaystyle\vec{a}\bullet\vec{z}_{j}>b$ and 0, otherwise (i.e., $\displaystyle rew(\vec{z})\in\{0,1\}$ for all $\displaystyle\vec{z}\in\mathbb{Z}^{r}$).

Definition 15 (Expected Total Reward)

Let $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ be aDTMC. For any $\displaystyle s_{0}\in\mathcal{S}$, the expected total reward $\displaystyle tr^{\mathcal{M}}_{s_{0}}\in\mathbb{R}\cup\{-\infty,\infty\}$ of $\displaystyle\mathcal{M}$ is

[TABLE]

whenever this limit exists in $\displaystyle\mathbb{R}\cup\{-\infty,\infty\}$. As argued above, the limit always exists in the special case of non-negative rewards. Therefore, in the case where $\displaystyle rew(s)\in\{0,1\}$ for all $\displaystyle s\in\mathcal{S}$, we have

[TABLE]

The following lemma shows the connection between the termination time and the total reward of a run. In the following, we say that a run $\displaystyle\pi=\left\langle\vec{z}_{0},\vec{z}_{1},\ldots\right\rangle$ is constant on violating states if $\displaystyle\vec{a}\bullet\vec{z}_{j}\leq b$ implies $\displaystyle\vec{z}_{j}=\vec{z}_{j+1}$ for all $\displaystyle j\in\mathbb{N}$.

Lemma 3 (Total Reward is Termination Time)

Let $\displaystyle\mathcal{P}$ be a program as in Def. 1. For every run $\displaystyle\pi$ that is constant on violating states, we have $\displaystyle\sum\nolimits_{j\in\mathbb{N}}\;rew(X^{\mathbb{Z}^{r}}_{j}(\pi))=T^{\mathcal{P}}(\pi)$.

Proof

First, we show that the equality holds for runs $\displaystyle\pi=\left\langle\vec{z}_{0},\vec{z}_{1},\ldots\right\rangle$ where $\displaystyle T^{\mathcal{P}}(\pi)=u<\infty$. So $\displaystyle\vec{a}\bullet\vec{z}_{j}>b$ for all $\displaystyle j<u$ and since $\displaystyle\pi$ is constant on violating states, we have $\displaystyle\vec{a}\bullet\vec{z}_{j}\leq b$ for all $\displaystyle j\geq u$. Here we obtain

[TABLE]

Now we consider a run $\displaystyle\pi=\left\langle\vec{z}_{0},\vec{z}_{1},\ldots\right\rangle$ such that $\displaystyle T^{\mathcal{P}}(\pi)=\infty$, i.e., $\displaystyle\vec{a}\bullet\vec{z}_{j}>b$ for all $\displaystyle j\in\mathbb{N}$. Then we have

[TABLE]

With Cor. 4 and 3 we can show that the expected runtime of a program $\displaystyle\mathcal{P}$ is identical to the expected total reward of its corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$. This is the crucial theorem which allows us to apply results on DTMCs also for probabilistic programs.

Theorem 0.B.1 (Expected Total Reward is Expected Runtime)

For any program $\displaystyle\mathcal{P}$ as in Def. 1, the expected runtime of $\displaystyle\mathcal{P}$ and the expected total reward of the corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$ are the same, i.e., for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$ we have $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}=tr^{\mathcal{M}_{\mathcal{P}}}_{\vec{x}_{0}}$.

Proof

Due to Def. 15 we have $\displaystyle tr^{\mathcal{M}_{\mathcal{P}}}_{\vec{x}_{0}}=\sum\nolimits_{u\in\overline{\mathbb{N}}}\;u\cdot\mathbb{P}_{\vec{x}_{0}}^{\mathcal{M}_{\mathcal{P}}}(A_{u})$, where $\displaystyle A_{u}=\{\pi\in(\mathbb{Z}^{r})^{\omega}\mid\sum\nolimits_{j\in\mathbb{N}}\;rew(X^{\mathbb{Z}^{r}}_{j}(\pi))=u\}$. Note that $\displaystyle pr^{\mathcal{M}_{\mathcal{P}}}_{\vec{x}_{0}}(\pi)=0$ if $\displaystyle\pi$ is not constant on violating states. Thus, $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{M}_{\mathcal{P}}}(A_{u})=\mathbb{P}_{\vec{x}_{0}}^{\mathcal{M}_{\mathcal{P}}}(A_{u}^{\prime})$ where

[TABLE]

Hence, we obtain

[TABLE]

Note that $\displaystyle pr^{\mathcal{P}}_{\vec{x}_{0}}(\pi)=0$ if $\displaystyle\pi$ is not constant on violating states. Thus, $\displaystyle\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(A_{u}^{\prime})=\mathbb{P}_{\vec{x}_{0}}^{\mathcal{P}}(A_{u}^{\prime\prime})$ where $\displaystyle A_{u}^{\prime\prime}=\{\pi\in(\mathbb{Z}^{r})^{\omega}\mid T^{\mathcal{P}}(\pi)=u\}$. So we get

[TABLE]

Now we introduce the transformer $\displaystyle\mathcal{L}$ that is used for DTMCs and corresponds to the expected runtime transformer for probabilistic programs. In the following, we restrict ourselves to DTMCs with non-negative rewards to ensure that the expected total reward exists.

Definition 16 ($\displaystyle\mathcal{L}^{\mathcal{M}}$, cf. [32, Eq. 7.1.5])

Let $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ be a DTMC with only non-negative rewards. We define the mapping $\displaystyle\mathcal{L}^{\mathcal{M}}:(\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}})\to(\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}})$ such that for every function $\displaystyle f:\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}}$ and every $\displaystyle s\in\mathcal{S}$, we have

[TABLE]

The following corollary shows that the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ of a program $\displaystyle\mathcal{P}$ is the same as the transformer $\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$ of the corresponding DTMC $\displaystyle\mathcal{M}_{\mathcal{P}}$.

Corollary 5 ($\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$ is Expected Runtime Transformer $\displaystyle\mathcal{L}^{P}$)

For any program $\displaystyle\mathcal{P}$, the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ from Def. 4 is identical to the transformer $\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$ from Def. 16.

Proof

Let $\displaystyle\mathcal{P}$ be a program as in Def. 1 and let $\displaystyle\mathcal{M}_{\mathcal{P}}=(\mathbb{Z}^{r},P,rew)$. Consider an arbitrary function $\displaystyle f:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq_{0}}}$ and an $\displaystyle s\in\mathbb{Z}^{r}$. If $\displaystyle\vec{a}\bullet s\leq b$ then $\displaystyle rew(s)=0$, $\displaystyle P(s,s)=1$, and $\displaystyle P(s,s^{\prime})=0$ for $\displaystyle s^{\prime}\neq s$. Hence

[TABLE]

If $\displaystyle\vec{a}\bullet s>b$ then

[TABLE]

Now that we know that the transformers $\displaystyle\mathcal{L}^{\mathcal{P}}$ and $\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$ are the same, we can use existing results on DTMCs to obtain results for programs $\displaystyle\mathcal{P}$. More precisely, for any DTMC $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ with only non-negative rewards, it is known that the expected total reward function $\displaystyle tr^{\mathcal{M}}:\mathcal{S}\to\overline{\mathbb{R}_{\geq 0}}$ with $\displaystyle tr^{\mathcal{M}}(s_{0})=tr^{\mathcal{M}}_{s_{0}}$ for any $\displaystyle s_{0}\in\mathcal{S}$ is a fixpoint of $\displaystyle\mathcal{M}$’s transformer $\displaystyle\mathcal{L}^{\mathcal{M}}$.

Theorem 0.B.2 (Expected Total Reward is Fixpoint)

Let $\displaystyle\mathcal{M}$ be a DTMC with only non-negative rewards. Then $\displaystyle tr^{\mathcal{M}}$ is a fixpoint of $\displaystyle\mathcal{L}^{\mathcal{M}}$.

Proof

The proof can be found in [32, Thm. 7.1.3]. Note that it requires the assumption that the expected total reward exists [32, Assumption 7.1.1] which is ensured by a non-negative reward function. ∎

Moreover, the expected total reward function is smaller or equal than any other fixpoint of $\displaystyle\mathcal{L}^{\mathcal{M}}$ (and than every function $\displaystyle f$ which satisfies the inequality $\displaystyle f\geq\mathcal{L}^{\mathcal{M}}(f)$).

Theorem 0.B.3 (Expected Total Reward is Smaller Than Other Fix-points)

Let $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ be a DTMC with only non-negative rewards and let there be a function $\displaystyle f:\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}}$ such that $\displaystyle f\geq\mathcal{L}^{\mathcal{M}}(f)$. Then $\displaystyle f\geq tr^{\mathcal{M}}$.

Proof

The proof of the finite case, i.e., $\displaystyle f(s)<\infty$ for all $\displaystyle s\in\mathcal{S}$, can be found in [32, Thm. 7.2.2]. Note that in our case there is a unique strategy (since we restrict ourselves to DTMCs) and we have only non-negative rewards. Therefore, the proof holds for functions $\displaystyle f$ that map to infinity as well. ∎

Thm. 0.B.2 and 0.B.3 imply that the expected total reward function $\displaystyle tr^{\mathcal{M}}$ is the least fixpoint of the transformer $\displaystyle\mathcal{L}^{\mathcal{M}}$.

Corollary 6 (Expected Total Reward is Least Fixpoint)

Let $\displaystyle\mathcal{M}=(\mathcal{S},P,rew)$ be a DTMC with only non-negative rewards. Then $\displaystyle tr^{\mathcal{M}}$ is the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{M}}$, i.e., for any $\displaystyle s_{0}\in\mathcal{S}$ we have $\displaystyle\mathrm{lfp}(\mathcal{L}^{\mathcal{M}})(s_{0})=tr^{\mathcal{M}}_{s_{0}}$.

The following theorem shows that $\displaystyle\mathcal{L}^{\mathcal{M}}$ is continuous for any DTMC $\displaystyle\mathcal{M}$ with only non-negative rewards. This is needed to apply Kleene’s Fixpoint Theorem, i.e., to show that the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{M}}$ is $\displaystyle\sup\{\mathfrak{0},\mathcal{L}^{\mathcal{M}}(\mathfrak{0}),(\mathcal{L}^{\mathcal{M}})^{2}(\mathfrak{0}),\ldots\}$.

Theorem 0.B.4 (Continuity of $\displaystyle\mathcal{L}^{\mathcal{M}}$, cf.  [32, Lemma 7.1.5.c])

Let $\displaystyle\mathcal{M}$ be a DTMC with only non-negative rewards. Then $\displaystyle\mathcal{L}^{\mathcal{M}}$ is continuous.

Proof

Let $\displaystyle S=\{f_{0},f_{1},\ldots\}$ be a chain in $\displaystyle\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}}$, i.e., we have $\displaystyle f_{j}\leq f_{j+1}$ for all $\displaystyle j\in\mathbb{N}$. Then $\displaystyle(\sup S)$ is the function $\displaystyle(\sup S):\mathcal{S}\to\overline{\mathbb{R}_{\geq_{0}}}$ with $\displaystyle(\sup S)(s)=\sup_{j\in\mathbb{N}}\left(f_{j}(s)\right)$ for all $\displaystyle s\in\mathcal{S}$. Therefore, for any $\displaystyle s\in\mathcal{S}$ we have

[TABLE]

where $\displaystyle\mathcal{L}^{\mathcal{M}}(S)=\{\mathcal{L}^{\mathcal{M}}(f_{0}),\mathcal{L}^{\mathcal{M}}(f_{1}),\ldots\}$. ∎

Now we can prove Thm. 2.1 which states that the expected runtime of a program $\displaystyle\mathcal{P}$ is the least fixpoint of its expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ and that it can be obtained as the supremum of $\displaystyle\{\mathfrak{0},\mathcal{L}^{\mathcal{P}}(\mathfrak{0}),(\mathcal{L}^{\mathcal{P}})^{2}(\mathfrak{0}),\ldots\}$. As usual, a function $\displaystyle f:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq 0}}$ is a fixpoint of $\displaystyle\mathcal{L}^{\mathcal{P}}$ if $\displaystyle\mathcal{L}^{\mathcal{P}}(f)=f$. Such a fixpoint $\displaystyle f$ is the least fixpoint of $\displaystyle\mathcal{L}^{\mathcal{P}}$ (i.e., $\displaystyle f=\mathrm{lfp}(\mathcal{L}^{\mathcal{P}})$) if $\displaystyle f\leq g$ for any other fixpoint $\displaystyle g$ of $\displaystyle\mathcal{L}^{\mathcal{P}}$.

See 2.1

Proof

By Thm. 0.B.1, the expected runtime of $\displaystyle\mathcal{P}$ is the same as the expected total reward of the corresponding DTMC $\displaystyle\mathcal{M}_{P}$. Cor. 6 showed that the expected total reward is the least fixpoint of the transformer $\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$, and $\displaystyle\mathcal{L}^{\mathcal{M}_{\mathcal{P}}}$ is the same as the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ due to Cor. 5.

As the continuity of $\displaystyle\mathcal{L}^{\mathcal{M}_{P}}=\mathcal{L}^{P}$ was shown in Thm. 0.B.4, by Kleene’s Fixpoint Theorem we have $\displaystyle\mathrm{lfp}(\mathcal{L}^{P})=\sup\{\mathfrak{0},\mathcal{L}^{P}(\mathfrak{0}),(\mathcal{L}^{P})^{2}(\mathfrak{0}),\ldots\}$. ∎

Appendix 0.C Proofs for Sect. 3

See 3.1

Proof

The expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$ is continuous (and thus, monotonic) by Thm. 2.1. Hence, by induction on $\displaystyle j$ one can show that $\displaystyle f\geq\mathcal{L}^{\mathcal{P}}(f)$ implies $\displaystyle f\geq(\mathcal{L}^{\mathcal{P}})^{j}(\mathfrak{0})$ for any function $\displaystyle f:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq 0}}$ and any $\displaystyle j\in\mathbb{N}$. So $\displaystyle f\geq\mathcal{L}^{\mathcal{P}}(f)$ implies $\displaystyle f\geq\sup\{\mathfrak{0},\mathcal{L}^{\mathcal{P}}(\mathfrak{0}),(\mathcal{L}^{\mathcal{P}})^{2}(\mathfrak{0}),\ldots\}=\mathrm{lfp}(\mathcal{L}^{\mathcal{P}})$. By Thm. 2.1, this means that $\displaystyle f(\vec{x}_{0})\geq\mathrm{lfp}(\mathcal{L}^{\mathcal{P}})(\vec{x}_{0})=rt^{\mathcal{P}}_{\vec{x}_{0}}$ for all $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$.

Hence, to prove Thm. 3.1, it suffices to show $\displaystyle f\geq\mathcal{L}^{\mathcal{P}}(f)$ for the function $\displaystyle f:\mathbb{Z}^{r}\to\overline{\mathbb{R}_{\geq 0}}$ with $\displaystyle f(\vec{x})=\tfrac{1}{p^{\prime}}$ if $\displaystyle\vec{a}\bullet\vec{x}>b$ and $\displaystyle f(\vec{x})=0$ if $\displaystyle\vec{a}\bullet\vec{x}\leq b$.

For $\displaystyle\vec{x}$ with $\displaystyle\vec{a}\bullet\vec{x}\leq b$, we have $\displaystyle\mathcal{L}^{\mathcal{P}}(f)(\vec{x})=f(\vec{x})$. If $\displaystyle\vec{a}\bullet\vec{x}>b$, then we get

[TABLE]

Appendix 0.D Proofs for Sect. 4

In this section we present the proofs of Sect. 4. It is divided into three subsections in which we will give the proofs for the respective subsections of Sect. 4.

0.D.1 Proofs for Sect. 4.1

To prove Thm. 4.1, we need an auxiliary lemma.

Lemma 4 (Connections between $\displaystyle\mathcal{P}$ and $\displaystyle\mathcal{P}^{\mathit{rdw}}$)

Let $\displaystyle\mathcal{P}$ be a CP program as in Def. 1 and let $\displaystyle\mathit{rdw}_{\mathcal{P}}^{\omega}$ be the function which applies $\displaystyle\mathit{rdw}_{\mathcal{P}}$ componentwise to runs. Then we have:

1. (a)

$\displaystyle T^{\mathcal{P}^{\mathit{rdw}}}\circ\mathit{rdw}_{\mathcal{P}}^{\omega}=T^{\mathcal{P}}$** 2. (b)

Let $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$. Then for any prefix run $\displaystyle\left\langle y_{0},\ldots,y_{j}\right\rangle\in\mathbb{Z}^{j+1}$ we have:

[TABLE]

Here, for any $\displaystyle M\subseteq\mathbb{Z}^{\omega}$ we have $\displaystyle(\mathit{rdw}_{\mathcal{P}}^{\omega})^{-1}(M)=\{\pi\in(\mathbb{Z}^{r})^{\omega}\mid\mathit{rdw}_{\mathcal{P}}^{\omega}(\pi)\in M\}$.

Proof

1. (a)

Let $\displaystyle\left\langle\vec{z}_{0},\vec{z_{1}},\ldots\right\rangle\in(\mathbb{Z}^{r})^{\omega}$ such that $\displaystyle T^{\mathcal{P}}(\left\langle\vec{z}_{0},\vec{z_{1}},\ldots\right\rangle)=j\in\overline{\mathbb{N}}$. So if $\displaystyle j\in\mathbb{N}$, then $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z}_{0}),\ldots,\mathit{rdw}_{\mathcal{P}}(\vec{z}_{j-1})>0$ and $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z}_{j})\leq 0$. Similarly, if $\displaystyle j=\infty$, then $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z}_{j})>0$ for every $\displaystyle j\in\mathbb{N}$. So in both cases, we have

[TABLE] 2. (b)

First note that for any prefix run $\displaystyle\left\langle y_{0},\ldots,y_{j}\right\rangle\in\mathbb{Z}^{j+1}$, we have

[TABLE]

As usual, “$\displaystyle\uplus$” denotes the disjoint union, i.e., we have $\displaystyle Cyl^{\mathbb{Z}^{r}}(\pi)\cap Cyl^{\mathbb{Z}^{r}}(\pi^{\prime})\linebreak=\varnothing$ for prefix runs $\displaystyle\pi\neq\pi^{\prime}$ of the same length. Note that both sides of the equality 13 can be empty, i.e., there might not be any $\displaystyle\vec{z}_{u}$ with $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z}_{u})=y_{u}$ for some $\displaystyle 1\leq u\leq j$. For $\displaystyle x_{0}=\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})$, we prove that

[TABLE]

The result then follows by 13. For the left-hand side we get $\displaystyle\mathbb{P}^{\mathcal{P}^{\mathit{rdw}}}_{x_{0}}(Cyl^{\mathbb{Z}}(\langle y_{0},\linebreak\ldots,y_{j}\rangle)=0$ if $\displaystyle y_{0}\neq x_{0}$ and otherwise, we have

[TABLE]

For the right-hand side recall that $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})=x_{0}$ and that we only regard tuples $\displaystyle\vec{z}_{0}$ where $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{z}_{0})=y_{0}$. So if $\displaystyle y_{0}\neq x_{0}$, then all of these tuples $\displaystyle\vec{z}_{0}$ are different from $\displaystyle\vec{x}_{0}$. Hence, then the right-hand side is also 0. Otherwise, we have the following, where $\displaystyle d_{\mathcal{P}}=\mathit{rdw}_{\mathcal{P}}(\vec{d})$:

[TABLE]

For Equation $\displaystyle(\dagger)$, note that $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0}+\vec{c}_{v_{1}})=\vec{a}\bullet(\vec{x}_{0}+\vec{c}_{v_{1}})-b=\vec{a}\bullet\vec{x}_{0}+\vec{a}\bullet\vec{c}_{v_{1}}-b=\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0})+\vec{a}\bullet\vec{c}_{v_{1}}=y_{0}+\vec{a}\bullet\vec{c}_{v_{1}}$. Hence, $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0}+\vec{c}_{v_{1}})=y_{1}$ means that $\displaystyle y_{1}-y_{0}=\vec{a}\bullet\vec{c}_{v_{1}}$. Similarly, $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0}+\vec{c}_{v_{1}}+\vec{c}_{v_{2}})=y_{0}+\vec{a}\bullet\vec{c}_{v_{1}}+\vec{a}\bullet\vec{c}_{v_{2}}=y_{1}+\vec{a}\bullet\vec{c}_{v_{2}}$. So $\displaystyle\mathit{rdw}_{\mathcal{P}}(\vec{x}_{0}+\vec{c}_{v_{1}}+\vec{c}_{v_{2}})=y_{2}$ means that $\displaystyle y_{2}-y_{1}=\vec{a}\bullet\vec{c}_{v_{2}}$, etc. ∎

See 4.1

Proof

For any $\displaystyle j\in\mathbb{N}$ and any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$ we obtain the following.

[TABLE]

[TABLE]

As the above equality holds for every $\displaystyle j\in\mathbb{N}$ it also holds for $\displaystyle j=\infty$. ∎

0.D.2 Proofs for Sect. 4.2

For the proof of Thm. 4.2, we use results on random walks [21, 33, 17]. We first recapitulate the required notions from probability theory.

Consider a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ (i.e., for every $\displaystyle A\in\mathfrak{F}\subseteq 2^{\Omega}$, $\displaystyle\mathbb{P}(A)$ is the probability that an event from the set $\displaystyle\Omega$ is in the subset $\displaystyle A$) and a stochastic process $\displaystyle\mathbf{Y}=(Y_{j})_{j\in\mathbb{N}}$ where each $\displaystyle Y_{j}:\Omega\to\mathbb{Z}$ is a random variable. $\displaystyle\mathbf{Y}$ is independent and identically distributed (i.i.d.) on $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ if for all $\displaystyle j,j^{\prime}\in\mathbb{N}$ with $\displaystyle j\neq j^{\prime}$ and all $\displaystyle y,z\in\mathbb{Z}$:

• $\displaystyle\bullet$

$\displaystyle Y_{j}$ and $\displaystyle Y_{j^{\prime}}$ are identically distributed, i.e., $\displaystyle\mathbb{P}(Y_{j}=z)=\mathbb{P}(Y_{j^{\prime}}=z)$

• $\displaystyle\bullet$

$\displaystyle Y_{j}$ and $\displaystyle Y_{j^{\prime}}$ are independent, i.e., $\displaystyle\mathbb{P}(Y_{j}=y,Y_{j^{\prime}}=z)=\mathbb{P}(Y_{j}=y)\cdot\mathbb{P}(Y_{j^{\prime}}=z)$

Here, $\displaystyle\mathbb{P}(Y_{j}=y,Y_{j^{\prime}}=z)=\mathbb{P}(Y_{j}^{-1}(\{y\})\cap Y_{j^{\prime}}^{-1}(\{z\}))$ is the probability that an event $\displaystyle\pi\in\Omega$ satisfies both $\displaystyle Y_{j}(\pi)=y$ and $\displaystyle Y_{j^{\prime}}(\pi)=z$. So independence means that one random variable does not influence the value of the other.

Now we recapitulate the notion of a random walk created by an i.i.d. stochastic process.

Definition 17 (Random Walk[21])

Let $\displaystyle\mathbf{Y}=(Y_{j})_{j\in\mathbb{N}}$ be an i.i.d. stochastic process for a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ with $\displaystyle Y_{j}:\Omega\to\mathbb{Z}$ and let $\displaystyle X_{0}:\Omega\to\mathbb{Z}$ be a random variable such that $\displaystyle\mathbb{P}(X_{0}=x_{0})=1$ for some $\displaystyle x_{0}\in\mathbb{Z}$. The (one-dimensional) random walk for $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ induced by $\displaystyle\mathbf{Y}$ with starting point $\displaystyle X_{0}$ is the sequence $\displaystyle\mathbf{S}=(S_{j})_{j\in\mathbb{N}}$ of random variables444Note that we define $\displaystyle S_{j}=X_{0}+\sum\nolimits_{0\leq u\leq j-1}\;Y_{u}$ instead of $\displaystyle S_{j}=x_{0}+\sum\nolimits_{0\leq u\leq j-1}\;Y_{u}$. In this way, the random variables $\displaystyle X_{0},Y_{0},Y_{1},\ldots$ only generate a single random walk that does not depend on $\displaystyle x_{0}$. Instead, the different possible initial values $\displaystyle x_{0}$ are taken care of by choosing different probability spaces $\displaystyle(\Omega,\mathfrak{F},\mathbb{P}_{x_{0}})$ where $\displaystyle\mathbb{P}_{x_{0}}(X_{0}=x_{0})=1$. $\displaystyle S_{j}=X_{0}+\sum\nolimits_{0\leq u\leq j-1}\;Y_{u}$. We denote the random walk $\displaystyle\mathbf{S}$ by $\displaystyle(X_{0},\mathbf{Y})$.

Analogous to the termination time for programs from Def. 2, the hitting time is the time when the random walk “hits” a certain subset of $\displaystyle\mathbb{Z}$ for the first time.

Definition 18 (Hitting Time)

The hitting time for a random walk $\displaystyle(S_{j})_{j\in\mathbb{N}}$ is the random variable $\displaystyle T^{hit}:\Omega\to\overline{\mathbb{N}}$ with $\displaystyle T^{hit}(\pi)=\inf\{j\in\mathbb{N}\mid S_{j}(\pi)\leq 0\}$.

If $\displaystyle\mathbf{Y}=(Y_{j})_{j\in\mathbb{N}}$ is i.i.d., then $\displaystyle\mathbb{E}(Y_{0})=\mathbb{E}(Y_{j})$ for all $\displaystyle j\in\mathbb{N}$. Hence, we define $\displaystyle\mu=\mathbb{E}(Y_{0})$ to be the drift, i.e., the expected change in each step of the random walk. For such random walks, a result similar to Thm. 4.2 is already known.

Lemma 5 (Drift and Hitting Time [33, Thm. 17.1, Prop. 18.1])

Let $\displaystyle\mathbf{Y}$ be i.i.d. for a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ and let $\displaystyle(X_{0},\mathbf{Y})$ be a random walk for $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ such that $\displaystyle\mu=\mathbb{E}(Y_{0})<\infty$ (note that the drift $\displaystyle\mu$ does not depend on $\displaystyle X_{0}$). Let $\displaystyle T^{hit}$ be the hitting time for $\displaystyle(X_{0},\mathbf{Y})$. Then we have:

• $\displaystyle\bullet$

If $\displaystyle\mu>0$, then $\displaystyle\mathbb{P}(T^{hit}=\infty)>0$.

• $\displaystyle\bullet$

If $\displaystyle\mu=0$ and $\displaystyle\mathbb{P}(Y_{0}=0)\neq 1$, then $\displaystyle\mathbb{P}(T^{hit}=\infty)=0$ but $\displaystyle\mathbb{E}(T^{hit})=\infty$.

• $\displaystyle\bullet$

If $\displaystyle\mu<0$, then $\displaystyle\mathbb{E}(T^{hit})<\infty$.

In order to use Lemma 5 to prove Thm. 4.2, our aim is to represent the stochastic process $\displaystyle\mathbf{X}^{\mathbb{Z}}$ from Def. 11 (for $\displaystyle r=1$) as a random walk $\displaystyle\mathbf{X}^{\mathbb{Z}}=(X_{0}^{\mathbb{Z}},\mathbf{Y}^{\mathbb{Z}})$ for a suitable stochastic process $\displaystyle\mathbf{Y}^{\mathbb{Z}}$.

To this end, we take the stochastic process $\displaystyle\mathbf{Y}^{\mathbb{Z}}=(Y_{j}^{\mathbb{Z}})_{j\in\mathbb{N}}$ with $\displaystyle Y_{j}^{\mathbb{Z}}=(X_{j+1}^{\mathbb{Z}}-X_{j}^{\mathbb{Z}})$ for all $\displaystyle j\in\mathbb{N}$, i.e., $\displaystyle Y_{j}^{\mathbb{Z}}$ is the change of the program variable in the $\displaystyle(j+1)$-th loop iteration. Then $\displaystyle\mathbf{X}^{\mathbb{Z}}$ can be obtained as the random walk $\displaystyle(X_{0}^{\mathbb{Z}},\mathbf{Y}^{\mathbb{Z}})$, since $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}(X_{0}^{\mathbb{Z}}=x_{0})=1$ and $\displaystyle X_{j}^{\mathbb{Z}}=X_{0}^{\mathbb{Z}}+\sum\nolimits_{0\leq u\leq j-1}(X_{u+1}^{\mathbb{Z}}-X_{u}^{\mathbb{Z}})=X_{0}^{\mathbb{Z}}+\sum\nolimits_{0\leq u\leq j-1}Y_{u}^{\mathbb{Z}}$ for all $\displaystyle j\in\mathbb{N}$.

Unfortunately, $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ is not i.i.d. for the probability measure $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}$, because the probability that $\displaystyle Y_{j}^{\mathbb{Z}}=0$ (i.e., that $\displaystyle X_{j+1}^{\mathbb{Z}}=X_{j}^{\mathbb{Z}}$ holds) depends on $\displaystyle j$. More precisely, the probability for $\displaystyle X_{j+1}^{\mathbb{Z}}=X_{j}^{\mathbb{Z}}$ is $\displaystyle p_{0}$ plus the probability that the program has already reached a value $\displaystyle x\leq 0$ (i.e., that the program’s termination time is at most $\displaystyle j$). The reason is that according to the probability measure $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}$, the value of $\displaystyle x$ remains unchanged as soon as $\displaystyle x\leq 0$. Thus, we obtain $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}(Y_{j}^{\mathbb{Z}}=0)=p_{0}+\mathbb{P}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\leq j)$, where $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}}\leq j)$ clearly depends on $\displaystyle j$.

Therefore, we now introduce a new adapted probability measure $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$ such that $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ is i.i.d. on the probability space $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}_{x_{0}}^{\mathcal{P}})$ and at the same time, $\displaystyle\mathbf{E}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}})\linebreak=\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)$, where $\displaystyle\mathbf{E}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}})$ denotes the expected value of the termination time $\displaystyle T^{\mathcal{P}}$ under the probability measure $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$. In the following definition, $\displaystyle q_{x_{0}}^{\mathcal{P}}$ corresponds to the function $\displaystyle pr_{x_{0}}^{\mathcal{P}}$ from Def. 9 that maps any prefix run to its probability if $\displaystyle x_{0}$ is the initial value of the program variable. When defining $\displaystyle pr_{x_{0}}^{\mathcal{P}}$, the probability for a prefix run $\displaystyle\left\langle z_{0},\ldots,z_{j-1},z_{j}\right\rangle$ where $\displaystyle z_{j-1}\leq 0$ and $\displaystyle z_{j-1}\neq z_{j}$ was 0. In contrast, for $\displaystyle q_{x_{0}}^{\mathcal{P}}$ we continue to execute the program also if $\displaystyle x\leq 0$. This corresponds to a variant of the program where the loop condition $\displaystyle x>0$ is replaced by true.

Definition 19 (Probability Measure $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$)

For any random walk program $\displaystyle\mathcal{P}\!$ as in Def. 5 without direct termination, any $\displaystyle x_{0}\in\mathbb{Z}$, and any prefix run $\displaystyle\left\langle z_{0},z_{1},\ldots,z_{j}\right\rangle$, let $\displaystyle q_{x_{0}}^{\mathcal{P}}(\left\langle z_{0}\right\rangle)=\delta_{x_{0},z_{0}}$ and if $\displaystyle j\geq 1$, we define:

[TABLE]

$\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$ is the probability measure with $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}(Cyl^{\mathbb{Z}}(\pi))\!=\!q_{x_{0}}^{\mathcal{P}}(\pi)$ for any prefix run $\displaystyle\pi$.

Example 24 (Adapted Probability Measure for $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$)

Consider runs that start with $\displaystyle 1$, $\displaystyle-2$, and $\displaystyle-6$. Here, we have $\displaystyle Y^{\mathbb{Z}}_{0}(\left\langle 1,-2,-6,\ldots\right\rangle)=(-2)\,-\,1=-3$ and $\displaystyle Y^{\mathbb{Z}}_{1}(\left\langle 1,-2,-6,\ldots\right\rangle)=(-6)\,-\,(-2)=-4$. For $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ of Ex. 5, when using the probability measure $\displaystyle\mathbb{P}^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}$ from Def. 10, we obtain $\displaystyle\mathbb{P}^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}(Cyl^{\mathbb{Z}}(\left\langle 1,-2,-6\right\rangle))=pr^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}(\left\langle 1,-2,-6\right\rangle)=p^{\mathit{rdw}}_{-3}\cdot p^{\mathit{rdw}}_{-4}\cdot\delta_{-2,-6}=0$, since the value of $\displaystyle x$ should not change anymore after reaching the non-positive value $\displaystyle-2$. In contrast, the adapted probability measure $\displaystyle\mathbf{P}^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}$ from Def. 19 yields $\displaystyle\mathbf{P}^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}(Cyl^{\mathbb{Z}}(\langle 1,-2,$ $\displaystyle-6\rangle))=q^{\mathcal{P}^{\mathit{rdw}}_{race}}_{1}(Cyl^{\mathbb{Z}}(\left\langle 1,-2,-6\right\rangle))=p^{\mathit{rdw}}_{-3}\cdot p^{\mathit{rdw}}_{-4}=\tfrac{1}{22}\cdot\tfrac{1}{22}=\tfrac{1}{484}$.

For the termination time $\displaystyle T^{\mathcal{P}}$ one only regards the time that it takes until the program variable $\displaystyle x$ is non-positive for the first time. Thus, it does not matter whether $\displaystyle x$ is kept unchanged afterwards (as in the probability measure $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}$) or whether the loop body is executed further afterwards (as in $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$). So the expected runtime is the same, no matter whether one uses $\displaystyle\mathbb{E}_{x_{0}}^{\mathcal{P}}$ or $\displaystyle\mathbf{E}_{x_{0}}^{\mathcal{P}}$.

Lemma 6 ($\displaystyle T^{\mathcal{P}}$ is Identically Distributed Under $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}$ and $\displaystyle\mathbf{P}_{x_{0}}^{\mathcal{P}}$)

For any random walk program $\displaystyle\mathcal{P}$ without direct termination, any $\displaystyle x_{0}\in\mathbb{Z}$, and any $\displaystyle j\in\overline{\mathbb{N}}$, we have $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}\left(T^{\mathcal{P}}=j\right)=\mathbf{P}_{x_{0}}^{\mathcal{P}}\left(T^{\mathcal{P}}=j\right)$. Thus, $\displaystyle\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)=\mathbf{E}_{x_{0}}^{\mathcal{P}}\left(T^{\mathcal{P}}\right)$.

Proof

First of all, by the definition of $\displaystyle T^{\mathcal{P}}$, for any $\displaystyle j\in\mathbb{N}$ we have

[TABLE]

First, we consider $\displaystyle x_{0}\leq 0$. Then any cylinder set with positive probability w.r.t. $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}$ resp. $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$ has the form $\displaystyle\mathit{Cyl}^{\mathbb{Z}}(\pi)$ where $\displaystyle\pi$ starts with $\displaystyle x_{0}\leq 0$. But for any run $\displaystyle\tau\in\mathit{Cyl}^{\mathbb{Z}}(\pi)$ we have $\displaystyle T^{\mathcal{P}}(\tau)=0$. Therefore, we conclude $\displaystyle\mathbb{P}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}}=0)=1=\mathbf{P}_{x_{0}}^{\mathcal{P}}(T^{\mathcal{P}}=0)$.

We now show that for $\displaystyle x_{0}>0$

[TABLE]

The reason is that we have:

[TABLE]

Therefore, for all $\displaystyle j\in\mathbb{N}$ we obtain:

[TABLE]

Finally, $\displaystyle\mathbb{P}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}=\infty\right)=1-\sum\limits_{j\in\mathbb{N}}\mathbb{P}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}=j\right)=1-\sum\limits_{j\in\mathbb{N}}\mathbf{P}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}=j\right)=\linebreak\mathbf{P}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}=\infty\right)$. ∎

Now we show that the process $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ with $\displaystyle Y_{j}^{\mathbb{Z}}=X_{j+1}^{\mathbb{Z}}-X_{j}^{\mathbb{Z}}$ is i.i.d. w.r.t. the probability measure $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$ and thus, $\displaystyle(X_{0}^{\mathbb{Z}},\mathbf{Y}^{\mathbb{Z}})$ is a random walk for $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}^{\mathcal{P}}_{x_{0}})$. So the expected value of $\displaystyle Y_{j}^{\mathbb{Z}}$ under $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$, is the same for all $\displaystyle j$. In fact, this expected value is the drift $\displaystyle\mu_{\mathcal{P}}$ of the program, irrespective of the start value $\displaystyle x_{0}$.

Lemma 7 (Y is i.i.d. and its Expected Value is the Drift of the Program)

Let $\displaystyle\mathbf{X}^{\mathbb{Z}}$ be the stochastic process as in Def. 11. We define the process $\displaystyle\mathbf{Y}^{\mathbb{Z}}=(Y_{j}^{\mathbb{Z}})_{j\in\mathbb{N}}$ by $\displaystyle Y_{j}^{\mathbb{Z}}=X_{j+1}^{\mathbb{Z}}-X_{j}^{\mathbb{Z}}$ for all $\displaystyle j\in\mathbb{N}$. Then for any random walk program $\displaystyle\mathcal{P}$ without direct termination and any $\displaystyle x_{0}\in\mathbb{Z}$, $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ is i.i.d. w.r.t. $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}^{\mathcal{P}}_{x_{0}})$ and thus, $\displaystyle(X_{0}^{\mathbb{Z}},\mathbf{Y}^{\mathbb{Z}})$ is a random walk for this probability space. Furthermore, for any $\displaystyle x_{0}\in\mathbb{Z}$ and any $\displaystyle j\in\mathbb{N}$, we have $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(Y_{j}^{\mathbb{Z}})=\mu_{\mathcal{P}}$.

Proof

We first show that the $\displaystyle Y_{j}^{\mathbb{Z}}$ are identically distributed. More precisely, we prove that for all $\displaystyle u,x_{0}\in\mathbb{Z}$ and all $\displaystyle j\in\mathbb{N}$ we have $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}(Y_{j}^{\mathbb{Z}}=u)=p_{u}$. Similar to our handling of multivariate programs in App. 0.B, for any random walk program $\displaystyle\mathcal{P}$ as in Def. 5 we define $\displaystyle p_{v}=0$ for $\displaystyle v>m$ or $\displaystyle v<-k$.

[TABLE]

[TABLE]

As $\displaystyle p_{u}$ is independent of $\displaystyle j$, the $\displaystyle Y_{j}^{\mathbb{Z}}$ are identically distributed. Furthermore, the expected value of $\displaystyle Y_{j}^{\mathbb{Z}}$ under $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$ is

[TABLE]

which is the drift of the program.

It remains to show the independence of the random variables. Let $\displaystyle j\neq j^{\prime}\in\mathbb{N}$ and w.l.o.g. assume $\displaystyle j^{\prime}>j$.

[TABLE]

[TABLE]

Now we can prove Thm. 4.2 based on the results of Lemma 5 for random walks.

See 4.2

Proof

Due to Lemma 7, $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ is i.i.d. w.r.t. $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}^{\mathcal{P}}_{x_{0}})$ and thus, $\displaystyle\mathbf{S}^{\mathbb{Z}}=(X_{0}^{\mathbb{Z}},\mathbf{Y}^{\mathbb{Z}})$ is a random walk w.r.t. this probability space for any $\displaystyle x_{0}\in\mathbb{Z}$. By Def. 17 we have $\displaystyle S_{j}^{\mathbb{Z}}=X_{0}^{\mathbb{Z}}+\sum\nolimits_{0\leq u\leq j-1}Y_{u}^{\mathbb{Z}}=X_{j}^{\mathbb{Z}}$ for any $\displaystyle j\in\mathbb{N}$. Hence, the hitting time $\displaystyle T^{hit}$ for the random walk $\displaystyle\mathbf{S}^{\mathbb{Z}}$ as defined in Def. 18 is exactly the termination time $\displaystyle T^{\mathcal{P}}$. As we proved in Lemma 7 that $\displaystyle\mathbf{E}_{x_{0}}^{\mathcal{P}}(Y_{0})=\mu_{\mathcal{P}}$ holds independent of $\displaystyle x_{0}\in\mathbb{Z}$, we can use Lemma 5 for all $\displaystyle x_{0}$. So we get for all $\displaystyle x_{0}\in\mathbb{Z}$:

• $\displaystyle\bullet$

If $\displaystyle\mu_{\mathcal{P}}\!>0$, then $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}}\!\!=\!\infty)\overset{\mathrm{Lemma}\;\ref{ert_unaffected}}{=}\mathbb{P}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}}\!\!=\!\infty)>0$, i.e., $\displaystyle\mathcal{P}$ is not AST.

• $\displaystyle\bullet$

Note that as $\displaystyle\mathcal{P}$ is non-trivial (i.e., $\displaystyle p_{0}\neq 1$), we have $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}(Y_{0}^{\mathbb{Z}}=0)\neq 1$. So if $\displaystyle\mu_{\mathcal{P}}=0$, then Lemma 5 implies $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}}=\infty)\overset{\mathrm{Lemma}\;\ref{ert_unaffected}}{=}\mathbb{P}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}}=\infty)=0$ but $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}})\overset{\mathrm{Lemma}\;\ref{ert_unaffected}}{=}\mathbb{E}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}})=\infty$, i.e., $\displaystyle\mathcal{P}$ is AST but not PAST.

• $\displaystyle\bullet$

If $\displaystyle\mu_{\mathcal{P}}<0$, then $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}})\overset{\mathrm{Lemma}\;\ref{ert_unaffected}}{=}\mathbb{E}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}})<\infty$, i.e., $\displaystyle\mathcal{P}$ is PAST. ∎

Example 25 (Termination of Variations of $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$)

We showed already in Sect. 4.2 that the drift of the program $\displaystyle\mathcal{P}^{\mathit{rdw}}_{race}$ in Ex. 5 is $\displaystyle-\tfrac{3}{2}<0$. So by Thm. 4.2 this program is PAST, i.e., the hare is expected to overtake the tortoise in a finite number of iterations.

Now consider the modified program $\displaystyle\mathcal{P}$:

[TABLE]

The distance still increases with probability $\displaystyle\tfrac{6}{11}$ but it decreases by at most $\displaystyle 4$. Its drift is $\displaystyle\mu_{\mathcal{P}}=1\cdot\tfrac{6}{11}+0\cdot\tfrac{3}{11}+(-2)\cdot\tfrac{1}{11}+(-4)\cdot\tfrac{1}{11}=0$. Hence, on average the distance $\displaystyle x$ between the tortoise and the hare remains unchanged after each loop iteration. By Thm. 4.2 this program is AST but not PAST. Hence, the hare wins with probability $\displaystyle 1$, but the expected number of required loop iterations is infinite.

Finally, we change the probabilities to obtain the program $\displaystyle\mathcal{P}^{\prime}$:

[TABLE]

Its drift is $\displaystyle\mu_{\mathcal{P}^{\prime}}=1\cdot\tfrac{6}{11}+0\cdot\tfrac{3}{11}+\tfrac{1}{22}\cdot\sum\nolimits_{-4\leq j\leq-1}j=\tfrac{1}{11}>0$. Thus, $\displaystyle\mathcal{P}^{\prime}$ is not AST by Thm. 4.2. So there is a positive probability that the hare never catches up with the tortoise and the race takes forever.

See 2

Proof

If $\displaystyle\mathcal{P}$ has direct termination (i.e., $\displaystyle p^{\prime}\neq 0$), then $\displaystyle\mathcal{P}$ and $\displaystyle\mathcal{P}^{\mathit{rdw}}$ are PAST by Thm. 3.1. Otherwise, by Thm. 4.1 we can reduce the termination of $\displaystyle\mathcal{P}$ to the termination of $\displaystyle\mathcal{P}^{\mathit{rdw}}$ on inputs which are in the image of $\displaystyle\mathit{rdw}_{\mathcal{P}}$. Note that the termination behavior of $\displaystyle\mathcal{P}^{\mathit{rdw}}$ is the same for all $\displaystyle x>0$. Hence, to show that $\displaystyle\mathcal{P}$ is (P)AST iff $\displaystyle\mathcal{P}^{\mathit{rdw}}$ (P)AST, we prove that $\displaystyle\mathit{rdw}_{\mathcal{P}}$’s image also includes positive values. To see this, note that $\displaystyle\vec{a}\neq\vec{0}$ implies $\displaystyle\vec{a}\bullet\vec{a}>0$. Hence, for any natural number $\displaystyle u>\tfrac{b}{\vec{a}\bullet\vec{a}}$ we obtain $\displaystyle\mathit{rdw}_{\mathcal{P}}(u\cdot\vec{a})=u\cdot\vec{a}\bullet\vec{a}-b>\tfrac{b}{\vec{a}\bullet\vec{a}}\cdot\vec{a}\bullet\vec{a}-b=0$. ∎

0.D.3 Proofs for Sect. 4.3

We now show that for CP programs $\displaystyle\mathcal{P}$ without direct termination, one can not only decide termination, but the construction for the proof of Thm. 4.2 also directly yields asymptotically exact bounds on their expected runtime. More precisely, we show that $\displaystyle rt^{\mathcal{P}}_{x_{0}}$ is asymptotically linear whenever $\displaystyle\mathcal{P}$ is PAST (and we even provide actual upper and lower bounds). To prove this result, we use Wald’s Lemma from probability theory. Again, we first consider random walk programs and then use the reduction of Sect. 4.1 to lift our result to arbitrary CP programs.

Recall that if a stochastic process $\displaystyle\mathbf{Y}=(Y_{j})_{j\in\mathbb{N}}$ on a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ is i.i.d., then $\displaystyle\mathbb{E}(Y_{0})=\mathbb{E}(Y_{j})$ for all $\displaystyle j\in\mathbb{N}$. Thus, we obtain

[TABLE]

By Wald’s Lemma, a similar statement even holds if instead of the constant $\displaystyle c$ we use a random variable $\displaystyle T$, provided that $\displaystyle T$ is independent from the stochastic process $\displaystyle\mathbf{Y}$. We use a consequence of Wald’s Lemma where $\displaystyle T$ does not need to be independent from the whole process $\displaystyle\mathbf{Y}$ but for every $\displaystyle j$, the random variable $\displaystyle Y_{j}$ is independent of whether $\displaystyle T$ is greater or equal to $\displaystyle j+1$. The required independence can be expressed formally by demanding that $\displaystyle Y_{j}$ must be independent of $\displaystyle\mathbb{I}_{\{T\geq j+1\}}:\Omega\to\{0,1\}$, where $\displaystyle\mathbb{I}_{\{T\geq j+1\}}(\pi)=1$ if $\displaystyle T(\pi)\geq j+1$ and $\displaystyle\mathbb{I}_{\{T\geq j+1\}}(\pi)=0$ otherwise. Then, to compute $\displaystyle\mathbb{E}\left(\sum\nolimits_{0\leq j\leq T-1}Y_{j}\right)$, by Wald’s Lemma one can apply $\displaystyle\mathbb{E}$ to both $\displaystyle T$ and $\displaystyle Y_{n}$ separately, i.e., one can compute $\displaystyle\mathbb{E}(T)\cdot\mathbb{E}(Y_{0})$.

Lemma 8 (Consequence of Wald’s Lemma, cf. [21, Lemma

10.2(9)])

Let $\displaystyle\mathbf{Y}=(Y_{j})_{j\in\mathbb{N}}$ be a stochastic process on a probability space $\displaystyle(\Omega,\mathfrak{F},\mathbb{P})$ which is i.i.d. and let $\displaystyle T:\Omega\to\overline{\mathbb{N}}$ be a random variable. Define the random variable $\displaystyle(\sum\nolimits_{0\leq j\leq T-1}\!Y_{j})\!:\!\Omega\!\to\!\mathbb{R},\pi\mapsto\!\sum\nolimits_{0\leq j\leq T(\pi)-1}\!Y_{j}(\pi)$. If $\displaystyle\mathbb{E}(Y_{0})\!<\!\infty$, $\displaystyle\mathbb{E}(T)\!<\infty$, and the random variables $\displaystyle Y_{j}$ and $\displaystyle\mathbb{I}_{\{T\geq j+1\}}$ are independent for all $\displaystyle j\!\in\!\mathbb{N}$, then

[TABLE]

Proof

In [3, Thm. 17.7] it is shown that

[TABLE]

i.e., the expected value of $\displaystyle\sum\nolimits_{0\leq j\leq T-1}Y_{j}$ exists. The proof of Lemma 8 is similar to the proof of [21, Lemma (9) in Sect. 10.2], but it is done under different preconditions.

[TABLE]

[TABLE]

In our setting, we consider the stochastic process $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ from Lemma 7 and the termination time $\displaystyle T^{\mathcal{P}}$. When regarding $\displaystyle\mathbb{P}^{\mathcal{P}}_{x_{0}}$, $\displaystyle Y_{j}$ (i.e., the difference between the $\displaystyle(j+1)$-th and the $\displaystyle j$-th element of a run) is clearly not independent of the question whether the run already terminated in (or before) the $\displaystyle j$-th element. The reason is that under the probability measure $\displaystyle\mathbb{P}^{\mathcal{P}}_{x_{0}}$, the elements of a run do not change anymore after termination. However, Lemma 9 shows that when regarding $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$ instead, the independence requirement of Lemma 8 is fulfilled.

Lemma 9 (Independence of $\displaystyle Y_{j}^{\mathbb{Z}}$ and $\displaystyle\mathbb{I}_{\{T^{\mathcal{P}}\geq j+1\}}$)

Let $\displaystyle\mathbf{Y}^{\mathbb{Z}}=(Y_{j}^{\mathbb{Z}})_{j\in\mathbb{N}}$ be the stochastic process from Lemma 7. Then for any random walk program $\displaystyle\mathcal{P}$ without direct termination, any $\displaystyle x_{0}\in\mathbb{Z}$, and any $\displaystyle j\in\mathbb{N}$, the random variables $\displaystyle Y_{j}^{\mathbb{Z}}$ and $\displaystyle\mathbb{I}_{\{T^{\mathcal{P}}\geq j+1\}}$ are independent w.r.t. the probability measure $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}$.

Proof

We show that for any $\displaystyle x,y\in\mathbb{Z}$, we have

[TABLE]

Note that the left- and the right-hand side are both zero whenever $\displaystyle y\notin\{0,1\}$. Thus, it is enough to show the claim for $\displaystyle y=0$ and $\displaystyle y=1$.

Case 1: $\displaystyle y=0$

[TABLE]

[TABLE]

Case 2: $\displaystyle y=1$

[TABLE]

[TABLE]

Now we can use Lemma 8 to infer linear upper and lower bounds for the expected runtime if the random walk program $\displaystyle\mathcal{P}$ is PAST (i.e., if $\displaystyle\mu_{\mathcal{P}}<0$).

Theorem 0.D.1 (Bounds on the Expected Runtime of Random Walk Programs)

Let $\displaystyle\mathcal{P}$ be a random walk program as in Def. 5 without direct termination where $\displaystyle\mu_{\mathcal{P}}<0$. Then $\displaystyle rt_{x_{0}}^{\mathcal{P}}=0$ for $\displaystyle x_{0}\leq 0$ and for $\displaystyle x_{0}>0$, we have

[TABLE]

So for $\displaystyle x_{0}>0$, $\displaystyle\mathcal{P}$’s expected runtime is asymptotically linear, i.e., $\displaystyle rt_{x_{0}}^{\mathcal{P}}\in\Theta(x_{0})$.

Proof

All prerequisites are satisfied to apply Wald’s Lemma (Lemma 8) for the stochastic process $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ on the probability space $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}^{\mathcal{P}}_{x_{0}})$ and the termination time $\displaystyle T^{\mathcal{P}}$: By Lemma 7, $\displaystyle\mathbf{Y}^{\mathbb{Z}}$ is i.i.d. w.r.t.  $\displaystyle(\mathbb{Z}^{\omega},\mathfrak{F}^{\mathbb{Z}},\mathbf{P}^{\mathcal{P}}_{x_{0}})$ and $\displaystyle\mathbf{E}^{\mathbb{Z}}_{x_{0}}(Y_{0}^{\mathbb{Z}})=\mu_{\mathcal{P}}<\infty$. Since $\displaystyle\mu_{\mathcal{P}}<0$, Thm. 4.2 yields that $\displaystyle\mathcal{P}$ is PAST and hence $\displaystyle rt^{\mathcal{P}}_{x_{0}}=\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)<\infty$. By Lemma 6 this implies $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)=\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)<\infty$. Furthermore, $\displaystyle Y_{j}^{\mathbb{Z}}$ and $\displaystyle\mathbb{I}_{\{T^{\mathcal{P}}\geq j+1\}}$ are independent by Lemma 9. Thus, Lemma 8 yields

[TABLE]

Let the random variable $\displaystyle X_{T^{\mathcal{P}}}:\Omega\!\to\!\mathbb{Z}$ map every run $\displaystyle\pi$ to the first non-positive value in $\displaystyle\pi$, i.e., to the value of the program variable when $\displaystyle\mathcal{P}$ terminates, or 0 otherwise. So $\displaystyle X_{T^{\mathcal{P}}}(\pi)=X_{T^{\mathcal{P}}(\pi)}(\pi)$ if $\displaystyle T^{\mathcal{P}}(\pi)\!<\!\infty$ and $\displaystyle X_{T^{\mathcal{P}}}(\pi)=0$ if $\displaystyle T^{\mathcal{P}}(\pi)\!=\!\infty$.

To infer linear bounds on the expected value of the termination time $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(T^{\mathcal{P}})$ resp. $\displaystyle\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)$, we first infer bounds on $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})$. Clearly, we have $\displaystyle X_{T^{\mathcal{P}}}(\pi)\leq 0$ for every $\displaystyle\pi\in\Omega$ by the definition of the termination time and of $\displaystyle X_{T^{\mathcal{P}}}$. Hence, this implies $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})\leq 0$, i.e., $\displaystyle 0$ is an upper bound for $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})$.

To infer a lower bound for $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})$, note that if $\displaystyle x_{0}>0$, then for every run $\displaystyle\pi=\left\langle z_{0},\ldots,z_{j-1},z_{j},\ldots\right\rangle$ where $\displaystyle\mathbf{P}^{\mathcal{P}}_{x_{0}}(\mathit{Cyl}^{\mathbb{Z}}(\pi))=q^{\mathcal{P}}_{x_{0}}(\pi)>0$ and $\displaystyle z_{j}$ is the first non-positive value in $\displaystyle\pi$, we have $\displaystyle j\geq 1$ and $\displaystyle z_{j}$ is at most $\displaystyle k$ smaller than $\displaystyle z_{j-1}$. Thus, $\displaystyle z_{j-1}\geq 1$ implies $\displaystyle z_{j}\geq z_{j-1}-k\geq 1-k$. Hence, for all these runs we have $\displaystyle X_{T^{\mathcal{P}}}(\pi)=z_{j}\geq 1-k$. Moreover, for runs $\displaystyle\pi$ without non-positive values, we also have $\displaystyle X_{T^{\mathcal{P}}}(\pi)\geq 1-k$, since $\displaystyle X_{T^{\mathcal{P}}}(\pi)=0$ and since $\displaystyle\mu_{\mathcal{P}}<0$ implies $\displaystyle k\geq 1$. Thus, we obtain $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})\geq 1-k$ whenever $\displaystyle x_{0}>0$.

So to summarize, we get the following upper and lower bounds for $\displaystyle\mathbf{E}^{\mathcal{P}}_{x_{0}}(X_{T^{\mathcal{P}}})$ if $\displaystyle x_{0}>0$:

[TABLE]

Recall that for every $\displaystyle j\geq 0$ we have $\displaystyle X_{j}^{\mathbb{Z}}=X_{0}^{\mathbb{Z}}+\sum\nolimits_{0\leq u\leq j-1}Y_{u}^{\mathbb{Z}}$. Hence, we also have $\displaystyle X_{T^{\mathcal{P}}}=X_{0}^{\mathbb{Z}}+\sum\nolimits_{0\leq u\leq T^{\mathcal{P}}-1}Y_{u}^{\mathbb{Z}}$. This implies:

[TABLE]

Hence, by 18 we obtain $\displaystyle-\tfrac{1}{\mu_{\mathcal{P}}}\cdot x_{0}\;\leq\;\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)\;\leq\;-\tfrac{1}{\mu_{\mathcal{P}}}\cdot x_{0}+\tfrac{1-k}{\mu_{\mathcal{P}}}$ for any $\displaystyle x_{0}>0$. This implies the theorem, since $\displaystyle rt^{\mathcal{P}}_{x_{0}}=\mathbb{E}^{\mathcal{P}}_{x_{0}}\left(T^{\mathcal{P}}\right)$. ∎

See 4.3

Proof

The result directly follows from Thm. 4.1 and 0.D.1.

Appendix 0.E Proofs for Sect. 5

See 1

Proof

We use Rouché’s Theorem: For a univariate polynomial $\displaystyle a_{v}\cdot x^{v}+\ldots+a_{1}\cdot x+a_{0}$, if there is a number $\displaystyle w\in\mathbb{R}_{>0}$ and an index $\displaystyle u\in\mathbb{N}$ with $\displaystyle 0\leq u\leq v$ such that

[TABLE]

then the polynomial has exactly $\displaystyle u$ (possibly complex) roots (counted with multiplicity) of absolute value less than $\displaystyle w$.

We now apply Rouché’s Theorem to the characteristic polynomial and proceed by case analysis. First, we consider the case where $\displaystyle p^{\prime}>0$. Here, we choose $\displaystyle w=1$ and $\displaystyle u=k$. Then 19 becomes

[TABLE]

As $\displaystyle|p_{0}-1|=1-p_{0}$ and $\displaystyle|p_{j}|=p_{j}$ for all $\displaystyle j$, this is equivalent to

[TABLE]

which is true since $\displaystyle p^{\prime}>0$. So by Rouché’s Theorem, the characteristic polynomial $\displaystyle\chi_{\mathcal{P}}$ has $\displaystyle k$ roots $\displaystyle\lambda$ with $\displaystyle|\lambda|<1$.

However, we would like to conclude that there are no more than $\displaystyle k$ roots $\displaystyle\lambda$ with $\displaystyle|\lambda|\leq 1$. Thus, we still need to show that $\displaystyle\chi_{\mathcal{P}}$ has no root $\displaystyle\lambda$ with $\displaystyle|\lambda|=1$. Clearly, $\displaystyle 0=\chi_{\mathcal{P}}(\lambda)$ is equivalent to $\displaystyle 0=\sum\nolimits_{-k\leq j\leq m}p_{j}\cdot\lambda^{k+j}-\lambda^{k}$. If $\displaystyle|\lambda|=1$ were true, then $\displaystyle 1=\sum\nolimits_{-k\leq j\leq m}p_{j}\cdot\lambda^{j}$ and

[TABLE]

by using $\displaystyle|p_{j}|=p_{j}$. However, this is a contradiction to $\displaystyle p^{\prime}>0$.

Now we consider the case where $\displaystyle p^{\prime}=0$ and thus $\displaystyle\sum\nolimits_{-k\leq j\leq m}p_{j}=1$. Our goal is to show that for all small enough $\displaystyle\varepsilon>0$, the inequality 19 holds if we set $\displaystyle w=1+\varepsilon$ and $\displaystyle u=k$. Then 19 becomes

[TABLE]

As $\displaystyle|p_{0}-1|=1-p_{0}$, $\displaystyle w=1+\varepsilon$, and $\displaystyle|p_{j}|=p_{j}$ for all $\displaystyle j$, this is equivalent to

[TABLE]

Note that555This notation means that $\displaystyle(1+\varepsilon)^{j}=1+j\cdot\varepsilon+f(\varepsilon)$ for a function $\displaystyle f$ with $\displaystyle f(x)\in\mathcal{O}(x^{2})$. Here, $\displaystyle k$, $\displaystyle m$, and the $\displaystyle p_{j}$ are considered to be constants, i.e., we write $\displaystyle\mathcal{O}(\varepsilon^{2})$ instead of $\displaystyle(1-p_{0})\cdot\mathcal{O}(\varepsilon^{2})$ or $\displaystyle\sum\nolimits_{-k\leq j\leq m,\;j\neq 0}p_{j}\cdot\mathcal{O}(\varepsilon^{2})$. $\displaystyle(1+\varepsilon)^{j}=1+j\cdot\varepsilon+\mathcal{O}(\varepsilon^{2})$ for any $\displaystyle j\geq 0$. Hence, we obtain

[TABLE]

By using $\displaystyle\sum\nolimits_{-k\leq j\leq m}p_{j}=1$, this simplifies to

[TABLE]

When dividing by $\displaystyle\varepsilon>0$, we get

[TABLE]

To satisfy this, it is sufficient to have

[TABLE]

This is equivalent to

[TABLE]

Since $\displaystyle\mu_{\mathcal{P}}<0$ as $\displaystyle\mathcal{P}$ is PAST (cf. Thm. 4.2), this is true for all sufficiently small $\displaystyle\varepsilon$. Hence, there are exactly $\displaystyle k$ roots of absolute value less than $\displaystyle 1+\varepsilon$, where $\displaystyle\varepsilon$ is sufficiently small, so in particular $\displaystyle k$ roots of absolute value $\displaystyle\leq 1$. ∎

See 2

Proof

To encode the requirement on the $\displaystyle a_{j,u}$, we modify (5) into a new constraint (20) which ensures $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$. More precisely, this new constraint (20) is a recurrence equation such that the characteristic polynomial $\displaystyle\chi_{0}$ of its homogeneous part has all the roots of $\displaystyle\chi_{\mathcal{P}}$ except those whose absolute value is greater than 1, i.e., $\displaystyle\chi_{0}(\lambda)=\prod\nolimits_{1\leq j\leq c,\;|\lambda_{j}|\leq 1}(\lambda-\lambda_{j})^{v_{j}}$. Thus, we can define the coefficients $\displaystyle q_{j}\in\mathbb{C}$ by

[TABLE]

Note that the degree of the polynomial $\displaystyle\chi_{0}$ is indeed $\displaystyle k$, because by Lemma 1 we have $\displaystyle\sum\nolimits_{1\leq j\leq c,\;|\lambda_{j}|\leq 1}v_{j}=k$.

Moreover, the constant add-on of the new recurrence equation is constructed in such a way that the particular solutions $\displaystyle C_{const}$ resp. $\displaystyle C_{lin}\cdot x$ of (5) are also solutions of the inhomogeneous recurrence equation. Thus, let $\displaystyle D_{const}=C_{const}\cdot\left(1-\sum\nolimits_{-k\leq j\leq-1}q_{j}\right)$ and $\displaystyle D_{lin}=-C_{lin}\cdot\sum\nolimits_{-k\leq j\leq-1}j\cdot q_{j}$. Instead of (5), we now consider the constraint

[TABLE]

where we choose $\displaystyle D=D_{const}$ if $\displaystyle p^{\prime}>0$ and $\displaystyle D=D_{lin}$ if $\displaystyle p^{\prime}=0$. We show the following two claims:

1. (a)

There is exactly one function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ which satisfies 4 and 20. 2. (b)

A function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ satisfies 20 iff $\displaystyle f$ satisfies 5 (thus, it has the form (9)) where $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$.

These two claims imply the statement of the lemma. To see this, note that by (a) there exists a function which satisfies 4 and 20 and by (b) this function also satisfies 5 and it has $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$. This function is unique, because if there were two different functions $\displaystyle f_{1}$ and $\displaystyle f_{2}$ that satisfy 4 and 5 and have $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$, then by (b) these two functions would also both satisfy 20. But this would be a contradiction to the uniqueness stated in (a).

We now prove the claims (a) and (b). For (a), note that the recurrence equation (20) is formulated in such a way that $\displaystyle f(x)$ only depends on the values of $\displaystyle f$ on the smaller values $\displaystyle x-1,\ldots,x-k$ (i.e., it is a recurrence of order $\displaystyle k$). By the constraint (4), the initial value of $\displaystyle f$ on negative values is uniquely determined (i.e., $\displaystyle f(0)=f(-1)=\ldots=f(-k+1)=0$). Hence, by induction on $\displaystyle x$, one can easily prove that there is a single unique function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ that satisfies both (4) and (20).

For the claim (b), we only have to show that $\displaystyle C_{const}$ is a solution of the inhomogeneous recurrence equation 20 if $\displaystyle p^{\prime}>0$ and $\displaystyle C_{lin}\cdot x$ is a solution of 20 if $\displaystyle p^{\prime}=0$. Once this is shown, it is clear that all solutions of 20 result from adding the particular solution $\displaystyle C_{const}$ resp. $\displaystyle C_{lin}\cdot x$ of the inhomogeneous equation to a solution of the homogeneous variant of 20 (where $\displaystyle D$ is replaced by 0). Any solution of this homogeneous variant can be represented as a linear combination of the solutions $\displaystyle\lambda_{j}^{x}\cdot x^{u}$ where $\displaystyle|\lambda_{j}|\leq 1$ and $\displaystyle u\in\{0,\ldots,v_{j}-1\}$. That these are linearly independent solutions of the homogeneous variant of 20 follows from the fact that $\displaystyle\chi_{0}$ is the corresponding characteristic polynomial. Thus, the solutions of 20 are all functions of the form (9) where $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$, which proves (b).

It remains to show that $\displaystyle C_{const}$ resp.  $\displaystyle C_{lin}\cdot x$ are particular solutions of the inhomogeneous recurrence equation 20. If $\displaystyle p^{\prime}>0$, then the definition of $\displaystyle D_{const}$ indeed implies $\displaystyle C_{const}=C_{const}\cdot\sum\nolimits_{-k\leq j\leq-1}q_{j}+D_{const}$. If $\displaystyle p^{\prime}=0$, then we have to show

[TABLE]

Since 1 is a root of $\displaystyle\chi_{\mathcal{P}}$ (i.e., one of the $\displaystyle\lambda_{j}$ with $\displaystyle|\lambda_{j}|\leq 1$ is $\displaystyle\lambda_{j}=1$), 1 is also a root of $\displaystyle\chi_{0}$. So we have $\displaystyle 0=\chi_{0}(1)=1-\sum\nolimits_{-k\leq j\leq-1}q_{j}$, which implies $\displaystyle\sum\nolimits_{-k\leq j\leq-1}q_{j}=1$. So (21) is equivalent to

[TABLE]

This holds due to the definition of $\displaystyle D_{lin}$. ∎

See 5.1

Proof

By Thm. 2.1, the expected runtime $\displaystyle rt^{\mathcal{P}}_{x}$ is the least fixpoint of the expected runtime transformer $\displaystyle\mathcal{L}^{\mathcal{P}}$, i.e., the smallest function $\displaystyle f(x):\mathbb{Z}\to\overline{\mathbb{R}_{\geq 0}}$ which satisfies 3, or equivalently, the smallest function which satisfies 4 and 5.

Since $\displaystyle f$ satisfies 5, it is a function of the form 9, i.e., there exist coefficients $\displaystyle a_{j,u}\in\mathbb{C}$ such that for all $\displaystyle x>-k$ we have

[TABLE]

If we had $\displaystyle a_{j,u}\not=0$ for a coefficient where $\displaystyle|\lambda_{j}|>1$, then $\displaystyle f(x)$ would not be bounded by a constant (if $\displaystyle p^{\prime}>0$) resp. by a linear function (if $\displaystyle p^{\prime}=0$). Thus, this would contradict Thm. 3.1 (if $\displaystyle p^{\prime}>0$) resp.  Thm. 4.3 (if $\displaystyle p^{\prime}=0$).

By Lemma 2 there is a single unique function $\displaystyle f:\mathbb{Z}\to\mathbb{C}$ which satisfies both 4 and 5 and has $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$. So this function must be the expected runtime (and hence, it maps any integer to a non-negative real number). Due to 5 the function must be of the form 9 for all $\displaystyle x>-k$ but at the same time it also has to satisfy $\displaystyle f(x)=0$ for all $\displaystyle x\leq 0$ due to 4. Therefore, it must satisfy the linear equations (11). On the other hand, the linear equations (11) cannot have more than one solution because otherwise this would yield two different functions that satisfy both 4 and 5 and have $\displaystyle a_{j,u}=0$ whenever $\displaystyle|\lambda_{j}|>1$, in contradiction to Lemma 2.

If $\displaystyle k=0$, then $\displaystyle p^{\prime}>0$ as $\displaystyle\mathcal{P}$ is PAST. Lemma 1 implies that $\displaystyle\chi_{\mathcal{P}}$ has no root with $\displaystyle|\lambda|\leq 1$ and thus, $\displaystyle rt^{\mathcal{P}}_{x}=C_{const}+\sum\nolimits_{1\leq j\leq c,\;|\lambda_{j}|\leq 1}\ldots=C_{const}$ for $\displaystyle x>0$. ∎

See 3

Proof

If $\displaystyle\mathcal{P}$ is trivial, then its expected runtime is obvious. Otherwise, by Cor. 2 one can decide if $\displaystyle\mathcal{P}$ is PAST and in that case, $\displaystyle\mathcal{P}^{\mathit{rdw}}$ is PAST as well. For any CP program $\displaystyle\mathcal{P}$, we have $\displaystyle rt_{\vec{x}}^{\mathcal{P}}=rt_{\mathit{rdw}_{\mathcal{P}}(\vec{x})}^{\mathcal{P}^{\mathit{rdw}}}$ due to Thm. 4.1. As $\displaystyle rt_{\mathit{rdw}_{\mathcal{P}}(\vec{x})}^{\mathcal{P}^{\mathit{rdw}}}$ can be computed exactly by Thm. 5.1, this also holds for $\displaystyle rt_{\vec{x}}^{\mathcal{P}}$. ∎

As mentioned in Sect. 5, Thm. 5.1 and 3 imply that for any $\displaystyle\vec{x}_{0}\in\mathbb{Z}^{r}$, the expected runtime $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}$ of a CP program $\displaystyle\mathcal{P}$ that is PAST and has only rational probabilities $\displaystyle p_{\vec{c}_{1}},\ldots,p_{\vec{c}_{n}},p^{\prime}\in\mathbb{Q}$ is always an algebraic number. This is due to the fact that $\displaystyle rt^{\mathcal{P}}_{\vec{x}_{0}}$ can be represented as a linear combination of algebraic numbers (the roots of the characteristic polynomial $\displaystyle\chi_{\mathcal{P}^{\mathit{rdw}}}$). The coefficients of this linear combination are the solution of a linear equation system 11 over algebraic numbers and hence, they are algebraic numbers themselves. Therefore, one could also compute a closed form for the exact expected runtime $\displaystyle rt^{\mathcal{P}}_{\vec{x}}$ using a representation with algebraic numbers instead of numerical approximations.

As also discussed in Sect. 5, while the exact computation of the expected runtime of a random walk program $\displaystyle\mathcal{P}$ according to Thm. 5.1 may yield a representation of $\displaystyle rt^{\mathcal{P}}_{x}$ with possibly complex number, one can easily obtain a more intuitive representation of $\displaystyle rt^{\mathcal{P}}_{x}$ that uses real numbers only.

As stated before, for any coefficients $\displaystyle a_{j,u},a_{j,u}^{\prime}\in\mathbb{C}$ with $\displaystyle j\in\{s+1,\ldots,s+t\}$ and $\displaystyle u\in\{0,\ldots,v_{j}-1\}$ there exist coefficients $\displaystyle b_{j,u}$ and $\displaystyle b_{j,u}^{\prime}$ such that

[TABLE]

holds for all $\displaystyle x\in\mathbb{Z}$. More precisely, $\displaystyle b_{j,u}=a_{j,u}+a_{j,u}^{\prime}$ and $\displaystyle b_{j,u}^{\prime}=(a_{j,u}-a_{j,u}^{\prime})\cdot i$. So any linear combination of the functions $\displaystyle\lambda_{j}^{x}\cdot x^{u}$ and $\displaystyle\overline{\lambda_{j}}^{x}\cdot x^{u}$ can be replaced by a linear combination of the functions $\displaystyle\mathrm{Re}(\lambda_{j}^{x})\cdot x^{u}$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})\cdot x^{u}$. In this way, one obtains $\displaystyle k+m$ linearly independent real solutions of the corresponding homogeneous recurrence equation. Hence, by Thm. 5.1 we now get the representation of the expected runtime in (12):

[TABLE]

Since $\displaystyle rt^{\mathcal{P}}_{x}$ is real-valued, $\displaystyle\lambda_{j}^{x}\in\mathbb{R}$ for $\displaystyle j\in\{1,\ldots,s\}$, and $\displaystyle\mathrm{Re}(\lambda_{j}^{x}),\mathrm{Im}(\lambda_{j}^{x})\in\mathbb{R}$ for $\displaystyle j\in\{s+1,\ldots,s+t\}$, all $\displaystyle a_{j,u}$ for $\displaystyle j\in\{1,\ldots,s\}$ and all $\displaystyle b_{j,u},b_{j,u}^{\prime}$ for $\displaystyle j\in\{s+1,\ldots,s+t\}$ are real numbers. As $\displaystyle b_{j,u}=a_{j,u}+a_{j,u}^{\prime}$, this means that $\displaystyle a_{j,u}^{\prime}$ is the conjugate of $\displaystyle a_{j,u}$, i.e., $\displaystyle a_{j,u}^{\prime}=\overline{a_{j,u}}$ and thus, $\displaystyle b_{j,u}=2\cdot\mathrm{Re}(a_{j,u})$ and $\displaystyle b_{j,u}^{\prime}=-2\cdot\mathrm{Im}(a_{j,u})$.

As mentioned, to compute $\displaystyle\mathrm{Re}(\lambda_{j}^{x})$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})$, we consider the polar representation of the non-real roots $\displaystyle\lambda_{j}$, i.e., for $\displaystyle j\in\{s+1,\ldots,s+t\}$ let $\displaystyle\lambda_{j}=w_{j}\cdot e^{\theta_{j}\cdot i}$ with $\displaystyle w_{j}\in\mathbb{R}_{>0}$ and $\displaystyle\theta_{j}\in(0,2\pi)$. Then $\displaystyle\lambda_{j}^{x}=w_{j}^{x}\cdot e^{\theta_{j}\cdot i\cdot x}$, and $\displaystyle\mathrm{Re}(\lambda_{j}^{x})=w^{x}_{j}\cdot\cos(\theta_{j}\cdot x)$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})=w^{x}_{j}\cdot\sin(\theta_{j}\cdot x)$.

Note that in Sect. 5.2, one could also already use the representation in 12 with $\displaystyle\mathrm{Re}(\lambda_{j}^{x})=w^{x}_{j}\cdot\cos(\theta_{j}\cdot x)$ and $\displaystyle\mathrm{Im}(\lambda_{j}^{x})=w^{x}_{j}\cdot\sin(\theta_{j}\cdot x)$ here. Then one would only have to solve a system of linear equations over the reals and can compute $\displaystyle b_{j,u}$ and $\displaystyle b_{j,u}^{\prime}$ directly.