Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time

TL;DR

This paper introduces a sound, automated, martingale-based method for proving the expected sensitivity of probabilistic programs with randomized, input-dependent termination times, extending previous fixed-iteration approaches.

Contribution

It extends expected sensitivity analysis to probabilistic while loops with randomized termination, providing a compositional, automated, martingale-based proof technique.

Findings

Effective on classical examples like Gambler's Ruin and stochastic gradient descent

Automated approach handles various probabilistic programs from literature

Demonstrates soundness and compositionality of the method

Abstract

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.

Tables

Table 1. Table 1 . Overview of Expected Sensitivity Results and Their Prerequisites

Program	Type	Theorem	Prerequisites
non-expansive	expected	Theorem 5.5	basic prerequisites*
	affine-sensitivity
non-expansive	expected	Theorem 5.15	basic prerequisites*
	linear-sensitivity		additional prerequisites**
	expected		(Definition 2.1)
expansive	affine-sensitivity	Theorem 6.1	basic prerequisites*
			difference-bounded condition (Definition 5.12)

Table 2. Table 2 . Experimental Results for Expected Affine-sensitivity (with ϵ = 1 italic-ϵ 1 \epsilon=1 , L = 1 𝐿 1 L=1 )

Example	Time/sec	$\eta \left(𝐛\right)$	$K$	$d$	$M$
mini-Roulette	5.97	$13\cdot x-13$	-13	11	13
rdwalk	3.91	$-5\cdot x+5000$	-5	1	5
prdwalk variant	4.88	$-0.2857\cdot x+285.7$	-1.429	5	$0.2857$
prspeed	4.31	$-1.7143\cdot x+1714.3$	$-5.143$	3	$1.7143$
race variant	5.43	$-1.43\cdot h+1.43\cdot t$	-4.29	4	2.86
ad. rdwalk 2D	4.55	$-0.77\cdot x+0.77\cdot y$	-2.31	3	1.54
ad. rdwalk 1D Variant	4.49	$2.86\cdot x$	-2.86	2	2.86
American Roulette	7.66	$20.27\cdot x-20.27$	-20.27	35	20.27

Table 3. Table 3 . Experimental Results for Expected Linear-sensitivity (with ϵ = 1 italic-ϵ 1 \epsilon=1 , L = 1 𝐿 1 L=1 )

Example	Time/sec	$\eta \left(𝐛\right)$	$K$	$d$	$M$	$c$
mini-roulette variant	12.69	$2.45\cdot x-2.45$	-4.91	9	2.45	22.08
single-room heating	5.21	$-0.833\cdot x+16.67$	-1.25	2.1	0.833	1.75
double-room heating	5.64	$-2.27\cdot x_1+45.45$	-3.41	2.87	2.27	6.518
rdwalk variant	4.44	$-2.5\cdot x+2500$	-7.5	3	2.5	7.5
prdwalk	4.46	$-0.5714\cdot x+571.4$	-2.86	5	$0.5714$	2.86
prspeed variant	5.00	$-0.5333\cdot x+533.3$	-2.67	5	$0.5333$	2.67
race	5.17	$-2\cdot h+2\cdot t$	-6	4	4	6
simple while loop	3.59	$-2\cdot x+2000$	-2	1	2	2
pollutant disposal	4.87	$n-5$	-3	3	1	3
ad. rdwalk 2D variant	6.07	$-0.606\cdot x+0.606\cdot y$	-2.424	4	1.212	2.424
ad. rdwalk 1D	5.16	$1.11\cdot x$	-2.22	2	1.11	2.22
American roulette variant	14.95	$2.08\cdot x-2.08$	-4.15	35	2.08	72.63

Equations

$$\text{while }\Phi \text{ do if }b\text{ then }P\text{ else }Q\text{ od}$$

$$\text{while}\Phi \text{do}P\text{od}$$

$$D_1\cdot \Vert \mathbf{b}-{\mathbf{b}}^{\prime }{\Vert }_{\infty }\le \mathfrak{d}(\mathbf{b},{\mathbf{b}}^{\prime })\le D_2\cdot \Vert \mathbf{b}-{\mathbf{b}}^{\prime }{\Vert }_{\infty }.$$

$$\text{mbox}if\mathfrak{d}(\mathbf{b},{\mathbf{b}}^{\prime })\le \theta \text{mbox}then|{\mathbb{E}}_{\mathbf{b}}(Z)-{\mathbb{E}}_{{\mathbf{b}}^{\prime }}(Z^{\prime })|\le A\cdot \mathfrak{d}(\mathbf{b},{\mathbf{b}}^{\prime })+B$$

$$x_i(k+1)=x_i(k)+b_i(x_a-x_i(k))+{\sum }_{i\ne j}{a}_{ij}(x_j(k)-x_i(k))+c_i+w_i(k)$$

$$|{\mathbb{E}}_{{\mathbf{b}}_n}(Z_{{\mathbf{b}}_n})-{\mathbf{b}}_n[z]|\le {\mathbb{E}}_{{\mathbf{b}}_n}(|{\mathbf{b}}_n[z]-Z_{{\mathbf{b}}_n}|)\le {\mathbb{E}}_{{\mathbf{b}}_n}\left(\frac{d}{D_1}\cdot T_{{\mathbf{b}}_n}\right)\le \frac{d}{D_1}\cdot \frac{\eta ({\mathbf{b}}_n)-K}{ϵ}.$$

$$|{\mathbb{E}}_{{\mathbf{b}}_n}(Z_{{\mathbf{b}}_n})-{\mathbb{E}}_{{\mathbf{b}}_n^{\prime }}(Z_{{\mathbf{b}}_n^{\prime }})|$$

$$(1-p)\cdot A_{\infty }+C+p\cdot A_0\le A_1$$

$$(1-p)\cdot A_{\infty }+C+p\cdot A_1\le A_2$$

$$⋮$$

$$(1-p)\cdot A_{\infty }+C+p\cdot A_{n-1}\le A_n$$

$$D=A_0\le A_1\le \cdots \le A_n\le A_{\infty }$$

$${\mathbb{E}}_{z^{\prime }}(Z^{\prime })-{\mathbb{E}}_{z^{\prime \prime }}(Z^{\prime \prime })={\sum }_{n=1}^{\infty }\mathbb{P}(T=n)\cdot 3^n\cdot |z^{\prime }-z^{\prime \prime }|={\sum }_{n=1}^{\infty }{\left(\frac{3}{2}\right)}^n\cdot |z^{\prime }-z^{\prime \prime }|=\infty .$$

$$A:=2\cdot A^{\prime }\cdot L^N+2\cdot A^{\prime }\cdot L^N\cdot \exp \left(-\frac{ϵ\cdot \eta ({\mathbf{b}}^{\ast })}{8\cdot c^2}\right)\cdot {\sum }_{n=1}^{\infty }{\left(L\cdot \exp \left(-\frac{3\cdot {ϵ}^2}{8\cdot c^2}\right)\right)}^n$$

$$B:=2\cdot B^{\prime }+2\cdot B^{\prime }\cdot \exp \left(-\frac{ϵ\cdot \eta ({\mathbf{b}}^{\ast })}{8\cdot c^2}\right)\cdot {\sum }_{n=1}^{\infty }\exp \left(-\frac{3\cdot {ϵ}^2}{8\cdot c^2}\cdot n\right)$$

$$\begin{array}{cc}[l](A1)& \{(x,w)\mid x\ge 1\wedge w\ge 0\}\subseteq \{(x,w)\mid -a_1\cdot x-a_2\cdot w\le a_3\}\\ (A2)& \{(x,w)\mid x\ge 1\wedge w\ge 0\wedge x<2\}\subseteq \{(x,w)\mid K\le a_1\cdot (x-1)+a_2\cdot w+a_3\le 0\}\\ (A3)& \{(x,w)\mid x\ge 1\wedge w\ge 0\}\subseteq \{(x,w)\mid 0\le \frac{1}{13}{a}_1-\frac{4}{5}{a}_2-ϵ\}\end{array}$$

$$\begin{array}{cc}[l](A1)& \{(x,w)\mid x\ge 1\wedge w\ge 0\}\subseteq \{(x,w)\mid -a_1\cdot x-a_2\cdot w\le a_3\}\\ (A2)& \{\left((x,w),r_6\right)\mid x\ge 1\wedge w\ge 0\wedge x<3\}\subseteq \{\left((x,w),r_6\right)\mid K\le a_1\cdot (x-r_6)+a_2\cdot w+a_3\le 0\}\\ (A3)& \{(x,w)\mid x\ge 1\wedge w\ge 0\}\subseteq \{(x,w)\mid 0\le \frac{53}{130}{a}_1-\frac{4}{5}{a}_2-ϵ\}\end{array}$$

$$\begin{array}{ccc}[l](A4)& \{(x,w)\mid x\ge 1\wedge w\ge 0\}\subseteq & \{(x,w)\mid |a_1\cdot r_1+2a_2|\le c\wedge |a_2\cdot r_2+3a_2|\le c\wedge |a_3\cdot r_3+4a_2|\le c\\ & & \wedge |a_4\cdot r_4+5a_2|\le c\wedge |a_5\cdot r_5+6a_2|\le c\wedge |a_6\cdot r_6|\le c\}\end{array}$$

$$\eta (\mathbf{w}-\gamma \cdot \nabla G_i(\mathbf{w}))-\eta (\mathbf{w})$$

$$|(\nabla G(\mathbf{w})-\nabla G({\mathbf{w}}^{\prime }){)}^{\mathrm{T}}\cdot \gamma \cdot \nabla G_i(\mathbf{w})|$$

$${\mathbb{E}}_i(\eta (\mathbf{w}-\gamma \cdot \nabla G_i(\mathbf{w})))-\eta (\mathbf{w})=\frac{1}{n}\cdot {\sum }_{i=1}^n\left[\eta (\mathbf{w}-\gamma \cdot \nabla G_i(\mathbf{w}))-\eta (\mathbf{w})\right]=-\frac{\gamma }{n}\cdot \parallel \nabla G(\mathbf{w}){\parallel }_2^2+C$$

$$A_{\gamma }:=2\cdot A_{\gamma }^{\prime }\cdot L_{\gamma }^{N_{\gamma }}+2\cdot A^{\prime }\cdot L_{\gamma }^{N_{\gamma }}\cdot \exp \left(-\frac{ϵ\cdot \eta ({\mathbf{w}}^{\ast },{\vartheta }^{\ast })}{8\cdot c^2}\right)\cdot {\sum }_{n=1}^{\infty }{\left(L_{\gamma }\cdot \exp \left(-\frac{3\cdot {ϵ}^2}{8\cdot c^2}\right)\right)}^n$$

$$B_{\gamma }:=2\cdot B_{\gamma }^{\prime }+2\cdot B_{\gamma }^{\prime }\cdot \exp \left(-\frac{ϵ\cdot \eta ({\mathbf{w}}^{\ast },{\vartheta }^{\ast })}{8\cdot c^2}\right)\cdot {\sum }_{n=1}^{\infty }\exp \left(-\frac{3\cdot {ϵ}^2}{8\cdot c^2}\cdot n\right)$$

$$L_{\gamma }^{N_{\gamma }}=(1+C\cdot \gamma {)}^{\lfloor 4\cdot \frac{\eta ({\mathbf{w}}^{\ast },{\vartheta }^{\ast })}{M_1\cdot \gamma }\rfloor +1}\le (1+C\cdot \gamma {)}^{4\cdot \frac{\eta ({\mathbf{w}}^{\ast },{\vartheta }^{\ast })}{M_1\cdot \gamma }+1}\le e^{4\cdot \frac{C}{M_1}\cdot \eta ({\mathbf{w}}^{\ast },{\vartheta }^{\ast })}\cdot (1+C\cdot \gamma ).$$

$$⟨stmt⟩$$

$$\mid ⟨stmt⟩\text{‘;’}⟨stmt⟩\mid \text{mbox}‘{while}^{\prime }⟨bexpr⟩\text{‘do’}⟨stmt⟩\text{‘od’}\text{vspace}\text{baselineskip}$$

$$\displaystyle\mid\mbox{`{if}'}\,\mbox{`{prob}' `('$p$`)'}\,\mbox{`{then}'}\,\langle\mathit{stmt}\rangle\,\mbox{`{else}'}\,\langle\mathit{stmt}\rangle\,\mbox{`{fi}'}$$

$$⟨bexpr⟩$$

$$\mid ⟨bexpr⟩\text{mbox}‘{or}^{\prime }⟨bexpr⟩\mid ⟨bexpr⟩\text{mbox}‘{and}^{\prime }⟨bexpr⟩$$

$${\mathbb{E}}_{\mathbf{b}}(Z_{\mathbf{b}})=\int \sum _{\ell \in \mathbf{L}}{p}_{\ell }\cdot {\mathbb{E}}_{F(\ell ,\mathbf{b},\mathbf{r})}(Z_{F(\ell ,\mathbf{b},\mathbf{r})})\mathrm{d}\mathbf{r}$$

$${\mathbb{E}}_{\mathbf{b}}(Z_{\mathbf{b}})=$$

$$(\text{mbox}bythedefinitionofexpectation)$$

$$=$$

$$(\text{mbox}byunrollingtherun\omega \text{mbox}into(\ell ,\mathbf{r})\circ {\omega }^{\prime })$$

$$=$$

$$(\text{mbox}byFubin{i}^{\prime }sTheorem)$$

$$=$$

$$(\text{mbox}bythedefinitionofexpectation)$$

$$=$$

Full text

††doi: ††copyright: none††ccs: Software and its engineering General programming languages††ccs: Social and professional topics History of programming languages

1. Introduction

Continuity properties of systems. Continuity property for systems requires that the change in the output is bounded by a monotone function of the change in the input. Analysis of continuity properties are of great interest in program and reactive system analysis, such as: (a) robustness of numerical computations; (b) analysis of sensitivity of numerical queries (Dwork and Roth, 2014) in databases; (c) analysis of stability of learning algorithms (Bousquet and Elisseeff, 2002); and (d) robustness analysis of programs (Chaudhuri et al., 2010).

Probabilistic systems. Continuity analysis is relevant for probabilistic systems in a similar way, where the notion of continuity is extended with expectation to average over the probabilistic behaviours of the system. For example, statistical notions of differential privacy (Dwork et al., 2006); robustness analysis of Markov chains, Markov decision processes, and stochastic games (Aldous, 1983; Fu, 2012; van Breugel and Worrell, 2006; Desharnais et al., 2004; Chatterjee, 2012); stability analysis of randomized learning algorithms (Bousquet and Elisseeff, 2002; Hardt et al., 2016); all fall under the umbrella of continuity analysis of probabilistic systems.

Program sensitivity. A particular interest among continuity is *program sensitivity

• which specifies that the change in the output of a program is proportional to the change in the input. Formally, there is a constant $L$ (the Lipschitz constant) such that if the input changes by an amount $x$, then the change in the ouput is at most $L\cdot x$. In this work we consider the expected sensitivity of probabilistic programs given as (sequential composition of) probabilistic while loops.

Previous results. The expected sensitivity analysis of probabilistic programs was first considered in (Bousquet and Elisseeff, 2002; Hardt et al., 2016) for machine-learning algorithms such as stochastic gradient descent, through manual proofs. Then  (Barthe et al., 2018) proposed an elegant method based on a relational program logic framework. The heart of the analysis technique is coupling-based methods, and the approach is shown to work effectively on several examples from machine learning to statistical physics. A recent result (Huang et al., 2018b) implemented a computer-algebra based tool that calculates tight sensitivity bounds for probabilistic programs. Although these previous approaches address the expected sensitivity analysis well, they work only on examples of probabilistic while loops whose number of iterations is fixed and bounded (i.e., the number of iterations is fixed to a given number $T$). In reality, many examples of probabilistic while loops do not have fixed number of iterations, rather the number of iterations is randomized and depends on the input values. Hence, such examples cannot be handled by the previous approaches. In this work, we focus on expected sensitivity analysis of such programs.

Our contributions. Our main contributions are as follows:

1. (1)

We present a sound approach for proving expected sensitivity of probabilistic while loops whose number of iterations is randomized and depends on the initial input values. 2. (2)

We show that our approach is compositional w.r.t sequential composition. 3. (3)

In contrast to the previous coupling and computer-algebra based approaches, our approach relies on ranking supermartingales (RSMs) (see (Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2018c)), a central notion in proving termination properties of probabilistic programs. 4. (4)

Since RSM based approaches can be automated through constraint solving (see e.g. (Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2018c)), the same results in conjunction with our sound approach present an automated approach for sensitivity analysis of probabilistic programs. 5. (5)

We demonstrate the effectiveness of our approach through (i) a case study on stochastic gradient descent and (ii) experimental results on various probabilistic programs from the literature, including Gambler’s Ruin, stochastic hybrid systems, random walks, etc.

Technical contribution. In terms of technical contribution there are key differences between our result and the previous results. The previous approaches are either coupling-based proof rules, or through computer-algebra tools, and all of them are restricted to loops with a fixed number of loop iterations. In contrast, our approach is based on RSMs and can handle loops whose number of iterations is randomized and depends on the input. Moreover, we prove the non-trivial fact that our approach is compositional under sequential composition. Furthermore, as RSM-synthesis algorithms have been well-established in the literature, our sound approach directly lead to automated algorithms for proving expected sensitivity of probabilistic programs.

Limitation. Our approach mainly focuses on (sequential composition of) probabilistic while loops where there is no conditional branch. Although the exclusion of conditional branches makes our contribution seemingly restrictive, we argue that typically inclusion of conditional branches will break sensitivity properties in general. Consider a loop of the form

[TABLE]

where the programs $P,Q$ perform completely different executions. Then two close-by program inputs $x_{1},x_{2}\models\Phi$ such that () $x_{1}\models b$ but $x_{2}\not\models b$ will lead to values that differ significantly after just one loop iteration. Thus, irrespective of analysis methods this type of programs has bad sensitivity property. Previous results also reflect the difficulty on handling conditional branches. For example, in previous approaches such as (Barthe et al., 2018; Aguirre et al., 2019), it must be manually ensured that the conditions of all conditional branches are either (i) both satisfied or (ii) both not satisfied by two close-by program valuations (i.e., the situation () above not allowed) (see (Barthe et al., 2018, Figure 3) and (Aguirre et al., 2019, Figure 1)). Moreover, in all the experimental examples from (Huang et al., 2018b), conditional-branches within for-loops are either restricted to a finite set of values or directly transformed into probabilistic branches. For a possible extension to conditional branches see Remark 5.

2. Probabilistic Programs

We first present the syntax and semantics of our probabilistic programming language, then define the syntactical subclass of simple while loops to which our approach applies. Throughout the paper, we denote by $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{R}$ the sets of all natural numbers, integers, and real numbers, respectively.

The Syntax. Our probabilistic programming language is imperative and consists of statements. We present a succinct description below (see Appendix A for the detailed syntax).

• •

Variables. Expressions $\langle\mathit{pvar}\rangle$ (resp. $\langle\mathit{rvar}\rangle$) range over program (resp. sampling) variables, respectively. Program variables are normal variables that control the flow of the program, while each sampling variable is a special variable whose value is sampled from a fixed predefined probability distribution each time the variable is accessed in the program.

• •

Constants. Expressions $\langle\mathit{const}\rangle$ range over decimals.

• •

Arithmetic Expressions. Expressions $\langle\mathit{expr}\rangle$ (resp. $\langle\mathit{pexpr}\rangle$) range over arithmetic expressions over both program and sampling variables (resp. program variables only). For example, if $x,y$ are program variables and $r$ is a sampling variable, then $x+3\cdot y$ is an instance of $\langle\mathit{pexpr}\rangle$ and $x-y+2\cdot r$ is an instance of $\langle\mathit{expr}\rangle$. In this paper, we consider a general setting of arithmetic expressions and do not fix a detailed syntax for $\langle\mathit{expr}\rangle$ and $\langle\mathit{pexpr}\rangle$.

• •

Boolean Expressions. Expressions $\langle\mathit{bexpr}\rangle$ are boolean expressions over program variables, for which atomic propositions are comparisons between expressions from $\langle\mathit{pexpr}\rangle$ and general expressions are built from atomic propositions and propositional operators.

• •

Statements $\langle\mathit{stmt}\rangle$. Assignment statements are indicated by ‘$:=$’; ‘skip’ is the statement that does nothing; Standard conditional branches are indicated by the keyword ‘if’ with its then- and else-branches, and a boolean expression that serves as the condition for the conditional branch. Probabilistic choices are modelled as probabilistic branches with the key word “if prob$(p)$” that lead to the then-branch with probability $p$ and to the else-branch with probability $1-p$. While-loops are indicated by the keyword ‘while’ with a boolean expression as the loop guard. Finally, sequential compositions are indicated by semicolons.

Note that probabilistic branches can be implemented as a sampling of Bernoulli distribution followed by a conditional branch, but for algorithmic purpose we consider probabilistic branches directly. In this work, we consider probabilistic programs without non-determinism.

The Semantics. To define the semantics, we first recall several standard notions from probability theory as follows (see e.g. standard textbooks (Williams, 1991; Billingsley, 1995) for details).

Probability Spaces. A probability space is a triple $(\Omega,\mathcal{F},\mathbb{P})$, where $\Omega$ is a nonempty set (so-called sample space), $\mathcal{F}$ is a sigma-algebra over $\Omega$ (i.e., a collection of subsets of $\Omega$ that contains the empty set $\emptyset$ and is closed under complementation and countable union), and $\mathbb{P}$ is a probability measure on $\mathcal{F}$, i.e., a function $\mathbb{P}\colon\mathcal{F}\rightarrow[0,1]$ such that (i) $\mathbb{P}(\Omega)=1$ and (ii) for all set-sequences $A_{1},A_{2},\dots\in\mathcal{F}$ that are pairwise-disjoint (i.e., $A_{i}\cap A_{j}=\emptyset$ whenever $i\neq j$) it holds that $\sum_{i=1}^{\infty}\mathbb{P}(A_{i})=\mathbb{P}\left(\bigcup_{i=1}^{\infty}A_{i}\right)$. Elements in $\mathcal{F}$ are called events. An event $A\in\mathcal{F}$ is said to hold almost surely (a.s.) if $\mathbb{P}(A)=1$.

Random Variables. A random variable (r.v.) $X$ on a probability space $(\Omega,\mathcal{F},\mathbb{P})$ is an $\mathcal{F}$-measurable function $X\colon\Omega\rightarrow\mathbb{R}\cup\{-\infty,+\infty\}$, i.e., a function satisfying the condition that for all $d\in\mathbb{R}\cup\{-\infty,+\infty\}$, the set $\{\omega\in\Omega\mid X(\omega)<d\}$ belongs to $\mathcal{F}$. By convention, we abbreviate $+\infty$ as $\infty$.

Expectation. The expected value of a random variable $X$ on a probability space $(\Omega,\mathcal{F},\mathbb{P})$, denoted by $\mathbb{E}(X)$, is defined as the Lebesgue integral of $X$ w.r.t $\mathbb{P}$, i.e., $\mathbb{E}(X)\coloneqq\int X\,\mathrm{d}\mathbb{P}$; the precise definition of Lebesgue integral is somewhat technical and is omitted here (cf. (Williams, 1991, Chapter 5) for a formal definition). In the case that $\mbox{\sl ran}~{}X=\{d_{0},d_{1},\dots,d_{k},\dots\}$ is countable with distinct $d_{k}$’s, we have that $\mathbb{E}(X)=\sum_{k=0}^{\infty}d_{k}\cdot\mathbb{P}(X=d_{k})$.

To present the semantics, we also need the notion of valuations.

Valuations. Let $V$ be a finite set of variables with an implicit linear order over its elements. A valuation on $V$ is a vector $\mathbf{b}$ in $\mathbb{R}^{|V|}$ such that for each $1\leq i\leq|V|$, the $i$-th coordinate of $\mathbf{b}$, denoted by $\mathbf{b}[i]$, is the value for the $i$-th variable in the implicit linear order on $V$. For the sake of convenience, we write $\mathbf{b}[y]$ for the value of a variable $y$ in a valuation $\mathbf{b}$.

Program and Sampling Valuations. Let $V_{\mathrm{p}}$ (resp. $V_{\mathrm{r}}$) be the set of program (resp. sampling) variables appearing in a probabilistic program, respectively. A program valuation (or program state) is a valuation on $V_{\mathrm{p}}$. A sampling valuation is a valuation on $V_{\mathrm{r}}$. Given a program valuation $\mathbf{b}$ and a boolean expression $\Phi$, the satisfaction relation $\models$ is defined in the standard way so that we have $\mathbf{b}\models\Phi$ iff $\Phi$ holds when program variables in $\Phi$ are substituted by their corresponding values in $\mathbf{b}$.

Now we give a brief description of the semantics for probabilistic programs. We follow the standard operational semantics through Markov chains. Given a probabilistic program (without non-determinism), its semantics is given as a general state-space Markov chain (GSSMC) (Meyn and Tweedie, 1993, Chapter 3), where (i) the state space consists of all pairs of program counters and program valuations for which the program counter refers to the next command to be executed and the program valuation specifies the current values for the program variables, and (ii) the kernel function that specifies the stochastic transitions between states is given by the individual commands in the program. For any initial state $\mathfrak{c}=({\mathsf{in}},\mathbf{b})$ where ${\mathsf{in}}$ is the program counter of the first command and $\mathbf{b}$ is the input program valuation, each probabilistic program induces a unique probability space through its corresponding GSSMC, where the sample space consists of all infinite sequences of states in the GSSMC (as runs), the sigma-algebra is generated by all cylinder sets of runs induced by finite Cartisian products of measurable subsets of the state space, and the probability measure is uniquely determined by the kernel function and the initial state. The detailed semantics can be found in (Chatterjee et al., 2018c; Chakarov and Sankaranarayanan, 2013; Fu and Chatterjee, 2019).

Under our semantics, we denote by $\mathbb{P}_{\mathbf{b}}$ the probability measure for a probabilistic program with the input program valuation $\mathbf{b}$ (note that the program counter ${\mathsf{in}}$ is determined by the program), and by $\mathbb{E}_{\mathbf{b}}(-)$ the expectation under the probability measure $\mathbb{P}_{\mathbf{b}}$.

Simple While Loops. In this paper, we focus on (sequential composition of) simple probabilistic while loops and investigate sound approaches for proving expected sensitivity over such programs. A simple (probabilistic) while loop is of the form

[TABLE]

where $\Phi$ is the loop guard and the loop body $P$ is a program without nested while loops. As simple while loops are syntactically restricted, we present succinct notions for such programs.

Update Functions. Given a simple while loop in the form (1) with the disjoint sets $V_{\mathrm{p}}$ and $V_{\mathrm{r}}$ of program and sampling variables, we abstract away detailed executions of the loop body $P$ by an update function $F:\mathbf{L}\times\mathbb{R}^{|V_{\mathrm{p}}|}\times\mathbb{R}^{|V_{\mathrm{r}}|}\rightarrow\mathbb{R}^{|V_{\mathrm{p}}|}$ that describes the input-output relationship for one iteration of the loop body as follows. First, we let $\mathcal{L}$ be the set of all program counters that refer to a probabilistic branch (i.e., $\textbf{if prob}(p)~{}\dots$) in the loop body of $P$. Then we define $\mathbf{L}$ to be the set of all functions from $\mathcal{L}$ into the choices of branches (i.e., then- or else-branch). Informally, such a function specifies for each probabilistic branch in $P$ which branch is chosen in the current loop iteration. Finally, the update function $F$ simply gives the program valuation $F(\ell,\mathbf{b},\mathbf{r})$ after the current loop iteration given (i) an element $\ell\in\mathbf{L}$ that specifies the probabilistic choices for probabilistic branches, (ii) a program valuation $\mathbf{b}$ that specifies the values for program variables before the current loop iteration and (iii) a sampling valuation $\mathbf{r}$ that gives all the sampled values for the sampling variables in the current loop iteration. In this way, we abstract away the detailed execution within the loop body $P$ and represent it simply by an update function. Note that as the loop body $P$ does not involve nested while loops, one can compute its update function symbolically through a recursive algorithm on the structure of $P$.

Runs. We also simplify the notion of runs over simple while loops. A run for a loop in the form (1) is an infinite sequence $\{\mathbf{b}_{n}\}_{n\geq 0}$ of program valuations such that each $\mathbf{b}_{n}$ is the program valuation right before the $(n+1)$-th loop iteration. Note that if $\mathbf{b}_{n}\models\Phi$, then $\mathbf{b}_{n+1}=F(\ell_{n},\mathbf{b}_{n},\mathbf{r}_{n})$ where $\ell_{n}$ (resp. $\mathbf{r}_{n}$) specifies the probabilistic resolution to all the probabilistic branches (resp. the sampled values for the sampling variables) at the $(n+1)$-th loop iteration, respectively; otherwise, $\mathbf{b}_{n+1}=\mathbf{b}_{n}$.

Notations. To ease the use of notations, we always use $\mathbf{b}$ for a program valuation, $\mathbf{r}$ for a sampling valuation and $\ell$ for an element in $\mathbf{L}$, with possible super-/sub-scripts. Given a simple while loop $Q$ in the form (1), we always use $V_{\mathrm{p}}$ for its set of program variables, $V_{\mathrm{r}}$ for sampling variables, $F$ for the update function, $\Phi$ for the loop guard, and $P$ for the loop body. Moreover, we denote by ${\llbracket}{\Phi}{\rrbracket}$ the set $\{\mathbf{b}\mid\mathbf{b}\models\Phi\}$ of program valuations that satisfy the loop guard $\Phi$.

To reason about expected sensitivity of simple while loops, we require that the loop body is Lipschitz continuous. This requirement is standard and corresponds to the “$\eta$-expansiveness” introduced in (Hardt et al., 2016, Definition 2.3). This continuity condition needs the standard notion of metrics that measures the distance between two program valuations, as follows.

Metrics. A metric is a function $\mathfrak{d}:\mathbb{R}^{|V_{\mathrm{p}}|}\times\mathbb{R}^{|V_{\mathrm{p}}|}\rightarrow[0,\infty)$ that satisfies (i) $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})=0$ iff $\mathbf{b}=\mathbf{b}^{\prime}$, (ii) $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})=\mathfrak{d}(\mathbf{b}^{\prime},\mathbf{b})$ (symmetry) and (iii) $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime\prime})+\mathfrak{d}(\mathbf{b}^{\prime\prime},\mathbf{b}^{\prime})$ (triangle inequality). Informally, $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ is interpreted as the distance between the two program valuations. For example, we can define $\mathfrak{d}$ either through the max norm by $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime}):={\|}{\mathbf{b}-\mathbf{b}^{\prime}}{\|}_{\infty}$ where the max norm ${\|}{\centerdot}{\|}_{\infty}$ is given as ${\|}{\mathbf{b}^{\prime\prime}}{\|}_{\infty}:=\max_{z\in V_{\mathrm{p}}}|\mathbf{b}^{\prime\prime}[z]|$, or through the Euclidean norm by $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime}):={\|}{\mathbf{b}-\mathbf{b}^{\prime}}{\|}_{2}$ where ${\|}{\centerdot}{\|}_{2}$ is given as ${\|}{\mathbf{b}^{\prime\prime}}{\|}_{2}:=\sqrt{(\mathbf{b}^{\prime\prime})^{\mathrm{T}}\mathbf{b}^{\prime\prime}}$. In this paper, we consider metrics that are comparable with the max norm, i.e., there exist real constants $D_{1},D_{2}>0$ such that

[TABLE]

Note that the comparability is naturally satisfied for metrics derived from norms of finite dimension.

Below we describe the continuity of the loop body under a metric $\mathfrak{d}$.

Definition 2.1 (Lipschitz Continuity $L$ of the Loop Body).

We say that the loop body of a simple while loop in the form (1) is Lipschitz continuous if there exists a real constant $L>0$ such that

• (B1)

$\forall\ell\,\forall\mathbf{r}\,\forall\mathbf{b},\mathbf{b}^{\prime}\colon\left[\mathbf{b},\mathbf{b}^{\prime}\models\Phi\Rightarrow\mathfrak{d}(F(\ell,\mathbf{b},\mathbf{r}),F(\ell,\mathbf{b}^{\prime},\mathbf{r}))\leq L\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\right]$ .

If we can choose $L=1$ in (B1), then the loop is non-expansive; otherwise it is expansive (i.e., the minimum $L$ is greater than $1$).

Remark 1 (Simple While Loops).

In general, any imperative probabilistic program can be transformed equivalently into a simple while loop by adding a variable for the program counter and then simulating the original program through transitions between program counters and valuations. However, the class of simple while loops that can be handled by our approach is restricted to those with Lipschitz-continuous loop body. Thus generally, our approach cannot handle conditional branches that usually breaks the continuity property.

Example 2.2 (The Running Example).

Consider the simple while loop in Figure 3. In the program, $x$ is a program variable and $r$ is a sampling variable. In every loop iteration, the value of $x$ is increased by a value sampled w.r.t the probability distribution of $r$ until it is greater than $1000$. There is no probabilistic branch so $\mathbf{L}$ is a singleton set that only contains the empty function. The update function $F$ for the loop body is then given by $F(\ell,\mathbf{b},\mathbf{r})[x]=\mathbf{b}[x]+\mathbf{r}[r]$ for program valuation $\mathbf{b}$ and sampling valuation $\mathbf{r}$, where $\ell$ is the only element in $\mathbf{L}$. By definition, the loop is non-expansive.

3. Expected Sensitivity Analysis of Probabilistic Programs

In this paper, we focus on averaged sensitivity which is one of the most fundamental sensitivity notions in expected sensitivity analysis of probabilistic programs. Informally, averaged sensitivity compares the distance between the expected outcomes from two close-by input program valuations. The notion of averaged sensitivity has an important applicational value in that it can be used to model algorithmic stability in many machine-learning algorithms (see e.g. (Bousquet and Elisseeff, 2002)).

Below we illustrate the notion of averaged sensitivity formally. To ensure well-definedness, we only consider probabilistic programs that terminate with probability one (i.e., with almost-sure termination (Chakarov and Sankaranarayanan, 2013)) for all input program valuations. Furthermore, as our approach will rely on ranking supermartingales, we actually require that the probabilistic programs we consider terminate with finite expected termination time (Chatterjee et al., 2018c). Below we fix a probabilistic program $Q$ and a metric $\mathfrak{d}:\mathbb{R}^{|V_{\mathrm{p}}|}\times\mathbb{R}^{|V_{\mathrm{p}}|}\rightarrow[0,\infty)$.

Definition 3.1 (Averaged Sensitivity (Bousquet and

Elisseeff, 2002; Barthe et al., 2018)).

We say that the program $Q$ is averaged affine-sensitive over a subset $U\subseteq\mathbb{R}^{|V_{\mathrm{p}}|}$ of input program valuations if there exist real constants $A,B\geq 0$ and $\theta\in(0,\infty]$ such that for all program variables $z$ and $\mathbf{b},\mathbf{b}^{\prime}\in U$,

[TABLE]

where $Z,Z^{\prime}$ are random variables representing the values of $z$ after the execution of the program $Q$ under the input program valuations $\mathbf{b},\mathbf{b}^{\prime}$, respectively. Furthermore, if we can choose $B=0$ in (3), then the program $Q$ is said to be averaged linear-sensitive in the program variable $z$.

In the definition, the constants $A,B$ are sensitivity coefficients, while $\theta$ is the threshold below which the sensitivity is applicable; if $\theta=\infty$ then the sensitivity is applicable regardless of the distance between $\mathbf{b},\mathbf{b}^{\prime}$. Informally, a program $Q$ is averaged affine-sensitive if the difference in the expected value of any program variable $z$ after the termination of $Q$ is bounded by an affine function in the difference of the input program valuations. Likewise, the program is averaged linear-sensitive if the difference can be bounded by a linear function. In this way, we consider the expected sensitivity of the return values where each program variable represents an individual return value. Note that another subtle issue arising from the well-definedness is that the random variables $Z,Z^{\prime}$ in (3) may not be integrable. In the following, we will always guarantee that the random variables are integrable.

As we only consider averaged sensitivity, in the rest of the paper we will refer to averaged affine-/linear-sensitivity simply as expected affine-/linear-sensitivity. It is worth noting that in  (Barthe et al., 2018), a coupling-based definition for expected sensitivity is proposed. Compared with their definition, our definition treats expected sensitivity directly and do not consider couplings.

4. Motivating Examples

In the following, we show several motivating examples for expected sensitivity analysis of probabilistic programs. We consider in particular probabilistic programs with a randomized number of loop iterations that also depends on the input program valuation. As existing results (Barthe et al., 2018; Huang et al., 2018b; Hardt et al., 2016) only consider probabilistic loops with a fixed number of loop iterations, none of the examples in this section can be handled by these approaches.

Example 4.1 (Mini-roulette).

A particular gambler’s-ruin game is called mini-roulette, which is a popular casino game based on a 13-slot wheel. A player starts the game with $x$ amount of chips. He needs one chip to make a bet and he bets as long as he has chips. If he loses a bet, the chip will not be returned, but a winning bet will not consume the chip and results in a specific amount of (monetary) reward, and possibly even more chips. The following types of bets can be placed at each round. (1) Even-money bets: In these bets, $6$ specific slots are chosen. Then the ball is rolled and the player wins the bet if it lands in one of the $6$ slots. So the player has a winning probability of $\frac{6}{13}$. Winning them gives a reward of two unit and one extra chip. (2) 2-to-1 bets: these bets correspond to $4$ chosen slots and winning them gives a reward of $3$ and $2$ extra chips. (3) 3-to-1, 5-to-1 and 11-to-1 bets: These are defined similarly and have winning probabilities of $\frac{3}{13}$, $\frac{2}{13}$ and $\frac{1}{13}$ respectively. Suppose at each round, the player chooses each type of bets with the same probability (i.e., chooses each type with probability $\frac{1}{5}$). The probabilistic program for this example is shown in Figure 4(left), where the program variable $x$ represents the amount of chips and the program variable $w$ records the accumulated rewards. (In the program we consider that $x$ can take a real value.) We also consider a continuous variant of the mini-roulette example in Figure 4(right), where we replace increments to the variable $x$ by uniformly-distributed sampling variables $r_{i}(i=1,\dots,6)$ and one may choose $r_{1}\sim\mathsf{unif}(1,2)$, $r_{2}\sim\mathsf{unif}(2,3)$, $r_{3}\sim\mathsf{unif}(3,4)$, $r_{4}\sim\mathsf{unif}(4,5)$, $r_{5}\sim\mathsf{unif}(8,9)$, $r_{6}\sim\mathsf{unif}(1,2)$ or other uniform distributions that ensure the termination of the program. Note that the number of loop iterations in all the programs in Figure 4 is randomized and depends on the input program valuation as the loop guard is $x\geq 1$ and the increment/decrement of $x$ is random in each loop iteration. In both the examples, we consider the expected sensitivity in the output program variable $w$ that records the accumulated reward.

Example 4.2 (Multi-room Heating).

We consider a case study on multi-room heating from (Abate et al., 2010), modelled as a stochastic hybrid system that involves discrete and probabilistic dynamics. In the case study, there are $n$ rooms each equipped with a heater. The heater can heat the room and the heat can be transferred to another room if the rooms are adjacent. We follow the setting from (Abate et al., 2010) that the average temperature of each room, say room $i$, evolves according to the following stochastic difference equation that describes the transition from the $k$-th time step to the $(k+1)$-th time step, with constant time-interval $\Delta t$:

[TABLE]

where (i) $x_{a}$ represents the ambient temperature (assumed to be constant and equal for the whole building), (ii) the quantities $b_{i}$, $a_{ij}$, $c_{i}$ are nonnegative constants representing respectively the average heat transfer rate from room $i$ to the ambient (i.e., $b_{i}$), to adjacent rooms $j\neq i$ (i.e., $a_{ij}$’s), supplied to room $i$ by the heater (i.e., $c_{i}$), and (iii) $w_{i}(k)$ is the noise that observes a predefined probability distribution, such as Gaussian, Poisson or uniform distribution, etc. In this paper, we consider two simplified scenarios. The first is a single-room heating modelled as the probabilistic program in Figure 6, where the program variable $x$ represents the current room temperature, the constants $x_{a},b,c$ are as in (4) and $w$ is the noise (as a sampling variable); the goal in the first scenario is to raise the room temperature up to $20\text{\,}\mathrm{\SIUnitSymbolCelsius}$. We assume that the starting room temperature is between $0\text{\,}\mathrm{\SIUnitSymbolCelsius}$ and $20\text{\,}\mathrm{\SIUnitSymbolCelsius}$. The second is a double-room heating modelled in Figure 6, where the heater of the main room is on and the heater for the side room is off. In the figure, the program variable $x_{1}$ (i.e., $x_{2}$) represents the temperature for the main room (resp. the side room), respectively; the constants $x_{a},b_{i},c_{i},a_{ij}$ are as in (4); the sampling variables $w_{1},w_{2}$ represent the noises. In the program, we adopt the succinct form of simultaneous vector assignment for updates to $x_{1},x_{2}$. In both scenarios, we have a loop counter $n$ that records the number of stages until the (main) room reaches $20\text{\,}\mathrm{\SIUnitSymbolCelsius}$. We consider in particular the expected sensitivity w.r.t the total number of stages as recorded in $n$, for which we assume that the value of $n$ always starts with [math].

Example 4.3 (Stochastic Gradient Descent).

The most widely-used method in machine learning is stochastic gradient descent (SGD). The general form of an SGD algorithm is illustrated in Figure 3 on Page 3. In the figure, an SGD algorithm with $n$ training data is modelled as a simple while loop, where (i) $\mathsf{unif}[1,\ldots,n]$ is a sampling variable whose value is sampled uniformly from $1,2,\dots,n$, (ii) $\mathbf{w}$ is a vector of program variables that represents parameters to be learned, (iii) $i$ is a program variable that represents the sampled index of the training data, and (iv) $\gamma$ is a positive constant that represents the step size. The symbol $\nabla$ represents the gradient, while each $G_{i}$ ($1\leq i\leq n$) is the loss function for the $i$th training data. By convention, the total loss function $G$ is given as the expected sum of all $G_{i}$’s, i.e., $G:=\frac{1}{n}\sum_{i}G_{i}$. At each loop iteration, a data $i$ is chosen uniformly from all $n$ training data and the parameters in $\mathbf{w}$ are adjusted by the product of the step size and the gradient of the $i$th loss function $G_{i}$. The loop guard $\Phi$ can either be practical so that a fixed number of iterations is performed (as is analyzed in existing approaches (Hardt et al., 2016; Barthe et al., 2018; Huang et al., 2018b)), or the local criteria that the magnitude ${\parallel}{\nabla G}{\parallel}_{2}$ of the gradient of the total loss function $G$ is small enough, or the global criteria that the value of $G$ is small enough. In this paper, we consider the global criteria, i.e., the loop guard is of the form $G(\mathbf{w})\geq\zeta$ where $\zeta$ is the threshold for “small enough”. Note that the SGD algorithm with the global criteria has randomized loop iterations which depends on the initial parameters.

5. Proving Expected Sensitivity for Non-expansive Simple Loops

In this section, we demonstrate a sound approach for proving expected sensitivity over non-expansive simple while loops, whose number of loop iterations is randomized and depends on the input program valuation. The main difficulty is that when the number of loop iterations depends on both the randomized execution and the input program valuation, the executions from two close-by input program valuations may be non-synchronous in the sense that they do not terminate at the same time. The following example illustrates this situation.

Example 5.1 (Non-synchronicity).

Consider our running example in Figure 3, where the sampling variable $r$ observes the Dirac distribution such that $\mathbb{P}(r=1)=1$, so that the program is completely deterministic. Choose the initial inputs $x^{*}_{1},x^{*}_{2}$ by setting $x^{*}_{1}=1-\epsilon$ and $x^{*}_{2}=1+\epsilon$, where $\epsilon>0$ can be sufficiently small. Since we add $1$ to the value of $x$ in each loop iteration, the output value $x^{\mathrm{out}}_{2}$ under the input $x^{*}_{2}$ equals $1000+\epsilon$, while at the same step the execution from $x^{*}_{2}$ stops, the execution from $x^{*}_{1}$ does not terminate as the corresponding value is $1000-\epsilon$. Note that the final output from $x^{*}_{1}$ is $1001-\epsilon$.

The non-synchronicity prevents us from inferring the total expected sensitivity from the local sensitivity incurred in each loop iteration. To address this issue, we explore a martingale-based approach. In previous results such as (Chatterjee et al., 2018c; Chakarov and Sankaranarayanan, 2013), martingales have been successfully applied to prove termination properties of probabilistic programs. Besides qualitative termination properties, martingales can also derive tight quantitative upper/lower bounds for expected termination time and resource usage (Chatterjee et al., 2018c; Ngo et al., 2018; Chatterjee et al., 2018a; Wang et al., 2019). In this paper, we utilize the quantitative feature of martingales to bound the difference caused by non-synchronous situations.

We first recall the notion of ranking-supermartingale maps (RSM-maps), a core notion in the application of martingale-based approaches to probabilistic programs. As we consider simple while loops as the basic building block of probabilistic programs, we present a simplified version for simple while loops. Below we fix a simple while loop $Q$ in the form (1).

Definition 5.2 (RSM-maps (Chakarov and

Sankaranarayanan, 2013; Chatterjee et al., 2018c)).

A ranking-supermartingale map (RSM-map) is a Borel-measurable function $\eta:\mathbb{R}^{|V_{\mathrm{p}}|}\rightarrow\mathbb{R}$ such that there exist real numbers $\epsilon>0,K\leq 0$ satisfying the following conditions:

• (A1)

\forall\mathbf{b}:\big{(}\mathbf{b}\models\Phi\Rightarrow\eta(\mathbf{b})\geq 0\big{)};

• (A2)

\forall\mathbf{b}\,\forall\ell\,\forall\mathbf{r}:\big{(}(\mathbf{b}\models\Phi\wedge F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi)\Rightarrow K\leq\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq 0\big{)};

• (A3)

\forall\mathbf{b}:\big{(}\mathbf{b}\models\Phi\Rightarrow\mathbb{E}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r})))\leq\eta(\mathbf{b})-\epsilon\big{)};

where $\mathbb{E}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r})))$ is the expected value of $\eta(F(\ell,\mathbf{b},\mathbf{r}))$ such that $\mathbf{b}$ is treated as a constant vector and $\mathbf{r}$ (resp. $\ell$) observes the joint probability distributions of sampling variables (resp. the probabilities of the probabilistic branches), respectively.

Informally, (A1) specifies that the RSM-map should be non-negative before program termination, (A2) specifies the condition at loop termination, and (A3) specifies the ranking condition that the expected value of the RSM-map should decrease (by the positive amount $\epsilon$) after each loop iteration.

The existence of an RSM-map provides a finite upper bound on the expected termination time of a probabilistic program (Chatterjee et al., 2018c) (see Theorem C.1 in Appendix C). In this way, an RSM-map controls the randomized number of loop iterations. However, simply having an upper bound for the expected termination time is not enough, as what we need to bound is the difference between the expected values in non-synchronous situations. To resolve the non-synchronicity, we need some additional conditions. The first is the bounded-update requiring that the value-change in one loop iteration is bounded. The second is the RSM-continuity specifying that the RSM-map should be Lipschitz continuous over the loop guard. Below we fix a metric $\mathfrak{d}$.

Definition 5.3 (Bounded Update $d$).

We say that a simple while loop $Q$ has bounded update if there exists a real constant $d\geq 0$ such that

• (B2)

\forall\ell\,\forall\mathbf{b}\,\forall\mathbf{r}:\big{(}\mathbf{b}\models\Phi\Rightarrow\mathfrak{d}(\mathbf{b},F(\ell,\mathbf{b},\mathbf{r}))\leq d\big{)}.

The bounded-update condition simply bounds the change of values during each loop iteration. This condition is standard as it comes from the “$\sigma$-finiteness” proposed in the analysis of stochastic gradient descent (Hardt et al., 2016, Definition 2.4).

Definition 5.4 (RSM-continuity $M$).

An RSM-map $\eta$ has RSM-continuity if there exists a real constant $M>0$ such that

• (B3)

$\forall\mathbf{b},\mathbf{b}^{\prime}:|\eta(\mathbf{b})-\eta(\mathbf{b}^{\prime})|\leq M\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$.

By definition, the RSM-continuity bounds the difference of the RSM-map value proportionally in the metric $\mathfrak{d}$ when the program valuations $\mathbf{b},\mathbf{b}^{\prime}$ are close. This condition is used to bound the difference in non-synchronous situations and is naturally satisfied if the RSM-map is linear. Although this condition seems a bit restrictive, latter we will show that it can be relaxed (see Remark 4 and Remark 7). We keep the condition in its current form for the sake of brevity.

Below we first present our result for affine sensitivity, then linear sensitivity. We fix a metric $\mathfrak{d}$.

5.1. Proving Expected Affine-Sensitivity

The main result for proving expected affine-sensitivity of non-expansive simple loops is as follows.

Theorem 5.5.

A non-expansive simple while loop $Q$ in the form (1) is expected affine-sensitive over its loop guard ${\llbracket}{\Phi}{\rrbracket}$ if we have that

• •

$Q$* has bounded update, and*

• •

there exists an RSM-map for $Q$ that has RSM-continuity.

In particular, we can choose $\theta=\infty$ and $A=2\cdot\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}},B=-2\cdot\frac{d\cdot K}{\epsilon\cdot D_{1}}$ in (3), where the parameters $d,M,\epsilon,K,D_{1}$ are from Definition 5.2, Definition 5.3, Definition 5.4 and (2).

Proof Sketch.

Choose any program variable $z$. Let $d$ be a bound from Definition 5.3, and $\eta$ be an RSM-map with the parameters $\epsilon,K$ from Definition 5.2 that has RSM-continuity with a constant $M$ from Definition 5.4. Consider input program valuations $\mathbf{b},\mathbf{b}^{\prime}$ such that $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$. Let $\delta:=\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Denote by $T_{\mathbf{b}^{\prime\prime}}$ (resp. $Z_{\mathbf{b}^{\prime\prime}}$) the random variable for the number of loop iterations (resp. the value of $z$ after the execution of $Q$) from an input program valuation $\mathbf{b}^{\prime\prime}$, respectively. Define $\mathbf{W}_{\mathbf{b}^{\prime\prime}}$ as the vector of random variables that represents the program valuation after the execution of $Q$, starting from $\mathbf{b}^{\prime\prime}$. We illustrate the main proof idea through clarifying the relationships between any runs $\omega=\{\mathbf{b}_{n}\}_{n\geq 0}$, $\omega^{\prime}=\{\mathbf{b}^{\prime}_{n}\}_{n\geq 0}$ that start from respectively $\mathbf{b},\mathbf{b}^{\prime}$ (i.e., $\mathbf{b}_{0}=\mathbf{b}$ and $\mathbf{b}^{\prime}_{0}=\mathbf{b}^{\prime}$) and follow the same probabilistic branches and sampled values in every loop iteration. Consider at a step $n$ the event $\min\{T_{\mathbf{b}},T_{\mathbf{b}^{\prime}}\}\geq n$ holds (i.e., both the executions do not terminate before the $n$th loop iteration). We have the following cases:

• Case 1.

Both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$ violate the loop guard $\Phi$, i.e., $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}\models\neg\Phi$. This case describes that the loop $Q$ terminates exactly after the $n$th loop iteration for both the executions. From the non-expansiveness, we obtain directly that $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta$. Hence $|\mathbf{b}_{n}[z]-\mathbf{b}^{\prime}_{n}[z]|\leq\frac{\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})}{D_{1}}\leq\frac{\delta}{D_{1}}$.

• Case 2.

Exactly one of $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. This is the non-synchronous situation that needs to be addressed through martingales. W.l.o.g., we can assume that $\mathbf{b}_{n}\models\Phi$ and $\mathbf{b}^{\prime}_{n}\models\neg\Phi$. From the upper-bound property of RSM-maps (see Theorem C.1 in Appendix C), we derive that $\mathbb{E}_{\mathbf{b}_{n}}(T_{\mathbf{b}_{n}})\leq\dfrac{\eta(\mathbf{b}_{n})-K}{\epsilon}$. From the bounded-update condition (B2) and the triangle inequality of metrics, we have that $|\mathbf{b}_{n}[z]-Z_{\mathbf{b}_{n}}|\leq\frac{1}{D_{1}}\cdot\mathfrak{d}(\mathbf{b}_{n},\mathbf{W}_{\mathbf{b}_{n}})\leq\frac{d}{D_{1}}\cdot T_{\mathbf{b}_{n}}$. Thus, we obtain that

[TABLE]

By the non-expansiveness, we have $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta$. Then by the RSM-continuity (B3), we have $|\eta(\mathbf{b}_{n})-\eta(\mathbf{b}^{\prime}_{n})|\leq M\cdot\delta$. Furthermore, from (A2) we have $\eta(\mathbf{b}^{\prime}_{n})\leq 0$. So we obtain that $\eta(\mathbf{b}_{n})\leq M\cdot\delta$. It follows that

[TABLE]

• Case 3.

Neither $\mathbf{b}_{n}$ nor $\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. In this case, the loop $Q$ will continue from both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$. Then in the next iteration, the same analysis can be carried out for the next program valuations $\mathbf{b}_{n+1},\mathbf{b}^{\prime}_{n+1}$, and so forth.

From Theorem C.1 (in Appendix C), the probability that the third case happens infinitely often equals zero. Thus, the sensitivity analysis eventually reduces to the first two cases. In these two cases, the difference contributed to the total expected sensitivity $|\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}})|$ when one of the runs terminates after the $n$th loop iteration is at most $\mathbb{P}(T_{\mathbf{b}}=n\vee T_{\mathbf{b}^{\prime}}=n)\cdot\left(\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}}\cdot\delta-\frac{d\cdot K}{\epsilon\cdot D_{1}}\right)$ which is no greater than $(\mathbb{P}(T_{\mathbf{b}}=n)+\mathbb{P}(T_{\mathbf{b}^{\prime}}=n))\cdot\left(\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}}\cdot\delta-\frac{d\cdot K}{\epsilon\cdot D_{1}}\right)$. Then by a summation over all $n$’s, we derive the desired result that $|\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}})|\leq A\cdot\delta+B$ where $A:=2\cdot\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}}$ and $B:=-2\cdot\frac{d\cdot K}{\epsilon\cdot D_{1}}$. The detailed proof requires an explicit representation of the expected values through Lebesgue integral (see Appendix C). In particular, the integral representation allows us to consider the same probabilistic branches and sampled values in each loop iteration. Another subtle point is that the integrability of the random variables $Z,Z^{\prime}$ in (3) are guaranteed by the bounded-update condition and finite expected termination time from Theorem C.1. ∎

Remark 2.

Although in the statement of Theorem 5.5 we do not bound the constant $B$, the result is non-trivial as it applies to all program valuations that satisfies the loop guard. This is because input program valuations in the satisfaction set may lead to unbounded expected outcome as the expected number of loop iterations depend on input program valuations. Thus, simply raising the value of $B$ does not suffice to bound the unbounded expected outcomes.

Remark 3.

In Theorem 5.5 we only consider the sensitivity over the loop guard. The reason is that since we consider loops with randomized and input-dependent loop iterations, sensitivity usually applies to the loop guard only. Consider the (nonprobabilistic) loop in Figure 3 on Page 3. We can construct an RSM-map $\eta$ by $\eta(x,y):=y$ with parameters $\epsilon=1,K=-1$. Then by Theorem 5.5 (where we set $d=M=1$ and $\mathfrak{d}$ to be the max-norm) we derive that the loop is expected affine-sensitive over its loop guard. However, it is straightforward to observe that if we choose two input program valuations $\mathbf{b},\mathbf{b}^{\prime}$ such that $\mathbf{b}[x]=n$, $\mathbf{b}^{\prime}[x]=n-\epsilon$ and $\mathbf{b}[y]=\mathbf{b}^{\prime}[y]=n$, where $n$ is a natural number that can be arbitrarily large and $\epsilon$ is a positive real number that can be arbitrarily close to zero (so that $\mathbf{b}\models\Phi$ and $\mathbf{b}^{\prime}\not\models\Phi$), then the expected affine-sentivity does not hold. The reason is that the execution from $\mathbf{b}$ enters the loop and ends with $-1$ for $y$, and that from $\mathbf{b}^{\prime}$ does not enter the loop and hence keeps its input value $n$.

Example 5.6 (The Running Example).

Consider our running example in Figure 3. We choose the sampling variable $r$ to observe the Bernoulli distribution $\mathbb{P}(r=0)=\mathbb{P}(r=1)=\frac{1}{2}$ and the metric $\mathfrak{d}$ as the max norm. Then we can construct an RSM-map $\eta(x)=1000-x$ with $\epsilon=\frac{1}{2},K=-1$. Moreover, the RSM-map $\eta$ has the RSM-continuity with $M=1$, and the loop has bounded update with $d=1$. Hence by Theorem 5.5, the loop is expected affine-sensitive over its loop guard.

Example 5.7 (Mini-roulette).

We show that the Mini-roulette example in Figure 4(left) is expected affine-sensitive in the program variable $w$ over its loop guard. To show this, we construct the function $\eta(x,w)=13\cdot x-13$ with $\epsilon=1,K=-13$. We also clarify the following points.

1. (1)

For any values $x_{1},x_{2}$ to the program variable $x$ before a loop iteration and any $\ell\in\mathbf{L}$ that resolves the probabilistic branches, we have that $|(x_{1}+a)-(x_{2}+a)|=|x_{1}-x_{2}|$ after the loop iteration where the value of $a$ is determined by the probabilistic branch (i.e for branch $5$, $a=11$). The same applies to the program variable $w$. Thus the loop is non-expansive. 2. (2)

All increments to $x$ and $w$ are bounded, hence the loop has bounded update, which ensures (B2). 3. (3)

The loop guard $x\geq 1$ implies $\eta(x,w)=13\cdot x-13\geq 0$, thus (A1) is satisfied. When $x\geq 1$, $\ell\in\mathbf{L}$ and $F(\ell,(x,w),-)<1$, we have $-13\leq\eta(F(\ell,(x,w),-))\leq 0$, ensuring (A2). When $x\geq 1$, $\ell\in\mathbf{L}$, we have $\mathbb{E}_{\ell}(\eta(F(\ell,(x,w),-)))\leq\eta(x,w)-1$. Thus $\eta$ is an RSM-map. 4. (4)

Given any values $x_{1},x_{2}\geq 1$ and $w_{1},w_{2}$ to the program variables $x,w$, we have $|\eta(x_{1},w_{1})-\eta(x_{2},w_{2})|=13\cdot|x_{1}-x_{2}|$. Thus $\eta$ has RSM-continuity.

By Theorem 5.5, we obtain that the program is expected affine-sensitive over its loop guard.

Remark 4.

For proving expected affine sensitivity, one can relax the RSM-continuity to the condition that $\exists C>0.\forall\mathbf{b},\mathbf{b}^{\prime}.\left[(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi)\Rightarrow\eta(\mathbf{b})\leq C\right]$, so that the difference in non-synchronous situations is guaranteed to be bounded by $C$.

Remark 5 (Conditional Branches).

In certain scenarios, it is possible to extend Theorem 5.5 to conditional branches at which it may happen that one program valuation satisfies the condition of the branch and another close-by valuation does not. Consider a scenario where we are to use piecewise-linear functions to approximate a complex loop body. If the approximation is sufficiently strong to ensure that neighbouring pieces of functions behave similarly, then our approach can handle the scenario as follows. We first relax the Lipschitz continuity in Definition 2.1 to “$\leq L\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})+V$” where $V$ is a nonnegative constant that bounds the difference between neighbouring pieces of functions in each loop iteration (which is small for sufficiently strong approximation). This ensures that the final sensitivity would be $A\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})+(B+V\cdot\mathbb{E}(T))$ in the non-expansive case where $\mathbb{E}(T)$ is the expected termination time of the loop (that depends on the initial input).

5.2. Proving Expected Linear-Sensitivity

To develop a sound approach for proving expected linear-sensitivity, one possible way is to extend the approach for expected affine-sensitivity. However, simply extending the approach is not correct, as is shown by the following example.

Example 5.8.

Consider our running example in Figure 3. We first consider that the sampling variable $r$ observes the Dirac distribution such that $\mathbb{P}(r=1)=1$, the same as in Example  5.1. By choosing the same initial values $x^{*}_{1}$ and $x^{*}_{2}$ from Example 5.1, we have that the outcomes satisfy $|x^{\mathrm{out}}_{1}-x^{\mathrm{out}}_{2}|=1-2\cdot\epsilon$. Hence, we could not find a constant $A$ such that $|x^{\mathrm{out}}_{1}-x^{\mathrm{out}}_{2}|\leq A\cdot|x^{*}_{1}-x^{*}_{2}|=2\cdot A\cdot\epsilon$ when $\epsilon\rightarrow 0$. Similar situation happens even if we have non-Dirac discrete probability distributions. For example, consider now that the sampling variable $r$ observes the distribution such that $\mathbb{P}(r=0)=\mathbb{P}(r=1)=0.5$. Then with the same initial values $x^{*}_{1}$ and $x^{*}_{2}$, as the increment to the program variable $x$ is either [math] or $1$, we have the same outputs $x^{\mathrm{out}}_{1},x^{\mathrm{out}}_{2}$, refuting expected linear-sensitive.

The reason why we have such a situation in Example 5.8 is again due to the non-synchronous situation where the number of loop iterations depends on the input program valuation. While proving expected affine-sensitivity we can use a constant $B$ (cf. Definition 3.1) to bound the difference caused by non-synchronous situations, in proving linear-sensitivity we need to set $B=0$, leading to a difficulty that cannot be resolved by the technique developed for affine-sensitivity. To address this issue, we introduce another Lipschitz continuity w.r.t a given metric $\mathfrak{d}$.

Definition 5.9 (Lipschitz Continuity in Next-step Termination $L^{\prime}$).

We say that a simple while loop $Q$ in the form (1) is Lipschitz continuous in next-step termination if there exists a constant $L^{\prime}>0$ such that

• (B4)

$\forall\ell\,\forall\mathbf{b},\mathbf{b}^{\prime}:\left(\mathbf{b},\mathbf{b}^{\prime}\models\Phi\Rightarrow\mathbb{P}_{\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\neg\Phi)\leq L^{\prime}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\right)$

where given the program valuations $\mathbf{b},\mathbf{b}^{\prime}$ before the loop iteration and the resolution $\ell$ for the probabilistic branches, the value $\mathbb{P}_{\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\neg\Phi)$ is the probability regarding the sampled values that after one loop iteration we have $F(\ell,\mathbf{b},\mathbf{r})$ can still enter the loop, while $F(\ell,\mathbf{b}^{\prime},\mathbf{r})$ violates the loop guard.

The condition (B4) specifies that when the program valuations $\mathbf{b},\mathbf{b}^{\prime}$ are close, the probability that after the current loop iteration one of them stays in the loop while the other jumps out of the loop is small as it is proportional to the distance between $\mathbf{b},\mathbf{b}^{\prime}$. This condition handles the non-synchronous situation in the sense that the probability of non-synchronous situations is bounded linearly by the distance between the program valuations before a loop iteration. For simple while loops with only discrete probability distributions, this condition is usually not met. This is because in discrete probability distributions there often exists a vector $\mathbf{r}$ of sampled values with a minimum probability $p>0$ that $F(\ell,\mathbf{b},\mathbf{r})\models\Phi$ and $F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi$. In some cases such probability $p$ may be very large, e.g., in our running example (Example 5.8), with $\mathbb{P}(r=1)=1$ we have that $\mathbb{P}_{r}(F(\ell,999-\epsilon,r)\models\Phi\wedge F(\ell,999+\epsilon,r)\models\neg\Phi)=1$, and with $\mathbb{P}(r=0)=\mathbb{P}(r=1)=\frac{1}{2}$ we have that the same probability is $\frac{1}{2}$, when $\epsilon\rightarrow 0$. In contrast, loops with continuous distributions often satisfy this condition. For example, consider again our running example where $r$ now observes the uniform distribution over the interval $[0,1]$. Then for any initial values $x^{\prime\prime}\leq x^{\prime}\leq 1000$ for the program variable $x$, the probability that $x^{\prime}+r>1000$ but $x^{\prime\prime}+r\leq 1000$ equals the chance that the sampled value of $r$ falls in $(1000-x^{\prime},1000-x^{\prime\prime}]$, which is no greater than $|x-x^{\prime}|$ as the probability density function of $r$ is $1$ over the interval $[0,1]$.

In the following, we show that a large class of affine simple while loops with continuous distributions guarantees the (B4) condition. Below we say that an update function $F$ is affine if for all $\ell\in\mathbf{L}$, we have that $F(\ell,\mathbf{b},\mathbf{r})=\mathbf{B}\cdot\mathbf{b}+\mathbf{C}\cdot\mathbf{r}+\mathbf{c}$ for constant matrices $\mathbf{B},\mathbf{C}$ and vector $\mathbf{c}$. Moreover, a boolean expression $\Phi$ is said to be affine if $\Phi$ can be equivalently rewritten into a disjunctive normal form (DNF) $\bigvee_{i\in\mathcal{I}}(\mathbf{A}_{i}\cdot\mathbf{b}\leq\mathbf{d}_{i})$ with constant matrices $\mathbf{A}_{i}$ and vectors $\mathbf{d}_{i}$ so that for all program valuations $\mathbf{b}$, we have $\mathbf{b}\models\Phi$ iff the disjunctive formula $\bigvee_{i\in\mathcal{I}}(\mathbf{A}_{i}\cdot\mathbf{b}\leq\mathbf{d}_{i})$ holds. The class of simple while loops that guarantees (B4) is as follows.

Lemma 5.10.

Consider a simple while loop $Q$ in the form (1) that satisfies the following conditions:

1. (1)

both $F$ and $\Phi$ are affine and $\Phi$ is equivalent to some DNF $\bigvee_{i\in\mathcal{I}}(\mathbf{A}_{i}\cdot\mathbf{b}\leq\mathbf{d}_{i})$; 2. (2)

all sampling variables are continuously-distributed whose probability density functions have bounded values; 3. (3)

for all $i\in\mathcal{I}$, $\ell\in\mathbf{L}$ and program valuations $\mathbf{b}\models\Phi$, the coefficients for the sampling variables $\mathbf{r}$ in $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b},\mathbf{r})$ are not all zero at each row, i.e., the truth value of each disjunctive clause in $\Phi$ for $F(\ell,\mathbf{b},\mathbf{r})$ depends on $\mathbf{r}$ at every row.

*Then the loop $Q$ is Lipschitz continuous in next-step termination w.r.t any metric $\mathfrak{d}$. *

Informally, the lemma guarantees the (B4) condition by requiring that (i) both the update function and the loop guard are affine, (ii) all sampling variables are continuously-distributed, and (iii) the truth value of every linear inequality in the loop guard after the current loop iteration depends on the sampled values. The proof of Lemma 5.10 is elementary and is put in Appendix D.

Remark 6.

We note that Lemma 5.10 serves as a sound condition only, and there are situations where the prerequsite of Lemman 5.10 fails but the condition (B4) still holds. For example, consider that a program variable $x$ is assigned to $1$ every time in a loop iteration, and the loop guard involves the condition $x\leq 2$. Then the condition $x\leq 2$ does not affect the truth value of the loop guard since it is always satisfied, but has zero coefficients for all sampling variables. While to derive weaker conditions is possible, in this work we consider Lemma 5.10 as a simple guarantee for ensuring (B4).

Now we demonstrate our approach for proving expected linear-sensitivity. Our first result is a sound approach for proving local linear-sensitivity. Below given a program valuation $\mathbf{b}\models\Phi$, a radius $\rho>0$ and a metric $\mathfrak{d}$, we denote by $U_{\Phi,\mathfrak{d}}(\mathbf{b},\rho)$ the neighbourhood $\{\mathbf{b}^{\prime}\mid\mathbf{b}^{\prime}\models\Phi\wedge\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\rho\}$.

Proposition 5.11.

A non-expansive simple while loop $Q$ in the form (1) has expected linear-sensitivity over some neighbourhood $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$ of any given $\mathbf{b}^{*}\in{\llbracket}{\Phi}{\rrbracket}$ if $Q$ has (i) bounded update, (ii) an RSM-map with RSM-continuity and (iii) the Lipschitz continuity in next-step termination.

The proof resembles the one for expected affine-sensitivity (Theorem 5.5). The obtained the coefficient $A$ (cf. Definition 3.1) depends on the expected termination time from the input program valuation $\mathbf{b}^{*}$. See Appendix D for details.

Proposition 5.11 gives a sound approach for proving local linear-sensitivity in that the coefficient $A$ only works for a small neighbourhood of a given input. A natural question arises whether we can obtain global linear-sensitivity so that the coefficient $A$ works for all program valuations that satisfy the loop guard. The major barrier in the proof of Proposition 5.11 to obtain global linear sensitivity is that in general we can only treat every program valuation uniformly, without distinguishing between program valuations with large and small RSM-map values. To overcome this difficulty, we partition program valuations into finitely many classes so that each class shares a common coefficient, but different classes may have different coefficients. Based on the partition, we utilize the inter-relationship between different classes to prove the existence of a collection of coefficients for the expected linear-sensitivity. The partition relies on the difference-bounded condition for RSM-maps proposed for proving concentration properties of termination time (Chatterjee et al., 2018c).

Definition 5.12 (The Difference-bounded Condition (Chatterjee et al., 2018c)).

We say that an RSM-map $\eta$ (for a simple while loop) is difference-bounded if there exists a constant $c\geq 0$ such that

• (A4)

$\forall\mathbf{b}\,\forall\ell\,\forall\mathbf{r}:\left(\mathbf{b}\models\Phi\Rightarrow|\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})|\leq c\right)$ .

The difference-bounded condition ensures the concentration property for program termination (Chatterjee et al., 2018c), see Theorem E.1 in Appendix E. Below we demonstrate how this condition helps to partition the program valuations into finitely-many regions by their corresponding RSM-map values. First we show that this condition derives a minimum positive probability that the value of an RSM-map decreases by a minimum positive amount.

Lemma 5.13.

If $\eta$ is a difference-bounded RSM-map with the parameters $\epsilon,c$ specified in Definition 5.2 and Definition 5.12, then there exists a constant $p\in(0,1]$ such that

• (†)

$\forall\mathbf{b}:\left(\mathbf{b}\models\Phi\Rightarrow\mathbb{P}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})\leq-\frac{1}{2}\cdot\epsilon)\geq p\right)$**

where the probability $\mathbb{P}_{\mathbf{r},\ell}(-)$ is taken w.r.t the sampled valuation $\mathbf{r}$ and the resolution $\ell$ for probabilistic branches, and treats the program valuation $\mathbf{b}$ as constant. In particular, we can take $p:=\frac{\epsilon}{2\cdot c-\epsilon}$.

Proof Sketch.

The proof is through Markov’s inequality. See Appendix D for details. ∎

The finite partition. Based on Lemma 5.13, we partition the satisfaction set ${\llbracket}{\Phi}{\rrbracket}$ into finitely many regions. Our aim is to have a partition $R_{1},\dots,R_{n^{*}},R_{\infty}$ based on which we find individual sensitivity coefficients on each $R_{k}$. First we choose a smallest natural number $n^{*}$ such that $(n^{*}-1)\cdot\frac{1}{2}\cdot\epsilon\leq c+1<n^{*}\cdot\frac{1}{2}\cdot\epsilon$. (Note that $n^{*}\geq 3$ as $\epsilon\leq c$.) Then we define the region $R_{k}:=\{\mathbf{b}\in{\llbracket}{\Phi}{\rrbracket}\mid(k-1)\cdot\frac{1}{2}\cdot\epsilon\leq\eta(\mathbf{b})<k\cdot\frac{1}{2}\cdot\epsilon\}$ for natural numbers $1\leq k\leq n^{*}$, and $R_{\infty}:=\{\mathbf{b}\in{\llbracket}{\Phi}{\rrbracket}\mid\eta(\mathbf{b})\geq n^{*}\cdot\frac{1}{2}\cdot\epsilon\}$. It follows that ${\llbracket}{\Phi}{\rrbracket}$ is a disjoint union of all $R_{k}$’s. Especially, we treat $R_{\infty}$ as the region for program valuations with “large enough” RSM-map values. After the partitioning, we are to prove that for each $R_{k}$ there is a coefficient $A_{k}$ for Definition 3.1, and for different $R_{k}$’s there may be different $A_{k}$’s. The following result presents the first step of the proof, where each $A_{k}$ ($1\leq k\leq n^{*}$) represents the coefficient for $R_{k}$ and $A_{\infty}$ for $R_{\infty}$.

Proposition 5.14.

For any natural number $n\geq 1$, real numbers $C,D\geq 0$ and probability value $p\in(0,1]$, the following system of linear inequalities (with real variables $A_{k}$’s ($0\leq k\leq n$) and $A_{\infty}$)

[TABLE]

has a solution.

Proof Sketch.

First, we equate all inequalities but the last line above (i.e., $D=A_{0}\leq A_{1}\leq\dots\leq A_{n}\leq A_{\infty}$), so that we directly get the solution as follows:

• •

$A_{\infty}=\frac{1}{p^{n+1}}\cdot(\sum_{m=1}^{n+1}p^{m-1})\cdot C+D=\frac{1}{p^{n+1}}\cdot\frac{1-p^{n+1}}{1-p}\cdot C+D$,

• •

$A_{k}=(\frac{1-p^{k}}{p^{n+1}}\cdot(\sum_{m=1}^{n+1}p^{m-1})+(\sum_{m=1}^{k}p^{m-1}))\cdot C+D=(\frac{1-p^{k}}{p^{n+1}}\cdot\frac{1-p^{n+1}}{1-p}+\frac{1-p^{k}}{1-p})\cdot C+D$ for $1\leq k\leq n$.

Then we check that the inequalities in the last line above hold. See Appendix D for details. ∎

Now we state our main result for proving global linear sensitivity on non-expansive simple loops.

Theorem 5.15.

A non-expansive simple while loop $Q$ in the form (1) has expected linear-sensitivity over its loop guard ${\llbracket}{\Phi}{\rrbracket}$ if $Q$ has (i) bounded update, (ii) a difference-bounded RSM-map with RSM-continuity and (iii) the Lipschitz continuity in next-step termination. In particular, we can choose $\theta=\frac{1}{M}$ in (3) where the parameter $M$ is from the RSM-continuity (Definition 5.4).

Proof Sketch.

Choose any program variable $z$. Denote by $T,T^{\prime}$ (resp. $Z_{n},Z^{\prime}_{n}$) the random variables for the number of loop iterations (resp. the value of $z$ at the $n$-th step), from two close-by input program valuations $\mathbf{b},\mathbf{b}^{\prime}$, respectively. For each natural number $n\geq 0$, we define $\delta_{n}(\mathbf{b},\mathbf{b}^{\prime}):=\mathbb{E}_{\mathbf{b}}(Z_{T\wedge n})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{T^{\prime}\wedge n})$, where the random variable $T\wedge n$ is defined as $\min\{T,n\}$ and $T^{\prime}\wedge n$ likewise. We also define $\delta(\mathbf{b},\mathbf{b}^{\prime}):=\mathbb{E}_{\mathbf{b}}(Z_{T})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{T^{\prime}})$. First, we prove from the Dominated Convergence Theorem that $\lim\limits_{n\rightarrow\infty}\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})=\delta(\mathbf{b},\mathbf{b}^{\prime})$. Second, given a difference-bounded RSM-map $\eta$ with RSM-continuity, we construct the regions $R_{k}$’s ($1\leq k\leq n^{*}$) and $R_{\infty}$ as in the paragraph below Lemma 5.13, and solve $A_{k}$’s and $A_{\infty}$ from Proposition 5.14. Third, based on the solved $A_{k}$’s and $A_{\infty}$, we prove by induction on $n\geq 0$ that for all $k\in\{1,\dots,n^{*},\infty\}$ and all program valuations $\mathbf{b},\mathbf{b}^{\prime}$, we have $\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})\leq A_{k}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ when $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$ and $\mathbf{b}\in R_{k}$. In the inductive proof, (i) we apply Lemma 5.13 to tackle the regions $R_{k}$ ($1\leq k\leq n^{*}$) and use the inequality $(1-p)\cdot A_{\infty}+C+p\cdot A_{k-1}\leq A_{k}$ from Proposition 5.14 to prove the inductive case, and (ii) for $R_{\infty}$ we ensure the fact that starting from two close-by program valuations in $R_{\infty}$, the loop will not terminate after the current loop iteration from both the program valuations, as is guaranteed by (A1), (A2), (A4) and the RSM-continuity. Finally, the result follows from taking the limit $n\rightarrow\infty$ and the fact that we have finitely many regions. The detailed proof is put in Appendix D. ∎

Remark 7.

For expected linear sensitivity, one can relax the RSM-continuity as follows. First, we require the relaxed condition in Remark 4 to tackle the non-synchronous situation. Second, we need the relaxed condition $\exists D>0.\forall\mathbf{b},\mathbf{b}^{\prime}.\left[(\mathbf{b},\mathbf{b}^{\prime}\models\Phi\wedge\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\theta\wedge\eta(\mathbf{b})>D)\Rightarrow\eta(\mathbf{b}^{\prime})>c\right]$, so that the neighourbood around $\mathbf{b}$ w.r.t the threshold $\theta$ will not lead to termination after one loop iteration.

Example 5.16.

We now show that the mini-roulette variant in Figure 4(right) is expected linear-sensitive in the program variable $w$ over its loop guard. To show this, we construct the function $\eta(x,w)=2.45\cdot x-2.45$ with $\epsilon=1,K=-4.91$. We also clarify the following points.

1. (1)

For any values $x_{1},x_{2}$ to the program variable $x$ before a loop iteration and any $\ell\in\mathbf{L}$ that resolves the probabilistic branches, we have that $|(x_{1}+r_{i})-(x_{2}+r_{i})|=|x_{1}-x_{2}|$ after the loop iteration where the value of $r_{i}$ is decided by the executed branch and its distribution(i.e for branch $5$, $r_{i}:=r_{5}\sim unif(8,9)$). The same applies to the program variable $w$. Thus the loop body is non-expansive. 2. (2)

All increments to $x$ and $w$ are bounded, hence the loop has bounded update, which ensures (B2). 3. (3)

The loop guard $x\geq 1$ implies $\eta(x,w)=2.45\cdot x-2.45\geq 0$, thus (A1) is satisfied. When $x\geq 1$, $\ell\in\mathbf{L}$ and $F(\ell,(x,w),-)<1$, we have $-4.91\leq\eta(F(\ell,(x,w),-))\leq 0$, ensuring (A2). When $x\geq 1$, $\ell\in\mathbf{L}$, we have $\mathbb{E}_{\mathbf{r},\ell}(\eta(F(\ell,(x,w),\mathbf{r})))\leq\eta(x,w)-1$, ensuring (A3). Thus, $\eta$ is an RSM-map. 4. (4)

Given any values $x_{1},x_{2}\geq 1$ and $w_{1},w_{2}$ to the program variables $x,w$, we have $|\eta(x_{1},w_{1})-\eta(x_{2},w_{2})|=2.45\cdot|x_{1}-x_{2}|$. Thus $\eta$ has RSM-continuity. 5. (5)

When $x\geq 1$, we have $|\eta(F(\ell,(x,w),\mathbf{r}))-\eta(x,w)|\leq|\eta(F(\ell,(x,w),r_{5}))-\eta(x,w)|=|2.45\cdot(x+r_{5})-2.45-2.45\cdot x+2.45|\leq 2.45\cdot 9=22.05$, ensuring (A4). Thus, $\eta$ is difference-bounded. 6. (6)

Due to the fact that both the update function and the loop guard are affine, all sampling variables are bounded continuously-distributed, and the coefficients for the current sampling variables are not all zero in the loop guard of the next iteration, we can verify that the loop has the Lipschitz continuity in next-step termination by Lemma 5.10.

Then by Theorem 5.15, we can conclude that this probabilistic program is expected linear-sensitive over its loop guard.

6. Proving Expected Sensitivity for Expansive Simple While Loops

In this section, we show how our sound approach for proving expected sensitivity of non-expansive loops can be extended to expansive simple while loops. We first illustrate the main difficulty, and then enhance RSM-maps to be difference-bounded and show how they can address the difficulty.

The main difficulty to handle expansive loops is that the difference between two program valuations may tend to infinity as the number of loop iterations increases. For example, consider a simple while loop where at every loop iteration (i) the value of a program variable $z$ is tripled and (ii) the loop terminates immediately after the current loop iteration with probability $\frac{1}{2}$. Then given two different initial values $z^{\prime},z^{\prime\prime}$ for $z$, we have that

[TABLE]

where $Z^{\prime},Z^{\prime\prime}$ are given by the same way of $Z,Z^{\prime}$ as in (3) and $T$ is the termination time random variable. Thus the expected-sensitivity properties do not hold for this example, as the increasing speed of $z$ is higher than that for program termination. To cope with this point, we consider again RSM-maps to be difference-bounded, as in Definition 5.12. The main idea is to use the exponential decrease from difference-bounded RSM-maps (Theorem E.1 in Appendix E) to counteract the unbounded increase in the difference between input program valuations.

Below we illustrate the main result of this section. Recall that given a program valuation $\mathbf{b}$, a radius $\rho>0$ and a metric $\mathfrak{d}$, we denote by $U_{\Phi,\mathfrak{d}}(\mathbf{b},\rho)$ the neighbourhood $\{\mathbf{b}^{\prime}\mid\mathbf{b}^{\prime}\models\Phi\wedge\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\rho\}$.

Theorem 6.1.

Consider a simple while loop $Q$ in the form (1) that satisfies the following conditions:

• •

the loop body $P$ is Lipschitz continuous with a constant $L$ specified in Definition 2.1, and has bounded update;

• •

there exists a difference-bounded RSM-map $\eta$ for $Q$ with RSM-continuity and parameters $\epsilon,K,c$ from Definition 5.2 and Definition 5.12 such that $L<\mathrm{exp}({\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}}})$.

Then for any program valuation $\mathbf{b}^{*}$ such that $\mathbf{b}^{*}\models\Phi$ and $\eta(\mathbf{b}^{*})>0$, there exists a radius $\rho>0$ such that the loop $Q$ is expected affine-sensitive over $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$. In particular, we can choose in Definition 3.1 that

[TABLE]

where $A^{\prime}=\frac{d\cdot M+\epsilon}{D_{1}\cdot\epsilon}$, $B^{\prime}=-\frac{d\cdot K}{D_{1}\cdot\epsilon}$ and $N=\lfloor 4\cdot\frac{\eta(\mathbf{b}^{*})}{\epsilon}\rfloor+1$, for which the parameters $d,M,\epsilon,K,D_{1}$ are from Definition 5.2, Definition 5.3, Definition 5.4 and (2).

The proof resembles the one for Theorem 5.5 and compares $L$ with the exponential-decreasing factor $\mathrm{exp}({\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}}})$, see Appendix E for the detailed proof. Note that in the statement of the theorem we do not care for $\theta$, this is because we have already restricted the threshold to the neighbourhood $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$.

Theorem 6.1 cannot be directly extended to linear sensitivity as the technique to derive linear sensitivity (e.g. Theorem 5.15) requires non-expansiveness as an important prerequisite. We leave a more detailed investigation of the expansive case (including the linear sensitivity) as a future work.

Summary of Prerequisites for Expected Sensitivity. In Table 1, we summarize the prerequisites for expected sensitivity. The first column specifies the program type (i.e. non-expansive/expansive loops), the second column specifies the sensitivity type (i.e. expected affine/linear-sensitive) for the program, the third column specifies the related theorem for this expected sensitivity of the program, and the last column contains all the prerequisites of this expected sensitivity.

Remark 8.

All our results cover the degenerate case where the number of loop iterations is fixed and bounded. To see this, suppose that the number of loop iterations is fixed to be $n$, and there is a program variable $i$ that serves as the loop counter. Then we can choose $n-i$ as a (difference-bounded) RSM-map that is independent of the program variables other than $i$, so that our result for expected affine-sensitivity (Theorem 5.5) holds directly for this degenerate case. Furthermore, the condition (B4) is satisfied directly as the termination depends only on the loop counter $i$, so that our linear-sensitivity result (Theorem 5.15) holds for the degenerate case; for expansive loops, we even do not need to check whether $L<\exp(\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}})$ in Theorem 6.1 as the number of loop iterations is bounded.

7. Sequential Composition of Simple While Loops

In this section, we demonstrate the compositionality of our martingale-based approach for proving expected sensitivity of probabilistic programs. We follow the previous work (Barthe et al., 2018) to consider the sequential composition of probabilistic programs. We show that under the same side condition from  (Barthe et al., 2018), our approach is compositional under sequential composition.

We first show that the compositionality under sequential composition does not hold in general. The main point is that if the output range of a preceding program $Q$ does not match the input range over which the latter program $Q^{\prime}$ is expected sensitive, then the global expected sensitivity for the sequential composition $Q;Q^{\prime}$ may not hold. A detailed example is as follows.

Example 7.1.

Consider the sequential composition $Q=\mathbf{skip};Q^{\prime}$ where $Q^{\prime}$ is the simple while loop from Remark 3. We know that $\mathbf{skip}$ is expected sensitive over all input program valuations. From Theorem 5.5 and Remark 3, we have $Q^{\prime}$ is expected affine-sensitive only over its loop guard. Then the program $Q$ is not expected affine-sensitive over all input program valuations, as one can choose two input program valuations such that one satisfies the loop guard of $Q^{\prime}$ but the other does not.

Thus, in order to ensure compositionality, we need to require that the output range of the preceding program should match the input sensitivity range of the latter program, as is also required in  (Barthe et al., 2018). Under this side condition, we prove that our approach is compositional over sequential composition of non-expansive simple while loops. Below for a probabilistic program $Q$, we denote by $\mathsf{out}(Q)$ the set of all possible outcome program valuations after the execution of $Q$ under some input program valuation in the satisfaction set of its loop guard.

Theorem 7.2.

Consider a non-expansive simple while loop $Q$ with bounded-update and an RSM-map with RSM-continuity, and a general program $Q^{\prime}$ that has expected affine-sensitivity over a subset $U$ of input program valuations with threshold $\theta$ in (3). If $\mathsf{out}(Q)\subseteq U$ and assuming integrability in (3), then the sequential composition $Q;Q^{\prime}$ is expected affine-sensitive over the satisfaction set of the loop guard of $Q$ with threshold $\theta$.

Proof Sketch.

The proof is basically an extension to the previous proof for Theorem 5.5. We consider the same three cases from the previous proof, and use the expected affine-sensitivity from $Q^{\prime}$ to derive the new sensitivity coefficients. The detailed proof is put in Appendix F. ∎

Theorem 7.2 presents a general compositional result where the program $Q^{\prime}$ can be an arbitrary probabilistic program. By extending the proof for Theorem 5.15 in a similar way as from Theorem 5.5 to Theorem 7.2, we can also derive a compositional result for expected linear-sensitivity. However, we now need to consider $Q^{\prime}$ as a sequential composition of simple while loops and impose linearity on the RSM-maps. (An RSM-map is linear if it can be expressed as a linear combination of program variables and a possible constant term.) Then for a sequential composition $Q=Q_{1};\dots;Q_{n}$ of simple while loops, we require the condition (‡) that (i) each $Q_{i}$ having bounded update and a linear RSM-map $\eta_{i}$ that witnesses its expected linear-sensitivity (i.e., that satisfies the conditions (A1) – (A4).) and (ii) $\mathsf{out}(Q_{i})\subseteq{\llbracket}{\Phi_{i+1}}{\rrbracket}$ for all $i$, where $\Phi_{i+1}$ is the loop guard of $Q_{i+1}$. By extending the proof for Theorem 5.15 (see Appendix F for the detailed proof), we establish the following theorem.

Theorem 7.3.

Consider a non-expansive simple while loop $Q$ with loop guard $\Phi$ that has (i) bounded-update, (ii) a difference-bounded linear RSM-map with RSM-continuity, and (iii) the Lipschitz continuity in next-step termination. Then for any sequential composition $Q^{\prime}$ of simple while loops that (a) satisfies the condition (‡) (defined right before the theorem) and (b) has expected linear-sensitivity over a subset $U$ of input program valuations, if ${\llbracket}{\Phi}{\rrbracket}\cup\mathsf{out}(Q)\subseteq U$, then the sequential composition $Q;Q^{\prime}$ is expected linear-sensitive over the satisfaction set of the loop guard of $Q$.

By an iterated application of Theorem 7.2 and Theorem 7.3 (i.e., loop-by-loop), we obtain directly the compositionality over sequential composition of non-expansive simple while loops.

Remark 9 (Expansive Loops).

Up till now we only consider non-expansive loops. The main issue arising from expansive loops is that the expected sensitivity is restricted to a small neighbourhood of a fixed input program valuation, and the sensitivity coefficients often depend on the input program valuation. More precisely, these coefficients may be exponential in general (see Theorem 6.1). Thus, compositionality for expansive loops depends on the exact post probability distribution after the execution of the preceding loops. To overcome this difficulty, new technique needs to be developed and we plan it as a future work.

Remark 10 (Comparison with (Barthe et al., 2018)).

A similar compositional result is established in (Barthe et al., 2018, Proposition 4.3) for loops with a fixed number of loop iterations. The approach is similar to ours as it also considers sequential composition and requires that the output range of the preceding loop should match the input sensitivity range of the latter loop, and treats each individual program in the sequential composition separately. The only difference is that they prove directly that their coupling-based sensitivity has the compositional property regardless of the detailed program structure, while our approach requires an explicit RSM-map for each loop. This is however due to the fact that our approach considers the more complex situation that the loop iterations are randomized and depend on the input program valuation.

Remark 11 (Compositionality).

We would like to note that the level of compositionality depends on the side condition in an approach. Some authors insist that compositionality should require no side condition, while other authors allow side conditions (Kupferman and Vardi, 1997). Our approach, like the approach in (Barthe et al., 2018), has the least side condition, as we only require that the output range of the preceding program matches the input sensitivity range of the latter. Our result is also different from the original one in (Barthe et al., 2018) as in our case we need to tackle the non-trivial point of non-synchronicity (see Example 5.1).

8. An Automated Approach through RSM-synthesis Algorithms

In this section, we describe an automated algorithm that, given a non-expansive probabilistic loop $Q$ in the form (1), synthesizes an RSM-map with extra conditions required for proving expected sensitivity. We consider affine programs whose loop guard and update function are affine, and linear templates for an RSM-map. Our algorithm runs in polynomial time and reduces the problem of RSM-map synthesis to linear programming by applying Farkas’ Lemma. We strictly follow the framework from previous synthesis algorithms (Chatterjee et al., 2018c; Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2016; Chatterjee et al., 2018a, 2017; Wang et al., 2019; Feng et al., 2017). As our synthesis framework is not novel, we describe only the essential details of the algorithm.

We first recall Farkas’ Lemma.

Theorem 8.1 (Farkas’ Lemma (Farkas, 1894)).

Let $\mathbf{A}\in\mathbb{R}^{m\times n}$, $\mathbf{b}\in\mathbb{R}^{m}$, $\mathbf{c}\in\mathbb{R}^{n}$ and $d\in\mathbb{R}$. Suppose that $\{\mathbf{x}\in\mathbb{R}^{n}\mid\mathbf{A}\mathbf{x}\leq\mathbf{b}\}\neq\emptyset$. Then $\{\mathbf{x}\in\mathbb{R}^{n}\mid\mathbf{A}\mathbf{x}\leq\mathbf{b}\}\subseteq\{\mathbf{x}\in\mathbb{R}^{n}\mid\mathbf{c}^{\mathrm{T}}\mathbf{x}\leq d\}$ iff there exists $\mathbf{y}\in\mathbb{R}^{m}$ such that $\mathbf{y}\geq\mathbf{0}$, $\mathbf{A}^{\mathrm{T}}\mathbf{y}=\mathbf{c}$ and $\mathbf{b}^{\mathrm{T}}\mathbf{y}\leq d$.

Intuitively, Farkas’ Lemma transforms the inclusion problem of a nonempty polyhedron within a halfspace into a feasibility problem of a system of linear inequalities. As a result, one can decide the inclusion problem in polynomial time through linear programming.

The RSM-synthesis Algorithm. Our algorithm has the following four steps:

1. (1)

Template. The algorithm sets up a column vector $\mathbf{a}$ of $|V_{\mathrm{p}}{}|$ fresh variables and a fresh scalar variable $b$ such that the template for an RSM-map $\eta$ is $\eta(\mathbf{b})=\mathbf{a}^{\mathrm{T}}\cdot\mathbf{b}+b$. Note that since we use linear templates, the RSM-continuity condition is naturally satisfied. 2. (2)

Constraints on $\mathbf{a}$ and $b$. The algorithm first encodes the condition (A1) for the template $\eta$ as the inclusion assertion $\{\mathbf{b}\mid\mathbf{b}\models\Phi\}\subseteq\{\mathbf{b}\mid\mathbf{c}_{1}^{\mathrm{T}}\cdot\mathbf{b}\leq d_{1}\}$ where $\mathbf{c}_{1},d_{1}$ are unique linear combinations of unknown coefficients $\mathbf{a},b$ satisfying that $\mathbf{c}_{1}^{\mathrm{T}}\cdot\mathbf{b}\leq d_{1}\Leftrightarrow\eta(\mathbf{b})\geq 0$. Next, the algorithm encodes the condition (A2) as the inclusion assertion $\{(\mathbf{b},\mathbf{r})\mid\mathbf{b}\models\Phi\wedge F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi\}\subseteq\{(\mathbf{b},\mathbf{r})\mid K\leq\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq 0\}$ parameterized with $\mathbf{a},b,K$ for every $\ell\in\mathbf{L}$, where $K$ is a fresh unknown constant. Then the algorithm encodes (A3) as $\{\mathbf{b}\mid\mathbf{b}\models\Phi\}\subseteq\{\mathbf{b}\mid\mathbf{c}_{2}^{\mathrm{T}}\cdot\mathbf{b}\leq d_{2}\}$ where $\mathbf{c}_{2},d_{2}$ are unique linear combinations of unknown coefficients $\mathbf{a},b$ satisfying that $\mathbf{c}_{2}^{\mathrm{T}}\cdot\mathbf{b}\leq d_{2}\Leftrightarrow\mathbb{E}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r})))\leq\eta(\mathbf{b})-\epsilon$. The algorithm can also encode (A4) as $\{(\mathbf{b},\mathbf{r})\mid\mathbf{b}\models\Phi\}\subseteq\{(\mathbf{b},\mathbf{r})\mid|\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})|\leq c\}$ parameterized with $\mathbf{a},b,c$ for every $\ell\in\mathbf{L}$, where $c$ is a fresh unknown constant. All the inclusion assertions (with parameters $\mathbf{a},b,K,\epsilon,c$) are grouped conjunctively so that these inclusions should all hold. 3. (3)

Applying Farkas’ Lemma. The algorithm applies Farkas’ Lemma to all the inclusion assertions from the previous step and obtains a system of linear inequalities with the parameters $\mathbf{a},b,K,\epsilon,c$, where we over-approximate all strict inequalities (with ‘$<$’) by non-strict ones (with ‘$\leq$’). 4. (4)

Constraint Solving. The algorithm calls a linear programming (LP) solver on the linear program consisting of the system of linear inequalities generated in the previous step.

Besides the RSM-synthesis, we guarantee the non-expansiveness either directly from the structure of the program or by manually inspection (note that it can also be verified automatically through SMT solvers on the first order theory of reals). We check the bounded-update condition by a similar application of Farkas’ Lemma (but without unknown parameters), and the Lipschitz continuity in next-step termination by Lemma 5.10. If the output of the algorithm is successful, i.e. if the obtained system of linear inequalities is feasible, then the solution to the LP obtains concrete values for $\mathbf{a},b,K,\epsilon,c$ and leads to a concrete (difference-bounded) RSM-map $\eta$.

As our algorithm is based on LP solvers, we obtain polynomial-time complexity of our algorithm.

Theorem 8.2.

Our RSM-synthesis algorithm has polynomial-time complexity.

Example 8.3.

Consider the mini-roulette example showed in Figure 4(left) (Page 4).

1. (1)

The algorithm sets a linear template $\eta(x,w):=a_{1}\cdot x+a_{2}\cdot w+a_{3}$. 2. (2)

The algorithm encodes the conditions (A1)–(A3) as the inclusion assertions:

[TABLE] 3. (3)

The algorithm applies Farkas’ Lemma to all the inclusion assertions generated in the previous step and obtains a system of linear inequalities involving the parameters $a_{1},a_{2},a_{3},K,\epsilon$, where we over-approximate all strict inequalities (with ‘$<$’) by non-strict ones (with ‘$\leq$’). 4. (4)

The algorithm calls a linear programming (LP) solver on the linear program consisting of the system of linear inequalities generated in the previous step.

Finally, the algorithm outputs an optimal answer $\eta(x)=13\cdot x-13$ with $\epsilon=1,K=-13$(see Example 5.7). We can verify this $\eta$ is an RSM-map with RSM-continuity. Due to the fact that this loop is non-expansive and has bounded-update, we can conclude that this loop is expected affine-sensitive over its loop guard by Theorem 5.5.

Example 8.4.

Consider the mini-roulette variant example showed in Figure 4(right) (Page 4).

1. (1)

The algorithm sets a linear template $\eta(x,w):=a_{1}\cdot x+a_{2}\cdot w+a_{3}$. 2. (2)

The algorithm encodes the conditions (A1)–(A4) as the inclusion assertions:

[TABLE]

[TABLE] 3. (3)

The algorithm applies Farkas’ Lemma to all the inclusion assertions generated in the previous step and obtains a system of linear inequalities involving the parameters $a_{1},a_{2},a_{3},K,\epsilon$, where we over-approximate all strict inequalities (with ‘$<$’) by non-strict ones (with ‘$\leq$’). 4. (4)

The algorithm calls a linear programming (LP) solver on the linear program consisting of the system of linear inequalities generated in the previous step.

Finally, the algorithm outputs an optimal answer $\eta(x,w)=2.45\cdot x-2.45$ with $\epsilon=1,K=-4.91$(see Example 5.16). We can verify this $\eta$ a difference-bounded RSM-map with RSM-continuity. In this example, we find both the update function and the loop guard are affine, all sampling variables are bounded continuously-distributed, and the coefficients for the current sampling variables are not all zero in the loop guard of the next iteration, so we can conclude this loop has the Lipschitz continuity in next-step termination by Lemma 5.10. Therefore, by Theorem 5.15, we can obtained that this loop is expected linear-sensitive over its loop guard.

Remark 12 (Scalability).

As our approach is based on martingale synthesis, the scalability of our approach relies on the efficiency of martingale synthesis algorithms (Chatterjee et al., 2018c; Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2016; Chatterjee et al., 2018a, 2017; Wang et al., 2019; Feng et al., 2017).

9. Case Studies and Experimental Results

We demonstrate the effectiveness of our approach through case studies and experimental results. First, we consider two case studies of the SGD algorithm. Then in the experimental results, we use existing RSM-synthesis algorithms  (Chatterjee et al., 2018c; Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2016) (as is illustrated in the previous section) to synthesize linear RSM-maps for non-expansive simple loops such as the mini-roulette examples, the heating examples and many other examples from the literature. Note that by Theorem 5.5 and Theorem 5.15, the existence of RSM-maps with proper conditions (such as (A4), (B1)–(B4), etc.) leads to the expected sensitivity of all these examples.

9.1. Case Studies on Stochastic Gradient Descent

For the general SGD algorithm from Figure 3, we view each value $i$ from $1,2,\dots,n$ a probabilistic branch with probability $\frac{1}{n}$. By viewing so, we have that the value after one loop iteration is $F(\mathbf{w},i)$ where $F$ is the update function, $\mathbf{w}$ is the program valuation before the loop iteration and $i$ is the random integer sampled uniformly from $1,2,\dots,n$. In the case studies, we consider the metric defined from the Euclidean distance. To prove the expected affine-sensitivity of the SGD algorithm, we recall several properties for smooth convex functions (see e.g. (Nesterov, 2004)).

Definition 9.1 (Smooth Convex Functions).

A continuous differentiable function $f:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is convex if for all $u,v\in\mathbb{R}^{n}$, we have that $f(v)\geq f(u)+\langle(\nabla f)(u),v-u\rangle$.

In the following, we denote by $\mathcal{F}^{1}(\mathbb{R}^{n})$ the class of convex continuous differentiable Lipschitz-continuous functions, and by $\mathcal{F}^{1,1}_{\beta}(\mathbb{R}^{n})$ the subclass of convex continuous differentiable Lipschitz-continuous functions whose gradient is Lipschitz-continuous with a Lipschitz constant $\beta$. We also denote by $\mathbf{0}$ the zero vector. The following results can be found in  (Nesterov, 2004; Hardt et al., 2016).

Proposition 9.2.

If $f\in\mathcal{F}^{1}(\mathbb{R}^{n})$ and $(\nabla f)(u^{*})=\mathbf{0}$, then $u^{*}$ is the global minimum of $f$ on $\mathbb{R}^{n}$.

Proposition 9.3.

For any function $f\in\mathcal{F}^{1,1}_{\beta}(\mathbb{R}^{n})$ and real number $0<\gamma\leq\frac{2}{\beta}$, we have that the function $g$ defined by $g(u):=u-\gamma\cdot(\nabla f)(u)$ is Lipschitz-continuous with Lipschitz constant $1$.

We consider the SGD algorithm in Figure 3 whose execution time is randomized and depends on the input program valuation. Recall that we consider the loop guard $\Phi$ of the SGD algorithm to be $G(\mathbf{w})\geq\zeta$ so that $\zeta$ is the acceptable threshold of the (non-negative) loss function $G$ and the aim of the algorithm is to find a solution $\mathbf{w}^{*}$ satisfying $G(\mathbf{w}^{*})<\zeta$, as described in Example 4.3. Following (Hardt et al., 2016), we assume that each loss function $G_{i}$ lies in $\mathcal{F}^{1,1}_{\beta}(\mathbb{R}^{n})$ (so that the Euclidean magnitude of its gradient will always be bounded by a constant $M$), with a single Lipschitz constant $\beta$ for all $i$. For practical purpose, we further consider the following assumptions:

1. (1)

the function $G$ has a global minimum $\zeta_{\min}$ at $\mathbf{w}_{\min}$ so that $G(\mathbf{w}_{\min})=\zeta_{\min}$, which is satisfied by many convex functions; 2. (2)

the parameters $\mathbf{w}$ will always be bounded during the execution of the SGD algorithm, i.e., $\|\mathbf{w}\|_{2}\leq R$ for some radius $R>0$. This can be achieved by e.g. regularization techniques where a penalty term is added to each $G_{i}$ to prevent the parameters from growing too large; 3. (3)

in order to ensure termination of the algorithm, we consider that the threshold value $\zeta$ is strictly greater than the global minimum $\zeta_{\min}$.

Below we illustrate the case studies, showing the expected (approximately linear) sensitivity of the SGD algorithm. The first fixes the vector $\vartheta$ of $n$ training data that results in a non-expansive loop, while the second considers sensitivity w.r.t the training data and leads to an expansive loop in general.

Case Study A: sensitivity w.r.t initial parameters. In this case study, we fix the training data $\vartheta$. By Proposition 9.3, we have that the loop is non-expansive w.r.t the Euclidean distance if the step size $\gamma$ is small enough, for all $i$. Moreover, from the bound $M$, we have that the loop body has bounded update in $\mathbf{w}$, with a bound $d=M^{\prime\prime}\cdot\gamma$ for some constant $M^{\prime\prime}$ determined by $M$.

Define the RSM-map $\eta$ by $\eta(\mathbf{w}):=G(\mathbf{w})-\zeta$. We show that $\eta$ is indeed an RSM-map when the step size $\gamma$ is sufficiently small. Since $G$ is smooth convex, we have from Proposition 9.2 that $\nabla G(\mathbf{w})=\mathbf{0}$ iff $\mathbf{w}$ is the global minimum on $\mathbb{R}^{n}$. Thus by the compactness from the radius $R$, we have that $G(\mathbf{w})\geq\zeta>\zeta_{\min}$ implies ${\parallel}{\nabla G(\mathbf{w})}{\parallel}^{2}_{2}\geq\delta$ for a fixed constant $\delta>0$. Then by the Mean-Value Theorem, there is a vector $\mathbf{w^{\prime}}$ on the line segment between $\mathbf{w}$ and $\mathbf{w}-\gamma\cdot\nabla G_{i}(\mathbf{w})$ such that

[TABLE]

By the smoothness and the Cauchy-Schwarz’s Inequality, we have that

[TABLE]

It follows that

[TABLE]

where $|C|\leq\gamma^{2}\cdot\beta\cdot M^{2}$. Hence by choosing a step size $\gamma$ small enough, whenever $G(\mathbf{w})\geq\zeta$ and the SGD algorithm enters the loop, we have $\mathbb{E}_{i}(\eta(\mathbf{w}-\gamma\cdot\nabla G_{i}(\mathbf{w})))\leq\eta(\mathbf{w})-\frac{\delta\cdot\gamma}{2\cdot n}$. Thus, we can choose $\epsilon=\frac{\delta\cdot\gamma}{2\cdot n}$ to fulfill the condition (A3). Moreover, by choosing $K=-\gamma\cdot M^{\prime}$ for some positive constant $M^{\prime}$ determined by $M$, we have that when the SGD algorithm terminates, it is guaranteed that $K\leq\eta(\mathbf{w})\leq 0$. Hence, $\eta$ is an RSM-map for the SGD algorithm. Then by Theorem 5.5, we obtain the desired result that the SGD algorithm is expected affine-sensitive w.r.t the initial input parameters. In detail, we have the coefficients $A_{\gamma},B_{\gamma}$ from Theorem 5.5 that $A_{\gamma}=2\cdot\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}},B_{\gamma}=-2\cdot\frac{d\cdot K}{\epsilon\cdot D_{1}}$. As both $d,K,\epsilon$ are proportional to the step size $\gamma$, when $\gamma\rightarrow 0$, we have that $A_{\gamma}$ remains bounded and $B_{\gamma}\rightarrow 0$. Thus, our approach derives that the SGD algorithm is approximately expected linear sensitive (over all $G(\mathbf{w})\geq\zeta$) when the step size tends to zero.

Case Study B: sensitivity w.r.t both initial parameters and training data. Second, we consider the expected affine-sensitivity around a neighbourhood of initial parameters $\mathbf{w}^{*}$ and the training data $\vartheta^{*}$. Similar to the first case study, we consider that the values of the parameters $\mathbf{w}$ are always bounded in some radius and the magnitude of each individual training data is also bounded. A major difference in this case study is that we cannot ensure the non-expansiveness of the loop as the variation in the training data may cause the loop to be expansive. Instead, we consider the general case that the loop is expansive with the Lipschitz constant $L_{\gamma}=1+\gamma\cdot C$ for some constant $C>0$.

Define the RSM-map $\eta$ again as $\eta(\mathbf{w},\vartheta):=G(\mathbf{w},\vartheta)-\zeta$. Similarly, we can show that $\eta$ is an RSM-map when the step size $\gamma$ is sufficiently small, with parameters $\epsilon,K,d,M$ derived in the same way as in the first case study; in particular, both $d,K,\epsilon,c$ are proportional to the step size $\gamma$ and we denote $\epsilon=M_{1}\cdot\gamma$. Moreover, the RSM-map $\eta$ is difference bounded with bound $c=M_{2}\cdot\gamma$, where $M_{2}$ is a constant determined by $M$. Then by Theorem 6.1, we obtain that the SGD algorithm is expected affine-sensitive w.r.t both the initial input parameters and the training data. By a detailed calculation, we have the coefficients $A_{\gamma},B_{\gamma}$ from Theorem 6.1 that

[TABLE]

where $A^{\prime}_{\gamma}=\frac{d\cdot M+\epsilon}{D_{1}\cdot\epsilon}$, $B^{\prime}_{\gamma}=-\frac{d\cdot K}{D_{1}\cdot\epsilon}$ and $N_{\gamma}=\lfloor 4\cdot\frac{\eta(\mathbf{w}^{*},\vartheta^{*})}{\epsilon}\rfloor+1$. As both $d,K,\epsilon,c$ are proportional to the step size $\gamma$, we have that $A^{\prime}_{\gamma}$ remains bounded and $B^{\prime}_{\gamma}\rightarrow 0$. Moreover, we have that

[TABLE]

where we recall that $e$ is the base for natural logarithm. Hence, $L_{\gamma}^{N_{\gamma}}$ remains bounded when $\gamma\rightarrow 0$. Furthermore, as $\frac{\epsilon}{c^{2}}\rightarrow\infty$ and $\frac{\epsilon^{2}}{c^{2}}$ is constant when $\gamma\rightarrow 0$, we obtain that $A_{\gamma}$ remain bounded and $B_{\gamma}\rightarrow 0$ when the step size tends to zero. Thus, we can also assert in this case that the SGD algorithm is approximately expected linear-sensitive (around a neighbourhood of the given input parameters and training data) when the step size tends to zero.

9.2. Experimental Results

We implemented our approach in Section 8 and obtained experimental results on a variety of programs. Recall we use Lemma 5.10 to ensure the Lipschitz continuity in next-step termination, and manually check whether a loop is non-expansive (which as mentioned in Section 8 can also be automated).

Experimental Examples. We consider examples and their variants from the literature (Abate et al., 2010; Chatterjee et al., 2018b, c; Ngo et al., 2018; Wang et al., 2019). Single/double-room heating is from (Abate et al., 2010). Mini-roulette, American roulette are from (Chatterjee et al., 2018b). Ad rdwalk 1D, Ad rdwalk 2D are from (Chatterjee et al., 2018c). rdwalk, prdwalk, prspeed and race are from (Ngo et al., 2018). Simple-while-loop, pollutant-disposal are from (Wang et al., 2019). See Appendix G for these detailed examples. All the assignment statements in these examples (except for single/double-room heating) are of the form $x:=x+r$, where $r$ is a constant or a random variable, so we can find these examples are non-expansive.

For single/double-room heating (Figure 6 and Figure 6), we choose the values of the parameters $b,b_{1},b_{2},a_{12},a_{21}$ be small enough, so that we can find the two examples non-expansive by manually inspection. In our experiments, we choose $x_{a}=10,b=b_{1}=0.03,c=c_{1}=1.5,w~{}\sim\mathsf{unif}(-0.3,0.3)$, $b_{2}=0.02,a_{12}=a_{21}=0.04,w_{1}~{}\sim\mathsf{unif}(-0.3,0.3),w_{2}~{}\sim\mathsf{unif}(-0.2,0.2)$. We use the max-norm as the metric. In this example, as the loop counter $n$ starts always with [math], our experimental results show that the programs are expected affine/linear sensitive in $n$ (i.e., the number of loop iterations).

Implementations and Results. We implemented our approach in Matlab R2018b. The results were obtained on a Windows machine with an Intel Core i5 2.9GHz processor and 8GB of RAM. Examples of expected affine-sensitivity are illustrated in Table 2, where the first column specifies the example and the program variable of concern, the second is the running time (in seconds) for the example, the third column is the RSM-map, and the last columns specify its related constants. Examples of expected linear-sensitivity are illustrated in Table 3 with similar layout.

Remark 13.

In this work, we only consider the synthesis of linear RSM-maps to prove expected sensitivity. Given that algorithms for synthesis of polynomial RSM-maps are also present (see (Chatterjee et al., 2016; Feng et al., 2017)), it is also possible to tackle the case studies in Section 9.1 if the number of training data is fixed (so that the number of program variables is fixed) and the loss function $G$ is polynomial. We plan the further investigation of automated synthesis of complex RSM-maps for proving expected sensitivity as a future work.

10. Related Work

In program verification Lipschitz continuity has been studied extensively: a SMT-based method for proving programs robust for a core imperative language is presented in (Chaudhuri et al., 2010); a linear type system for proving sensitivity has been developed in (Reed and Pierce, 2010); approaches for differential privacy in higher-order languages have also been considered (de Amorim et al., 2017; Gaboardi et al., 2013; Winograd-Cort et al., 2017).

For probabilistic programs computing expectation properties have been studied over the decades, such as, influential works on PPDL (Kozen, 1985) and PGCL (Morgan et al., 1996). Various approaches have been developed to reason about expected termination time of probabilistic programs (Kaminski et al., 2016; Fu and Chatterjee, 2019; Chatterjee et al., 2018c) as well as to reason about whether a probabilistic program terminates with probability one (McIver et al., 2017; Huang et al., 2018a; Agrawal et al., 2018; Chatterjee et al., 2017). However, these works focus on non-relational properties, such as, upper bounds expected termination time, whereas expected sensitivity is intrinsically relational. To the best of our knowledge while RSMs have been used for non-relational properties, we are the first to apply for relational properties.

There is also a great body of literature on relational analysis of probabilistic programs, such as, relational program logics  (Barthe et al., 2009) and differential privacy of algorithms (Barthe et al., 2012). However, this line of works does not consider relational expectation properties. There have also been several works on relational expectation properties in several specific area, e.g., in the area of masking implementations in cryptography, quantitative masking (Eldib et al., 2015) and bounded moment model (Barthe et al., 2016).

The general framework to consider probabilistic program sensitivity was first considered in (Barthe et al., 2017), and later improved in (Barthe et al., 2018). Several classical examples such as stochastic gradient descent, population dynamics or Glauber dynamics can be analyzed in the framework of (Barthe et al., 2018). Another method for the sensitivity analysis of probabilistic programs has been proposed in (Huang et al., 2018b) and they analysed a linear-regression example derived from the SGD algorithm in (Barthe et al., 2018). For details of literature on relational analysis of probabilistic programs leading to the work of (Barthe et al., 2018) see (Barthe et al., 2018, Section 9).

Below we compare our result in detail with the most related results, i.e., (Barthe et al., 2018), (Huang et al., 2018b) and also a recent arXiv submission (Aguirre et al., 2019). Recall that we have discussed the issue of conditional branches at the end of Section 1. Here we compare other technical aspects.

Comparison with (Barthe et al., 2018). The result of (Barthe et al., 2018) is based on the classical notion of couplings. Coupling is a powerful probabilistic proof technique to compare two distributions $X$ and $Y$ by creating a random distribution $W$ who marginal distributions correspond to $X$ and $Y$. Given a program with two different inputs $x$ and $y$, let $X_{i}$ and $Y_{i}$ denote the respective probability distribution after the $i$-th iteration. If the number of iterations is fixed, then coupling can be constructed for each $i$-th step. However, if the number of iterations is randomized and variable-dependent, then in one case termination could be achieved while the other case still continues with the loop. In such situation, a suitable coupling is cumbersome to obtain. Thus, while coupling present an elegant technique for fixed number of iterations, our approach applies directly to the situation where the number of iterations is randomized as well as variable dependent. The advantage of coupling-based proof rules is that such approach can handle variable-dependent sampling and complex data structures through manual proofs. This leads to the fact that their approach can prove rapid mixing of population dynamics and glauber dynamics, while our approach in its current form cannot handle such examples. A strengthening of our approach to handle these type of examples (through e.g. an integration with coupling) is an interesting future direction.

Comparison with (Huang et al., 2018b). The result of (Huang et al., 2018b) develops an automated tool based on computer algebra that calculates tight sensitivity bounds for probabilistic programs. As computer algebra requires to unroll every loop into its sequential counterpart without looping, the approach is suitable only for programs with a bounded number of loop iterations and cannot handle variable-dependent randomized loop iterations that typically lead to unbounded loop iterations. In contrast, our approach can handle unbounded variable-dependent randomized loop iterations.

Comparison with a recent arXiv submission. Recently, there is an arXiv submission (Aguirre et al., 2019) that also involves sensitivity analysis of probabilistic programs. Although their approach can handle randomized loop iterations to some extent, the approach requires that the executions from two close-by inputs should synchronize strictly, and simply assigns $\infty$ to non-synchronous situations such as one program valuation enters the loop while the other does not (see the definition for if-branch and while loop in  (Aguirre et al., 2019, Figure 1)). Moreover, all the examples for illustrating their approach have fixed and bounded number of loop iterations, while all our examples have variable-dependent randomized loop iterations.

11. Conclusion

In this work we studied expected sensitivity analysis of probabilistic programs, and presented sound approaches for the analysis of (sequential composition of) probabilistic while loops whose termination time is randomized and depends on the input values, rather than being fixed and bounded. Our approach can be automated and can handle a variety of programs from the literature. An interesting future direction is to extend our approach to a wider class of programs (e.g., programs with expansive loops, conditional branches and variable-dependent sampling, synthesis of complex RSM-maps, etc.). Another important direction is to consider methods for generating tight bounds for sensitivity. Besides, integration with coupling-based approaches and practical issues arising from e.g. floating-point arithmetics would also be worthwhile to address.

Acknowledgements.

We thank anonymous reviewers for helpful comments, especially for pointing to us a scenario of piecewise-linear approximation (Remark 5). We are grateful to Prof. Yuxi Fu, director of the BASICS Lab at Shanghai Jiao Tong University, for his support.

Appendix A The Detailed Syntax

The detailed syntax is in Figure 7.

Appendix B Proof for the Integral Expansion

Theorem B.1 (Integral Expansion).

Let $Q$ be a simple probabilistic while loop in the form (1) and $z$ be a program variable. For any input program valuation $\mathbf{b}$ such that $\mathbf{b}\models\Phi$, we have

[TABLE]

where $Z_{\mathbf{b}^{\prime}}$ is the random variable for the value of $z$ after the execution of $Q$ from the input program valuation $\mathbf{b}^{\prime}$, and $p_{\ell}$ is the probability that the probabilistic branches follows the choices in $\ell$.

Proof.

The result follows from the following derivations:

[TABLE]

∎

Appendix C Proofs for Section 5

To prove Theorem 5.5 we need the following known result.

Theorem C.1.

(Chatterjee et al., 2018c; Fu and Chatterjee, 2019)* If there exists an RSM-map $\eta$ with $\epsilon,K$ given as in Definition 5.2 for a simple probabilistic while loop $Q$ in the form (1), then for any input program valuation $\mathbf{b}$ we have $\mathbb{E}_{\mathbf{b}}(T)\leq\frac{\eta(\mathbf{b})-K}{\epsilon}$, where $T$ is the random variable for the number of loop iterations.*

Theorem 5.5. A simple non-expansive while loop $Q$ in the form (1) is expected affine-sensitive over its loop guard ${\llbracket}{\Phi}{\rrbracket}$ if we have that

• •

$Q$ has bounded update, and

• •

there exists an RSM-map for $Q$ that has RSM-continuity.

In particular, we can choose $\theta=\infty$ and $A=2\cdot\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}},B=-2\cdot\frac{d\cdot K}{\epsilon\cdot D_{1}}$ in (3), where the parameters $d,M,\epsilon,K,D_{1}$ are from Definition 5.2, Definition 5.3, Definition 5.4 and (2).

Proof.

Consider any program variable $z$. Let $d$ be a bound from Definition 5.3, and $\eta$ be an RSM-continuous RSM-maps with $\epsilon,K$ from Definition 5.2 and the constant $M$ from Definition 5.4. Consider any input program valuations $\mathbf{b},\mathbf{b}^{\prime}$ such that $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$. Denote $\delta:=\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. We use $T_{\mathbf{b}^{\prime\prime}}$ to denote the random variable for the number of loop iterations of the executions starting from an input program valuation $\mathbf{b}^{\prime\prime}$. We also use $Z_{\mathbf{b}^{\prime\prime}}$ to denote the random variable for the value of $z$ after the execution of $Q$ from $\mathbf{b}^{\prime\prime}$. We illustrate the main idea through clarifying the relationships between program valuations $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ in any runs $\omega=\{\mathbf{b}_{n}\}_{n\geq 0}$, $\omega^{\prime}=\{\mathbf{b}^{\prime}_{n}\}_{n\geq 0}$ that start from respectively $\mathbf{b},\mathbf{b}^{\prime}$ and use the same sampled values in each loop iteration. Consider that the event $\min\{T_{\mathbf{b}},T_{\mathbf{b}^{\prime}}\}\geq n$ holds (i.e., both the executions do not terminate before the $n$th step). We have the following cases:

• Case 1.

Both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$ violate the loop guard $\Phi$, i.e., $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}\models\neg\Phi$. This case describes that the loop $Q$ terminates exactly after the $n$-th iteration of the loop for both the initial valuations. From the condition (B1), we obtain directly that $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta$. Hence $|\mathbf{b}_{n}[z]-\mathbf{b}^{\prime}_{n}[z]|\leq\frac{\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})}{D_{1}}\leq\frac{\delta}{D_{1}}$.

• Case 2.

Exactly one of $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. This is the non-synchronous situation that needs to be addressed through martingales. W.l.o.g., we can assume that $\mathbf{b}_{n}\models\Phi$ and $\mathbf{b}^{\prime}_{n}\models\neg\Phi$. From the upper-bound property of RSM-maps (see Theorem C.1 in Appendix C), we derive that $\mathbb{E}_{\mathbf{b}_{n}}(T_{\mathbf{b}_{n}})\leq\dfrac{\eta(\mathbf{b}_{n})-K}{\epsilon}$. From the bounded-update condition (B2) and the triangle inequality of metrics, we have that $|\mathbf{b}_{n}[z]-Z_{\mathbf{b}_{n}}|\leq\frac{1}{D_{1}}\cdot\mathfrak{d}(\mathbf{b}_{n},\mathbf{W}_{\mathbf{b}_{n}})\leq\frac{d}{D_{1}}\cdot T_{\mathbf{b}_{n}}$. Thus, we obtain that

[TABLE]

From the non-expansiveness we have $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta$. Then by the RSM-continuity (B3), we have $|\eta(\mathbf{b}_{n})-\eta(\mathbf{b}^{\prime}_{n})|\leq M\cdot\delta$. Furthermore, from (A2) we have $\eta(\mathbf{b}^{\prime}_{n})\leq 0$. So we obtain that $\eta(\mathbf{b}_{n})\leq M\cdot\delta$. It follows that

[TABLE]

• Case 3.

Neither $\mathbf{b}_{n}$ nor $\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. In this case, the loop $Q$ will continue from both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$. Then in the next iteration, the same analysis can be carried out for the next program valuations $\mathbf{b}_{n+1},\mathbf{b}^{\prime}_{n+1}$.

From the termination property ensured by RSM-maps (Theorem C.1), the probability that the third case happens infinitely often equals zero. Thus, the sensitivity analysis eventually reduces to the first two cases, and the first two cases derives the expected affine-sensitivity.

In the following, we demonstrate the detailed proof. By Theorem B.1 (in Appendix B), for a program valuation $\mathbf{b}^{\prime\prime}$ satisfying the loop guard $\Phi$, we can derive that

[TABLE]

On the other hand, if $\mathbf{b}^{\prime\prime}\not\models\Phi$, then we obtain straightforwardly that $\mathbb{E}_{\mathbf{b}^{\prime\prime}}(Z_{\mathbf{b}^{\prime\prime}})=\mathbf{b}^{\prime\prime}[z]$. Note that if for a particular sampled valuation $\mathbf{r}$ we have $F(\ell,\mathbf{b}^{\prime\prime},\mathbf{r})\models\Phi$, then we can use Theorem B.1 to expand the integrand further into an integral, i.e.,

[TABLE]

Note that once we have $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$, we can derive from the linearity of integral that

[TABLE]

Then using (6), we can expand the integral above into an arbitrary depth until we reach an end situation $\mathbb{E}_{\mathbf{b}_{1}}(Z_{\mathbf{b}_{1}})-\mathbb{E}_{\mathbf{b}_{2}}(Z_{\mathbf{b}_{2}})$ such that either $\mathbf{b}_{1}\not\models\Phi$ or $\mathbf{b}_{2}\not\models\Phi$. (This situation corresponds to the first two cases demonstrated previously and will eventually happen since we have $\mathbb{P}(T_{\mathbf{b}}<\infty)=\mathbb{P}(T_{\mathbf{b}^{\prime}}<\infty)=1$.)

Below given any program valuation $\mathbf{b}^{\prime\prime}$ and any infinite sequence $\rho=\{\mathbf{r}_{n}\}$ where each $\mathbf{r}_{n}$ represents the sampled valuation in the $(n+1)$-th loop iteration, we define the infinite sequence $\omega_{\mathbf{b}^{\prime\prime},\rho}$ as the unique execution that starts from $\mathbf{b}^{\prime\prime}$ and follows the samplings in $\rho$.

Consider any program valuations $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$ and any infinite sequence $\rho$ of sampled valuations such that either $T_{\mathbf{b}}(\omega_{\mathbf{b},\rho})=m$ or $T_{\mathbf{b}^{\prime}}(\omega_{\mathbf{b}^{\prime},\rho})=m$, for a natural number $m$. Denote $\omega_{\mathbf{b},\rho}=\{\mathbf{b}_{n}\}_{n\geq 0}$ and $\omega_{\mathbf{b}^{\prime},\rho}=\{\mathbf{b}^{\prime}_{n}\}_{n\geq 0}$. Then this sequence corresponds to an integral expansion path from $\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}})$ to an end situation $\mathbb{E}_{\mathbf{b}_{m}}(Z_{\mathbf{b}_{m}})-\mathbb{E}_{\mathbf{b}^{\prime}_{m}}(Z_{\mathbf{b}^{\prime}_{m}})$ such that either $\mathbf{b}_{m}\not\models\Phi$ or $\mathbf{b}^{\prime}_{m}\not\models\Phi$. Since this situation falls in the first two cases discussed previously in the proof, we obtain that

[TABLE]

Denote $A^{\prime}:=\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}}$ and $B^{\prime}:=\frac{d\cdot K}{\epsilon\cdot D_{1}}$. Since the choice of $\rho$ is arbitrary, we have that the total amount contributed to the value of the integral in (7) under the situation “either $T_{\mathbf{b}}=m$ or $T_{\mathbf{b}^{\prime}}=m$” is no more than

[TABLE]

which is no greater than

[TABLE]

By summing up all steps $m$’s, we obtain that

[TABLE]

where $A:=2\cdot A^{\prime}$ and $B:=2\cdot B^{\prime}$. ∎

Appendix D Proofs for Section 5.2

Lemma 5.10. Consider a simple while loop $Q$ in the form (1) that satisfies the following conditions:

1. (1)

both $F$ and $\Phi$ are affine and $\Phi$ is equivalent to some DNF $\bigvee_{i\in\mathcal{I}}(\mathbf{A}_{i}\cdot\mathbf{b}\leq\mathbf{d}_{i})$; 2. (2)

all sampling variables are continuously-distributed whose probability density functions have bounded values; 3. (3)

for all $i\in\mathcal{I}$, $\ell\in\mathbf{L}$ and program valuations $\mathbf{b}\models\Phi$, the coefficients for the sampling variables $\mathbf{r}$ in $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b},\mathbf{r})$ are not all zero at each row, i.e., the truth value of each disjunctive clause in $\Phi$ for $F(\ell,\mathbf{b},\mathbf{r})$ depends on $\mathbf{r}$ at every row.

Then the loop $Q$ has the Lipschitz continuity in next-step termination w.r.t any metric $\mathfrak{d}$.

Proof.

Denote the update function $F$ by $F(\ell,\mathbf{b},\mathbf{r})=\mathbf{B}\cdot\mathbf{b}+\mathbf{C}\cdot\mathbf{r}+\mathbf{c}$ . Consider any $\ell\in\mathbf{L}$ and any program valuations $\mathbf{b},\mathbf{b}^{\prime}$ that satisfy $\Phi$. Then the probability $p$ that $F(\ell,\mathbf{b},(r_{1},r_{2}))\models\Phi$ and $F(\ell,\mathbf{b}^{\prime},(r_{1},r_{2}))\not\models\Phi$ is smaller than the probability that for some $i$, $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b},(r_{1},r_{2}))\leq\mathbf{d}_{i}$ and $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b}^{\prime},(r_{1},r_{2}))\,{\not\leq}\,\mathbf{d}_{i}$. Let $p_{i}$ be the probability that $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b},(r_{1},r_{2}))\leq\mathbf{d}_{i}$ and $\mathbf{A}_{i}\cdot F(\ell,\mathbf{b}^{\prime},(r_{1},r_{2}))\,{\not\leq}\,\mathbf{d}_{i}$. Then $p_{i}$ equals the probability of the event that

[TABLE]

Furthermore, the event (8) implies that for some row $j$, the event

[TABLE]

holds. Denote the probability of the event (9) by $p_{ij}$. By the third condition in the statement of the lemma, we have that $(\mathbf{A}_{i}\cdot\mathbf{C})_{j}$ is not the zero vector. Then following from the fact that all the sampling variables are continuously-distributed and have bounded probability density functions, the probability $p_{ij}$ is no greater than $L^{\prime}_{ij}\cdot{\parallel}{\mathbf{b}-\mathbf{b}^{\prime}}{\parallel}_{\infty}$ where $L^{\prime}_{ij}$ is a constant. To clarify this point, we can assume that there are only two sampling variables $r_{1},r_{2}$. The situation for more variables is similar. Under this assumption, we have $(\mathbf{A}_{i}\cdot\mathbf{C})_{j}\cdot\mathbf{r}=a_{1}\cdot r_{1}+a_{2}\cdot r_{2}$ (note that $a_{1},a_{2}$ are not all zero) and the event (9) becomes

[TABLE]

If both $a_{1},a_{2}$ are non-zero and $a_{2}>0$, then we derive directly that

[TABLE]

where $f_{1},f_{2}$ are probability density functions for respectively $r_{1},r_{2}$ and

[TABLE]

[TABLE]

Thus we have $p_{ij}\leq L^{\prime}_{ij}\cdot{\parallel}{\mathbf{b}-\mathbf{b}^{\prime}}{\parallel}_{\infty}$ where the constant $L^{\prime}_{ij}$ is determined by $a_{2},(\mathbf{A}_{i}\cdot\mathbf{B})_{j}$ and the bound for $f_{2}$. The situation for other cases is similar. So we have that $p\leq\sum_{i,j}p_{ij}\leq(\sum_{i,j}L^{\prime}_{i,j})\cdot{\parallel}{\mathbf{b}-\mathbf{b}^{\prime}}{\parallel}_{\infty}\leq\frac{\sum_{i,j}L^{\prime}_{i,j}}{D_{1}}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Finally, we sum up all the probabilistic choices $\ell\in\mathbf{L}$ and obtain the desired result. ∎

Proposition 5.11. A non-expansive simple while loop $Q$ in the form (1) has expected linear-sensitivity over any neighbourhood $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$ of any given $\mathbf{b}^{*}\in{\llbracket}{\Phi}{\rrbracket}$ if $Q$ has (i) bounded update, (ii) an RSM-map with RSM-continuity and (iii) the Lipschitz continuity in next-step termination.

Proof.

The proof resembles the one for expected affine-sensitivity (Theorem 5.5). Consider runs $\omega=\{\mathbf{b}_{n}\}_{n\geq 0}$, $\omega^{\prime}=\{\mathbf{b}^{\prime}_{n}\}_{n\geq 0}$ starting from respectively program valuations $\mathbf{b},\mathbf{b}^{\prime}\in U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$ and use the same sampled values for each loop iteration. We first analyze the case that $\mathbf{b}=\mathbf{b}^{*}$. Consider that the event $\min\{T_{\mathbf{b}},T_{\mathbf{b}^{\prime}}\}\geq n$ holds. We have exactly the three cases demonstrated in the expected affine-sensitivity analysis, and again the sensitivity analysis eventually reduces to the first two cases (see the proof for Theorem 5.5). As we enhance the conditions in Theorem 5.5 with the Lipschitz continuity in next-step termination, we have a strengthened analysis for the second case (i.e., exactly one of $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ violates the loop guard) as follows. W.l.o.g, we assume that $\mathbf{b}_{n}\models\Phi$ and $\mathbf{b}^{\prime}_{n}\not\models\Phi$ in the second case. As in the proof of Theorem 5.5, we define $\delta:=\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\rho$ and obtain that $|\mathbb{E}_{\mathbf{b}_{n}}(Z_{\mathbf{b}_{n}})-\mathbb{E}_{\mathbf{b}^{\prime}_{n}}(Z_{\mathbf{b}^{\prime}_{n}})|\leq A\cdot\delta+B\leq A\cdot\rho+B=:C$ where $A:=\frac{d\cdot M+\epsilon}{\epsilon\cdot D_{1}}$ and $B:=\frac{d\cdot K}{\epsilon\cdot D_{1}}$. From the Lipschitz continuity in next-step termination, we have that the second case happens with probability at most $L^{\prime}\cdot\mathfrak{d}(\mathbf{b}_{n-1},\mathbf{b}^{\prime}_{n-1})$, where $L^{\prime}>0$ is from Definition 5.9. Thus, the difference contributed to the total sensitivity $|\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}_{n}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}_{n}})|$ in the first two cases is at most

[TABLE]

where the first summand is from the first case and the second is from the second case. From the non-expansiveness, we have that $\mathfrak{d}(\mathbf{b}_{n-1},\mathbf{b}^{\prime}_{n-1}),\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta$. By summing up all $n$’s together, using the fact that $\mathbb{E}_{\mathbf{b}}(T_{\mathbf{b}})=\sum_{n=0}^{\infty}\mathbb{P}(T_{\mathbf{b}}>n)$, we obtain that

[TABLE]

For the case $\mathbf{b}\neq\mathbf{b}^{*}$, we simply have

[TABLE]

that implies the desired local linear sensitivity. ∎

Lemma 5.13. If $\eta$ is a difference-bounded RSM-map with the parameters $\epsilon,c$ specified in Definition 5.2 and Definition 5.12, then there exists a constant $p\in(0,1]$ such that

• (†)

$\forall\mathbf{b}:\left(\mathbf{b}\models\Phi\Rightarrow\mathbb{P}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})\leq-\frac{1}{2}\cdot\epsilon)\geq p\right)$

where the probability $\mathbb{P}_{\mathbf{r},\ell}(-)$ is taken w.r.t the sampled valuation $\mathbf{r}$ and the resolution $\ell$ for probabilistic branches, and treats the program valuation $\mathbf{b}$ as constant. In particular, we can take $p:=\frac{\epsilon}{2\cdot c-\epsilon}$.

Proof.

Consider any program valuation $\mathbf{b}$ such that $\mathbf{b}\models\Phi$. Denote $u:=\mathbb{E}_{\mathbf{r}}(\eta(F(\ell,\mathbf{b},\mathbf{r})))-\eta(\mathbf{b})$ and $q:=\mathbb{P}_{\mathbf{r},\ell}(\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b},\mathbf{r})\leq-\frac{1}{2}\cdot\epsilon)$. By (A3) and (A4) we have that $u\leq-\epsilon<0$ and $0<\epsilon\leq c$. Then from (A4) and the Markov’s inequality, we have that

[TABLE]

By taking $p:=1-\frac{c-\epsilon}{c-\frac{1}{2}\cdot\epsilon}=\frac{\epsilon}{2\cdot c-\epsilon}$, we obtain the desired result. ∎

Proposition 5.14. For any natural number $n\geq 1$, real numbers $C,D\geq 0$ and probability value $p\in(0,1]$, the following system of linear inequalities (with real variables $A_{k}$’s ($1\leq k\leq n$) and $A_{\infty}$)

[TABLE]

has a solution.

Proof.

We find a solution to the system of linear inequalities by equating each $(1-p)\cdot A_{\infty}+C+p\cdot A_{k}$ with $A_{k+1}$. After the equating, we have from induction on $k$ that

[TABLE]

By solving the last equation, we obtain that

• •

$A_{\infty}=\frac{1}{p^{n+1}}\cdot(\sum_{m=1}^{n+1}p^{m-1})\cdot C+D=\frac{1}{p^{n+1}}\cdot\frac{1-p^{n+1}}{1-p}\cdot C+D$,

• •

$A_{k}=(\frac{1-p^{k}}{p^{n+1}}\cdot(\sum_{m=1}^{n+1}p^{m-1})+(\sum_{m=1}^{k}p^{m-1}))\cdot C+D=(\frac{1-p^{k}}{p^{n+1}}\cdot\frac{1-p^{n+1}}{1-p}+\frac{1-p^{k}}{1-p})\cdot C+D$ for $1\leq k\leq n$.

Below we show that this solution (together with $A_{0}=D$) satisfies that $A_{0}\leq A_{1}\leq\dots\leq A_{n}\leq A_{\infty}$. First we show that $A_{0}\leq A_{1}$ and $A_{n}\leq A_{\infty}$. This follows directly from the fact that

[TABLE]

Then as $(1-p)\cdot A_{\infty}+C+p\cdot A_{k}=A_{k+1}$ for $1\leq k<n$, we easily prove by induction on $k$ that $A_{k}\leq A_{k+1}$ for all $1\leq k<n$. ∎

Theorem 5.15. A non-expansive simple while loop $Q$ in the form (1) has expected linear-sensitivity over its loop guard ${\llbracket}{\Phi}{\rrbracket}$ if $Q$ has (i) bounded update, (ii) a difference-bounded RSM-map with RSM-continuity and (iii) the Lipschitz continuity in next-step termination. In particular, we can choose $\theta=\frac{1}{M}$ in (3) where the parameter $M$ is from the RSM-continuity (Definition 5.4).

Proof.

Choose any program variable $z$. Denote by $T,T^{\prime}$ (resp. $Z_{n},Z^{\prime}_{n}$) the random variables for the number of loop iterations (resp. the value of $z$ at the $n$-th step), from the input program valuations $\mathbf{b},\mathbf{b}^{\prime}$, respectively. For each natural number $n\geq 0$, define $\delta_{n}(\mathbf{b},\mathbf{b}^{\prime}):=\mathbb{E}_{\mathbf{b}}(Z_{T\wedge n})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{T^{\prime}\wedge n})$ for program valuations $\mathbf{b},\mathbf{b}^{\prime}$, where the random variable $T\wedge n$ is defined as $\min\{T,n\}$ and $T^{\prime}\wedge n$ likewise. We also define $\delta(\mathbf{b},\mathbf{b}^{\prime}):=\mathbb{E}_{\mathbf{b}}(Z_{T})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{T^{\prime}})$. By Theorem C.1, we have $\mathbb{E}_{\mathbf{b}}(T),\mathbb{E}_{\mathbf{b}^{\prime}}(T^{\prime})<\infty$. Then from the bounded-update condition and Dominated Convergence Theorem, we have that $\lim\limits_{n\rightarrow\infty}\mathbb{E}(Z_{T\wedge n})=\mathbb{E}(Z_{T})$ and the same holds for $Z_{T^{\prime}\wedge n}$. Thus, we have that $\lim\limits_{n\rightarrow\infty}\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})=\delta(\mathbf{b},\mathbf{b}^{\prime})$.

Let $\eta$ be a difference-bounded RSM-continuous RSM-map with the parameters $c,\epsilon,M$ as specified in (A3), (A4), (B3). By Lemma 5.13, we can obtain a probability value $p=\frac{\epsilon}{2\cdot c-\epsilon}$ such that the condition $({\dagger})$ holds. We also construct the regions $R_{k}$’s ($1\leq k\leq n^{*}$) and $R_{\infty}$ as in the paragraph below Lemma 5.13, and have the solution $A_{k}$’s and $A_{\infty}$ from Proposition 5.14, for which we choose $C=\max\{L^{\prime}\cdot C^{\prime},\frac{1}{D_{1}}\}$ and $D=\frac{1}{D_{1}}=A_{0}$, where the definition of $C^{\prime}$ will be given below. For the sake of convenience, we also define that $R_{0}:=\{\mathbf{b}\mid\mathbf{b}\not\models\Phi\}$. Below we prove by induction on $n\geq 0$ that

• (*)

for all $k\in\{1,\dots,n^{*},\infty\}$ and all program valuations $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$, if $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\frac{1}{M}=\theta$, then we have $|\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})|\leq A_{k}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ when $\mathbf{b}\in R_{k}$ for $1\leq k\leq n^{*}$, and $|\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})|\leq A_{\infty}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ when $\mathbf{b}\in R_{n^{*}}$.

Base Step $n=0$. By definition, we have that for all program valuations $\mathbf{b},\mathbf{b}^{\prime}\in R_{k}$, $\delta_{0}(\mathbf{b},\mathbf{b}^{\prime})=\mathbf{b}[z]-\mathbf{b}^{\prime}[z]$ and $|\delta_{0}(\mathbf{b},\mathbf{b}^{\prime})|=|\mathbf{b}[z]-\mathbf{b}^{\prime}[z]|\leq\frac{1}{D_{1}}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})=A_{0}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq A_{k}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$.

Inductive Step. Suppose that the induction hypothesis (*) holds for $n$. We prove the case for $n+1$. We first consider $1\leq k\leq n^{*}$ and program valuations $\mathbf{b},\mathbf{b}^{\prime}$ such that $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$, $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\theta$ and $\mathbf{b}\in R_{k}$. From the integral expansion (Theorem B.1), we have that

[TABLE]

and similarly,

[TABLE]

From (†), we have that with probability at least $p=\frac{\epsilon}{2\cdot c-\epsilon}$, it happens that $\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})\leq-\frac{1}{2}\cdot\epsilon$. It follows that with probability at least $p$, $F(\ell,\mathbf{b},\mathbf{r})\in\bigcup_{m=0}^{k-1}R_{m}$. Note that

[TABLE]

where the first integral corresponds to the case that the executions from $\mathbf{b},\mathbf{b}^{\prime}$ both terminate after one loop iteration, the second and third integrals correspond to the case that one execution terminates but the other does not, and the last integral correspond to the case that both the executions do not terminate. In the first integral, we have from the non-expansiveness that

[TABLE]

In the second and third integral, we have from the second case in the proof of Theorem 5.5 and the fact $T\wedge n\leq T$ that

[TABLE]

[TABLE]

Furthermore, we have

[TABLE]

Denote

• •

$q_{1}:=\mathbb{P}_{\ell,\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi)$;

• •

$q_{2}:=\mathbb{P}_{\ell,\mathbf{r}}((F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\Phi)\vee(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi))$;

• •

$p^{\prime}:=\mathbb{P}_{\ell,\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\Phi\wedge\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq\eta(\mathbf{b})-\frac{\epsilon}{2})$;

• •

$\overline{p}:=\mathbb{P}_{\ell,\mathbf{r}}(\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq\eta(\mathbf{b})-\frac{\epsilon}{2})$.

Then $q_{1}+q_{2}+p^{\prime}\geq\overline{p}\geq p$. From the Lipschitz continuity in next-step termination, we have that $q_{2}\leq L^{\prime}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Then from $A_{0}\leq A_{1}\leq\dots\leq A_{k}\leq A_{\infty}$ and the induction hypothesis, we have

[TABLE]

Then we consider the case $\mathbf{b}\in R_{\infty}$. In this case, since $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\frac{1}{M}$ and $\eta(\mathbf{b})>c+1$, we have from the RSM-continuity that $\eta(F(\ell,\mathbf{b},\mathbf{r})),\eta(F(\ell,\mathbf{b}^{\prime},\mathbf{r}))>0$). It follows that both $F(\ell,\mathbf{b},\mathbf{r}),F(\ell,\mathbf{b}^{\prime},\mathbf{r})$ satisfy the loop guard . Hence, we have from the induction hypothesis that $|\mathbb{E}_{\mathbf{b}}(Z_{T\wedge(n+1)})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{T^{\prime}\wedge(n+1)})|\leq A_{\infty}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Thus, the induction step is proved. By taking the limit $n\rightarrow\infty$, we obtain that the whole loop $Q$ is expected linear-sensitive in each $R_{k}$. By taking the maximum constant $A_{\infty}$ for the global expected linear-sensitivity, we obtain the desired result. ∎

Appendix E Proofs for Section 6

Theorem E.1.

(Chatterjee et al., 2018c)* If there exists a difference-bounded RSM-map $\eta$ with $\epsilon,K,K^{\prime}$ from Definition 5.2 and $c$ from Definition 5.12, then for any initial program valuation $\mathbf{b}$ we have $\mathbb{P}(T>n)\leq\mathrm{exp}({-\frac{(\epsilon\cdot n-\eta(\mathbf{b}))^{2}}{2\cdot n\cdot c^{2}}})$ for all $n>\frac{\eta(\mathbf{b})}{\epsilon}$.*

Theorem 6.1. Consider a simple while loop $Q$ in the form (1) that satisfies the following conditions:

• •

the loop body $P$ is Lipschitz continuous with a constant $L$ specified in Definition 2.1, and has bounded update;

• •

there exists a difference-bounded RSM-map $\eta$ for $Q$ with RSM-continuity and parameters $\epsilon,K,c$ from Definition 5.2 and Definition 5.12 such that $L<\mathrm{exp}({\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}}})$.

Then for any program valuation $\mathbf{b}^{*}$ such that $\mathbf{b}^{*}\models\Phi$ and $\eta(\mathbf{b}^{*})>0$, there exists a radius $\rho>0$ such that the loop $Q$ is expected affine-sensitive over $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$. In particular, we can choose in Definition 3.1 that

[TABLE]

where $A^{\prime}=\frac{d\cdot M+\epsilon}{D_{1}\cdot\epsilon}$, $B^{\prime}=-\frac{d\cdot K}{D_{1}\cdot\epsilon}$ and $N=\lfloor 4\cdot\frac{\eta(\mathbf{b}^{*})}{\epsilon}\rfloor+1$, for which the parameters $d,M,\epsilon,K,D_{1}$ are from Definition 5.2, Definition 5.3, Definition 5.4 and (2).

Proof.

The proof follows similar arguments as in the proof for Theorem 5.5. Choose an arbitrary program variable $z$. Let $d$ be a bound for $z$ from Definition 5.3 and $M$ be a constant from Definition 5.4. Consider any $\mathbf{b}^{*}\models\Phi$ such that $\eta(\mathbf{b}^{*})>0$. Choose $\rho=\frac{\eta(\mathbf{b}^{*})}{2\cdot M}$. Then for all $\mathbf{b}\in U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$ we have $\eta(\mathbf{b})\geq\frac{\eta(\mathbf{b}^{*})}{2}>0$, hence $\mathbf{b}\models\Phi$. Let $\mathbf{b},\mathbf{b}^{\prime}\in U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$ be any input program valuations and define $\delta:=\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq 2\cdot\rho$. Consider any runs $\omega=\{\mathbf{b}_{n}\}_{n\geq 0}$, $\omega^{\prime}=\{\mathbf{b}^{\prime}_{n}\}_{n\geq 0}$ starting from respectively $\mathbf{b},\mathbf{b}^{\prime}$ such that $\omega,\omega^{\prime}$ follow the same sequence of sampled valuations and $\min\{T_{\mathbf{b}}(\omega),T_{\mathbf{b}^{\prime}}(\omega^{\prime})\}\geq n$. Similar to the proof of Theorem 5.5, we have three cases below.

• Case 1.

Both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$ violate the loop guard $\Phi$, i.e., $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}\models\neg\Phi$. From the condition (B1), we obtain directly that $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq L^{n}\cdot\delta$.

• Case 2.

One of $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$ and the other does not. W.l.o.g., we assume that $\mathbf{b}_{n}\models\Phi$ and $\mathbf{b}^{\prime}_{n}\models\neg\Phi$. From the analysis in the previous case we have $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq L^{n}\cdot\delta$. Furthermore, by the RSM continuity (B3), we have $|\eta(\mathbf{b}_{n})-\eta(\mathbf{b}^{\prime}_{n})|\leq M\cdot L^{n}\cdot\delta$. Moreover, from the condition (A3) we have $\eta(\mathbf{b}^{\prime}_{n})\leq 0$, so we obtain that $\eta(\mathbf{b}_{n})\leq M\cdot L^{n}\cdot\delta$. By Theorem C.1, we have that $\mathbb{E}_{\mathbf{b}_{n}}(T_{\mathbf{b}_{n}})\leq\dfrac{\eta(\mathbf{b}_{n})-K}{\epsilon}$, which implies that

[TABLE]

Hence we have

[TABLE]

• Case 3.

Neither $\mathbf{b}_{n}$ nor $\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. In this case, the loop $Q$ will continue with valuations $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$. Then in the next iteration, the same analysis can be carried out for the next program valuations $\mathbf{b}_{n+1},\mathbf{b}^{\prime}_{n+1}$.

Again, the situation that the third case happens infinitely often has probability zero, since our program is almost-surely terminating from the existence of an RSM-map. Thus, the sensitivity analysis eventually reduces to the first two cases. By taking into account the exponentially-decreasing property for Theorem E.1 and a detailed calculation, we can obtain that if the constant $L$ (i.e., the speed that the difference between program valuations grows larger) is less than the exponential decreasing factor of program termination, then the loop $Q$ is expected affine-sensitive.

The detailed calculation is as follows. Denote $A^{\prime}:=\frac{d\cdot M+\epsilon}{D_{1}\cdot\epsilon}$ and $B^{\prime}:=-\frac{d\cdot K}{D_{1}\cdot\epsilon}$. Then the total amount contributed to the total sensitivity at the $n$th step is no more than $\mathbb{P}(T_{\mathbf{b}}=n\vee T_{\mathbf{b}^{\prime}}=n)\cdot(A^{\prime}\cdot L^{n}\cdot\delta+B^{\prime})$, which is no greater than $(\mathbb{P}(T_{\mathbf{b}}=n)+\mathbb{P}(T_{\mathbf{b}^{\prime}}=n))\cdot(A^{\prime}\cdot L^{n}\cdot\delta+B^{\prime})$. Note that if $n\geq\frac{\eta(\mathbf{b})}{\epsilon}$, then by Theorem E.1 we have

[TABLE]

Furthermore, if $n\geq 2\cdot\frac{\eta(\mathbf{b})}{\epsilon}$, then we can derive that $p_{n}\leq\exp(-\frac{\epsilon^{2}\cdot n}{8\cdot c^{2}})\leq\exp(-\frac{\epsilon\cdot\eta(\mathbf{b})}{4\cdot c^{2}})$ and

[TABLE]

Similarly, for $n\geq\frac{\eta(\mathbf{b}^{\prime})}{\epsilon}$ we have

[TABLE]

and for $n\geq 2\cdot\frac{\eta(\mathbf{b}^{\prime})}{\epsilon}$, we have that $\frac{p^{\prime}_{n+1}}{p^{\prime}_{n}}\leq\exp\left(-\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}}\right)$ and $p^{\prime}_{n}\leq\exp(-\frac{\epsilon\cdot\eta(\mathbf{b}^{\prime})}{4\cdot c^{2}})$. Since $|\eta(\mathbf{b}^{\prime})-\eta(\mathbf{b})|\leq M\cdot\delta\leq 2\cdot M\cdot\rho$, we obtain that for $n\geq 2\cdot\frac{\eta(\mathbf{b})}{\epsilon}+4\cdot\frac{M\cdot\rho}{\epsilon}$, the values of $p_{n}$’s and $p^{\prime}_{n}$’s decrease exponentially with the factor $\exp\left(-\frac{3\cdot\epsilon^{2}}{8\cdot c^{2}}\right)$ and are no greater than $\exp(-\frac{\epsilon\cdot\eta(\mathbf{b}^{*})}{8\cdot c^{2}})$ (as $\eta(\mathbf{b}),\eta(\mathbf{b}^{\prime})\geq\frac{\eta(\mathbf{b}^{*})}{2}$). By summing up all $n$’s greater than $N:=\lfloor 2\cdot\frac{\eta(\mathbf{b}^{*})}{\epsilon}+4\cdot\frac{M\cdot\rho}{\epsilon}\rfloor+1=\lfloor 4\cdot\frac{\eta(\mathbf{b}^{*})}{\epsilon}\rfloor+1$, we obtain that

[TABLE]

where we have

[TABLE]

[TABLE]

It follows that the loop $Q$ is expected affine-sensitive over the neighbourhood $U_{\Phi,\mathfrak{d}}(\mathbf{b}^{*},\rho)$. ∎

Appendix F Proofs for Section 7

Theorem 7.2. Consider a non-expansive simple while loop $Q$ with bounded-update and an RSM-map with RSM-continuity, and a general program $Q^{\prime}$ that has expected affine-sensitivity over a subset $U$ of input program valuations with threshold $\theta$ in (3). If $\mathsf{out}(Q)\subseteq U$ and assuming integrability in (3), then the sequential composition $Q;Q^{\prime}$ is expected affine-sensitive over the satisfaction set of the loop guard of $Q$ with threshold $\theta$.

Proof.

The proof is basically an extension to the one for Theorem 5.5. Suppose that $Q$ is in the form  (1) with the bound $d$ from Definition 5.3 and an RSM-map $\eta$ with the parameters $\epsilon,K$ from Definition 5.2 that has RSM-continuity with a constant $M$ from Definition 5.4. Suppose a general probabilistic program $Q^{\prime}$ to be expected affine-sensitive over $U$ with the coefficients $A_{Q^{\prime}},B_{Q^{\prime}}$ in Definition 5.2. Consider two input program valuations $\mathbf{b},\mathbf{b}^{\prime}\in{\llbracket}{\Phi}{\rrbracket}$ such that $\delta:=\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\theta$. Let $\omega=\{\mathbf{b}_{n}\}_{n\in\mathbb{N}}$, $\omega^{\prime}=\{\mathbf{b}^{\prime}_{n}\}_{n\in\mathbb{N}}$ be any two runs under $Q$ that start from respectively $\mathbf{b},\mathbf{b}^{\prime}$ and follow the same sampled values for each loop iteration of the loop $P$. Consider for a step $n$ the event $\min\{T_{\mathbf{b}},T_{\mathbf{b}^{\prime}}\}\geq n$ holds (i.e., both the executions do not terminate before the $n$th step), where $T_{\mathbf{b}},T_{\mathbf{b}^{\prime}}$ are the random variables for the number of loop iterations of $Q$ when starting from $\mathbf{b},\mathbf{b}^{\prime}$, respectively. We have the following cases as in the proof for Theorem 5.5:

• Case 1.

Both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$ violate the loop guard $\Phi$, i.e., $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}\models\neg\Phi$. This case describes that the loop $Q$ terminates exactly after the $n$th iteration of the loop for both the executions. From the non-expansiveness, we obtain directly that $\mathfrak{d}(\mathbf{b}_{n},\mathbf{b}^{\prime}_{n})\leq\delta\leq\theta$. Then from $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}\in U$ and by the expected affine-sensitivity from $Q^{\prime}$, we obtain that $|\mathbb{E}_{\mathbf{b}_{n}}(Z^{Q^{\prime}}_{\mathbf{b}_{n}})-\mathbb{E}_{\mathbf{b}^{\prime}_{n}}(Z^{Q^{\prime}}_{\mathbf{b}^{\prime}_{n}})|\leq A_{Q^{\prime}}\cdot\delta+B_{Q^{\prime}}$, where $Z^{Q^{\prime}}_{\mathbf{b}_{n}},Z^{Q^{\prime}}_{\mathbf{b}^{\prime}_{n}}$ are the random variables representing the value of $z$ after the execution of $Q^{\prime}$ starting from the input program valuations $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$.

• Case 2.

Exactly one of $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. W.l.o.g., we can assume that $\mathbf{b}_{n}\not\models\Phi$ and $\mathbf{b}^{\prime}_{n}\models\Phi$. From the expected affine-sensitivity of $Q$, we obtain that

[TABLE]

where $\mathbf{b}^{\prime\prime}$ is the random program valuation after the execution of $Q$ from $\mathbf{b}^{\prime}_{n}$. By the triangle inequality and the bounded update condition, we have that

[TABLE]

Thus, we have that

[TABLE]

As shown in the second case of the proof of Theorem 5.5, we have that

[TABLE]

Hence we have that

[TABLE]

where $A:=A_{Q^{\prime}}\cdot\left(1+\frac{d\cdot M}{\epsilon}\right)$ and $B:=-A_{Q^{\prime}}\cdot\frac{d\cdot K}{\epsilon}+B_{Q^{\prime}}$.

• Case 3.

Neither $\mathbf{b}_{n}$ nor $\mathbf{b}^{\prime}_{n}$ violates the loop guard $\Phi$. In this case, the loop $Q$ will continue from both $\mathbf{b}_{n}$ and $\mathbf{b}^{\prime}_{n}$. Then in the next iteration, the same analysis can be carried out for the next program valuations $\mathbf{b}_{n+1},\mathbf{b}^{\prime}_{n+1}$, and so forth.

From the termination property ensured by RSM-maps (Theorem C.1), the probability that the third case happens infinitely often equals zero. Thus, the sensitivity analysis eventually reduces to the first two cases. From the first two cases, the difference contributed to the total expected sensitivity $|\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}})|$ when one of the runs terminates at a step $n$ is at most

[TABLE]

Then by a summation for all $n$, we derive the desired result that $|\mathbb{E}_{\mathbf{b}}(Z_{\mathbf{b}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z_{\mathbf{b}^{\prime}})|\leq 2\cdot A\cdot\delta+2\cdot B$ where $A,B$ are given as above. ∎

To prove Theorem 7.3, we need the following lemma.

Lemma F.1.

Consider a sequential composition $Q=Q_{1};\dots;Q_{n}$ of non-expansive simple while loops that satisfies the condition (‡). Let $\mathbf{b}$ be a random program valuation that satisfies the loop guard of $Q_{1}$ a.s, and $Y$ be a non-negative random variable such that for all program variables $z$, $|\mathbf{b}[z]|\leq Y$ a.s. Then there exists a linear function $f$ determined by $\eta_{1},\dots,\eta_{n}$ such that $\mathbb{E}_{\mathbf{b}}(|Z_{Q}|)\leq f(Y)$ for all program variables $z$.

Proof.

We prove by induction on $n\geq 1$. We denote by $d$ the bound for bounded update for all loops in $Q$, and by $K_{i},\epsilon_{i}$ the parameters for $\eta_{i}$. We also denote by $T_{1}$ the random variale for the number of loop iterations of $Q_{1}$. Moreover, we denote by $|\mathbf{b}|$ the vector obtained by taking the absolute value of every component in $\mathbf{b}$.

Base Step $n=1$, i.e., $Q=Q_{1}$. Then by Theorem C.1, we have that $\mathbb{E}_{\mathbf{b}}(|Z_{Q}|)\leq|\mathbf{b}[z]|+\mathbb{E}_{\mathbf{b}}(\frac{d}{D_{1}}\cdot T_{1})\leq|\mathbf{b}[z]|+\frac{d}{D_{1}}\cdot\frac{\eta_{1}(\mathbf{b})-K_{1}}{\epsilon_{1}}$. In this case, we can choose $f$ from $\eta_{1}$ and obtain the desired result.

Inductive Step $Q=Q_{1};Q^{\prime}$ where $Q^{\prime}$ is a sequential composition of simple while loops that satisfy (${\ddagger}$). By Theorem C.1, we have that $\mathbb{E}_{\mathbf{b}}(T_{1})\leq\frac{\eta_{1}(\mathbf{b})-K_{1}}{\epsilon_{1}}$. Denote by $\mathbf{b}^{\prime}$ the random program valuation after the execution of $Q_{1}$ from the input random program valuation $\mathbf{b}$. Then from the triangle inequality and the bounded-update condition, we have that $\mathfrak{d}(\mathbf{b}^{\prime},\mathbf{b})\leq d\cdot T_{1}$. By induction hypothesis, we have that $\mathbb{E}_{\mathbf{b}^{\prime}}(|Z_{Q}|)\leq f^{\prime}(|\mathbf{b}|+\frac{d}{D_{1}}\cdot T_{1})$ where $f^{\prime}$ is a linear function determined by linear RSM-maps from $Q^{\prime}$. Hence, we have that $\mathbb{E}_{\mathbf{b}}(|Z_{Q}|)=\mathbb{E}_{\mathbf{b}}(\mathbb{E}_{\mathbf{b}^{\prime}}(|Z_{Q^{\prime}}|))\leq\mathbb{E}_{\mathbf{b}}(f^{\prime}(|\mathbf{b}|+\frac{d}{D_{1}}\cdot T_{1}))\leq f(|\mathbf{b}|)$, where the last inequality is obtained by finding a linear function $f$ resulting from the expansion of the linear terms in $\mathbb{E}_{\mathbf{b}}(f^{\prime}(|\mathbf{b}|+\frac{d}{D_{1}}\cdot T_{1}))$ and the fact that $\mathbb{E}_{\mathbf{b}}(T_{1})\leq\frac{\eta_{1}(\mathbf{b})-K_{1}}{\epsilon_{1}}$. As $|\mathbf{b}|\leq Y$, we obtain the desired result. ∎

Theorem 7.3. Consider a non-expansive simple while loop $Q$ with loop guard $\Phi$ that has (i) bounded-update, (ii) a difference-bounded linear RSM-map with RSM-continuity, and (iii) the Lipschitz continuity in next-step termination. Then for any sequential composition $Q^{\prime}$ of simple while loops that (a) satisfies the condition (‡) (defined right before the theorem) and (b) has expected linear-sensitivity over a subset $U$ of input program valuations, if ${\llbracket}{\Phi}{\rrbracket}\cup\mathsf{out}(Q)\subseteq U$, then the sequential composition $Q;Q^{\prime}$ is expected linear-sensitive over the satisfaction set of the loop guard of $Q$.

Proof.

The proof is an extension of that for Theorem 5.15. Let the sensitivity coefficient of $Q^{\prime}$ be $A_{Q^{\prime}}$ and $\theta^{\prime}$ and the bound for bounded-update of $Q$ be $d$. Choose any program variable $z$. Denote by $T,T^{\prime}$ (resp. $\mathbf{b}_{n},\mathbf{b}^{\prime}_{n}$) the random variables for the number of loop iterations (resp. the valuation at the $n$-th step), from the input program valuations $\mathbf{b},\mathbf{b}^{\prime}$ and in the execution of the loop $Q$, respectively. Also denote by $Z_{Q^{\prime\prime}}$ the random variable that represents the value of $z$ after the execution of a proabilistic program $Q^{\prime\prime}$. For each natural number $n\geq 0$, define

[TABLE]

for program valuations $\mathbf{b},\mathbf{b}^{\prime}$, where the random variable $T\wedge n$ is defined as $\min\{T,n\}$ and $T^{\prime}\wedge n$ likewise. We also define $\delta(\mathbf{b},\mathbf{b}^{\prime}):=\mathbb{E}_{\mathbf{b}}(\mathbb{E}_{\mathbf{b}_{T}}(Z_{Q^{\prime}}))-\mathbb{E}_{\mathbf{b}^{\prime}}(\mathbb{E}_{\mathbf{b}^{\prime}_{T^{\prime}}}(Z^{\prime}_{Q^{\prime}}))$. By Lemma F.1 and the fact that $|\mathbf{b}_{T\wedge n}[z^{\prime}]|\leq\mathbf{b}[z^{\prime}]+\frac{d}{D_{1}}\cdot(T\wedge n)\leq\mathbf{b}[z^{\prime}]+\frac{d}{D_{1}}\cdot T=:Y$, we have that $\mathbb{E}_{\mathbf{b}_{T\wedge n}}(|Z_{Q^{\prime}}|)\leq f(Y)$ and the same holds for $\mathbf{b}^{\prime}_{T\wedge n}$ with another linear function $f^{\prime}$. By Theorem C.1, we have $\mathbb{E}_{\mathbf{b}}(f(Y))<\infty$ and the same holds for $\mathbb{E}_{\mathbf{b}^{\prime}}(f^{\prime}(Y))<\infty$. Then by the Dominated Convergence Theorem, we have that $\lim\limits_{n\rightarrow\infty}\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})=\delta(\mathbf{b},\mathbf{b}^{\prime})$.

Let $\eta$ be a difference-bounded RSM-continuous RSM-map for $Q$ with the parameters $c,\epsilon,M,K$ as specified in (A3), (A4), (B3). By Lemma 5.13, we can obtain a probability value $p=\frac{\epsilon}{2\cdot c-\epsilon}$ such that the condition $({\dagger})$ holds. We also construct the regions $R_{k}$’s ($1\leq k\leq n^{*}$) and $R_{\infty}$ as in the paragraph below Lemma 5.13, and have the solution $A_{k}$’s and $A_{\infty}$ from Proposition 5.14, for which we choose $C:=\max\{L^{\prime}\cdot C^{\prime},D\}$ and $D:=A_{Q^{\prime}}=:A_{0}$, where the definition of $C^{\prime}$ will be given below. For the sake of convenience, we also define that $R_{0}:=\{\mathbf{b}\mid\mathbf{b}\not\models\Phi\}$. Below we prove by induction on $n\geq 0$ that

• (*)

for all $k\in\{1,\dots,n^{*},\infty\}$ and all program valuations $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$ (where $\Phi$ is the loop guard of $Q$), if $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\min\{\frac{1}{M},\theta^{\prime}\}=:\theta$, then we have $|\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})|\leq A_{k}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ when $\mathbf{b}\in R_{k}$ for $1\leq k\leq n^{*}$, and $|\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})|\leq A_{\infty}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$ when $\mathbf{b}\in R_{n^{*}}$.

Base Step $n=0$. By the expected linear sensitivity of $Q^{\prime}$, we have that for all program valuations $\mathbf{b}\in R_{k}$, $|\delta_{0}(\mathbf{b},\mathbf{b}^{\prime})|=|\mathbb{E}_{\mathbf{b}}(Z_{Q^{\prime}})-\mathbb{E}_{\mathbf{b}^{\prime}}(Z^{\prime}_{Q^{\prime}})|\leq A_{Q^{\prime}}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})=A_{0}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq A_{k}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$.

Inductive Step. Suppose that the induction hypothesis (*) holds for $n$. We prove the case for $n+1$. We first consider $1\leq k\leq n^{*}$ and program valuations $\mathbf{b},\mathbf{b}^{\prime}$ such that $\mathbf{b},\mathbf{b}^{\prime}\models\Phi$, $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\theta$ and $\mathbf{b}\in R_{k}$. From the integral expansion (Theorem B.1), we have that

[TABLE]

and similarly,

[TABLE]

From (†), we have that with probability at least $p=\frac{\epsilon}{2\cdot c-\epsilon}$, it happens that $\eta(F(\ell,\mathbf{b},\mathbf{r}))-\eta(\mathbf{b})\leq-\frac{1}{2}\cdot\epsilon$. It follows that with probability at least $p$, $F(\ell,\mathbf{b},\mathbf{r})\in\bigcup_{m=0}^{k-1}R_{m}$. Note that

[TABLE]

where the first integral corresponds to the case that the executions of $Q$ from $\mathbf{b},\mathbf{b}^{\prime}$ both terminate after one loop iteration, the second and third integrals correspond to the case that one execution terminates but the other does not, and the last integral correspond to the case that both the executions do not terminate. In the first integral, we have from the non-expansiveness that

[TABLE]

In the second case, w.l.o.g. we can assume that $F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi$ and $F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\Phi$. From the expected linear-sensitivity of $Q^{\prime}$, we obtain that

[TABLE]

By the triangle inequality and the bounded update condition, we have that

[TABLE]

Thus, we have that

[TABLE]

Furthermore, we have

[TABLE]

where $\alpha=\mathbb{E}_{F(\ell,\mathbf{b},\mathbf{r})}(\mathbb{E}_{F(\ell,\mathbf{b},\mathbf{r})_{T\wedge n}}(Z_{Q^{\prime}}))-\mathbb{E}_{F(\ell,\mathbf{b}^{\prime},\mathbf{r})}(\mathbb{E}_{F(\ell,\mathbf{b}^{\prime},\mathbf{r})_{T^{\prime}\wedge n}}(Z^{\prime}_{Q^{\prime}}))$. Denote

• •

$q_{1}:=\mathbb{P}_{\ell,\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi)$;

• •

$q_{2}:=\mathbb{P}_{\ell,\mathbf{r}}((F(\ell,\mathbf{b},\mathbf{r})\not\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\Phi)\vee(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\not\models\Phi))$;

• •

$p^{\prime}:=\mathbb{P}_{\ell,\mathbf{r}}(F(\ell,\mathbf{b},\mathbf{r})\models\Phi\wedge F(\ell,\mathbf{b}^{\prime},\mathbf{r})\models\Phi\wedge\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq\eta(\mathbf{b})-\frac{\epsilon}{2})$;

• •

$\overline{p}:=\mathbb{P}_{\ell,\mathbf{r}}(\eta(F(\ell,\mathbf{b},\mathbf{r}))\leq\eta(\mathbf{b})-\frac{\epsilon}{2})$.

Then $q_{1}+q_{2}+p^{\prime}\geq\overline{p}\geq p$. From the Lipschitz continuity in next-step termination, we have that $q_{2}\leq L^{\prime}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Then from $A_{0}\leq A_{1}\leq\dots\leq A_{k}\leq A_{\infty}$ and the induction hypothesis, we have

[TABLE]

Then we consider the case $\mathbf{b}\in R_{\infty}$. In this case, since $\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})\leq\theta\leq\frac{1}{M}$ and $\eta(\mathbf{b})>c+1$, we have from the RSM-continuity that $\eta(F(\ell,\mathbf{b}^{\prime},\mathbf{r})),\eta(F(\ell,\mathbf{b}^{\prime},\mathbf{r}))>0$). It follows that both $F(\ell,\mathbf{b},\mathbf{r}),F(\ell,\mathbf{b}^{\prime},\mathbf{r})$ satisfy the loop guard. Hence, we have from the induction hypothesis that $|\delta_{n}(\mathbf{b},\mathbf{b}^{\prime})|\leq A_{\infty}\cdot\mathfrak{d}(\mathbf{b},\mathbf{b}^{\prime})$. Thus, the induction step is proved. By taking the limit $n\rightarrow\infty$, we obtain that the whole loop $Q$ is expected linear-sensitive in each $R_{k}$. By taking the maximum constant $A_{\infty}$ for the global expected linear-sensitivity, we obtain the desired result. ∎

Appendix G Details for Experimental results

We consider examples and their variants from the literature (Chatterjee et al., 2016; Chatterjee et al., 2018b, c; Ngo et al., 2018). Below we show all the experimental examples.