arXiv:1510.08517v1 [cs.LO] 28 Oct 2015

Algorithmic Analysis of Qualitative and Quantitative
Termination Problems for Affine Probabilistic Programs ∗
Krishnendu Chatterjee

Hongfei Fu †

Petr Novotný

IST Austria
Krishnendu.Chatterjee@ist.ac.at

IST Austria
State Key Laboratory of Computer
Science, Institute of Software, Chinese
Academy of Sciences
hongfei.fu@ist.ac.at

IST Austria
petr.novotny@ist.ac.at

Rouzbeh Hasheminezhad
Sharif University of Technology
hasheminezhad@ce.sharif.edu

Abstract

moreover, the NP-hardness result holds already for A PP’s without
probability and demonic non-determinism. Secondly, we show that
the concentration problem over LRA PP can be solved in the same
complexity as for the membership problem of LRA PP. Finally, we
show that the expectation problem over LRA PP can be solved in
2EXPTIME and is PSPACE-hard even for A PP’s without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to
answer the qualitative and quantitative questions over A PP’s with
at most demonic non-determinism.

In this paper, we consider termination of probabilistic programs
with real-valued variables. The questions concerned are:
1. qualitative ones that ask (i) whether the program terminates
with probability 1 (almost-sure termination) and (ii) whether
the expected termination time is finite (finite termination);
2. quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound
B such that the probability to terminate after B steps decreases
exponentially (concentration problem).

1.

To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination
of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic
programs (A PP’s) with both angelic and demonic non-determinism.
An important subclass of A PP’s is LRA PP which is defined as the
class of all A PP’s over which a linear ranking-supermartingale exists.

Introduction

Probabilistic Programs Probabilistic programs extend the classical imperative programs with random-value generators that produce random values according to some desired probability distribution. They provide a rich framework to model a wide variety
of applications ranging from randomized algorithms [17, 39], to
stochastic network protocols [3, 33], to robot planning [29, 32],
just to mention a few. The formal analysis of probabilistic systems
in general and probabilistic programs in particular has received a
lot of attention in different areas, such as probability theory and
statistics [18, 27, 31, 42, 44], formal methods [3, 33], artificial intelligence [28, 29], and programming languages [12, 20, 22, 46].

Our main contributions are as follows. Firstly, we show that the
membership problem of LRA PP (i) can be decided in polynomial
time for A PP’s with at most demonic non-determinism, and (ii) is
NP-hard and in PSPACE for A PP’s with angelic non-determinism;
∗ The

research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE),
and ERC Start grant (279307: Graph Games). The research leading to
these results has received funding from the People Programme (Marie
Curie Actions) of the European Union’s Seventh Framework Programme
(FP7/2007-2013) under REA grant agreement No [291734].
† Supported by the Natural Science Foundation of China (NSFC) under
Grant No. 61532019 .

Qualitative and Quantitative Termination Questions The most
basic, yet important, notion of liveness for programs is termination. For non-probabilistic programs, proving termination is equivalent to synthesizing ranking functions [23], and many different approaches exist for synthesis of ranking functions over nonprobabilistic programs [9, 14, 43, 50]. While a ranking function
guarantees termination of a non-probabilistic program with certainty in a finite number of steps, there are many natural extensions
of the termination problem in the presence of probability. In general, we can classify the termination questions over probabilistic
programs as qualitative and quantitative ones. The relevant questions studied in this paper are illustrated as follows.
1. Qualitative Questions. The most basic qualitative question is on
almost-sure termination which asks whether a program terminates with probability 1. Another fundamental question is about
finite termination (aka positive almost-sure termination [7, 22])
which asks whether the expected termination time is finite. Note

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2015/10/30

• Infinite Probabilistic Choices with Non-determinism. The situ-

that finite expected termination time implies almost-sure termination, whereas the converse does not hold in general.
2. Quantitative Questions. We consider two quantitative questions, namely expectation and concentration questions. The expectation question asks to approximate the expected termination time of a probabilistic program (within some additive or
relative error), provided that the expected termination time is
finite. The concentration problem asks to compute a bound B
such that the probability that the termination time is below B is
concentrated, or in other words, the probability that the termination time exceeds the bound B decreases exponentially.

ation changes significantly in the presence of non-determinism.
The Lyapunov-ranking-function method as well as the rankingsupermartingale method are sound but not complete in the presence of non-determinism for finite termination [22]. However,
for a subclass of probabilistic programs with at most demonic
non-determinism, a sound and complete characterization for finite termination through ranking-supermartingale is obtained
in [22].
Our Focus We focus on ranking-supermartingale based algorithmic study for qualitative and quantitative questions on termination
analysis of probabilistic programs with non-determinism. In view
of the existing results, there are at least three important classes
of open questions, namely (i) efficient algorithms, (ii) quantitative
questions and (iii) complexity in presence of two different types of
non-determinism. Firstly, while [22] presents a fundamental result
on ranking supermartingales over probabilistic programs with nondeterminism, the generality of the result makes it difficult to obtain
efficient algorithms; hence an important open question that has not
been addressed before is whether efficient algorithmic approaches
can be developed for synthesizing ranking supermartingales of simple form over probabilistic programs with non-determinism. The
second class of open questions asks whether ranking supermartingales can be used to answer quantitative questions, which have not
been tackled at all to our knowledge. Finally, no previous work considers complexity to analyze probabilistic programs with both the
two types of non-determinism (as required for the synthesis problem with abstraction).

Besides, we would like to note that there exist other quantitative
questions such as bounded-termination question which asks to approximate the probability to terminate after a given number of steps
(cf. [38] etc.).
Non-determinism in Probabilistic Programs Along with probability, another fundamental aspect in modelling is non-determinism.
In programs, there can be two types of non-determinism: (i) demonic non-determinism that is adversarial (e.g., to be resolved
to ensure non-termination or to increase the expected termination
time, etc.) and (ii) angelic non-determinism that is favourable (e.g.,
to be resolved to ensure termination or to decrease the expected
termination time, etc.). The demonic non-determinism is necessary
in many cases, and a classic example is abstraction: for efficient
static analysis of large programs, it is infeasible to track all variables of the program; the key technique in such cases is abstraction of variables, where certain variables are not considered for the
analysis and they are instead assumed to induce a worst-case behaviour, which exactly corresponds to demonic non-determinism.
On the other hand, angelic non-determinism is relevant in synthesis. In program sketching (or programs with holes as studied extensively in [51]), certain expressions can be synthesized which helps
in termination, and this corresponds to resolving non-determinism
in an angelic way. The consideration of the two types of nondeterminism gives the following classes:
1.
2.
3.
4.

Our Contributions In this paper, we consider a subclass of probabilistic programs called affine probabilistic programs (A PP’s)
which involve both demonic and angelic non-determinism. In general, an A PP is a probabilistic program whose all arithmetic expressions are linear. Our goal is to analyse the simplest class of ranking
supermartingales over A PP’s, namely, linear ranking supermartingales. We denote by LRA PP the set of all A PP’s that admit a linear
ranking supermartingale. Our main contributions are as follows:

probabilistic programs without non-determinism;
probabilistic programs with at most demonic non-determinism;
probabilistic programs with at most angelic non-determinism;
probabilistic programs with both angelic and demonic nondeterminism.

1. Qualitative Questions. Our results are as follows.
Algorithm. We present an algorithm for probabilistic programs
with both angelic and demonic non-determinism that decides
whether a given instance of an A PP belongs to LRA PP (i.e.,
whether a linear ranking supermartingale exists), and if yes,
then synthesize a linear ranking supermartingale (for proving
almost-sure termination). We also show that almost-sure termination coincides with finite termination over LRA PP. Our
result generalizes the one [12] for probabilistic programs without non-determinism to probabilistic programs with both the
two types of non-determinism. Moreover, in [12] even for
affine probabilistic programs without non-determinism, possible quadratic constraints may be constructed; in contrast, we
show that for affine probabilistic programs with at most demonic non-determinism, a set of linear constraints suffice, leading to polynomial-time decidability (cf. Remark 2).
Complexity. We establish a number of complexity results as
well. For programs in LRA PP with at most demonic nondeterminism our algorithm runs in polynomial time by reduction to solving a set of linear constraints. In contrast, we show
that for probabilistic programs in A PP’s with only angelic nondeterminism even deciding whether a given instance belongs
to LRA PP is NP-hard. In fact our hardness proof applies even
in the case when there are no probabilities but only angelic
non-determinism. Finally, for A PP’s with two types of nondeterminism (which is NP-hard as the special case with only
angelic non-determinism is NP-hard) our algorithm reduces to

Previous Results We discuss the relevant previous results for
termination analysis of probabilistic programs.
• Discrete Probabilistic Choices. In [36, 37], McIver and Morgan

presented quantitative invariants to establish termination, which
works for probabilistic programs with non-determinism, but
restricted only to discrete probabilistic choices.
• Infinite Probabilistic Choices without Non-determinism. On
one hand, the approach of [36, 37] was extended in [12] to ranking supermartingales resulting in a sound (but not complete)
approach to prove almost-sure termination for infinite-state
probabilistic programs with integer- and real-valued random
variables drawn from distributions including uniform, Gaussian, and Poison; the approach was only for probabilistic programs without non-determinism. On the other hand, Bournez
and Garnier [7] related the termination of probabilistic programs without non-determinism to Lyapunov ranking functions. For probabilistic programs with countable state-space and
without non-determinism, the Lyapunov ranking functions provide a sound and complete method for proving finite termination [7, 24]. Another relevant approach [38] is to explore the exponential decrease of probabilities upon bounded-termination
through abstract interpretation [16], resulting in a sound method
for proving almost-sure termination.

2

2015/10/30

Questions / Models
Qualitative
(Almost-sure,
Finite termination)

Prob prog without nondet

Prob prog with demonic nondet

PTIME

PTIME

Quantitative
(Expectation)

PSPACE-hard
2EXPTIME

PSPACE-hard
2EXPTIME

Prob prog with angelic nondet
NP-hard

Prob prog with both nondet
NP-hard

PSPACE
(QCQP)
PSPACE-hard
2EXPTIME†

PSPACE
(QCQP)
PSPACE-hard
2EXPTIME†

Table 1. Computational complexity of qualitative and quantitative questions for termination of probabilistic programs in LRA PP, where the
complexity of quantitative questions is for bounded LRA PPs with discrete probability choices. Results marked by † were obtained under
additional assumptions.
quadratic constraint solving. The problem of quadratic constraint solving is also NP-hard and can be solved in PSPACE;
we note that developing practical approaches to quadratic constraint solving (such as using semidefinite relaxation) is an active research area [6].
2. Quantitative Questions. We present three types of results. To
the best of our knowledge, we present the first complexity results (summarized in Table 1) for quantitative questions. First,
we show that the expected termination time is irrational in general for programs in LRA PP. Hence we focus on the approximation questions. For concentration results to be applicable, we
consider the class bounded LRA PP which consists of programs
that admit a linear ranking supermartingale with bounded difference. Our results are as follows.

2.

Preliminaries

2.1

Basic Notations

For a set A we denote by |A| the cardinality of A. We denote by N,
N0 , Z, and R the sets of all positive integers, non-negative integers,
integers, and real numbers, respectively. We use boldface notation
for vectors, e.g. x, y, etc, and we denote an i-th component of a
vector x by x[i].

Pn

An affine expression is an expression of the form d + i=1 ai xi ,
where x1 , . . . , xn are variables and d, a1 , . . . , an are real-valued
constants. Following the terminology of [30] we fix the following
nomenclature:
• Linear Constraint. A linear constraint is a formula of the form

Hardness Result. We show that the expectation problem is
PSPACE-hard even for deterministic programs in bounded
LRA PP.

ψ or ¬ψ, where ψ is a non-strict inequality between affine
expressions.
• Linear Assertion. A linear assertion is a finite conjunction of
linear constraints.
• Propositionally Linear Predicate. A propositionally linear
predicate is a finite disjunction of linear assertions.

Concentration Result on Termination Time. We present the
first concentration result on termination time through linear ranking-supermartingales over probabilistic programs in
bounded LRA PP. We show that by solving a variant version of
the problem for the qualitative questions, we can obtain a bound
B such that the probability that the termination time exceeds
n ≥ B decreases exponentially in n. Moreover, the bound B
computed is at most exponential. As a consequence, unfolding
a program upto O(B) steps and approximating the expected
termination time explicitly upto O(B) steps, imply approximability (in 2EXPTIME) for the expectation problem.

In this paper, we deem any linear assertion equivalently as a polyhedron defined by the linear assertion (i.e., the set of points satisfying
the assertion). It will be always clear from the context whether a
linear assertion is deemed as a logical formula or as a polyhedron.
2.2

Syntax of Affine Probabilistic Programs

In this subsection, we illustrate the syntax of programs that we
study. We refer to this class of programs as affine probabilistic
programs since it involves solely affine expressions.

Finer Concentration Inequalities. Finally, in analysis of supermartingales for probabilistic programs only Azuma’s inequality [2] has been proposed in the literature [12]. We show how to
obtain much finer concentration inequalities using Hoeffding’s
inequality [26, 35] (for all programs in bounded LRA PP) and
Bernstein’s inequalities [4, 35] (for incremental programs in
LRA PP, where all updates are increments/decrements by some
affine expression over random variables). Bernstein’s inequality
is based on the deep mathematical results in measure theory on
spin glasses [4], and we show how they can be used for analysis
of probabilistic programs.

Let X and R be countable collections of program and random variables, respectively. The abstract syntax of affine probabilistic programs (A PPs) is given by the grammar in Figure 1, where the expressions hpvari and hrvari range over X and R, respectively. The
grammar is such that hexpri and hrexpri may evaluate to an arbitrary affine expression over the program variables, and the program
and random variables, respectively (note that random variables can
only be used in the RHS of an assignment). Next, hbexpri may
evaluate to an arbitrary propositionally linear predicate.
The guard of each if-then-else statement is either a keyword angel
(intuitively, this means that the fork is non-deterministic and the
non-determinism is resolved angelically; see also the definition of
semantics below), a keyword demon (demonic resolution of nondeterminism), keyword prob(p), where p ∈ [0, 1] is a number
given in decimal representation (represents probabilistic choice,
where the if-branch is executed with probability p and the thenbranch with probability 1 − p), or the guard is a propositionally
linear predicate, in which case the statement represents a standard
deterministic conditional branching.
Example 1. We present an example of an affine probabilistic program shown in Figure 2. The program variable is x, and there is a
while loop, where given a probabilistic choice one of two statement

Experimental Results. We show the effectiveness of our approach to answer qualitative and concentration questions on
several classical problems, such as random walk in one dimension, adversarial random walk in one dimension and two
dimensions (that involves both probability and demonic nondeterminism).

Note that the most restricted class we consider is bounded LRA PP,
but we show that several classical problems, such as random walks
in one dimension, queuing processes, belong to bounded LRA PP,
for which our results provide a practical approach.

3

2015/10/30

A random variable in a probability space (Ω, F, P) is an Fmeasurable function X : Ω → R ∪ {∞}, i.e., a function such that
for every x ∈ R ∪ {∞} the set {ω ∈ Ω | X(ω) ≤ x} belongs
to F. We denote by E(X) the expected value of a random variable
X, i.e. the Lebesgue integral of X with respect to the probability
measure P. The precise definition of the Lebesgue integral of X is
somewhat technical and we omit it here, see, e.g., [45, Chapter 4],
or [5, Chapter 5] for a formal definition. A filtration of a probability
space (Ω, F, P) is a sequence {Fi }∞
i=0 of σ-algebras over Ω such
that F0 ⊆ F1 ⊆ · · · ⊆ Fn ⊆ · · · ⊆ F.

hstmti ::= hpvari ’:=’ hrexpri
| ’if’ hndbexpri ’then’ hstmti ’else’ hstmti ’fi’
| ’while’ hbexpri ’do’ hstmti ’od’
| hstmti ’;’ hstmti | ’skip’
hexpri ::= hconstanti | hpvari | hconstanti ’∗’ hpvari
| hexpri ’+’ hexpri | hexpri ’−’ hexpri
hrexpri ::= hexpri | hrvari | hpvari | hconstanti ’∗’ hrvari
| hconstanti ’∗’ hpvari | hrexpri ’+’ hrexpri

Stochastic Game Structures There are several ways in which one
can express the semantics of A PP’s with (angelic and demonic)
non-determinism [12, 22]. In this paper we take an operational approach, viewing our programs as 2-player stochastic games, where
one-player represents the angelic non-determinism, and the other
player (the opponent) the demonic non-determinism.
Definition 1. A stochastic game structure (SGS) is a tuple G =
(L, (X, R), `0 , x0 , 7→, Pr, G), where

| hrexpri ’−’ hrexpri
hbexpri := haffexpri | haffexpri ’or’ hbexpri
haffexpri ::= hliterali | hliterali ’and’ haffexpri
hliterali ::= hexpri ’≤’ hexpri | hexpri ’≥’ hexpri
| ¬hliterali
hndbexpri ::= ’angel’ | ’demon’ | ’prob(p)’ | hbexpri

• L is a finite set of locations partitioned into four pairwise

Figure 1. Syntax of affine probabilistic programs (A PP’s).
•

x := 0 ;
w h i l e x ≥ 0 do
i f prob ( 0 . 6 ) then
i f angel then
x := x + 1
else
x := x − 1
fi
else
i f demon t h e n
x := x + 1
else
x := x − 1
fi
fi
od

•
•

•

•

We stipulate that each location has at least one outgoing transition. Moreover, for every deterministic location ` we assume the
following: if τ1 , . . . , τk are all transitions outgoing from `, then
G(τ1 ) ∨ · · · ∨ G(τk ) ≡ true and G(τi ) ∧ G(τj ) ≡ false for each
1 ≤ i < j ≤ k. And we assume that each coordinate of D represents an integrable random variable (i.e., the expected value of the
absolute value of the random variable exists).

Figure 2. An example of a probabilistic program
blocks Q1 or Q2 is executed. The block Q1 (resp. Q2 ) is executed
if the probabilistic choice is at least 0.6 (resp. less than 0.4). The
statement block Q1 (resp., Q2 ) is an angelic (resp. demonic) conditional statement to either increment or decrement x.
2.3

For notational convenience we assume that the sets X and R are
endowed with some fixed linear ordering, which allows us to write
X = {x1 , x2 , . . . , x|X| } and R = {r1 , r2 , . . . , r|R| }. Every
update function f in a stochastic game can then be viewed as
a tuple (f1 , . . . , f|X| ), where each fi is of type R|X∪R| → R.
|X|
|R|
We denote by x = (x[i])i=1 and r = (r[i])i=1 the vectors of
concrete valuations of program and random variables, respectively.
In particular, we assume that each component of r lies within the
range of the corresponding random variable. We use the following
succinct notation for special update functions: by id we denote a
function which does not change the program variables at all, i.e.
for every 1 ≤ i ≤ |X| we have fi (x, r) = x[i]. For a function
g over the program and random variables we denote by [xj /g] the
update function f such that fj (x, r) = g(x, r) and fi (x, r) = x[i]
for all i 6= j.

Semantics of Affine Probabilistic Programs

We now formally define the semantics of A PP’s. In order to do this,
we first recall some fundamental concepts from probability theory.
Basics of Probability Theory The crucial notion is of the probability space. A probability space is a triple (Ω, F, P), where Ω is a
non-empty set (so called sample space), F is a sigma-algebra over
Ω, i.e. a collection of subsets of Ω that contains the empty set ∅, and
that is closed under complementation and countable unions, and P
is a probability measure on F, i.e., a function P : F → [0, 1] such
that
• P(∅) = 0,
• for all A ∈ F it holds P(Ω r A) = 1 − P(A), and
• for all pairwise disjoint countable set sequences
PA1 , A2 , · · · ∈

FS
(i.e., Ai ∩ Aj = ∅ for all i 6= j) we have
∞
P( i=1 Ai ).

∞
i=1

disjoint subsets LA , LD , LP , and LS of angelic, demonic,
probabilistic, and standard (deterministic) locations;
X and R are finite disjoint sets of real-valued program and
random variables, respectively. We denote by D the joint distribution of variables in R;
`0 is an initial location and x0 is an initial valuation of program
variables;
7→ is a transition relation, whose every member is a tuple of the
form (`, f, `0 ), where ` and `0 are source and target program
locations, respectively, and f : R|X∪R| → R|X| is an update
function;
Pr = {Pr ` }`∈LP is a collection of probability distributions,
where each Pr ` is a discrete probability distribution on the set
of all transitions outgoing from `.
G is a function assigning a propositionally linear predicates
(guards) to each transition outgoing from deterministic locations.

We say that an SGS G is normalized if all guards of all transitions
in G are in a disjunctive normal form.
Example 2. Figure 8 shows an example of stochastic game structure. Deterministic locations are represented by boxes, angelic locations by triangles, demonic locations by diamonds, and stochas-

P(Ai ) =

4

2015/10/30

that we typically omit from the notation, i.e. if there are no angelic
locations we write only Pπ etc.

tic locations by circles. Transitions are labelled with update functions, while guards and probabilities of transitions outgoing from
deterministic and stochastic locations, respectively, are given in
rounded rectangles on these transitions. For the sake of succinctness we do not picture tautological guards and identity update functions. Note that the SGS is normalized. We will describe in Example 3 how the stochastic game structure shown corresponds to the
program described in Example 1.

From Programs to Games To every affine probabilistic program
P we can assign a stochastic game structure GP whose locations
correspond to the values of the program counter of P and whose
transition relation captures the behaviour of P . The game GP has
the same program and random variables as P , with the initial
valuation x0 of the former and the distribution D of the latter being
specified in the program’s preamble. The construction of the state
space of GP can be described inductively. For each program P
out
the game GP contains two distinguished locations, `in
P and `P ,
the latter one being always deterministic, that intuitively represent
the state of the program counter before and after executing P ,
respectively.

Dynamics of Stochastic Games A configuration of an SGS G
is a tuple (`, x), where ` is a location of G and x is a valuation
of program variables. We say that a transition τ is enabled in a
configuration (`, x) if ` is the source location of τ and in addition,
x |= G(τ ) provided that ` is deterministic.
The possible behaviours of the system modelled by G are represented by runs in G. Formally, a finite path (or execution fragment)
in G is a finite sequence of configurations (`0 , x0 ) · · · (`k , xk ) such
that for each 0 ≤ i < k there is a transition (`i , f, `i+1 ) enabled in (`i , xi ) and a valuation r of random variables such that
xi+1 = f (xi , r). A run (or execution) of G is an infinite sequence
of configurations whose every finite prefix is a finite path. A configuration (`, x) is reachable from the start configuration (`0 , x0 )
if there is a finite path starting at (`0 , x0 ) that ends in (`, x).

1. Expression and Skips. For P = x:=E where x is a program
variable and E is an arithmetic expression, or P = skip, the
out
game GP consists only locations `in
P and `P (both determinisout
in
out
)
or
(`
,
[x/E],
`
tic) and a transition (`in
P , id, `P ), respecP
P
tively.
2. Sequential Statements. For P = Q1 ; Q2 we take the games
GQ1 , GQ2 and join them by identifying the location `out
Q1 with
out
out
in
in
`in
Q2 , putting `P = `Q1 and `P = `Q2 .
3. While Statements. For P = while φ do Q od we add a new
out
deterministic location `in
P which we identify with `Q , a new
in
out
deterministic location `P , and transitions τ = (`P , id, `in
Q ),
0
out
τ 0 = (`in
P , id, `P ) such that G(τ ) = φ and G(τ ) = ¬φ.
4. If Statements. Finally, for P = if ndb then Q1 else Q2 fi we
add a new location `in
P together with two transitions τ1 =
in
in
in
(`in
P , id, `Q1 ), τ2 = (`P , id, `Q2 ), and we identify the locaout
out
out
tions `Q1 and `Q1 with `P . In this case the newly added location `in
P is angelic/demonic if and only if ndb is the keyword ’angel’/’demon’, respectively. If ndb is of the form
prob(p), the location `in
P is probabilistic with Pr `in (τ1 ) = p
P
and Pr `in (τ2 ) = 1 − p. Otherwise (i.e. if ndb is a proposiP
tionally linear predicate), `in
P is a deterministic location with
G(τ1 ) = ndb and G(τ2 ) = ¬ndb.

Due to the presence of non-determinism and probabilistic choices,
an SGS G may exhibit a multitude of possible behaviours. The
probabilistic behaviour of G can be captured by constructing a
suitable probability measure over the set of all its runs. However,
before this can be done, non-determinism in G needs to be resolved.
To do this, we utilize the standard notion of a scheduler.
Definition 2. An angelic (resp., demonic) scheduler in an SGS
G is a function which assigns to every finite path in G that ends
in an angelic (resp., demonic) configuration (`, x), respectively, a
transition outgoing from `.
Intuitively, we view the behaviour of G as a game played between
two players, angel and demon, with angelic and demonic schedulers representing the strategies of the respective players. That is,
schedulers are blueprints for the players that tell them how to play
the game. The behaviour of G under angelic scheduler σ and demonic scheduler π can then be intuitively described as follows:
The game starts in the initial configuration (`0 , x0 ). In every step
i, assuming the current configuration to be (`i , xi ) the following
happens:

Once the game GP is constructed using the above rules, we put
G(τ ) = true for all transitions τ outgoing from deterministic locations whose guard was not set in the process, and finally we add a
self-loop on the location `out
P . This ensures that the assumptions in
Definition 1 are satisfied. Furthermore note that for SGS obtained
for a program P , since the only branching are conditional branching, every location ` has at most two successors `1 , `2 .
Example 3. We now illustrate step by step how the SGS of Example 2 corresponds to the program of Example 1. We first consider
the statements Q1 and Q2 (Figure 3), and show the corresponding
SGSs in Figure 4. Then consider the statement block Q3 which is
a probabilistic choice between Q1 and Q2 (Figure 5). The corresponding SGS (Figure 6) is obtained from the previous two SGSs
as follows: we consider a probabilistic start location where there is
a probabilistic branch to the start locations of the SGSs of Q1 and
Q2 , and the SGS ends in a location with only self-loop. Finally, we
consider the whole program as Q4 (Figure 7), and the corresponding SGS in (Figure 8). The SGS is obtained from SGS for Q3 , with
the self-loop replaced by a transition back to the probabilistic location (with guard x ≥ 0), and an edge to the final location (with
guard x < 0). The start location of the whole program is a new
location, with transition labeled x := 0, to the start of the while
loop location. We label the locations in Figure 8 to refer to them
later.

• A valuation vector r for the random variables of G is sampled

according to the distribution D.

• A transition τ = (`i , f, `0 ) enabled in (`i , xi ) is chosen accord-

ing to the following rules:
If `i is angelic (resp., demonic), then τ is chosen deterministically by scheduler σ (resp., π). That is, if `i is angelic
(resp., demonic) and c0 c1 · · · ci is the sequence of configurations observed so far, then τ equals σ(c0 c1 · · · ci ) (resp.,
π(c0 c1 · · · ci )).
If `i is probabilistic, then τ is chosen randomly according
to the distribution Pr `i .
If `i is deterministic, then by the definition of an SGS there
is exactly one enabled transition outgoing from `i , and this
transition is chosen as τ .
• The transition τ is traversed and the game enters a new configuration (`i+1 , xi+1 ) = (`0 , f (xi , r)).
In this way, the players and random choices eventually produce a
random run in G. The above intuitive explanation can be formalized
by showing that the schedulers σ and π induce a unique probability
measure Pσ,π over a suitable σ-algebra having runs in G as a
sample space. If G does not have any angelic/demonic locations,
there is only one angelic/demonic scheduler (an empty function)

5

2015/10/30

Q4 : x := 0 ; w h i l e ( x ≥ 0 ) do Q3 od

Q1 : i f a n g e l t h e n x := x + 1 e l s e x := x − 1 f i
Q2 : i f demon t h e n x := x + 1 e l s e x := x − 1 f i

Figure 7. Program Q4

Figure 3. Programs Q1 and Q2
`0
x:=x+1

`5
x:=x-1

x:=0
x:=x+1

x:=x-1

`1
x:=x+1

x:=x-1

x:=x-1
`9

x:=x+1

`6

`7

6
10

`2

x≥0

x<0

Figure 4. SGSs for Q1 (left) and Q2 (right)

`3

`8

4
10

`4

Figure 8. SGS of Q4

Q3 : i f p r o b ( 0 . 6 ) t h e n Q1 e l s e Q2 f i
Figure 5. Program Q3

x:=x+1

x:=x-1

Note that for all angelic schedulers σ and demonic schedulers π
we have Eσ,π [T ] < ∞ implies Pσ,π (T < ∞) = 1, however,
the converse does not hold in general. In other words, finitely
terminating implies a.s. terminating, but a.s. termination does not
imply finitely termination.
Definition 4 (Quantitative termination questions). Given a program P and its associated normalized SGS GP , we consider the
following notions:

6
10

4
10

1. Expected Termination Time. The expected termination time of
P is ET(P ) = inf σ supπ Eσ,π [T ].
2. Concentration bound. A bound B is a concentration bound if
there exists two positive constants c1 and c2 such that for all
x ≥ B, we have Thr(P, x) ≤ c1 · exp(−c2 · x), where
Thr(P, x) = inf σ supπ Pσ,π (T > x) (i.e., the probability that
the termination time exceeds x ≥ B decreases exponentially in
x).

x:=x-1
x:=x+1
Figure 6. SGS of Q3

2.4

Qualitative and Quantitative Termination Questions

Note that we assume that an SGS GP for a program P is already
given in a normalized form, as our algorithms assume that all
guards in GP are in DNF. In general, converting an SGS into
a normalized SGS incurs an exponential blow-up as this is the
worst-case blowup when converting a formula into DNF. However,
we note that for programs P that contain only simple guards,
i.e. guards that are either conjunctions or disjunctions of linear
constraints, a normalized game GP can be easily constructed in
polynomial time using de Morgan laws. In particular, we stress
that all our hardness results hold already for programs with simple
guards, so they do not rely on the requirement that GP must be
normalized.

We consider the most basic notion of liveness, namely termination,
for probabilistic programs, and present the relevant qualitative and
quantitative questions.
Qualitative question. We consider the two basic qualitative questions, namely, almost-sure termination (i.e., termination with probability 1) and finite expected termination time. We formally define
them below.
Given a program P , let GP be the associated SGS. A run ρ is
terminating if it reaches a configuration in which the location is
`out
P . Consider the random variable T which to every run ρ in GP
assigns the first point in time in which a configuration with the
location `out
is encountered, and if the run never reaches such a
P
configuration, then the value assigned is ∞.
Definition 3 (Qualitative termination questions). Given a program
P and its associated normalized SGS GP , we consider the following two questions:

3.

The Class LRA PP

For probabilistic programs a very powerful technique to establish
termination is based on ranking supermartingales. The simplest
form of ranking supermartingales are the linear ranking ones. In
this section we will consider the class of A PP’s for which linear
ranking supermartingales exist, and refer to it as LRA PP. Linear
ranking supermartingales have been considered for probabilistic
programs without any types of non-determinism [12]. We show
how to extend the approach in the presence of two types of nondeterminism. We also show that in LRA PP we have that a.s.
termination coincides with finite termination (i.e., in contrast to
the general case where a.s. termination might not imply finitetermination, for the well-behaved class of LRA PP we have a.s.
termination implies finite termination). We first present the general

1. Almost-Sure Termination. The program is almost-surely (a.s.)
terminating if there exists an angelic scheduler (called a.s terminating) σ such that for all demonic schedulers π we have
Pσ,π ({ρ | ρ is terminating }) = 1; or equivalently, Pσ,π (T <
∞) = 1.
2. Finite Termination. The program P is finitely terminating (aka
positively almost-sure terminating) if there exists an angelic
scheduler σ (called finitely terminating) such that for all demonic schedulers π it holds that Eσ,π [T ] < ∞.

6

2015/10/30

• C1: the function η(`, ) : R|X| → R is linear over the program

notion of ranking supermartingales, and will establish their role in
qualitative termination.
Definition 5 (Ranking Supermartingales [22]). A discrete-time
stochastic process {Xn }n∈N wrt a filtration {Fn }n∈N is a ranking supermartingale (RSM) if there exists K < 0 and  > 0 such
that for all n ∈ N, E(|Xn |) exists and it holds almost surely (with
probability 1) that

variables X;
• C2: if ` =
6 `out
P and x ∈
• C3: if ` = `out
P and x ∈
• C4:



Xn ≥ K and E(Xn+1 | Fn ) ≤ Xn −  · 1Xn ≥0 ,

In following proposition we establish (with detailed proof in the
appendix) the relationship between RSMs and certain notion of
termination time.
Proposition 1. Let {Xn }n∈N be an RSM wrt filtration {Fn }n∈N
and let numbers K,  be as in Definition 5. Let Z be the random
variable defined as Z := min{n ∈ N | Xn < 0}; which
denotes the first time n that the RSM Xn drops below 0. Then
P(Z < ∞) = 1 and E(Z) ≤ E(X1)−K .
Remark 1. WLOG we can consider that the constants K and  in
Definition 5 satisfy that K ≤ −1 and  ≥ 1, as an RSM can be
scaled by a positive scalar to ensure that  and the absolute value
of K are sufficiently large.

1. P is a.s. terminating; and
0
2. ET(P ) ≤ η(`0 ,x0 )−K . In particular, ET(P ) is finite.
Key proof idea. Let η be an LRSM, wrt a linear invariant I for GP .
Let σ be the angelic scheduler whose decisions optimize the value
of η at the last configuration of any finite path, represented by

To introduce the notion of linear ranking supermartingales, we need
the notion of linear invariants defined as follows.
Definition 6 (Linear Invariants). A linear invariant on X is a
function I assigning a finite set of non-empty linear assertions on
X to each location of GP such that for all configurations
(`, x)
S
reachable from (`0 , x0 ) in GP it holds that x ∈ I(`).

σ(`, x) = argmin(`,f,`0 )∈7→ η(`0 , x)
for all end configurations (`, x) such that ` ∈ LA and x ∈ R|X| .
Fix any demonic strategy π. Let the stochastic process {Xn }n∈N
be defined by: Xn (ω) := η(θn (ω), {xk,n (ω)}k ). We show that
{Xn }n∈N is an RSM, and then use Proposition 1 to obtain the
desired result (detailed proof in appendix).
Remark 3. Note that the proof of Theorem 1 also provides a way
to synthesize an angelic scheduler, given the LRSM, to ensure that
the expected termination time is finite (as our proof gives an explicit
construction of such a scheduler). Also note that the result provides
an upper bound, which we denote as UB(P ), on ET(P ).

Generation of linear invariants can be done through abstract interpretation [16], as adopted in [12]. We first extend the notion of preexpectation [12] to both angelic and demonic non-determinism.
Definition 7 (Pre-Expectation). Let η : L × R|X| → R be a
function. The function preη : L × R|X| → R is defined by:
(`,id,`0 )∈7→



I(`) → preη (`, x) ≤ η(`, x) −  .

Informally, LRSMs extend linear expression maps defined in [12]
with both angelic and demonic non-determinism. The following
theorem establishes the soundness of LRSMs.
Theorem 1. If there exists an LRSM η wrt I for GP , then

For the rest of the section we fix an affine probabilistic program
P and let GP = (L, (X, R), `0 , x0 , 7→, Pr, G) be its associated SGS. We fix the filtration {Fn }n∈N such that each Fn is
the smallest σ-algebra on runs that makes all random variables
in {θj }1≤j≤n , {xk,j }1≤k≤|X|,1≤j≤n measurable, where θj is the
random variable representing the location at the j-th step (note that
each location can be deemed as a natural number.), and xk,j is the
random variable representing the value of the program variable xk
at the j-th step.

P

[

I(`), then K ≤ η(`, x) ≤ K;

We refer to the above conditions as follows: C1 is the linearity condition; C2 is the non-terminating non-negativity condition, which
specifies that for every non-terminating location the RSM is nonnegative; C3 is the terminating negativity condition, which specifies that in the terminating location the RSM is negative (less than
−1) and lowerly bounded; C4 is the supermartingale difference
condition which is intuitively related to the  difference in the RSM
definition (cf Definition 5).
Remark 2. In [12], the condition C3 is written as K 0 ≤ η(`, x) <
0 and is handled by Motzkin’s Transposition Theorem, resulting
in possibly quadratic constraints. Here, we replace η(`, x) < 0
equivalently with η(`, x) ≤ K which allows one to obtain linear constraints through Farkas’ linear assertion, where the equivalence follows from the fact that maximal value of a linear program
can be attained if it is finite. This is crucial to our PTIME result
over programs with at most demonic non-determinism.

where E(Xn+1 | Fn ) is the conditional expectation of Xn+1 given
the σ-algebra Fn (cf. [53, Chapter 9]).

• preη (`, x) :=

` 6= `out
P ∧x ∈

S
x) ≥ 0;
S I(`), then η(`,
0

P r` (`, id, `0 ) · η (`0 , x) if ` is a

The class LRA PP. The class LRA PP consists of all A PP’s for which
there exists a linear invariant I such that an LRSM exists w.r.t I for
GP . It follows from Theorem 1 that programs in LRA PP terminate
almost-surely, and have finite expected termination time.

probabilistic location;
• preη (`, x) := max(`,id,`0 )∈7→ η(`0 , x) if ` is a demonic location;
• preη (`, x) := min(`,id,`0 )∈7→ η (`0 , x) if ` is an angelic location;
• preη (`, x) := η(`0 , ER (f (x, r))) if ` is a deterministic location, (`, f, `0 ) ∈7→ and x ∈ G(`, f, `0 ), where ER (f (x, r)) is
the expected value of f (x, ·).

4.

LRA PP: Qualitative Analysis

In this section we study the computational problems related to
LRA PP. We consider the following basic computational questions
regarding realizability and synthesis.

Intuitively, preη (`, x) is the one-step optimal expected value of η
from the configuration (`, x). In view of Remark 1, the notion of
linear ranking supermartingales is now defined as follows.
Definition 8 (Linear Ranking-Supermartingale Maps). A linear
ranking-supermartingale map (LRSM) wrt a linear invariant I for
GP is a function η : L × R|X| → R such that the following
conditions (C1-C4) hold: there exist  ≥ 1 and K, K 0 ≤ −1 such
that for all ` ∈ L and all x ∈ R|X| , we have

LRA PP realizability and synthesis. Given an A PPP with its normalized SGS GP and a linear invariant I, we consider the following
questions:
1. LRA PP realiazability. Does there exist an LRSM wrt I for GP ?
2. LRA PP synthesis. If the answer to the realizability question is
yes, then construct a witness LRSM.

7

2015/10/30

Rn | Ax ≤ b} 6= ∅. Then

Note that the existence of an LRSM implies almost-sure and finitetermination (Theorem 1), and presents affirmative answers to the
qualitative questions. We establish the following result.
Theorem 2. The following assertions hold:

{x ∈ Rn | Ax ≤ b} ∩ {x ∈ Rn | Bx < c} = ∅
iff there exist y ∈ Rm and z ∈ Rk such that y, z ≥ 0, 1T · z > 0,
AT y + BT z = 0 and bT y + cT z ≤ 0.
Remark 5. The version of Motzkin’s Transposition Theorem here
is a simplified one obtained by taking into account the assumption
{x ∈ Rn | Ax ≤ b} 6= ∅.

1. The LRA PP realizability and synthesis problems for programs
in A PPs can be solved in PSPACE, by solving a set of quadratic
constraints.
2. For programs in A PPs with only demonic non-determinism, the
LRA PP realizability and synthesis problems can be solved in
polynomial time, by solving a set of linear constraints.
3. Even for programs in A PPs with simple guards, only angelic
non-determinism, and no probabilistic choice, the LRA PP realizability problem is NP-hard.

Motzkin assertion Ψ. Given a polyhedron H = {x | Ax ≤ b}
with A ∈ Rm×n , b ∈ Rm and B ∈ Rk×n , c ∈ Rk , we define
assertion Ψ[H, B, c](ξ, ζ) (which we refer as Motzkin assertion)
for Motzkin’s Theorem by
Ψ[H, B, c](ξ, ζ) := ξ ≥ 0 ∧ ζ ≥ 0∧

Discussion and organization. The significance of our result is as
follows: it presents a practical approach (based on quadratic constraints for general A PPs, and linear constraints for A PPs with only
demonic non-determinism) for the problem, and on the other hand
it shows a sharp contrast in the complexity between the case with
angelic non-determinism vs demonic non-determinism (NP-hard
vs PTIME). In Section 4.1 we present an algorithm to establish the
first two items, and then establish the hardness result in Section 4.2.
4.1

1T · ζ > 0 ∧ AT ξ + BT ζ = 0 ∧ bT ξ + cT ζ ≤ 0 ,
where ξ (resp. ζ) is an m-dimensional (resp. k-dimensional)
column-vector variable. Note that if all the parameters H, B and
c are constant, then the assertion is linear, however, in general the
assertion is quadratic.
Handling emptiness check. The results described till now on linear inequalities require that certain sets defined by linear inequalities are nonempty. The following lemma presents a way to detect
whether such a set is empty (proof in the appendix).
Lemma 2. Let A ∈ Rm×n , B ∈ Rk×n , b ∈ Rm and d ∈
Rk . Then all of the following three problems can be decided in
polynomial time in the binary encoding of A, B, b, d:

Algorithm and Upper Bounds

Solution overview. Our algorithm is based on an encoding of the
conditions (C1–C4) for an LRSM into a set of universally quantified formulae. Then the universally quantified formulae are translated to existentially quantified formulae, and the key technical machineries are Farkas’ Lemma and Motzkin’s Transposition Theorem (which we present below).
Theorem 3 (Farkas’ Lemma [21, 48]). Let A ∈ Rm×n , b ∈ Rm ,
c ∈ Rn and d ∈ R. Assume that {x | Ax ≤ b} 6= ∅. Then

?

1. {x | Ax ≤ b} = ∅;
?

2. {x | Ax ≤ b ∧ Bx < d} = ∅;
?

3. {x | Bx < d} = ∅.

{x | Ax ≤ b} ⊆ {x | cT x ≤ d}

Below we fix an input A PP P .
Notations 1 (Notations for Our Algorithm). Our algorithm for
LRSM realizability and synthesis, which we call LRSMS YNTH,
is notationally heavy. To present the algorithm succinctly we will
use the following notations (that will be repeatedly used in the
algorithm).

iff there exists y ∈ Rm such that y ≥ 0, AT y = c and bT y ≤ d.
Farkas’ linear assertion Φ. Farkas’ Lemma transforms the inclusion testing of non-strict systems of linear inequalities into the
emptiness problem. For the sake of convenience, given a polyhedron H = {x | Ax ≤ b} with A ∈ Rm×n , b ∈ Rm and
c ∈ Rn , d ∈ R, we define the linear assertion Φ[H, c, d](ξ) (which
we refer to as Farkas’ linear assertion) for Farkas’ Lemma by

Sk

`
1. Hk,` : We let I(`) =
{Hk,` }, where each Hk,` is a
k=1
satisfiable linear assertion.
2. G(τ ): For each transition τ (in the SGS GP ), we deem the
propositionally linear predicate G(τ ) also as a set of linear
assertions whose members are exactly the conjunctive subclauses of G(τ ).
3. NS(H): For each linear assertion H, we define NS(H) as
follows: (i) if H = ∅, then NS(H) := ∅; and (ii) otherwise, the
polyhedron NS(H) is obtained by changing each appearance
of ‘<’ (resp. ‘>’) by ‘≤’ (resp. ‘≥’) in H. In other words,
NS(H) is the non-strict inequality version of H.
4. 7→` : We define

Φ[H, c, d](ξ) := ξ ≥ 0 ∧ AT ξ = c ∧ bT ξ ≤ d ,
where ξ is a column-vector variable of dimension n. Moreover, let
Φ[Rn , c, d](ξ) := c = 0 ∧ d ≥ 0 .
Note that Rn ⊆ {x | cT x ≤ d} iff c = 0 and d ≥ 0.
Below we show (proof in the appendix) that Farkas’ Lemma can be
slightly extended to strict inequalities.
Lemma 1. Let A ∈ Rm×n , B ∈ Rk×n , b ∈ Rm , d ∈ Rk ,
c ∈ Rn and d ∈ R. Let Z< = {x | Ax ≤ b ∧ Bx < d} and
Z≤ = {x | Ax ≤ b ∧ Bx ≤ d}. Assume that Z< 6= ∅. Then
for all closed subsets H ⊆ R|X| we have that Z< ⊆ H implies
Z≤ ⊆ H.
Remark 4. Lemma 1 is crucial to ensure that our approach can
be done in polynomial time when P does not involve angelic nondeterminism.

7→` := {(`0 , f, `00 ) ∈7→| `0 = `}
to be the set of transitions from ` ∈ L.
5. Op(`): For a location ` we call Op(`) the following open
sentence:
∀x ∈

[





I(`). preη (`, x) ≤ η(`, x) −  ;

which specifies the condition C4 for LRSM.
6. We will consider a` `∈L and b` `∈L as vector and scalar
variables, respectively,nandowill use c` ,nd` as
o vector/scalar lin-

The following theorem, entitled Motzkin’s Transposition Theorem,
handles general systems of linear inequalities with strict inequalities.
Theorem 4 (Motzkin’s Transposition Theorem [40]). Let A ∈
Rm×n , B ∈ Rk×n and b ∈ Rm , c ∈ Rk . Assume that {x ∈

ear expressions over

a`

0

and

`0 ∈L

0

b`

to be deter-

`0 ∈L

mined by PreExp (cf. Item 8 below), respectively. Similarly, for

8

2015/10/30

a transition τ we will alsonuse co`,τ (resp. cnτ ), do`,τ (resp., dτ )
0
0
as linear expressions over a`
and b`
.
`0 ∈L

equivalently into
k`
^
^

`0 ∈L

7. Half: We will use the following notation Half for polyhedrons
(or half-spaces) given by
`

n

`

|X|

x∈R

Half(c , d , ) =

` T

| c



T

k`
^
^

φ` :=

x ≤ d` −  ⇔ preη (`, x) ≤ η(`, x) − ,
`,τ



Φ NS(Hk,` ∧ φ0 ), c`,τ , d`,τ − 



n

0

k,`,φ
where we have fresh variables ξdt

o
k,`,φ0

(c ) x ≤ d −  ⇔ η(` , x) ≤ η(`, x) −  .
By Item 1 in Algorithm LRSMS YNTH (cf. below), one can observe that PreExp determines c` , d` , c`,τ , d`,τ , cτ , dτ in terms
of a` , b` .

.

k` 
^



Hk,` ⊆ SetOpτ ∈7→` Half(cτ , dτ , )

k=1

Running example. Since our algorithm is technical, we will illustrate the steps of the algorithm on the running example. We consider the SGS of Figure 8, and assign the invariant I such that
I(`0 ) = I(`1 ) = true, I(`i ) = x ≥ 0 for 2 ≤ i ≤ 8,
I(`9 ) = x < 0.

T

φ` :=

k,`,τ
Φ [NS(Hk,` ), cτ , dτ − ] ξdm



k,`,τ
where we have fresh variables ξdm
.
1≤k≤k`
Angelic case. The algorithm further transforms the sentence
equivalently into



k` 
^

Hk,` ∩

\ 

x∈R

|X|

τ T



τ

| (c ) x > d −  = ∅

;

τ ∈7→`

k=1

finally, from Motzkin’s Transposition Theorem, Lemma 1 and
Lemma 2, the algorithm transforms the sentence equivalently
into the nonlinear constraint (Motzkin assertion)

1. Template. The algorithm assigns a template η for an LRSM by
setting η(`, x) := (a` )T x + b` for each ` and x ∈ R|X| . This
ensures the linearity condition C1 (cf. Item 6 in Notations 1)
2. Variables for martingale difference and terminating negativity.
The algorithm assigns a variable  and variables K, K 0 .
3. Probabilistic
locations. For each probabilistic location ` ∈

L\ `out
, the algorithm transforms the open sentence Op(`)
P
equivalently into
Hk,` ⊆ Half(c` , d` , )

k`
^
^
k=1 τ ∈7→`

The steps of algorithm LRSMS YNTH are as follows: (i) the first
two steps are related to initialization; (ii) then steps 3–5 specify
condition C4 of LRSM, where step 3 considers probabilistic locations, step 4 deterministic locations, and step 5 both angelic and
demonic locations; (iii) step 6 specifies condition C2 and step 7
specifies condition C3 of LRSM; and (iv) finally, step 8 integrates
all the previous steps into a set of constraints. We present the algorithm, and each of the steps 3–7 are illustrated on the running
example immediately after the algorithm. Formally, the steps are as
follows:

k`
^


S

where SetOp is
for demonic location and
for angelic
location, such that PreExp(cτ , dτ , ) holds.
Demonic case. Using Farkas’ Lemma, Lemma 1 and Lemma 2,
the algorithm further transforms the open sentence equivalently
into the linear assertion

Algorithm LRSMS YNTH. Intuitively, our algorithm transform
conditions C1-C4 in Definition 8 into Farkas’ or Motzkin assertions; the transformation differs among different types of locations.

φ` :=

k`
^

Ψ NS(Hk,` ), C` , d`





k,`
τ
{ξag
}k,` , {ζag
}τ ∈7→`



k=1



k,`
with fresh variables ξag





1≤k≤k`


T

τ
, ζag

τ ∈7→`

where

(cτ1 )
dτ1


C` = −  ...  and d` = −  ...  +  · 1
dτm
(cτm )T







k=1

with 7→` = {τ1 , . . . , τm }.
6. Non-negativity for non-terminating location. For each location
` other than the terminating location `out
P , the algorithm transforms the open sentence

such that PreExp(c` , d` , ). Using Farkas’ Lemma, Lemma 1
and Lemma 2, the algorithm further transforms it equivalently
into the Farkas linear assertion
φ` :=

k`
^

Φ NS(Hk,` ), c` , d` − 





ξpk,`





ϕ` := ∀x. x ∈

[

I(`) → η(`, x) ≥ 0



k=1



where we have fresh variables ξpk,` k,` (cf. Notations 1 for
the meaning of Hk,` , PreExp, Half, NS(), Op etc.).
4. Deterministic
locations. For each deterministic location ` ∈

L\ `out
, the algorithm transforms the open sentence Op(`)
P

equivalently into
k`
^


Hk,` ⊆ Half(−a` , b` , 0)



.

k=1

9

0

k,`,φ
ξdt

5. Demonic and angelic locations. For each demonic (resp. angelic) location `, the algorithm transforms the open sentence
Op(`) equivalently into

0

τ

^

k=1 τ ∈7→` φ0 ∈G(τ )

`,τ

and similarly for PreExp(c , d , ). For τ ∈7→ from a
non-deterministic location ` to a target location `0 , we use
PreExp(cτ , dτ , ) to denote the following predicate:
τ T



such that the sentence ∀x ∈ G(τ ).PreExp(c`,τ , d`,τ , ) holds.
Using Farkas’ Lemma, Lemma 1 and Lemma 2, the algorithm
further transforms it equivalently into

·x≤d − ;

and similarly, Half(cτ , dτ , ) and Half(c`,τ , d`,τ , ).
8. PreExp: We will use PreExp(c` , d` , ) to denote the following
predicate:
c`

Hk,` ∧ φ0 ⊆ Half(c`,τ , d`,τ , )

k=1 τ ∈7→` φ0 ∈G(τ )

o

`

^ 

2015/10/30



• Non-negativity of non-terminating location: step 6. In our ex-

Using Farkas’ Lemma, Lemma 1 and Lemma 2, the algorithm
further transforms it equivalently into

ample, we have

k`

ϕ` :=

^

ϕ`i = Φ[R, −ai , bi ] for i ∈ {0, 1} and
ϕ`i = Φ[x ≥ 0, −ai , bi ] for 2 ≤ i ≤ 8 .

k,`
)
Φ NS(Hk,` ), −a` , b` (ξnt





k=1

• Terminating location: step 7. In our example, we have

k,`
ξnt

where
are fresh variables.
7. Negativity for terminating location. For the terminating location
`out
P , the algorithm transforms the open sentence



ϕ`out := ∀x. x ∈

[

P

0
out
I(`out
P ) → K ≤ η(`P , x) ≤ K

ϕ`9 = Φ[x ≤ 0, a9 , −b9 + K] ∧ Φ[x ≤ 0, −a9 , b9 − K 0 ] .
Remark 6. Note that it is also possible to follow the usage of
Motzkin’s Transposition Theorem in [30] for angelic locations to
first turn the formula into a conjunctive normal form and then
apply Motzkin’s Theorem on each disjunctive sub-clause. Instead
we present a direct application of Motzkin’s Theorem.



equivalently into
k`out

P h
^

out

out

Hk,` ⊆ Half(a`P , −b`P , −K)

Correctness and analysis. The construction of the algorithm ensures that there exists an LRSM iff the algorithm LRSMS YNTH
answers yes. Also note that if LRSMS YNTH answers yes, then a
witness LRSM can be obtained (for synthesis) from the solution
of the constraints. Moreover, given a witness we obtain an upper
bound UB(P ) on ET(P ) from Theorem 1. We now argue two aspects:

i

k=1
k`out

∧

P h
^

out

out

i

Hk,` ⊆ Half(−a`P , b`P , K 0 )

.

k=1

1. Linear constraints. First observe that for algorithm LRSMS YNTH, all steps, other than the one for angelic nondeterminism, only generates linear constraints. Hence it follows
that in the absence of angelic non-determinism we obtain a set
of linear constraints that is polynomial in the size of the input.
Hence we obtain the second item of Theorem 2.
2. Quadratic constraints. Finally, observe that for angelic nondeterminism the application of Motzkin’s Theorem generates
only quadratic constraints. Since the existential first-order theory of the reals can be decided in PSPACE [11], we get the first
item of Theorem 2.

Using Farkas’ Lemma, Lemma 1 and Lemma 2, the algorithm
further transforms it equivalently into
k`out

ϕ`out :=

P
^

h

out

out

Φ NS(Hk,`out ), a`P , −b`P + K

i

P

P

k,`out
P

ξt



k=1
k`out

∧

P
^

h

out

out

Φ NS(Hk,`out ), −a`P , b`P − K 0

i

P

k,`out
P

ξtt



k=1
k,`
where ξtk,` ’s and ξtt
’s are fresh variables.
8. Solving the constraint problem. For each location `, let φ`
and ϕ` be the formula obtained in steps 3–5, and steps 6–
7, respectively. The algorithm outputs whether the following
formula is satisfiable:

ΞP :=  ≥ 1 ∧ K, K 0 ≤ −1 ∧

^

4.2

We establish the third item of Theorem 2 (detailed proof in the
appendix).
Lemma 3. The LRA PP realizability problem for A PPs with angelic non-determinism is NP-hard, even for non-probabilistic nondemonic programs with simple guards.

(φ` ∧ ϕ` ) ,

`∈L

where the satisfiability is interpreted over all relevant open
variables in ΞP .
Example 4. (Illustration of algorithm LRSMS YNTH on running
example). We describe the steps of the algorithm on the running
example. For the sake of convenience, we abbreviate a`i , b`i by
ai , bi .

Proof (sketch). We show a polynomial reduction from 3-SAT to
the LRA PP realizability problem. For a propositional formula ψ
we construct a non-probabilistic non-demonic program Pψ whose
variables correspond to the variables of ψ and whose form is as
follows: the program consists of a single while loop within which
each variable is set to 0 or 1 via an angelic choice. The guard of
the loop checks whether ψ is satisfied by the assignment: if it is
not satisfied, then the program proceeds with another iteration of
the loop, otherwise it terminates. The test can be performed using
a propositionally linear predicate; e.g. for the formula (x1 ∨ x2 ∨
¬x3 )∧(¬x2 ∨x3 ∨x4 ) the loop guard will be x1 +x2 +(1−x3 ) ≤
1
∨ (1 − x2 ) + x3 + x4 ≤ 21 . To each location we assign a
2
simple invariant I which says that all program variables have values
between 0 and 1. The right hand sides of inequalities in the loop
guard are set to 21 in order for the reduction to work with this
invariant: setting them to 1, which might seem to be an obvious first
choice, would only work for an invariant saying that all variables
have value 0 or 1, but such a condition cannot be expressed by a
polynomially large propositionally linear predicate.

• Probabilistic location: step 3. In our example,

φ`2 = Φ[x ≥ 0, 0.6a3 + 0.4a4 − a2 , b2 − 0.6b3 − 0.4b4 − ]
• Deterministic location: step 4. In our example,

φ`0 = Φ[R, −a0 , b0 − b1 − ]
φ`1 = Φ[x ≥ 0, a2 − a1 , b1 − b2 − ]
∧ Φ[x ≤ 0, a9 − a1 , b1 − b9 − ]
φ`i = Φ[x ≥ 0, a1 − ai , bi − b1 −  − a1 ] for i ∈ {5, 7}
φ`i = Φ[x ≥ 0, a1 − ai , bi − b1 −  + a1 ] for i ∈ {6, 8} .
• Demonic location: step 5a. In the running example,

φ`4 := Φ[x ≥ 0, a8 − a4 , b4 − b8 − ]
∧ Φ[x ≥ 0, a7 − a4 , b4 − b7 − ] .

If ψ is not satisfiable, then the while loop obviously never terminates and hence by Theorem 1 there is no LRSM for Pψ with respect to any invariant, including I. Otherwise there is a satisfying
assignment ν for ψ which can be used to construct an LRSM η
with respect to I. Intuitively, η measures the distance of the current

• Angelic location: step 5b. In our example,

h

φ`3 = Ψ x ≥ 0,



a3 − a5
−b3 + b5 + 
,
a3 − a6
−b3 + b6 + 

 

i

Lower bound

.

10

2015/10/30

valuation of program variables from the satisfying assignment ν.
By using a scheduler σ that consecutively switches the variables
to the values specified by ν the angel ensures that η eventually
decreases to zero. Since the definition of a pre-expectation is independent of the scheduler used, we must ensure that the conditions C2 and C4 of LRSM hold also for those valuations x that
are not reachable under σ. This is achieved by multiplying the distance of each given variable xi from ν by a suitable penalty factor Pen in all locations in the loop that are positioned after the
branch in which xi is set. For instance, in a location that follows
the choice of x1 and x2 and precedes the choice of x3 and x4 the
expression assigned by η in the above example will be of the form
Pen · ((1 − x1 ) + x2 ) + (1 − x3 ) + x4 + d, where d is a suitable
number varying with program locations. This ensures that the value
of η for valuations that are not reachable under σ is very large, and
thus it can be easily decreased in the following steps by switching
to σ.

5.

i.e. that obeys the construction for angelic scheduler illustrated
below Theorem 1. Note that cmp(η) is non-empty (see Remark 3).
This condition is somewhat restrictive, as it might happen that
no near-optimal angelic scheduler is compatible with a martingale
η computed via methods in Section 3. On the other hand, this
definition captures the problem of extracting, from a given LRSM
η, as precise information about the expected termination time as
possible. Note that for programs without angelic non-determinism
the problem is equivalent to approximating ET(P ).
Our main results on are summarized below.
Theorem 5. 1. A concentration bound B can be computed in the
same complexity as for qualitative analysis (i.e., in polynomial
time with only demonic non-determinism, and in PSPACE in
the general case). Moreover, the bound B is at most exponential.
2. The quantitative approximation problem can be solved in a
doubly exponential time for bounded LRA PP with only discrete
probability choices. It cannot be solved in polynomial time
unless P = PSPACE, even for programs without probability
or non-determinism.
Remark 7. Note that the bound B is exponential, and our result (Lemma 5) shows that there exist deterministic programs in
bounded LRA PP that terminate exactly after exponential number
of steps (i.e., an exponential bound for B is asymptotically optimal
for bounded LRA PP).

LRA PP: Quantitative Analysis

In this section we consider the quantitative questions for LRA PP.
We first show a program P in LRA PP with only discrete probabilistic choices such that the expected termination time ET(P ) is
irrational.
n := 1 ;
w h i l e n ≥ 1 do
i f prob( 12 ) t h e n n := n + 1
e l s e n := n − 1 ; n := n − 1 f i od

5.1

Concentration Results on Termination Time

In this section, we present the first approach to show how LRSMs
can be used to obtain concentration results on termination time for
bounded LRA PP.

Figure 9. An example where ET(P ) is irrational.
Example 5. Consider the example in Fig. 9. The program P in the
figure represents an operation of a so called one-counter Markov
chain, a very restricted class of A PPs without non-determinism
and with a single integer variable. It follows from results of [10]
and [19] that the termination time of P is equal to a solution of
a certain system of quadratic√equations, which in this concrete
example evaluates to 2(5 + 5), an irrational number (for the
precise computation see appendix).

5.1.1

Concentration Inequalities

We first consider Azuma’s Inequality [2] which serves as a basic concentration inequality on supermartingales, and then adapt
finer inequalities such as Hoeffding’s Inequality [26, 35], and Bernstein’s Inequality [4, 35] to supermartingales.
Theorem 6 (Azuma’s Inequality [2]). Let {Xn }n∈N be a supermartingale wrt some filtration {Fn }n∈N and {cn }n∈N be a sequence of positive numbers. If |Xn+1 − Xn | ≤ cn for all n ∈ N,
then

Given that the expected termination time can be irrational, we focus
on the problem of its approximation. To approximate the termination time we first compute concentration bounds (see Definition 4).
Concentration bounds can only be applied if there exist bounds
on martingale change in every step. Hence we define the class of
bounded LRA PP.

−

P(Xn − X1 ≥ λ) ≤ e
for all n ∈ N and λ > 0.

Bounded LRA PP. An LRSM η wrt invariant I is bounded if there
exists an interval [a, b] such that the following holds: for S
all locations ` and
successors `0 of `, and all valuations x ∈
I(`)
S
and x0 ∈
I(`0 ) if (`0 , x0 ) is reachable in one-step from (`, x),
then we have (η(`0 , x0 ) − η(`, x)) ∈ [a, b]. Bounded LRA PP is
the subclass of LRA PP for which there exist bounded LRSMs for
some invariant. For example, for a program P , if all updates are
bounded by some constants (e.g., bounded domain variables, and
each probability distribution has a bounded range), then if it belongs to LRA PP, then it also belongs to bounded LRA PP. Note that
all examples presented in this section (as well several in Section 6)
are in bounded LRA PP.

2·

Pλn2

c2
k=2 n

Intuitively, Azuma’s Inequality bounds the amount of actual increase of a supermartingale at a specific time point. It can be refined
by Hoeffding’s Inequality. The original Hoeffding’s Inequality [26]
works for martingales; and we show how to extend to supermartingales.
Theorem 7 (Hoeffding’s Inequality on Supermartingales). Let
{Xn }n∈N be a supermartingale wrt some filtration {Fn }n∈N and
{[an , bn ]}n∈N be a sequence of intervals of positive length in R. If
X1 is a constant random variable and Xn+1 − Xn ∈ [an , bn ] a.s.
for all n ∈ N, then
−

P(Xn − X1 ≥ λ) ≤ e

We formally define the quantitative approximation problem for
LRA PPs as follows: the input is a program P in bounded LRA PP,
an invariant I for P , a bounded LRSM η with a bounding interval
[a, b], and a rational number δ ≥ 0. The output is a rational number
ν such that | inf σ∈cmp(η) supπ ET(P ) − ν| ≤ δ, where cmp(η)
is the set of all angelic schedulers σ that are compatible with η,

Pn

2λ2

k=2

(bk −ak )2

for all n ∈ N and λ > 0.
Remark 8. By letting the interval [a, b] be [−c, c] in Hoeffding’s
inequality, we obtain Azuma’s inequality. Thus, Hoeffding’s inequality is at least as tight as Azuma’s inequality and is strictly
tighter when [a, b] is not a symmetric interval.

11

2015/10/30

If variation and expected value of differences of a supermartingale
is considered, then Bernstein’s Inequality yields finer concentration
than Hoeffding’s Inequality.
Theorem 8 (Bernstein’s Inequality [4, 13]). Let {Xn }n∈N be a
supermartingale wrt some filtration {Fn }n∈N and M ≥ 0. If X1
is constant, Xn+1 − E(Xn+1 | Fn ) ≤ M a.s. and Var(Xn+1 |
Fn ) ≤ c2 for all n ≥ 1, then
−

P(Xn − X1 ≥ λ) ≤ e

in LRSMS YNTH in Section 4.1. Moreover for bounded LRA PP by
definition there exist valid constants a and b.
Key supermartingale construction. We now show that given the
LRSM η and the constants a, b synthesized wrt the conditions for
η above, how to obtain concentration results on termination time.
Define the stochastic process {Yn }n∈N by:
Yn = Xn +  · (min{T, n} − 1) .

λ2
2(n−1)c2 + 2M λ
3

The following proposition shows that {Yn }n∈N is a supermartingale and satisfies the requirements of Hoeffding’s Inequaltiy.
Proposition 2. {Yn }n∈N is a supermartingale and Yn+1 − Yn ∈
[a + , b + ] almost surely for all n ∈ N.

for all n ∈ N and λ > 0.
5.1.2

LRSMs for Concentration Results

LRSM and supermartingale to concentration result. We now
show how to use the LRSM and the supermartingale Yn to achieve
in
in
the concentration result. Let W0 := Y1 = (a`P )T x0 + b`P .
Fix an angelic strategy that fulfills supermartingale difference and
bounded change for LRSM; and fix any demonic strategy. By
Hoeffing’s Inequality, for all λ > 0, we have P(Yn − W0 ≥ λ) ≤

The only previous work which considers concentration results for
probabilistic programs is [12], that argues that Azuma’s Inequality
can be used to obtain bounds on deviations of program variables.
However, this technique does not present concentration result on
termination time. For example, consider that we have an additional
program variable to measure the number of steps. But still the invariant I (wrt which the LRSM is constructed) can ignore the additional variable, and thus the LRSM constructed need not provide
information about termination time. We show how to overcome this
conceptual difficulty. For the rest of this section, we fix a program
P in bounded LRA PP and its SGS GP . We first present our result
for Hoeffding’s Inequality (for bounded LRA PP) and then the result for Bernstein’s Inequality (for a subclass of bounded LRA PP).

−

2λ2

e (n−1)(b−a)2 . Note that T > n iff Xn ≥ 0 by conditions C2 and
C3 of LRSM. Let α = (n − 1) − W0 and α
b = (min{n, T } −
1) − W0 . Note that with the conjunct T > n we have that α and α
b
coincide. Thus, for P(T > n) = P(Xn ≥ 0 ∧ T > n) we have
P(Xn ≥ 0 ∧ T > n)

For the rest of this part we fix an affine probabilistic program
P and let GP = (L, (X, R), `0 , x0 , 7→, Pr, G) be its associated SGS. We fix the filtration {Fn }n∈N such that each Fn is
the smallest σ-algebra on runs that makes all random variables
in {θj }1≤j≤n , {xk,j }1≤k≤|X|,1≤j≤n measurable, where we recall
that θj is the random variable representing the location at the jth step, and xk,j is the random variable representing the value of
the program variable xk at the j-th step. We recall that T is the
termination-time random variable for P .

=
=
≤
=

P((Xn + α ≥ α) ∧ (T > n))
P((Xn + α
b ≥ α) ∧ (T > n))
P((Xn + α
b ≥ α))
P(Yn − Y1 ≥ (n − 1) − W0 )

≤

e

−

2((n−1)−W0 )2
(n−1)(b−a)2

for all n > W0 + 1. The first equality is obtained by simply adding
α on both sides, and the second equality uses that because of the
conjunct T > n we have min{n, T } = n which ensures α = α
b.
The first inequality is obtained by simply dropping the conjunct
T > n. The following equality is by definition, and the final
inequality is Hoeffding’s Inequality. Note that in the exponential
function the numerator is quadratic in n and denominator is linear
in n, and hence the overall function is exponentially decreasing in
n.

Constraints for LRSMs to apply Hoeffding’s Inequality. Let η
be an LRSM to be synthesized for P wrt linear invariant I. Let
{Xn }n∈N be the stochastic process defined by
Xn := η(θn , {xk,n }k )

Computational results for concentration inequality. We have the
following results which establish the second item of Theorem 5:

for all natural numbers n. To apply Hoeffding’s Inequality, we need
to synthesize constants a, b such that Xn+1 − Xn ∈ [a, b] a.s. for
all natural numbers n. We encode this condition as follows:

• Computation. Through the synthesis of the LRSM η and a, b,

a concentration bound B0 = W0 + 2 can be computed in
PSPACE in general and in PTIME without angelic nondeterminism (similar to LRSMS YNTH algorithm).
• Optimization. In order to obtain a better concentration bound
B, a binary search can be performed on the interval [0, B0 ] to
find an optimal B ∈ [0, B0 ] such that  · (B − 2) ≥ W0 is
consistent with the constraints for synthesis of η and a, b.
• Bound on B. Note that since B is computed in polynomial
space, it follows that B is at most exponential.
Remark 9 (Upper bound on Thr(P, x)). We now show that our
technique along with the concentration result also presents an
upper bound for Thr(P, x) as follows: To obtain an upper bound
for a given x, we first search for a large number M0 such that
M0 (b − a) ≤ (x − 1) − W0 and (x − 2) ≥ W0 are not
consistent with the conditions for η and a, b; then we perform a
binary search for an M ∈ [0, M0 ] such that the (linear) conditions
M (b − a) ≤ (x−1)−W0 and (x−2) ≥ W0 are consistent with
2
the conditions for η and a, b. Then Thr(P, x) ≤ e−2M /(x−1) .
Note that we already provide an upper bound UB(P ) for ET(P )
(recall Theorem 1 and Remark 6), and the upper bound UB(P )
holds for LRA PP, not only for bounded LRA PP.

• Probablistic or demonic locations. for all ` ∈ LP ∪ LD with

successor locations `1 , `2 , the following sentence holds:
∀x ∈

[

I(`). ∀i ∈ {1, 2}.

• Deterministic locations. for all `

∈ LS and all τ
(`, f, `0 ) ∈7→` , the following sentence holds:
∀x ∈

[



η(`i , x) − η(`, x) ∈ [a, b] .
=

I(`) ∧ G(τ ). ∀r. η(`0 , f (x, r)) − η(`, x) ∈ [a, b]



• Angelic location. for all ` ∈ LA with successor locations `1 , `2 ,

the following condition holds:
∀x ∈

[

I(`).∃i ∈ {1, 2}. a ≤ η(`i , x)−η(`, x) ≤ − ≤ b



• We require that − ∈ [a, b]. This is not restrictive since 

reflects the supermartingale difference.
We have that if the previous conditions hold, then a, b are valid constants. Note that all the conditions above can be transformed into an
existential formula on parameters of η and a, b by Farkas’ Lemma
or Motzkin’s Transposition Theorem, similar to the transformation

12

2015/10/30

Time

Applying Bernstein’s Inequality. To apply Bernstein’s Inequality,
the variance on the supermartingale difference needs to be evaluated, which might not exist in general for LRA PPs. We consider a
subclass of LRA PPs, namely, incremental LRA PPs.
Definition 9. A program P in LRA PP is incremental if all variable
updates are of the form x := x + g(r) where g is some linear
function on random variables r. An LRSM is incremental if it has
the same coefficients for each program variable at every location,
0
i.e. a` = a` for all `, `0 ∈ L.
Remark 10. The incremental condition for LRSMs can be encoded
as a linear assertion.
Result. We show that for incremental LRA PP, Bernstein’s Inequality can be applied for concentration results on termination time,
using the same technique we developed for applying Hoeffding’s
Inequality. The technical details are presented in the appendix.
5.2

Int RW 1D.

≤ 0.02 sec.

Real RW 1D.

≤ 0.01 sec.

Adv RW 1D.

≤ 0.01 sec.

Adv RW 2D.

≤ 0.02 sec.

Adv RW 2D. (Variant)

≤ 0.02 sec.

Complexity of quantitative approximation

We now show the second item of Theorem 5. The doubly exponential upper bound is obtained by obtaining a concentration bound
B via aforementioned methods and unfolding the program up to
O(B) steps (details in the appendix).
Lemma 4. The quantitative approximation problem can be solved
in a doubly exponential time for programs with only discrete probability choices.

B
47.00
84.50
122.00
159.50
197.00
92.00
167.00
242.00
317.00
392.00
41.00
74.33
107.67
141.00
174.33
162.00
262.00
362.00
462.00
562.00

UB(P )
46.00
83.50
121.00
158.50
196.00
91.00
166.00
241.00
316.00
391.00
40.00
73.33
106.67
140.00
173.33
122.00
152.00
182.00
212.00
242.00
161.00
261.00
361.00
461.00
561.00

Init. Cofig.
5
10
15
20
25
5
10
15
20
25
5
10
15
20
25
(5,10)
(10,10)
(15,10)
(20,10)
(25,10)
(5,0)
(10,0)
(15,0)
(20,0)
(25,0)

Table 2. Experimental results: the first column is the example
name, the second column is the time to solve the problem, the
following columns are our concentration bound and upper bound
on termination time for a given initial condition.

For the PSPACE lower bound we use the following lemma.
Lemma 5. For every C ∈ N the following problem is PSPACEhard: Given a program P without probability or non-determinism,
with simple guards, and belonging to bounded LRA PP; and a
number N ∈ N such that either ET(P ) ≤ N or ET(P ) ≥ N · C,
decide, which of these two alternatives hold.

6.

Experimental Results

In this section we present our experimental results. First observe
that one of the key features of our algorithm LRSMS YNTH is that it
uses only operations that are standard (such as linear invariant generation, applying Farkas’ Lemma), and have been extensively used
in programming languages as well as in several tools. Thus the efficiency of our approach is similar to the existing methods with such
operations, e.g., [12]. The purpose of this section is to demonstrate
the effectiveness of our approach, i.e., to show that our approach can
answer questions for which no previous automated methods exist.
In this respect we show that our approach can (i) handle probabilities and demonic non-determinism together, and (ii) provide useful
answers for quantitative questions, and the existing tools do not
handle either of them. By useful answers we mean that the concentration bound B and the upper bound UB(P ) we compute provide
reasonable answers. To demonstrate the effectiveness we consider
several classic examples and show how our method provides an effective automated approach to reason about them. Our examples
are (i) random walk in one dimension; (ii) adversarial random walk
in one dimension; and (iii) adversarial random walk in two dimensions.

Proof (Sketch). We first sketch the proof of item 1. Fix a number C.
We show a polynomial reduction from the following problem that
is PSPACE-hard for a suitable constant K: Given a deterministic
Turing machine (DTM) T such that on every input of length n the
machine T uses at most K · n tape cells, and given a word w over
the input alphabet of T , decide, whether T accepts w.
For a given DTM T and word w we construct a program P that
emulates, through updates of its variables, the computation of T
on w. This is possible due to the bounded space complexity of
T . The program P consists of a single while-loop whose every
iteration corresponds to a single computational step of T . The loop
is guarded by an expression m ≥ 1 ∧ r ≥ 1, where m, r are
special variables such that r is initialized to 1 and m to C ·J, where
J is such a number that if T accepts w, it does so in at most J
steps (J can be computed in polynomial time again due to bounded
space complexity of T ). The variable m is decremented in every
iteration of the loop, which guarantees eventual termination. If it
happens during the loop’s execution that T (simulated by P ) enters
an accepting state, then r is immediately set to zero, making P
terminate immediately after the current iteration of the loop. Now
P can be constructed in such a way that each iteration of the loop
takes the same amount W of time. If T does not accept w, then
P terminates in exactly C · J · W steps. On the other hand, if T
does accept w, then the program terminates in at most J · W steps.
Putting N = J · W , we get the proof of the first item.

Random walk (RW) in one dimension (1D). We consider two
variants of random walk (RW) in one dimension (1D). Consider a
RW on the positive reals such that at each time step, the walk moves
left (decreases value) or right (increases value). The probability
to move left is 0.7 and the probability to move right is 0.3. In
the first variant, namely integer-valued RW, every change in the
value is by 1; and in the second variant, namely real-valued RW,
every change is according to a uniform distribution in [0, 1]. The
walk starts at value n, and terminates if value zero or less is
reached. Then the random walk terminates almost-surely, however,
similar to Example 5 even in the integer-valued case the expected
termination time is irrational.

Remark 11. Both in proofs of Lemma 3 and Lemma 5 we have
only variables whose change in each step is bounded by 1. Hence
both the hardness proofs apply to bounded LRA PP.
Corollary 1. The quantitative approximation problem cannot be
solved in polynomial time unless P = PSPACE. Moreover, ET(P )
cannot be approximated up to any fixed additive or multiplicative
error in polynomial time unless P = PSPACE.

Adversarial RW in 1D. We consider adversarial RW in 1D that
models a discrete queuing system that perpetually processes tasks
incoming from its environment at a known average rate. In every
iteration there are r new incoming tasks, where r is a random vari-

13

2015/10/30

decrease it by 1, i.e. it is linear in n). For our experimental results,
the linear constraints generated by LRSMS YNTH was solved by
CPLEX [1]. The programs with the linear invariants are presented
in Section F of the appendix.
Significance of our result. We now highlight the significance of our
approach. The analysis of RW in 1D (even without adversary) is a
classic problem in probability theory, and the expected termination
time can be irrational and involve solving complicated equations.
Instead our experimental results show that using our approach
(which is polynomial time) we can compute upper bound on the
expected time that is a linear function. This shows that we provide
a practical and computational approach for quantitative reasoning
of probabilistic processes. Moreover, our approach also extends
to more complicated probabilistic processes (such as RW with
adversary, as well as in 2D), and compute upper bounds which are
linear, whereas precise mathematical analysis of such processes is
extremely complicated.

Figure 10. The plot of UB(P ) vs the initial location.
able taking value 0 with probability 12 , value 1 with probability 14
and value 2 with probability 41 . Then a task at the head of the queue
is processed in a way determined by a type of the task, which is not
known a priori and thus is assumed to be selected demonically. If
an urgent task is encountered, the system solves the task rapidly,
in one step, but there is a 18 chance that this rapid process ends in
failure that produces a new task to be handled. A standard task is
processed at more leisurely pace, in two steps, but is guaranteed to
succeed. We are interested whether for any initial number of tasks
in the queue the program eventually terminates (queue stability)
and in bounds on expected termination time (efficiency of task processing).

7.

Related Work

We have already discussed several related works, such as [7, 12, 22,
36, 37] in Section 1 (Previous results). We discuss other relevant
works here. The termination for concurrent probabilistic programs
under fairness was considered in [49]. A sound and complete characterization of almost-sure termination for countable state space
was given in [25]. A sound and complete method for proving termination of finite state programs was given in [20]. Termination
analysis of non-probabilistic programs has received a lot of attention over the last decade as well [8, 9, 14, 15, 34, 43, 50]. The
most closely related works to our work are [7, 12, 22] that consider
termination of probabilistic programs via ranking Lyapunov functions and supermartingales. However, most of the previous works
focus on proving a.s. termination and finite termination, and discuss
soundness and completeness. In contrast, in this work we consider
simple (linear) ranking supermartingales, and study the related algorithmic and complexity issues. Moreover, we present answers to
the quantitative termination questions, and also consider two types
of non-determinism together that has not been considered before.

Adversarial RW in 2D. We consider two variants of adversarial
RW in 2D.
1. Demonic RW in 2D. We consider a RW in two dimensions,
where at every time step either the x-axis or the y-axis changes,
according to a uniform distribution in [−2, 1]. However, at each
step, the adversary decides whether it is the x-axis or the y-axis.
The RW starts at a point (n1 , n2 ), and terminates if either the
x-axis or y-axis is reached.
2. Variant RW in 2D. We consider a variant of RW in 2D as
follows. There are two choices: in the first (resp. second) choice
(i) with probability 0.7 the x-axis (resp. y-axis) is incremented
by uniform distribution [−2, 1] (resp., [2, −1]), and (ii) with
probability 0.3, the y-axis (resp. x axis) is incremented by
[−2, 1] (resp., [2, −1]). In other words, in the first choice the
probability to move down or left is higher than the probability
to move up or right; and conversely in the second choice. At
every step the demonic choice decides among the two choices.
The walk starts at (n1 , n2 ) such that n1 > n2 , and terminates
if the x-axis value is at most the y-axis value (i.e., terminates
for values (n, n0 ) s.t. n ≤ n0 ).

8.

Conclusion and Future Work

In this work we considered the basic algorithmic problems related to qualitative and quantitative questions for termination of
probabilistic programs. Since our focus was algorithmic we considered simple (linear) ranking supermartingales, and established
several complexity results. The most prominent are that for programs with demonic non-determinism the qualitative problems can
be solved in polynomial time, whereas for angelic non-determinism
with no probability the qualitative problems are NP-hard. We also
present PSPACE-hardness results for the quantitative problems,
and present the first method through linear ranking supermartingales to obtain concentration results on termination time. There are
several directions for future work. The first direction is to consider
special cases of non-linear ranking supermartingales and study
whether efficient algorithmic approaches can be developed for
them. The second interesting direction would be to use the methods of martingale theory to infer deeper insights into the behaviour
of probabilistic programs, e.g. via synthesizing assertions about the
distribution of program variables (”stochastic invariants”).

Experimental results. Our experimental results are shown in Table 2 and Figure 10. Note that all examples considered, other
than demonic RW in 2D, are in bounded LRA PP (with no nondeterminism or demonic non-determinism) for which all our results are polynomial time. For the demonic RW in 2D, which is
not a bounded LRA PP (for explanation why this is not a bounded
LRA PP see Section F of the appendix), concentration results cannot be obtained, however we obtain the upper bound UB(P ) from
our results as the example belongs to LRA PP. Our experimental
result show that the concentration bound and upper bound on expected termination time (recall UB(P ) from Remark 6) we compute is a linear function in all cases (see Fig 10). This shows that
our automated method can effectively compute, or some of the most
classical random walks studied in probability theory, concentration bounds which are asymptotically tight (the expected number of
steps to decrease the value of a standard asymmetric random walk
by n is equal to n times the expected number of steps needed to

References
[1] IBM
ILOG
CPLEX
Optimizer.
http://www01.ibm.com/software/integration/optimization/cplex-optimizer/,
2010.

14

2015/10/30

[2] K. Azuma. Weighted sums of certain dependent random variables.
Tohoku Mathematical Journal, 19(3):357–367, 1967.

2015, Mumbai, India, January 15-17, 2015, pages 489–501. ACM,
2015. ISBN 978-1-4503-3300-9. .

[3] C. Baier and J.-P. Katoen. Principles of model checking. MIT Press,
2008. ISBN 978-0-262-02649-9.

[23] R. W. Floyd. Assigning meanings to programs. Mathematical Aspects
of Computer Science, 19:19–33, 1967.

[4] G. Bennett. Probability inequalities for the sum of independent random variables. Journal of the American Statistical Association, 57
(297):33–45, 1962.

[24] F. G. Foster. On the stochastic matrices associated with certain queuing processes. The Annals of Mathematical Statistics, 24(3):pp. 355–
360, 1953.

[5] P. Billingsley. Probability and Measure. Wiley, 3rd edition, 1995.

[25] S. Hart and M. Sharir. Concurrent probabilistic programs, or: How to
schedule if you must. SIAM J. Comput., 14(4):991–1012, 1985.

[6] A. Bockmayr and V. Weispfenning. Solving numerical constraints.
In J. A. Robinson and A. Voronkov, editors, Handbook of Automated
Reasoning (in 2 volumes), pages 751–842. Elsevier and MIT Press,
2001. ISBN 0-444-50813-9.

[26] W. Hoeffding. Probability inequalities for sums of bounded random
variables. Journal of the American Statistical Association, 58(301):
13–30, 1963.

[7] O. Bournez and F. Garnier. Proving positive almost-sure termination.
In RTA, pages 323–337, 2005.

[27] H. Howard. Dynamic Programming and Markov Processes. MIT
Press, 1960.

[8] A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle.
In ICALP, pages 1349–1361, 2005.

[28] L. P. Kaelbling, M. L. Littman, and A. W. Moore. Reinforcement
learning: A survey. Journal of Artificial Intelligence Research, 4:237–
285, 1996.

[9] A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with
reachability. In K. Etessami and S. K. Rajamani, editors, Computer
Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of
Lecture Notes in Computer Science, pages 491–504. Springer, 2005.
ISBN 3-540-27231-3. .

[29] L. P. Kaelbling, M. L. Littman, and A. R. Cassandra. Planning and acting in partially observable stochastic domains. Artificial intelligence,
101(1):99–134, 1998.
[30] J. Katoen, A. McIver, L. Meinicke, and C. C. Morgan. Linear-invariant
generation for probabilistic programs: - automated support for proofbased methods. In SAS, volume LNCS 6337, Springer, pages 390–406,
2010.

[10] T. Brázdil, J. Esparza, S. Kiefer, and A. Kučera. Analyzing Probabilistic Pushdown Automata. FMSD, 43(2):124–163, 2012.
[11] J. Canny. Some algebraic and geometric computations in pspace. In
Proceedings of the twentieth annual ACM symposium on Theory of
computing, pages 460–467. ACM, 1988.

[31] J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. D.
Van Nostrand Company, 1966.
[32] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logicbased reactive mission and motion planning. IEEE Transactions on
Robotics, 25(6):1370–1381, 2009.

[12] A. Chakarov and S. Sankaranarayanan. Probabilistic program analysis
with martingales. In N. Sharygina and H. Veith, editors, Computer
Aided Verification - 25th International Conference, CAV 2013, Saint
Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of
Lecture Notes in Computer Science, pages 511–526. Springer, 2013.
ISBN 978-3-642-39798-1. .

[33] M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification
of probabilistic real-time systems. In CAV, LNCS 6806, pages 585–
591, 2011.

[13] F. Chung and L. Lu. Concentration inequalities and martingale inequalities: A survey. Internet Mathematics, 3:79–127, 2011.

[34] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change
principle for program termination. In POPL, pages 81–92, 2001.

[14] M. Colón and H. Sipma. Synthesis of linear ranking functions. In
T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS
2001 Held as Part of the Joint European Conferences on Theory and
Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2031 of Lecture Notes in Computer Science, pages
67–81. Springer, 2001. ISBN 3-540-41865-2. .

[35] C. McDiarmid. Concentration. In Probabilistic Methods for Algorithmic Discrete Mathematics, pages 195–248. 1998.
[36] A. McIver and C. Morgan. Developing and reasoning about probabilistic programs in pGCL. In PSSE, pages 123–155, 2004.
[37] A. McIver and C. Morgan. Abstraction, Refinement and Proof for
Probabilistic Systems. Monographs in Computer Science. Springer,
2005.

[15] B. Cook, A. See, and F. Zuleger. Ramsey vs. lexicographic termination
proving. In TACAS, pages 47–61, 2013.

[38] D. Monniaux. An abstract analysis of the probabilistic termination
of programs. In P. Cousot, editor, Static Analysis, 8th International
Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings,
volume 2126 of Lecture Notes in Computer Science, pages 111–126.
Springer, 2001. ISBN 3-540-42314-1. . URL http://dx.doi.
org/10.1007/3-540-47764-0_7.

[16] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice
model for static analysis of programs by construction or approximation of fixpoints. In R. M. Graham, M. A. Harrison, and R. Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles
of Programming Languages, Los Angeles, California, USA, January
1977, pages 238–252. ACM, 1977. .

[39] R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge
University Press, New York, NY, USA, 1995. ISBN 0-521-47465-5,
9780521474658.

[17] D. Dubhashi and A. Panconesi. Concentration of Measure for
the Analysis of Randomized Algorithms. Cambridge University
Press, New York, NY, USA, 1st edition, 2009. ISBN 0521884276,
9780521884273.

[40] T. S. Motzkin. Beiträge zur Theorie der linearen Ungleichungen
(German). PhD thesis, Basel, Jerusalem, 1936.
[41] M. J. Osborne and A. Rubinstein. A course in game theory. 1994.

[18] R. Durrett. Probability: Theory and Examples (Second Edition).
Duxbury Press, 1996.

[42] A. Paz. Introduction to probabilistic automata (Computer science and
applied mathematics). Academic Press, 1971.

[19] J. Esparza, A. Kučera, and R. Mayr. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. In LICS,
pages 117–126. IEEE, 2005.

[43] A. Podelski and A. Rybalchenko. A complete method for the synthesis
of linear ranking functions. In B. Steffen and G. Levi, editors, Verification, Model Checking, and Abstract Interpretation, 5th International
Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings,
volume 2937 of Lecture Notes in Computer Science, pages 239–251.
Springer, 2004. ISBN 3-540-20803-8. .

[20] J. Esparza, A. Gaiser, and S. Kiefer. Proving termination of probabilistic programs using patterns. In CAV, pages 123–138, 2012.
[21] J. Farkas. A fourier-féle mechanikai elv alkalmazásai (Hungarian).
Mathematikaiés Természettudományi Értesitö, 12:457–472, 1894.

[44] M. Rabin. Probabilistic automata. Information and Control, 6:230–
245, 1963.

[22] L. M. F. Fioriti and H. Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In S. K. Rajamani and
D. Walker, editors, Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL

[45] J. S. Rosenthal. A First Look at Rigorous Probability Theory. World
Scientific Publishing Company, 2nd edition, 2006.

15

2015/10/30

[46] S. Sankaranarayanan, A. Chakarov, and S. Gulwani. Static analysis
for probabilistic programs: inferring whole program properties from
finitely many paths. In PLDI, pages 447–458, 2013.
[47] A. Schrijver. Theory of Linear and Integer Programming. WileyInterscience series in discrete mathematics and optimization. Wiley,
1999. ISBN 978-0-471-98232-6.
[48] A. Schrijver. Combinatorial Optimization - Polyhedra and Efficiency.
Springer, 2003. ISBN 978-3-540-44389-6.
[49] M. Sharir, A. Pnueli, and S. Hart. Verification of probabilistic programs. SIAM J. Comput., 13(2):292–314, 1984.
[50] K. Sohn and A. V. Gelder. Termination detection in logic programs
using argument sizes. In D. J. Rosenkrantz, editor, Proceedings of the
Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of
Database Systems, May 29-31, 1991, Denver, Colorado, USA, pages
216–226. ACM Press, 1991. ISBN 0-89791-430-9. .
[51] A. Solar-Lezama, R. M. Rabbah, R. Bodı́k, and K. Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI, pages
281–294, 2005.
[52] S. A. Vavasis. Approximation algorithms for indefinite quadratic
programming. Mathematical Programming, 57:279–311, 1992.
[53] D. Williams. Probability with Martingales. Cambridge University
Press, 1991.

16

2015/10/30

A.

Proofs for Section 3

where the terms are described below:
YP :=

Proposition 1. Let {Xn }n∈N be an RSM wrt filtration {Fn }n∈N
and constants K,  (cf. Definition 5). Let Z be the random variable
defined as Z := min{n ∈ N | Xn < 0}; which denotes the first
time n that the RSM Xn drops below 0. Then P(Z < ∞) = 1 and
E(Z) ≤ E(X1)−K .

n−1
X

1θn =` ·

`∈LP

X

YS :=

≤

E(Xn ) −  · E(1Xn ≥0 )

≤

E(X1 ) −  ·

=

E(X1 ) −  ·

YA :=

P∞
k=1

∞
X

P(Xk ≥ 0) .

YD :=

· Xn + YP0 + YS0 + YA + YD ,
Eσ,π (Xn+1 | Fn ) = 1θn =`out
p
· Xn , YA , YD are measurable in Fn , we have
because 1θn =`out
p
· Xn (and similarly for YA
·
X
Eσ,π (1θn =`out
n | Fn ) = 1θn =`out
p
p
and YD ); and for YP and YS we need their expectation as YP0 and
YS0 defined below. We have
YP0 :=

E(X1 ) − K
.


k=1

P(Xk ≥ 0) ≤

Xh

YS0 :=

X

1θn =` ·

`∈LP

X

i

P(B` = i) · η(`B` =i , {xk,n }k )

i∈{0,1}

h

X

1θn =`∧{xk,n }k |=G(τ ) ·η(`0 , Eσ,τ
R (f ({xk,n }k , r))

`∈LS (`,f,`0 )∈7→`

• P(Z = ∞) = limk→∞ P(Z ≥ k) = 0 and
• E(Z) ≤

1θn =` · η(π(ρ), {xk,n }k ),

where ρ is the finite path up to n steps. Then from properties of
conditional expectation [53, Page 88], one obtains:

It follows from Z ≥ k ⇒ Xk ≥ 0 that

P∞

X
`∈LD

P(Xk ≥ 0) converges and

k=1

1θn =` · η(σ(`, {xk,n }k ), {xk,n }k );

describes the semantics of angelic locations, where σ(`, {xk,n }k )
here denotes the target location of the transition chosen by the
scheduler; and similarly, for demonic locations by replacing σ by
π we have

Pn−1
P(Xk ≥ 0) −  · P(Xn ≥ 0)
Pk=1
n

P(Xk ≥ 0) ≤

X
`∈LA

E(X1 ) − E(Xn+1 )
E(X1 ) − K
P(Xk ≥ 0) ≤
≤
.



Hence the series

i

1θn =`∧{xk,n }k ∈G(τ ) ·η(`0 , f ({xk,n }k , r) ;

describes the semantics of deterministic locations.

The first equality is the total expectation law for conditional expectation; the first inequality is obtained from the fact that Xn is a supermartingale; the second inequality is obtained from the inductive
hypothesis; and the final equality is simply rearranging terms. Since
Xn ≥ K almost surely for all n ∈ N, we have that E(Xn ) ≥ K,
for all n. Hence from above we have that

k=1

h

`∈LS (`,f,`0 )∈7→`

P(Xk ≥ 0) .

The base step n = 1 is clear. The inductive step can be carried out
as follows:
E(Xn+1 ) = E (E(Xn+1 | Fn ))

n
X

1B` =i · η(`B` =i , {xk,n }k )

i∈{0,1}

X

k=1

k=1

i

X

where each random variable B` is the Bernoulli random variable
for the decision of the probabilistic branch and `B` =0 , `B` =1 are
the corresponding successor locations of `. Note that all B` ’s and
r’s are independent of Fn . In other words, YP describes the semantics of probabilistic locations.

Proof. The proof is similar to [22, Lemma 5.5]. We first prove by
induction on n ≥ 1 that
E(Xn ) ≤ E(X1 ) −  ·

Xh

Note that when θn ∈ LS ∪ LP ∪ LA , by definition we have
· Xn + YP0 + YS0 + YA ; and when
preη (θn , {xk,n }k ) = 1θn =`out
p
θn ∈ LD by definition we have YD ≤ preη (θn , {xk,n }k ). Hence
the result follows.

E(X1 )−K
.


The desired result follows.

Theorem 1. If there exists an LRSM η wrt I for GP , then

To prove Theorem 1, we need the following lemma which specifies
the relationship between pre-expectation and conditional expectation.
Lemma 6. Let η be an LRSM and σ be the angelic scheduler whose
decisions optimize the value of η at the last configuration of any
finite path, represented by

1. P is a.s. terminating; and
2. the expected termination time of P is at most
hence finite, i.e., ET(P ) < ∞.

η(`0 ,x0 )−K 0


and

Proof. We establish both the points. Let η be an LRSM wrt I for
GP . Define the angelic strategy σ which solely depends on the end
configuration of a finite path as follows:

σ(`, x) = argmin(`,f,`0 )∈7→ η(`0 , x)
for all end configuration (`, x) such that ` ∈ LA and x ∈ R|X| . Let
π be any demonic scheduler. Let the stochastic process {Xn }n∈N
be defined such that

σ(`, x) = argmin(`,f,`0 )∈7→ η(`0 , x)
for all ` ∈ LA and x ∈ R|X| . Fix any demonic strategy π. Let the
stochastic process {Xn }n∈N be defined by:

Xn := η(θn , {xk,n }1≤k≤|X| ) .

Xn := η(θn , {xk,n }k ).

Then for all n ∈ N,

For all n ∈ N, from Lemma 6, we have

Eσ,π (Xn+1 | Fn ) ≤ preη (θn , {xk,n }1≤k≤|X| ) .

Eσ,π (Xn+1 | Fn ) ≤ preη (θn , {xk,n }k ) .
Proof. For all n ∈ N, from the program syntax we have

By condition C4,
preη (θn , {xk,n }k ) ≤ η(θn , {xk,n }k ) −  · 1θn 6=`out

Xn+1 = 1θn =`out
· Xn + YP + YS + YA + YD
p

P

17

2015/10/30

i

.

to xi or 1 − xi depending on whether ξ is a positive literal or not,
respectively. The body of the program then has the form

for some  ≥ 1. Moreover, from C2, C3 and the fact that I is a
linear invariant, it holds almost-surely that θn 6= `out
P iff Xn ≥ 0.
Thus, we have

while ϕ do Q1 ; · · · ; Qn od

Eσ,π (Xn+1 | Fn ) ≤ Xn −  · 1Xn ≥0 .

where

It follows that {Xn }n∈N is an RSM. Hence by Proposition 1, it
follows that GP terminates almost surely and

• ϕ is a finite disjunction of linear constraints of the form

η(`0 , x0 ) − K 0
.
E (T ) ≤

The desired result follows.
σ,π

B.

m h
_

gξj,1 + gξj,2 + gξj,3 ≤

j=1

Proofs for Section 4.1

1
2

i

;

• Qi has the form if angel then xi := 1 else xi := 0 fi, for all

1 ≤ i ≤ n.
Lemma 1. Let A ∈ Rm×n , B ∈ Rk×n , b ∈ Rm , d ∈ Rk ,
c ∈ Rn and d ∈ R. Let Z< = {x | Ax ≤ b ∧ Bx < d} and
Z≤ = {x | Ax ≤ b ∧ Bx ≤ d}. Assume that Z< 6= ∅. Then
for all closed subsets H ⊆ R|X| we have that Z< ⊆ H implies
Z≤ ⊆ H.

Clearly, given a formula ψ the program Pψ can be constructed
in time polynomial in the size of ψ, and moreover, Pψ is nonprobabilistic and non-demonic.

Proof. Let z be any point such that Az ≤ b, Bz ≤ d and Bz 6< d.
Let y be a point such that Ay ≤ b and By < d. Then for all
λ ∈ (0, 1),

Note that each valuation x, reachable from the initial configuration
of GPψ , can be viewed as a bit vector, and hence we can identify
these reachable valuations with truth assignments to ψ. Also note
that for such a reachable valuation x it holds gξj,k (x) = 1 if and
only if x, viewed as an assignment, satisfies the formula ξj,k , and
gξj,k (x) = 0 otherwise.

λ · y + (1 − λ) · z ∈ {x | Ax ≤ b ∧ Bx < d} .
By letting λ → 1, we obtain that z ∈ H because H is closed.
m×n

k×n

Finally, let
VnI be an invariant assigning to every location a linear
assertion i=1 [0 ≤ xi ∧ xi ≤ 1]. Note that the invariant I is very
simple and it is plausible that it can be easily discovered without
employing any significant insights into the structure of Pψ .

m

Lemma 2. Let A ∈ R
, B ∈ R
, b ∈ R and d ∈
Rk . Then all of the following three problems can be decided in
polynomial time in the binary encoding of A, B, b, d:

We claim that Pψ admits a linear ranking supermartingale with
respect to I if and only if there exists a satisfying assignment for ψ.
First let us assume that ψ is not satisfiable. Then, as noted above,
for all reachable valuations x there is 1 ≤ j ≤ m such that for all
ξj,k , 1 ≤ k ≤ 3, it holds gξj,k (x) = 0. It follows that ϕ holds in
every reachable valuation and hence the program never terminates.
From Theorem 1 it follows that Pψ does not admit an LRSM for
any invariant I.

?

1. {x | Ax ≤ b} = ∅;
?

2. {x | Ax ≤ b ∧ Bx < d} = ∅;
?

3. {x | Bx < d} = ∅.
Proof. The polynomial-time decidability of the first problem is
well-known (cf. [47]). The second problem can be solved by
checking whether the optimal value of the following linear program
is greater than zero:
max z subject to Ax ≤ b;

Bx + z · 1 ≤ d;

Let us now assume that there exists an assignment
ν : {x1 , . . . , xn } → {0, 1} satisfying ψ. We use ν to construct an LRSM for Pψ with respect to I. First, let us fix the
following notation of locations of GPψ : by `i we denote the
initial location of the sub-program Qi , by `1i and `0i the locations
corresponding to ”then” and ”else” branches of Qi , respectively,
and by `n+1 and `out the initial and terminal locations of GPψ ,
respectively. Next, we fix a penalty constant Pen = 4n + 3 and
for every pair of indexes 1 ≤ i ≤ n + 1, 1 ≤ j ≤ n we define a
linear expression

z ≥ 0.

The proof for the third problem is similar to the second one.

C.

Proofs for Section 4.2

Lemma 3. The LRA PP realizability problem for A PPs with angelic non-determinism is NP-hard, even for non-probabilistic nondemonic programs with simple guards.
Proof. We show a polynomial reduction from 3-SAT to the LRA PP
realizability problem.

hi,j

Let ψ be any propositional formula in a conjunctive normal form
with three literals per clause. Let C1 , . . . , Cm be all the clauses and
x1 , . . . , xn all the variables of ψ. For every 1 ≤ j ≤ m we write
Cj ≡ ξj,1 ∨ ξj,2 ∨ ξj,3 , where each ξj,k is either a positive or a
negative literal, i.e. a variable or its negation.


1 − xj




(1 − xj ) · Pen
=
xj



xj · Pen

if ν(xj ) = 1 and i ≤ j,
if ν(xj ) = 1 and i > j,
if ν(xj ) = 0 and i ≤ j,
if ν(xj ) = 0 and i > j.

Note that for x ∈ [0, 1]n the value hi,j (x) equals either |ν(xj ) −
x[j]| or |ν(xj ) − x[j]| · Pen depending on whether i ≤ j or not.
Finally, we define an LRSM η as follows: for every 1 ≤ i ≤ n + 1
we put

We construct a program Pψ as follows: the program variables of
Pψ correspond to the variables in ψ, the program has no random
variables. All the program variables are initially set to 1. To construct the body of the program, we define, for each literal ξ of ψ
involving a variable xi , a linear expression gξ which is equal either

η(`i , x) =

n
X

hi,j (x) + (n − i + 1) · 2.

j=1

18

2015/10/30

Next, for every 1 ≤ i ≤ n we put
ν(x )
η(`i i , x)

=

n
X

hi,j (x) + (2(n − i) + 1)
xwhile,else

j=1
1−ν(xi )
η(`i
, x)

= n · Pen + 2n + 1.

ywhile,while

Finally, we put η(`out , x) = −1/2.
ywhile,else
We show that η is an LRSM wrt I.
n
As hi,j
S(x) ≥ 0 whenever x ∈ [0, 1] , it is easy to check that
x ∈
I(`) ⇒ η(`, x) ≥ 0 for every non-terminal location `.
Next, for each x ∈ Rn and each angelic state `i it holds that
ν(x )
η(`i , x) = η(`i i , x) + 1; hence preη (`i , x) ≤ η(`i , x) − 1.
Further, let us observe that for all x ∈ [0, 1]n and all 1 ≤ i ≤ n + 1
we have η(`i , x) ≤ n · Pen + 2n; thus for all 1 ≤ i ≤ n it holds
1−ν(xi )
1−ν(xi )
that preη (`i
, x) ≤ η(`i
, x) − 1. Also, for all such x
and i it holds that

Intuitively, the variable x`,`0 represents the probability that when
starting in location ` with variable n having some value k, the first
location in which the value of n decreases to k − 1 is `0 (note that
this probability is independent of k). Next, y`,`0 is the conditional
expected number of steps needed to decrease n by 1, conditioned by
the event that we start in ` and the first state in which n drops below
the initial value is `0 . Formally, it is shown in [10] and [19] that
these probabilities and expectations are the minimal non-negative
solutions of the system.

ν(x )

=
≥

1 2
(xwhile,while + xwhile,else )
2
1
1
= + (xwhile,while · xwhile,else )
2
2
1
(3
+
2ywhile,while · x2while,while + (ywhile,else + 1) · xwhile,else )
= 2
xwhile,while
3
1
+ 2 (3 + ywhile,while + ywhile,else ) · xwhile,while · xwhile,else
= 2
xwhile,else
(2)

xwhile,while =

η(`i i , x)
η(`i+1 , [xi /ν(xi )](x)) + hi,i (x)
− hi,i+1 ([xi /ν(xi )](x)) + 1
η(`i+1 , [xi /ν(xi )](x)) + 1 ,

It is then easy to check that the expected termination time of P is
given by the formula
1 + xwhile,while (ywhile,while + 1) + xwhile,else (ywhile,else + 2).

Examining the solutions of (2) (we used √Wolfram Alpha to√iden5−1
3− 5
, xwhile,else
,
tify them) we get that
2
2
√ xwhile,while =
√ =
ywhile,while = (85 + 43 5)/10, ywhile,else = (15√
+ 29 5)/10. Plugging this into (3) we get that ET(P ) = 2(5 + 5).

where the latter inequality follows from hi,i+1 ([xi /ν(xi )](x)) =
0 and non-negativity of hi,i (x) for x ∈ [0, 1]n . Hence,
ν(x )
ν(x )
preη (`i i , x) ≤ η(`i i , x) − 1. Finally, let us focus on `n+1 .
Let x be such that x |= ϕ ∧ I(`n+1 ). It is easy to check that

D.2
preη (`n+1 , x) = η(`n+1 , x)+2n−(Pen −1)·

n
X

(3)

|ν(xi )−x[i]|.

Proof of Lemma 4

Lemma 4. The quantitative approximation problem can be solved
in a doubly exponential time for programs with only discrete probability choices.

i=1

(1)
Now since x |= ϕ, there is 1 ≤ j ≤ m such that (gξj,1 + gξj,2 +
gξj,3 )(x) ≤ 21 , which implies gξj,k (x) ≤ 21 for all 1 ≤ k ≤ 3,
as all these numbers are non-negative. On the other hand, there
is 1 ≤ k0 ≤ 3 such that ν(ξj,k0 ) = 1, as ν is a satisfying
assignment. Let xi be the variable in ξj,k0 . If ξj,k0 is a positive
literal, then ν(xi ) = 1 and x[i] = gξj,k0 (x) ≤ 21 , and if ξj,k0
is negative, then νxi = 0 and x[i] = 1 − gξj,k0 (x) ≥ 21 . In
both cases we get |ν(xi ) − x[i]| ≥ 21 . Plugging this into (1)
and combining with the fact that (Pen − 1)/2 ≥ 2n + 1 we
get that preη (`n+1 , x) ≤ η(`n+1 , x) − 1. Hence, η is indeed an
LRSM.

Proof. The algorithm proceeds via analysing a suitable finite unfolding of the input program P . Formally, an n-step unfolding of
P , where n ∈ N, is an SGS Unf (P, n) such that
• the set locations of Unf (P, n) consists of certain finite paths

in GP (i.e. in the SGS associated to P ). Namely, we take
those finite paths whose starting configuration is the initial
configuration of GP and whose length is at most n. The type
of such a location w is determined by the type of a location in
the last configuration of GP appearing on w.
• Unf (P, n) has the same program and random variables as

D.

GP (i.e. the same ones as P ) and the initial configuration of
Unf (P, n) is the tuple ((`0 , x0 ), x0 ), where (`0 , x0 ) is the initial configuration of GP (it can be identified with a finite path
of length 0).

Details of Section 5

• For every pair w, w 0 of locations of Unf (P, n) (i.e., w, w 0 are

D.1

finite paths in GP ) such that w0 can be formed by performing
a single transition τ out of the last configuration of w, there
is a transition (w, f, w0 ) in Unf (P, n), where f is an update
function of τ . Moreover, for every history w of length n that is
also a location of Unf (P, n) there is a transition (w, id, w) in
Unf (P, n).

Irrationality of expected termination time

Let us again consider the program P in Figure 9. We claim that
ET(P ) is irrational. Note that the stochastic game structure GP has
six locations, where the following two are of interest for us: the
location corresponding to the beginning of the while loop, which
we denote by while, and the location entered after executing the first
assignment in the else branch, which we denote by else. Consider
the following systems of polynomial equations:

• The probability distributions and guard functions for probabilis-

tic/deterministic locations w of Unf (P, n) are determined, in a
natural way, by the probability distribution/guard functions of
the location in the last configuration of w.

19

2015/10/30

Note that that each configuration of Unf (P, n) reachable from
the initial configuration is of the form ((`0 , x0 ), . . . , (`i , xi ), xi ),
where (`j , xj ), 0 ≤ j ≤ i are configurations of Unf (P, n).
In particular, the values of program variables in every reachable
configuration (w, x) of Unf (P, n) are uniquely determined by w.
To avoid confusion, in the following we will denote the locations in
GP by `, `0 , `1 , . . . and locations in Unf (P, n) by w, w0 , w1 , . . . .

exponential bound then follows from the aforementioned bound on
the size of Unf (P, n).
First let us show how to compute n. Since P is a bounded
LRA PPand we are given the corresponding ranking supermartingale η with one-step change bounds a, b, by Theorem 5 we can
compute, in polynomial time, a concentration bound B which is at
most exponential in the size of P . That is, there are positive numbers c1 , c2 , which depend just on P , such that for each x ≥ B it
holds Thr(P, x) ≤ c1 · exp(−c2 · x). Moreover, numbers c1 and
c2 are also computable in polynomial time and at most exponential in the size of P , as witnessed in the proof of Theorem 5. Now
denote by M0 the value of the LRSM η in the initial configuration
of P . Note that M0 , as well as the bounds a, b, are at most exponential in the size of P as η, a and b can be obtained by solving
a system of linear inequalities with coefficients determined by P .
We compute (in polynomial time) the smallest integer n ≥ B such
that c1 · e−c2 ·n · (n + (M0 + n · (b − a))/) ≤ δ, where  is as in
Definition 8 (the minimal expected decrease of the value of η in a
single step). It is straightforward to verify that such an n exists and
that it is polynomial in M0 , , and a, b, and hence exponential in
the size of P .

Given P and n it is possible to construct Unf (P, n) in time exponential in n and in the encoding size of P . To see this, observe that
the graph of Unf (P, n) is a tree of depth n and so Unf (P, n) has
at most 2n locations. We can construct Unf (P, n) by, e.g. depthfirst enumeration of all finite paths in GP of length ≤ n. To bound
the complexity of the construction we need to bound the magnitude
of numbers (i.e. variable values) appearing on these finite paths –
these are needed to determine which transition to take in deterministic locations. Note that for every A PP P there is a positive number
K at most exponential in the encoding size of P such that in every step the absolute value of any variable of P can increase by the
factor of at most K in every step. Hence, after n steps the absolute
value of every variable is bounded by K n · L, where L is a maximal absolute value of any variable of P upon initialization (L is
again at most exponential in the size of P ). The exponential (in n
and size of P ) bound on the time needed to construct Unf (P, n)
follows.

Now let us construct the cost function cost. The initial location
gets cost 0 and all other locations get cost 1 except for locations w
that represents the paths in GP of lenth n. The latter locations get a
special cost C = (M0 + n · (b − a))/.

After constructing Unf (P, n), we post-process the SGS by removing all transitions outgoing from angelic locations that violate the
supermartingale property of η. Formally, for every angelic location w of Unf (P, n) and each its successor w0 we denote by c and
c0 the last configurations on w and w0 , respectively. We then check
whether preη (c) = η(c0 ), and if not, we remove the transition from
w to w0 .

We prove that for any pair of schedulers σ, π, σ ∈ cmp(η), it holds
|Eσ,π T − E∆(σ),Γ(π) W | ≤ δ. So fix an arbitrary such pair. We
start by proving that Eσ,π T ≤ E∆(σ),Γ(π) W . Since the behaviour
of the schedulers in the first n steps is mimicked by ∆(σ) and Γ(π)
in Unf (P, n), and in the latter SGS we accumulate one unit of cost
per each of the first n − 1 steps, it suffices to show that the expected
number of steps needed to terminate with these schedulers from any
configuration of GP that is reachable in exactly n steps is bounded
by C. Since the value of η can change by at most (b − a) in every
step, and σ ∈ cmp(η), the value of η after n steps in GP is at
most M0 + n · (b − a). By Theorem 1 the expected number of step
to terminate from a configuration with such an η-value is at most
(M0 + n · (b − a))/ as required.

There is a natural many-to-one surjective correspondence Γ between demonic schedulers in GP and demonic schedulers in
Unf (P, n) (the schedulers in GP that have the same behaviour up
to step n are mapped to a unique scheduler in Unf (P, n) which
induces this behaviour). Similarly, there is a many-to-one correspondence ∆ between angelic schedulers that belong to cmp(η) in
GP and angelic schedulers in Unf (P, n).

To finish the proof we show that E∆(σ),Γ(π) W ≤ Eσ,π T + δ. First
note that E∆(σ),Γ(π) W − Eσ,π T can be bounded by p · C, where p
is the probability that a run in GP does not terminate in first n steps
under these schedulers. Since n ≥ B it holds p ≤ c1 · e−c2 ·n . Thus
p · C ≤ c1 · e−c2 ·n · (n + (M0 + n · (b − a))/) ≤ δ, the last
inequality following from the choice of n.

Let T ermn be the set of all locations w in Unf (P, n) that, when
interpreted as paths in GP , end with a configuration of the form
(`out
P , x) for some x. It is easy to verify that for any adversarial
scheduler π in GP the probability Pπ (T ≤ x)) is equal to the
probability of reaching T ermn under Φ(π) in Unf (P, n).
To solve the quantitative approximation problem we proceed as
follows: First we compute number n, at most exponential in the
size of P , such that the infimum (among all angelic schedulers in
cmp(η)) probability of not terminating in the first n steps is ”sufficiently small” in GP . Then we construct, in time exponential in n
and size of P the unfolding Unf (P, n) and assign a non-negative
cost cost(w) to each location w of Unf (P, n). We then define
a random variable W which to each
(w0 , x0 ), (w1 , x1 ), . . .
Prun
j
in Unf (P, n) assigns the number
cost(wi ), where j =
i=0
min{n, min{k | wk ∈ T ermn }}. Using the fact that in GP we
terminate with very high probability in the first n steps, we will
show how to construct the cost function cost in such a way that
for every pair of schedulers σ, π, where σ ∈ cmp(η), it holds
|Eσ,π T − E∆(σ),Γ(π) W | ≤ δ (the construction of cost can be
done in time polynomial in the size of Unf (P, n)). Hence, to solve
the quantitative approximation problem it will suffice to compute
0 0
inf σ0 supπ0 Eσ ,π W , where the infimum and supremum are taken
over schedulers in Unf (P, n). This computation can be done in
polynomial time via standard backward iteration [41]. The doubly-

D.3

Proofs for Section 5.2

Lemma 5. For every C ∈ N the following problem is PSPACEhard: Given a program P without probability or non-determinism,
with simple guards, and belonging to bounded LRA PP; and a
number N ∈ N such that either ET(P ) ≤ N or ET(P ) ≥ N · C,
decide, which of these two alternatives hold.
Proof. Let us fix a constant C.
We start by noting that there exists a constant K such that the
following K-LINEARLY BOUNDED MEMBERSHIP PROBLEM is
PSPACE-hard: Given a deterministic Turing machine (DTM) T
such that on every input of length n the machine T uses at most
K · n tape cells, and given a word w over the input alphabet of T ,
decide, whether T accepts w. This is because there exists K for
which there is a DTM TQBF satisfying the above condition which

20

2015/10/30

program terminates in exactly C · J · W steps. On the other hand,
if T does accept w, then the program terminates in at most J · W
steps. To finish the reduction, we put the number N mentioned in
item 1. equal to J · W .

decides the QBF problem (TQBF works by performing a simple recursive search of the syntax tree of the input formula). We show
a polynomial-time reduction from this membership problem to our
problems.
Let T , w be an instance of the membership problem. Since T has
a linearly bounded complexity with a known coefficient K, there
is a number J computable in time polynomial in size of T and w
such that if T accepts w, it does so in at most J steps (note that the
magnitude of J is exponential in size of T and w). The intuition
behind the reduction is as follows: we construct a deterministic
affine program P simulating the computation of T on input w. The
program consists of a single while-loop guarded by an expression
m ≥ 1 ∧ r ≥ 1, where m is a ”master” variable of the program
initialized in the preamble to C · J · |w|, while r is initialized to
1. The body of the while loop encodes the transition function of T .
The current configuration of T is encoded in variables of P : for
every state s we have a variable xs which is equal to 1 when the
current state is s and 0 otherwise; next, for every 1 ≤ i ≤ K · |w|,
where |w| is the length of w, and every symbol a of the tape
alphabet of T we have a variable xi,a , which is equal to 1 if
a is currently on the i-th tape cell, and 0 otherwise; and finally
we have a variable xhead which stores the current position of the
head. Additionally, we add a variable xstep which records, whether
the current configuration was already updated during the current
iteration of the while-loop. The variables are initialized so as to
represent the initial configuration of T on input w, e.g. xhead = 1
and xi,a = 1 if and only if either i ≤ |w| and a is the i-th
symbol of w, or i > |w| and a is the symbol of an empty cell. It
is then straightforward to encode the transition function using just
assignments and if-then-else statements, see below. At the end of
each iteration of the while loop the master variable m is decreased
by 1. However, if the current state is also an accepting state of T ,
then r is immediately set to 0 and thus the program terminates.

E.

Proofs for Section 5.1

Theorem 7. Let {Xn }n∈N be a supermartingale wrt some filtration
{Fn }n∈N and {[an , bn ]}n∈N be a sequence of intervals of positive
length in R. If X1 is a constant random variable and Xn+1 − Xn ∈
[an , bn ] a.s. for all n ∈ N, then
−

P(Xn − X1 ≥ λ) ≤ e

2λ2

Pn

k=2

(bk −ak )2

for all n ∈ N and λ > 0.
Proof. The proof goes through the characteristic method similar to
the original proof of Hoeffding’s Inequality [26, 35], and hence we
present only the important details. For each n ≥ 2 and t > 0, we
have (using standard arguments similar to [26, 35]):
E(etXn )

=

E E(etXn | Fn−1 )

=

E E et(Xn −Xn−1 ) · etXn−1 | Fn−1

=

E etXn−1 · E E et(Xn −Xn−1 ) | Fn−1








.

Note that for all x ∈ [an , bn ],
etx

≤
≤

More formally, to a transition δ of T saying that in a configuration
(s, a) the state should be changed to s0 , the symbol rewritten by b,
and the head moved by h ∈ {−1, 0, +1}, we assign the following
WK·|w|
affine program Qδ in which a guard ϕδ = i=1 (xs = 1 and
xstep = 0 and xhead = i and xi,a = 1) is used:

x − an
bn − x
· etan +
· etbn
bn − an
bn − an
bn etbn − an etan
x
· (etbn − etan ) +
.
bn − an
bn − an

Then from Xn − Xn−1 ∈ [an , bn ] a.s. and E(Xn | Fn−1 ) ≤
Xn−1 , we obtain

 bn etbn − an etan

E(etXn ) ≤ E etXn−1 ·

.
bn − an
By applying the analysis in the proof of [35, Lemma 2.6] (taking
a = an and b = bn ), we obtain

i f ϕδ t h e n
xs := 0 ; xs0 := 1 ; xi,a := 0 ; xi,b := 1 ;
xhead := xhead + h ; xstep = 1
else
skip
fi
i f xsacc = 1 t h e n r := 0 e l s e s k i p f i ;

2
1 2
bn etbn − an etan
≤ e 8 t (bn −an ) .
bn − an
This implies that
1 2 (b

E(etXn ) ≤ E etXn−1 · e 8 t



The overall program then looks as follows:

2
n −an )

.

By induction, it follows that
w h i l e m ≥ 1 ∧ r ≥ 1 do
m := m − 1 ;
xstep := 0
Qδ1 ; · · · Qδm
od ,

E(etXn )

1 t2

≤

E etX1 · e 8

=

etE(X1 ) · e 8



1 t2

Pn
k=2

Pn
k=2

(bk −ak )2

(bk −ak )2

.

Thus, by Markov Inequality, for all λ > 0,
P(Xn − X1 ≥ λ)

where δ1 , . . . , δm are all transitions of T . Clearly the program
always terminates and belongs to bounded LRA PP: there is a trivial
bounded LRSM whose value in the beginning of the while loop is
m while in further locations inside the while loop it takes the form
m + d, for suitably small constants d. Since m changes by at most
1 in every step, this LRSM is bounded.

By choosing t = Pn
k=2

Each iteration of the while loop takes the same amount of steps,
since exactly one of the programs Qδj enters the if-branch (we can
assume that the transition function of T is total). Let us denote this
number by W . It is easy to see that if T does not accept w, then the

=

P(et(Xn −X1 ) ≥ etλ )

≤

e−tλ · E et(Xn −X1 )

≤

e

1 t2
−tλ+ 8

4λ
,
(bk −ak )2

Pn
k=2



(bk −ak )2

.

we obtain
−

P(Xn − X1 ≥ λ) ≤ e

Pn

2λ2

k=2

(bk −ak )2

.

The desired result follows.

21

2015/10/30

where x is the updated program variable, ax` is the coefficient
vector variable of a` on program variable x and VarR (f (x, r))
is the variance on random variables r.

Proposition 2. {Yn }n∈N is a supermartingale and Yn+1 − Yn ∈
[a + , b + ] almost surely for all n ∈ N.
Proof. Recall that

Note that the formulae above can be transformed into existentiallyquantified non-strict linear assertions by Farkas’ Lemma. Also note
that there are no conditions for angelic or demonic locations since
once the angelic and demonic strategies are fixed, then there is no
stochastic behavior in one step for such locations, and hence the
variance is zero.

Yn = Xn +  · (min{T, n} − 1) .
Consider the following random variable:
Un = min{T, n + 1} − min{T, n} ,
and observe that this is equal to 1T >n . From the properties of
conditional expectation [53, Page 88] and the facts that (i) the event
T > n is measurable in Fn (which implies that E(1T >n | Fn ) =
1T >n ); and (ii) Xn ≥ 0 iff T > n (cf. conditions C2 and C3), we
have

Then we can apply Bernstein’s Inequality in the same way as for
Hoeffding’s Inequality. Define the stochastic process {Zn }n∈N by
Zn = Xn +  · (min{T, n} − 1) ;

similar to Yn for Proposition 2. We have the following proposition.
Proposition 3. {Zn }n∈N is a supermartingale. Moreover, Zn+1 −
E(Yn+1 | Fn ) − Yn = E(Xn+1 | Fn ) − Xn +  · E(Un | Fn )
2
= E(Xn+1 | Fn ) − Xn +  · E(1T >n | Fn ) E(Zn+1 | Fn ) ≤ M and Var(Zn+1 | Fn ) ≤ c , for all n ∈ N.
= E(Xn+1 | Fn ) − Xn +  · 1T >n
Proof. By the same analysis in Proposition 2, we have {Zn } is a
≤ − · 1Xn ≥0 +  · 1T >n
supermartingale. Consider the following random variable: Un =
= 0 .
min{T, n + 1} − min{T, n}, which is equal to 1T >n . From the
properties of conditional expectation [53, Page 88] and the facts
Note that the inequality above is due to the fact that Xn is a ranking
that (i) the event T > n is measurable in Fn (which implies that
out
supermartingale. Moreover, since T ≤ n implies θn = `P and
Var(1T >n (Xn+1 − Xn ) | Fn ) = 1T >n Var(Xn+1 − Xn | Fn ))
Xn+1 = Xn we have that (Xn+1 − Xn ) = 1T >n · (Xn+1 − Xn ).
we have the following:
Hence we have
Yn+1 − Yn

=
=
=

Xn+1 − Xn +  · Un
(Xn+1 − Xn ) +  · 1T >n
1T >n · (Xn+1 − Xn + ) .

Zn+1 − E(Zn+1 | Fn ) ≤ Xn+1 − E(Xn+1 | Fn ) ≤ M
and
Var(Zn+1 | Fn )

Hence Yn+1 − Yn ∈ [a + , b + ].

=
=
=
∗

Applying Bernstein Inequality for incremental programs in
LRA PP. Let η be an incremental LRSM template to be synthesized
for P and {Xn }n∈N be the stochastic process defined by
Xn := η(θn , {xk,n }k ) .

=
=

Var(1T >n · (Xn+1 − Xn + ) | Fn )
1T >n · Var(Xn+1 − Xn | Fn )

≤

c2 .

where (*) follows from the fact that T ≤ n implies θn = `out
P
and Xn+1 = Xn , and the last inequality follows the fact that
Var(Xn+1 − Xn | Fn ) ≤ c2 since c is obtained from the synthesis
of the LRSM.

To apply Bernstein’s Inequality, we need to synthesize constants
c, M to fulfill that for all n ∈ N,

p

Var(Xn+1 | Fn ) ≤ c and Xn+1 − E(Xn+1 | Fn ) ≤ M .

These conditions can be encoded by the following formulae:

Then similar to the derivation for Hoeffding’s Inequality, we have
P(T > n)

• for all ` ∈ LP with successor locations `1 , `2 ∈ L and the

≤

P(Zn − Z1 ≥ (n − 1) − W0 )

≤

e

branch probability value p, the sentence



∀x.∀i ∈ {1, 2}. η(`i , x) − preη (`, x) ≤ M
∧

p

p

1θn =` · Var(Xn+1 | Fn ) ≡ 1θn =` ·

p(1 − p)· b`1 − b`2

−

((n−1)−W0 )2
2c2 (n−1)+ 2 ·M ((n−1)−W0 )
3

.

The optimal choice of concentration threshold is the same as for
Hoeffding’s Inequality, and the optimality of upper bounds is reduced to a binary search on z satisfying



p(1 − p) · b`1 − b`2 ≤ c

((n − 1) − W0 )2
≥z
2c2 (n − 1) + 32 · M ((n − 1) − W0 )

holds, where one can obtain from easy calculation (on Bernoulli
random variables) that

p

Var(Zn+1 − Zn | Fn )
Var(Xn+1 − Xn +  · Un | Fn )
Var(Xn+1 − Xn +  · 1T >n | Fn )

;

and the constraints for LRSMs, the constraint  · (n − 2) ≥ W0
and the constraint for c, M , which can be solved by quadratic
programming [52].

• for all ` ∈ LS and all τ = (`, f, `0 ) ∈7→` , the sentence



∀x.∀r. η(`0 , f (x, r)) − η(`0 , ER (f (x, r))) ≤ M
∧

ax`

·

p

F.



VarR (f (x, r)) ≤ c

We present below the details of the code modeling the various
random walks of Section 6, along with the invariants specified in
the brackets. Also in the description we use Unif to denote the
uniform distribution.

holds, for which

p

1θn =` · Var(Xn+1 | Fn ) ≡ 1θn =` · ax` ·

Details related to Experimental Results

p

VarR (f (x, r))

22

2015/10/30

Explanation why RW in 2D not bounded LRA PP. We explain why
the example RW in 2D is not a bounded LRA PP: in this example at
any point either the x or the y coordinates changes by at most 2,
hence intuitively, the difference between two steps is bounded.
However, to exploit such a fact one needs to consider a martingale
defining min{x, y}, i.e., the minimum of two coordinate. However
such a martingale is not linear. For this example, the LRSM is not a
bounded martingale as the difference between the two coordinates
can be large.

[x ≥ 0]
w h i l e n ≥ 0 do
[x ≥ 0]
x := x + r ;
[x ≥ 0]
i f demon t h e n
[x ≥ 0]
i f prob( 78 ) t h e n
[x ≥ 0]
x := x − 1
else
[x ≥ 0]
x := x + 1
fi
else
[ x ≥ 0 ] s k i p ; [ x ≥ 0 ] x := x − 1
fi
od

x := n ;
[ x ≥ −1 ]
w h i l e x ≥ 0 do
[x ≥ 0]
i f prob(0.3) t h e n
[x ≥ 0]
x := x + 1
else
[x ≥ 0]
x := x − 1 ;
fi
od
[x < 0]

[x < 0]

Figure 11. Integer-valued random walk in one dimension, along
with linear invariants in square brackets.

Figure 13. A queuing example: Adversarial random walk in one
dimension. The linear invariants in square brackets. The distribution of the random variable r is described on page 14
.

x := n ;
[ x ≥ −1 ]
w h i l e x ≥ 0 do
[x ≥ 0]
i f prob(0.3) t h e n
[x ≥ 0]
x := x + Unif[0, 1]
else
[x ≥ 0]
x := x − Unif[0, 1] ;
fi
od
[x < 0]

x := n1 ; y = n2 ;

Figure 12. Real-valued random walk in one dimension, along with
linear invariants in square brackets.

[ x ≥ −2 ∧ y ≥ −3 ]
w h i l e ( x ≥ 0 ∧ y ≥ 0 ) do
[x ≥ 0 ∧ y ≥ 0]
i f ( demon )
[x ≥ 0 ∧ y ≥ 0]
x := x + Unif[−2, 1]
else
[x ≥ 0 ∧ y ≥ 0]
y := y + Unif[−2, 1]
od
[x < 0 ∨ y < 0]
Figure 14. A 2D random walk example: adversarial random walk
in two dimension, along with linear invariants in square brackets.

23

2015/10/30

x := n1 ; y = n2 ;
[ x − y ≥ −3 ]
w h i l e ( x ≥ y ) do
[x ≥ y]
i f ( demon ) [ x ≥ y ]
i f ( prob ( 0 . 7 ) )
[ x ≥ y ] x := x + Unif[−2, 1]
else
[ x ≥ y ] y := y + Unif[−2, 1]
else [x ≥ y]
i f ( prob ( 0 . 7 ) )
[ x ≥ y ] y := y + Unif[2, −1]
else
[ x ≥ y ] x := x + Unif[2, −1]
od
[x < y]
Figure 15. A 2D random walk example: Variant adversarial random walk in two dimension. The linear invariants in square brackets.

24

2015/10/30

