Termination Analysis of Probabilistic Programs
through Positivstellensatz’s⋆

arXiv:1604.07169v1 [] 25 Apr 2016

Krishnendu Chatterjee1 , Hongfei Fu1,2 , and Amir Kafshdar Goharshady1
1

2

IST Austria
State Key Laboratory of Computer Science, Institute of Software, Chinese
Academy of Sciences, P.R. China
Abstract. We consider nondeterministic probabilistic programs with
the most basic liveness property of termination. We present efficient
methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through
synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other
hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz’s, yielding an
efficient method which is not only sound, but also semi-complete over
a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient
quadratic ranking-supermartingales when a linear one does not exist even
for simple affine programs.

1

Introduction

Probabilistic Programs. Classic imperative programs extended with randomvalue generators gives rise to probabilistic programs. Probabilistic programs
provide the appropriate framework to model applications ranging from randomized algorithms [39,18], to stochastic network protocols [5,35], to robot planning [34,31], etc. Nondeterminism plays a crucial role in modeling, such as, to
model behaviors over which there is no control, or for abstraction. Thus nondeterministic probabilistic programs are crucial in a huge range of problems, and
hence their formal analysis has been studied across disciplines, such as probability theory and statistics [19,29,33,43,40], formal methods [5,35], artificial
intelligence [32,31], and programming languages [11,22,44,20].
Basic Termination Questions. Besides safety properties, the most basic property
for analysis of programs is the liveness property. The most basic and widely used
notion of liveness for programs is termination. In absence of probability (i.e., for
⋆

A conference version of the paper appears in [12]

nonprobabilistic programs), the synthesis of ranking functions and proof of termination are equivalent [23], and numerous approaches exist for synthesis of
ranking functions for nonprobabilistic programs [9,14,41,49]. The most basic extension of the termination question for probabilistic programs is the almost-sure
termination question which asks whether a program terminates with probability 1. Another fundamental question is about finite termination (aka positive
almost-sure termination [22,8]) which asks whether the expected termination
time is finite. The next interesting question is the concentration bound computation problem that asks to compute a bound M such that the probability that
the termination time is below M is concentrated, or in other words, the probability that the termination time exceeds the bound M decreases exponentially.
Previous Results. We discuss the relevant previous results for termination analysis of probabilistic programs.
– Probabilistic Programs. First, quantitative invariants was introduced to establish termination of discrete probabilistic programs with demonic nondeterminism [36,37], This was extended in [11] to ranking supermartingales
resulting in a sound (but not complete) approach to prove almost-sure termination of probabilistic programs without nondeterminism but with integerand real-valued random variables from distributions like uniform, Gaussian,
and Poison, etc. For probabilistic programs with countable state-space and
without nondeterminism, the Lyapunov ranking functions provide a sound
and complete method for proving finite termination [8,24]. Another sound
method is to explore bounded-termination with exponential decrease of probabilities [38] through abstract interpretation [16]. For probabilistic programs
with nondeterminism, a sound and complete characterization for finite termination through ranking-supermartingale is obtained in [22]. Ranking supermartingales thus provide a very powerful approach for termination analysis
of probabilistic programs.
– Ranking Functions/supermartingales Synthesis. Synthesis of linear
ranking-functions/ranking-supermartingales has been studied extensively in [41,14,11,13]. In context of probabilistic programs, the algorithmic
study of synthesis of linear ranking supermartingales for probabilistic
programs (cf. [11]) and probabilistic programs with nondeterminism (cf.
our previous result [13]) has been studied. The major technique adopted in
these results is Farkas’ Lemma [21] which serves as a complete reasoning
method for linear inequalities. Beyond linear ranking functions, polynomial
ranking functions have also been considered. Heuristic synthesis method of
polynomial ranking-functions is studied in [4,10]: Cook et al. [4] checked
termination of deterministic polynomial programs by detecting divergence
on program variables and Bradley et al. [10] extended to nondeterministic
programs through an analysis on finite differences over transitions. More
general methods for deterministic polynomial programs are given by [15,48]
where Cousot [15] uses Lagrangian Relaxation, and Shen et al. [48] use Putinar’s Positivstellensatz [42]. Complete methods of synthesizing polynomial
2

ranking-functions for nondeterministic programs are studied by Yang et
al. [52], where a complete method through root classification/real root
isolation of semi-algbebraic systems and quantifier elimination is proposed.
To summarize, while many different approaches has been studied, the algorithmic study of synthesis of ranking supermartingales for probabilistic programs has
only been limited to linear ranking supermartingales. For example, [11] presents a
method of synthesis of linear ranking supermartingales for probabilistic programs
without nondeterminism, and identifies synthesis of more general nonlinear supermartingales, or extension to probabilistic programs with nondeterminism as
important challenges. While the approach of [11] has been extended to probabilistic programs with nondeterminism in our previous result [13], it is restricted
to linear ranking supermartingales. Hence there is no algorithmic approach to
handle nonlinear ranking supermartingales even for probabilistic programs without nondeterminism.
Our Contributions. Our contributions are as follows:
1. Polynomial Ranking Supermartingales. First, we extend the notion of linear
ranking supermartingales (LRSM) to polynomial ranking supermartingales
(pRSM). We show (by a straightforward extension of LRSM) that pRSM
implies both almost-sure as well as finite termination.
2. Positivstellensatz’s. Second, we conduct a detailed investigation on the application of Positivstellensatz’s (German for “positive-locus-theorem” which
is related to polynomials over semialgebraic sets) (cf. Sect. 5.1) to synthesis
of pRSMs over nondeterministic probabilistic programs. To the best of our
knowledge, this is the first result which demonstrates the synthesis of a polynomial subclass of ranking supermartingales through Positivstellensatz’s.
3. New Approach for Non-probabilistic Programs. Our results also extend existing results for nonprobabilistic programs. We present the first result that
uses Schmüdgen’s Positivstellensatz [46] and Handelman’s Theorem [26] to
synthesize polynomial ranking-functions for nonprobabilistic programs.
4. Efficient Approach. The previous complete method [52] suffers from high
computational complexity due to the use of quantifier elimination. In contrast, our approach (sound but not complete) is efficient since the synthesis
can be accomplished through linear or semi-definite programming, which
can mostly be solved in polynomial time in the problem size [25]. In particular, our approach does not require quantifier elimination, and works for
nondeterministic probabilistic programs.
5. Experimental Results. We demonstrate the effectiveness of our approach on
several classical examples. We show that on classical examples, such as Gambler’s Ruin, and Random Walk, our approach can synthesize a pRSM efficiently. For these examples, LRSMs do not exist, and many of them cannot
be analysed efficiently by previous approaches.
Technical Contributions and Novelty. The main technical contributions and novelty are:
3

1. While Farkas’ Lemma and Motzkin’s Transposition Theorem are standard
techniques to linear ranking functions or linear ranking supermartingales,
they are not sufficient for pRSMs. Instead, our technical contributions is to
use various Positivstellensatz’s to synthesize pRSMs.
2. Even for nonprobabilistic programs, only a limited number of Positivstellensatz’s have been used, e.g., [48]; some of the Positivstellensatz’s we use (such
as Schmüdgen’s Positivstellensatz [46] and Handelman’s Theorem [26]) have
not even been used in the context of nonprobabilistic programs.
In summary, we study the use of Positivstellensatz’s for the first time for probabilistic programs, and for some of them, even for the first time for nonprobabilistic programs, and show that how they can be used for efficient algorithms
for program analysis.
Organization of the Paper. In Sect. 2, we present the syntax and semantics of
probabilistic programs. In Sect. 3, we define the problems to be studied. In
Sect. 4, we develop the notion of polynomial ranking supermartingale. Then in
Sect. 5, we present Positivstellensatz and our algorithm to synthesize polynomial ranking supermartingales. In Sect. 6, we present our experimental results.
Finally, Sect. 7 concludes the paper.

2
2.1

Probabilistic Programs
Basic Notations and Concepts

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].
Polynomial Predicates. Let X be a finite set of variables endowed with a fixed
linear order under which we have
 X = {x1, . . . , x|X| }. We denote the set of
real-coefficient polynomials by R x1 , . . . , x|X| or R[X]. A polynomial constraint
over X is a logical formula of the form g1 ⋊
⋉g2 , where g1 , g2 are polynomials
over X and ⋊
⋉∈ {<, ≤, >, ≥}. A propositional polynomial predicate over X is a
propositional formula whose all atomic propositional literals are either true, false
or polynomial constraints over X. The validity of the satisfaction assertion x |=
φ between a vector x ∈ R|X| (interpreted in the way that the value for xj
(1 ≤ j ≤ |X|) is x[j]) and a propositional polynomial predicate φ is defined in
the standard way w.r.t polynomial evaluation and normal semantics for logical
connectives (cf. Appendix A). The satisfaction set of a propositional polynomial
predicate φ is defined as JφK := {x ∈ R|X| | x |= φ}. For more on polynomials
(e.g., polynomial evaluation and arithmetic over polynomials), we refer to the
textbook [30, Chapter 3].
4

Probability Space. A probability space is a triple (Ω, F , P), where Ω is a non-empty
set (so-called sample space), F is a σ-algebra over Ω (i.e., a collection of subsets
of Ω that contains the empty set ∅ and is closed under complementation and
countable union), and P is a probability measure on F , i.e., a function P : F →
[0, 1] such that (i) P(Ω) = 1 and (ii) for all set-sequences A1 , A2 , · · P
· ∈ F that are
∞
pairwise-disjoint
(i.e.,
A
∩
A
=
∅
whenever
i
=
6
j)
it
holds
that
i
j
i=1 P(Ai ) =
S∞
P ( i=1 Ai ) .

Random Variables and Filtrations. A random variable X in a probability space
(Ω, F , P) is an F -measurable function X : Ω → R ∪ {−∞, +∞}, i.e., a function
satisfying the condition that for all d ∈ R∪{+∞, −∞}, the set {ω ∈ Ω | X(ω) ≤
d} belongs to F . The expected value of a random variable X, denote by RE(X), is
defined as the Lebesgue integral of X with respect to P, i.e., E(X) := X dP ;
the precise definition of Lebesgue integral is somewhat technical and is omitted
here (cf. [7, Chapter 5] for a formal definition). A filtration of a probability
space (Ω, F , P) is an infinite sequence {Fn }n∈N0 of σ-algebras over Ω such that
Fn ⊆ Fn+1 ⊆ F for all n ∈ N0 .

2.2

Probabilistic Programs

The Syntax. The class of probabilistic programs we consider encompasses basic programming mechanisms such as assignment statement (indicated by ‘:=’),
while-loop, if-branch, basic probabilistic mechanisms such as probabilistic branch
(indicated by ‘prob’) and random sampling, and demonic nondeterminism indicated by ‘⋆’. Variables (or identifiers) of a probabilistic program are of real type,
i.e., values of the variables are real numbers; moreover, variables are classified
into program and sampling variables, where program variables receive their values through assignment statements and sampling variables do through random
samplings. We consider that each sampling variable r is bounded, i.e., associated
with a one-dimensional cumulative distribution function Υr and a non-empty
bounded interval suppr such that any random variable z which respects Υr satisfies that z lies in the bounded interval with probability 1. Due to space limit, we
put details (e.g., grammar) in Appendix B. An example probabilistic program
is illustrated in Example 1.
Example 1. Consider the running example depicted in Fig. 1, where r is a sampling variable with the two-point distribution {1 7→ 0.5, −1 7→ 0.5} where the
probability to take values 1 and −1 are both 0.5. The probabilistic program
models a scenario of Gambler’s Ruin where the gambler has initial money x and
repeats gambling until he wins more than 10 or lose all his money. The result of
a gamble is nondeterministic: either win 1 with probability 0.5 (nondeterministic
branch); or lose with probability 0.51 (the probabilistic branch). The numbers
1 − 7 on the left are the program counters for the program, where 1 is the initial
program counter and 7 the terminal program counter.
5

1 : while 1 ≤ x ∧ x ≤ 10 do
2:
i f ⋆ then
3:
x := x + r
else
4:
i f prob ( 0.51) then
5:
x := x − 1
else
6:
x := x + 1
fi
fi
od
7:

7

x 7→ x + r

3
⋆

x < 1 ∨ x > 10

1

x ≥ 1 ∧ x ≤ 10

x 7→ x + 1

2

6
⋆

0.49

x 7→ x − 1
5

0.51

4

Fig. 2. The CFG of the Running Example

Fig. 1. The Running Example: Gambler’s
Ruin

The semantics. We use control flow graphs to capture the semantics of probabilistic programs, which we define below.
Definition 1 (Control Flow Graph). A control flow graph (CFG) is a tuple
G = (L, ⊥, (X, R), 7→) with the following components:
– L is a finite set of labels partitioned into four pairwise-disjoint subsets Ld ,
Lp , Lc and La of demonic, probabilistic, conditional-branching (branching for
short) and assignment labels, resp.; and ⊥ is a special label not in L called
the terminal label;
– X and R are disjoint finite sets of real-valued program and sampling variables respectively ;
– 7→ is a transition relation in which every member (called transition) is a
tuple of the form (ℓ, α, ℓ′ ) for which ℓ (resp. ℓ′ ) is the source label (resp.
target label) in L and α is either a real number in (0, 1) if ℓ ∈ Lp , or ⋆
if ℓ ∈ Ld , or a propositional polynomial predicate if ℓ ∈ Lc , or an update
function f : R|X| × R|R| → R|X| if ℓ ∈ La .
W.l.o.g, we assume that L ⊆ N0 . Intuitively, labels in Ld correspond to demonic
statements indicated by ‘⋆’; labels in Lp correspond to probabilistic-branching
statements indicated by ‘prob’; labels in Lc correspond to conditional-branching
statements indicated by some propositional polynomial predicate; labels in La
correspond to assignments indicated by ‘:=’ and the terminal label ⊥ denotes the
termination of a program. The transition relation 7→ specifies the transitions between labels together with the additional information specific to different types
of labels. The update functions are interpreted as follows: we first fix two linear
orders on X and R so that X = {x1 , . . . , x|X| } and R = {r1 , . . . , r|R| }, interpreting each vector x ∈ R|X| (resp. r ∈ R|R| ) as a valuation of program (resp.
sampling) variables in the sense that the value of xj (resp. rj ) is x[j] (resp. r[j]);
6

then each update function f is interpreted as a function which transforms a valuation x ∈ R|X| before the execution of an assignment statement into f (x, r)
after the execution of the assignment statement, where r is the valuation on R
obtained from a sampling before the execution of the assignment statement.
It is intuitively clear that any probabilistic program can be naturally transformed
into a CFG. Informally, each label represents a program location in an execution
of a probabilistic program for which the statement of the program location is
the next to be executed. A detailed construction is provided in Appendix C.
Example 2. The control flow graph of the running example (Example 1) is depicted in Fig. 2, where vertices correspond to labels specified in Fig. 1.
Now we present the semantics of probabilistic programs. In the rest of the section,
we fix a probabilistic program P with the set X = {x1 , . . . , x|X| } of program
variables and the set R = {r1 , . . . , r|R| } of sampling variables, and let G =
(L, ⊥, (X, R), 7→) be its associated CFG. We also fix ℓ0 and resp. x0 to be the
label corresponding to the first statement to be executed in P and resp. the
initial valuation of program variables.
The Semantics. A configuration (for P ) is a tuple (ℓ, x) where ℓ ∈ L ∪ {⊥}
and x ∈ R|X| . A finite path (of P ) is a finite sequence of configurations
(ℓ0 , x0 ), · · · , (ℓk , xk ) such that for all 0 ≤ i < k, either (i) ℓi+1 = ℓi = ⊥
and xi = xi+1 (i.e., the program terminates); or (ii) there exist (ℓi , α, ℓi+1 ) ∈7→
and r ∈ {r′ | ∀r ∈ R. r ′ (r) ∈ suppr } such that one of the following conditions
hold: (a) ℓi ∈ Lp ∪ Ld and xi = xi+1 (probabilistic or demonic transitions),
(b) ℓi ∈ Lc , xi = xi+1 and xi |= α (conditional-branch transitions), (c) ℓi ∈ La
and xi+1 = α(xi , r) (assignment transitions). A run (of P ) is an infinite sequence
of configurations whose all finite prefixes are finite paths over P . A configuration
(ℓ, x) is reachable from the initial configuration (ℓ0 , x0 ) if there exists a finite
path (ℓ0 , x0 ), · · · , (ℓk , xk ) such that (ℓ, x) = (ℓk , xk ).
The probabilistic feature of P can be captured by constructing a suitable probability measure over the set of all its runs. However, before this can be done,
nondeterminism in P needs to be resolved by some scheduler.
Definition 2 (Scheduler). A scheduler (for P ) is a function which assigns to
every finite path (ℓ0 , x0 ), . . . , (ℓk , xk ) with ℓk ∈ Ld a transition in 7→ with source
label ℓk .
The behaviour of P under a scheduler σ is standard: at each step, P first samples
a real number for each sampling variable and then evolves to the next step
according to its CFG or the scheduler choice (the details are in Appendix D).
In this way, the scheduler and random choices/samplings produce a run over P .
Moreover, each scheduler σ induces a unique probability measure Pσ over the
7

runs of P . In the rest of the paper, we will use Eσ (·) to denote the expected
values of random variables under Pσ .
Random Variables and Filtrations over Runs. We define the following (vectors of)
P
random variables on the set of runs of P : {θnP }n∈N0 , {xP
n }n∈N0 and {r n }n∈N0 :
P
each θn is the random variable representing the (integer-valued) label at the
P
n-th step; each xP
n is the vector of random variables such that each xn [i] is the
random variable representing the value of the program variable xi at the n-th
step; and each r P
n [i] is the random variable representing the sampled value of the
sampling variable ri at the n-th step. The filtration {HnP }n∈N0 is defined such
that each σ-algebra HnP is the smallest σ-algebra that makes all random variables
in {θkP }0≤k≤n and {xP
k }0≤k≤n measurable. We will omit the superscript P in all
the notations above if it is clear from the context.
Remark 1. Under the condition that each sampling variable is bounded, using
an inductive argument it follows that each xn is a vector of bounded random
variables. Thus Eσ (|xn [i]|) exists for each random variable xn [i].
Below we define the notion of polynomial invariants which logically captures
all reachable configurations. A polynomial invariant may be obtained through
abstract interpretation [16].
Definition 3 (Polynomial Invariant). A polynomial invariant (for P ) is a
function I assigning a propositional polynomial predicate over X to every label
in G such that for all configurations (ℓ, x) reachable from (ℓ0 , x0 ) in G, it holds
that x |= I(ℓ).

3

Termination over Probabilistic Programs

In this section, we first define the notions of almost-sure/finite termination and
concentration bounds over probabilistic programs, and then describe the computational problems studied in this paper. Below we fix a probabilistic program
P with its associated CFG G = (L, ⊥, (X, R), 7→) and an initial configuration
(ℓ0 , x0 ) for P .
Definition 4 (Termination [8,22,13]). A run ω = {(ℓn , xn )}n∈N0 over P is
terminating if ℓn = ⊥ for some n ∈ N0 . The termination time of P is a random
variable TP such that for each run ω = {(ℓn , xn )}n∈N0 , TP (ω) is the least number
n such that ℓn = ⊥ if such n exists, and ∞ otherwise. The program P is said
to be almost-sure terminating (resp. finitely terminating) if Pσ (TP < ∞) = 1
(resp. Eσ (TP ) < ∞) for all schedulers σ (for P ).
Note that Eσ (TP ) < ∞ implies that Pσ (TP < ∞) = 1, but the converse does
not necessarily hold (see [11, Example 5] for an example). i.e., finite-termination
8

implies almost-sure termination, but not vice-versa. To measure the expected
values of the termination time under all (demonic) schedulers, we further define
the quantity ET(P ) := supσ Eσ (TP ) .
Definition 5 (Concentration on Termination Time [38,13]). A concentration bound for P is a non-negative integer M such that there exist real constants c1 ≥ 0 and c2 > 0, and for all N ≥ M we have P(TP > N ) ≤ c1 · e−c2 ·N
.
Informally, a concentration bound characterizes exponential decrease of probability values of non-termination beyond the bound. On one hand, it can be
used to give an upper bound on probability of non-termination beyond a large
step; and on the other hand, it leads to an algorithm that approximates ET(P )
(cf. [13, Theorem 5]).
In this paper, we consider the algorithmic analysis of the following problems:
– Input: a probabilistic program P , a polynomial invariant I for P and an
initial configuration (ℓ0 , x0 ) for P ;
– Output: (Almost-Sure/Finite Termination) “yes” if the algorithm
finds that P is almost-sure/finite terminating and “fail” otherwise;
– Output: (Concentration on Termination) a concentration bound if the
algorithm finds one and “fail” otherwise.

4

Polynomial Ranking-Supermartingale

In this section, we develop the notion of polynomial ranking-supermartingale
which is an extension of linear ranking-supermartingale [11,13]. We fix a probabilistic program P , a polynomial invariant I for P and an initial configuration
(ℓ0 , x0 ) for P . Let G = (L, ⊥, (X, R), 7→) be the associated CFG of P , with
X = {x1 , . . . , x|X| } and R = {r1 , . . . , r|R| }. We first present the general notion
of ranking supermartingale, and then define that of polynomial ranking supermartingale.
Definition 6 (Ranking Supermartingale [22,13]). A discrete-time stochastic process {Xn }n∈N0 w.r.t a filtration {Fn }n∈N0 is a ranking supermartingale (RSM) if there exist K < 0 and ǫ > 0 such that for all n ∈ N0 ,
we have E(|Xn |) < ∞ and it holds almost surely (with probability 1) that
Xn ≥ K and E(Xn+1 | Fn ) ≤ Xn − ǫ · 1Xn ≥0 , where E(Xn+1 | Fn ) is the
conditional expectation of Xn+1 given Fn (cf. [51, Chapter 9]).
Informally, a polynomial ranking-supermartingale over P is a polynomial instantiation of an RSM through certain function η : (L ∪ {⊥}) × R|X| → R which
satisfies that each η(ℓ, ·) (for all ℓ ∈ L ∪ {⊥}) is essentially a polynomial function over X. Given such a function η, the intuition is to have conditions that
9

make the stochastic process Xn = η(θn , xn ) an RSM. To ensure this, we consider
the conditional expectation Eσ (Xn+1 | Hn ); this is captured by an extension of
pre-expectation [11,13] from the linear to the polynomial case. Below we define
L⊥ := L ∪ {⊥}. For a function g : R|X| × R|R| → R, we let ER (g, ·) : R|X| → R
be the function such that each ER (g, x) is the expected value E(g(x, r̂)), where
r̂ is any vector of independent random variables such that each r̂[i] is a random
variable that respects the cumulative distribution function Υri .
Definition 7 (Pre-Expectation). Let η : L⊥ × R|X| → R be a function such
that each η(ℓ, ·) (for all ℓ ∈ L⊥ ) is a polynomial function over X. The function
preη : L⊥ × R|X| → R is defined by:
P
– preη (ℓ, x) := (ℓ,z,ℓ′ )∈7→ z · η (ℓ′ , x) if ℓ ∈ Lp (probabilistic transitions);
– preη (ℓ, x) := max(ℓ,⋆,ℓ′ )∈7→ η(ℓ′ , x) if ℓ ∈ Ld (nondeterministic transitions);
– preη (ℓ, x) := η(ℓ′ , x) if ℓ ∈ Lc and (ℓ, φ, ℓ′ ) is the only transition in 7→ such
that x |= φ (conditional transitions);
– preη (ℓ, x) := ER (g, x) if ℓ ∈ La , where g is the function such that g(x, r) =
η (ℓ′ , f (x, r)) and (ℓ, f, ℓ′ ) is the only transition in 7→ (assignment transitions); and
– preη (ℓ, x) := η(ℓ, x) if ℓ = ⊥ (terminal location).
The following lemma establishes the relationship between pre-expectation and
conditional expectation whose proof is in Appendix E.
Lemma 1. Let η : L⊥ × R|X| → R be a function such that each η(ℓ, ·) (for
all ℓ ∈ L⊥ ) is a polynomial function over X, and σ be any scheduler. Let the
stochastic process {Xn }n∈N0 be defined by: Xn := η(θn , xn ). Then for all n ∈ N0 ,
we have Eσ (Xn+1 | Hn ) ≤ preη (θn , xn ).
Example 3. Consider the running example in Example 1 with CFG in Fig. 2.
Let η be the function specified in the second and fifth column of Table 1, where
g(x) := (x − 1)(10 − x). Then preη is given in the third and sixth column of
Table 1. Note that the case for i = 2 is obtained from preη (2, x) = max{g(x) +
9.6, g(x) + 9.6}, and the case for i = 3 is from preη (3, x) = ER (h, x), where h is
the function h(y, r) = g(y) − (2y − 11)r − r2 + 10.

i

η(i, x)

1

g(x) + 10

2
3
4

g(x) + 9.8
g(x) + 9.6
g(x) + 9.6

preη (i, x)
11≤x≤10 · (g(x) + 9.8)
+ 1x<1∨x>10 · (−0.2)
g(x) + 9.6
g(x) + 9
g(x) + 0.04x + 8.98
Table 1. η and preη for

10

i

η(i, x)

preη (i, x)

5

g(x) + 2x − 1.8

g(x) + 2x − 2

6
7

g(x) − 2x + 20.2
−0.2

g(x) − 2x + 20
−0.2

Example 1 and Fig. 2

We now define the notion of polynomial ranking-supermartingale. The intuition
is that we encode the RSM-difference condition as a logical formula, treat zero
as the threshold between terminal and non-terminal labels, and use the invariant
I to over-approximate the set of reachable configurations at each label. Below
for each ℓ ∈ Lc , we define PP(ℓ) to be the propositional polynomial predicate
W
(ℓ,φ,ℓ′ )∈7→,ℓ′ 6=⊥ φ; and for ℓ ∈ L\Lc , we let PP(ℓ) := true.

Definition 8 (Polynomial Ranking-Supermartingale). A d-degree polyonomial ranking-supermartingale map (in short, d-pRSM) w.r.t (P, I) is a function η : L⊥ × R|X| → R satisfying that there exist ǫ > 0 and K ≤ −ǫ such that
for all ℓ ∈ L⊥ and all x ∈ R|X| , the conditions (C1-C4) hold:
– C1:
d;
– C2:
– C3:
– C4:

the function η(ℓ, ·) : R|X| → R is a polynomial over X of order at most
if ℓ 6= ⊥ and x |= I(ℓ), then η(ℓ, x) ≥ 0;
if ℓ = ⊥, then η(ℓ, x) = K;
if ℓ 6= ⊥ and x |= I(ℓ) ∧ PP(ℓ), then preη (ℓ, x) ≤ η(ℓ, x) − ǫ .

Note that C2 and C3 together separate non-termination and termination by the
threshold 0, and C4 is the RSM difference condition which is intuitively related
to the ǫ difference in the RSM definition (cf. Definition 6). By generalizing our
previous proofs in [13] (from LRSM to pRSM), we establish the soundness of
pRSMs w.r.t both almost-sure and finite termination (proof in Appendix E).
Theorem 1. If there exists a d-pRSM η w.r.t (P, I) with constants ǫ, K (cf.
Definition 8), then P is a.s. terminating and ET(P ) ≤ UB(P ) := η(ℓ0 ,xǫ0 )−K .
Example 4. Consider the running example (cf. Example 1 and Example 2) and
the function η given in Example 3. Assuming that the initial valuation satisfies
1 ≤ x ∧ x ≤ 10, we assign the trivial invariant I such that I(1) = 0 ≤ x ∧ x ≤ 11,
I(j) = 1 ≤ x ∧ x ≤ 10 for 2 ≤ j ≤ 6 and I(7) = x < 1 ∨ x > 10. It is
straightforward to verify that η is a 2-pRSM with ǫ = 0.2 and K = −0.2 (cf.
Definition 8 for ǫ, K). Hence by Theorem 1, the program in Example 1 terminates
almost-surely under any scheduler and its expected termination time is at most
5 · (x0 − 1) · (10 − x0 ) + 51, given the initial value x0 .
Remark 2. The running example (cf. Example 1 and Example 2) does not admit
a linear (i.e. 1-) pRSM since ER (r) = 0 at label 3. This indicates that linear
pRSMs may not exist even over simple affine programs like Example 1. Thus,
this motivates the study of pRSMs even for simple affine programs.
Remark 3. The non-strict inequality symbol ‘≥’ in C2 can be replaced by its
strict counterpart ‘>’ since η + c (c > 0) remains to be a pRSM if η is a pRSM
and K (in C3) is sufficiently small. (By definition, preη+c = preη + c.) And the
non-strict inequality symbol ‘≤’ in C4 can be replaced by ‘<’ since a pRSM η
11

and a constant K (for C3) can be scaled by a constant factor (e.g. 1.1) so that
strict inequalities are ensured. Moreover, one can also assume that K = −1 and
ǫ = 1 in Definition 8. This is because one can first scale a pRSM with constants
ǫ, K by a positive scalar to ensure that ǫ = 1, and then safely set K = −1 due
to C2.
Theorem 1 answers the questions of almost-sure and finite termination in a
unified fashion. Generalizing our approach in [13], we show that by restricting a
pRSM to have bounded difference, we also obtain concentration results.
Definition 9 (Difference-Bounded pRSM). A d-pRSM η is differencebounded w.r.t a non-empty interval [a, b] ⊆ R if the following conditions hold:
– for all ℓ ∈ Ld ∪ Lp and (ℓ, α, ℓ′ ) ∈7→, and for all x ∈ JI(ℓ)K, it holds that
a ≤ η(ℓ′ , x) − η(ℓ, x) ≤ b;
– for all ℓ ∈ Lc and (ℓ, φ, ℓ′ ) ∈7→, and for all x ∈ JI(ℓ) ∧ φK, it holds that
a ≤ η(ℓ′ , x) − η(ℓ, x) ≤ b;
– for all ℓ ∈ La and (ℓ, f, ℓ′ ) ∈7→, for all x ∈ JI(ℓ)K and for all r ∈ {r′ | ∀r ∈
R. r′ [r] ∈ Suppr }, it holds that a ≤ η(ℓ′ , f (x, r)) − η(ℓ, x) ≤ b.
Note that if a d-pRSM η with constants ǫ, K (cf. Definition 8) is differencebounded w.r.t [a, b], then from definition a ≤ −ǫ; one can further assume that
−ǫ ≤ b since otherwise one can reset ǫ := −b. By definition, the stochastic
process Xn := η(θn , xn ) defined through a difference-bounded pRSM w.r.t [a, b]
satisfies that a ≤ Xn+1 − Xn ≤ b; then using Hoeffding’s Inequality [27,13], we
establish a concentration bound.
Theorem 2. Let η be a difference-bounded d-pRSM w.r.t [a, b] with constants
ǫ and K. For all n ∈ N, if ǫ(n − 1) > η(ℓ0 , x0 ), then P(TP > n) ≤
e

−

2(ǫ(n−1)−η(ℓ0 ,x0 ))2
(n−1)(b−a)2

.

From Theorem 2, a difference-bounded d-pRSM η implies a concentration bound
of η(ℓ0ǫ,x0 ) + 2 (detailed proof of the theorem is in Appendix F).
Example 5. Consider again our running example in Example 1 with invariant
given in Example 4. Let η be the function illustrated in Table 1. One can verify
that the interval [−10.2, 8.6] satisfies the conditions specified in Definition 9 for
η, as the following hold:
–
–
–
–
–
–

for
for
for
for
for
for

all
all
all
all
all
all

x ∈ [1, 10], η(2, x) − η(1, x) = −0.2;
x ∈ [0, 1) ∪ (10, 11], −10.2 ≤ η(7, x) − η(1, x) ≤ −0.2;
x ∈ [1, 10] and i ∈ {3, 4}, η(i, x) − η(2, x) = −0.2;
x ∈ [1, 10] and i ∈ {5, 6}, −9.4 ≤ η(i, x) − η(4, x) ≤ 8.6;
x ∈ [1, 10], η(1, x − 1) − η(5, x) = −0.2;
x ∈ [1, 10], η(1, x + 1) − η(6, x) = −0.2;
12

– for all x ∈ [1, 10] and r ∈ {−1, 1},

−9.6 ≤ η(1, x + r) − η(3, x) = −2rx − r2 + 11r + 0.4 ≤ 8.4 .

Then by Theorem 2, assuming that the program have initial value x0 = 5, one
can deduce that
P (TP > 50000) ≤ e−

2·(0.2·49999−30)2
49999·18.82

≈ 1.3016 · 10−5 .

We end this section with a result stating that whether a (difference-bounded)
d-pRSM exists can be decided (proof in Appendix G). However, the complexity
obtained for Theorem 3 is high since it involves quantifier elimination. In the
next section, we will present efficient algorithms for synthesizing pRSMs.
Theorem 3. For any fixed natural number d ∈ N, the problem whether a
(difference-bounded) d-pRSM w.r.t an input pair (P, I) exists is decidable.

5

The Synthesis Algorithm

In this section, we present an efficient algorithmic approach for solving almostsure/finite termination and concentration questions through synthesis of pRSMs.
Instead of quantifier elimination (of Theorem 3) we use Positivstellensatz (German for “positive-locus-theorem” which is related to polynomials over semialgebraic sets), and the approach of this section is sound but not complete (in
contrast to the computationally expensive but complete method of Theorem 3).
Note that by Theorem 1, the existence of a pRSM implies both almost-sure and
finite termination of a probabilistic program.
The General Framework. To synthesize a pRSM, the algorithm first sets up a
polynomial template with unknown coefficients. Next, the algorithm finds values
for the unknown coefficients, ǫ, K (cf. Definition 8) and [a, b] (cf. Definition 9) so
that C2-C4 in Definition 8 and concentration conditions in Definition 9 are satisfied. Note that from Definition 7, each preη (ℓ, ·) is a polynomial over X whose
coefficients are linear combinations of unknown coefficients from the polynomial
template. Instead of using quantifier elimination (cf. e.g. [52] or Theorem 3),
we utilize Positivstellensatz’s [45]. We observe that each universally-quantified
formula described in C2, C4 and Definition 9 can be decomposed (through disjunctive normal form of propositional polynomial predicate or transformation of
max in Definition 7 into two conjunctive clauses) into a conjunction of formulae
of the following pattern (†)
∀x ∈ R|X| . [(g1 (x) ≥ 0 ∧ · · · ∧ gm (x) ≥ 0) → g(x) > 0]

(†)

where each gi is a polynomial with constant coefficients and g is one with
unknown coefficients from the polynomial template. In the pattern, we overapproximate any possible ‘gj (x) > 0’ by ‘gj (x) ≥ 0’. By Remark 3, the difference
between ‘g(x) > 0’ and ‘g(x) ≥ 0’ does not matter.
13

Example 6. Consider again the program in Example 1 with CFG in Example 2.
Consider the invariant specified in Example 4. The instances of the pattern
for termination of this program are listed as follows, where each instance is
represented by a pair (Γ, g) where Γ and g corresponds to {g1 , . . . , gm } and
resp. g described in (†).
– (C4, label 1) ({x − 1, 10 − x, x, 11 − x}, η(1, x) − η(2, x) − ǫ);
– (C4, label 2) ({x−1, 10−x}, η(2, x)−η(3, x)−ǫ) and ({x−1, 10−x}, η(2, x)−
η(4, x) − ǫ);
– (C4, label 3) ({x − 1, 10 − x}, η(3, x) − ER ((y, r) 7→ η(1, y + r), x) − ǫ);
– (C4, label 4) ({x − 1, 10 − x}, η(4, x) − 0.51η(5, x) − 0.49η(6, x) − ǫ);
– (C4, label 5) ({x − 1, 10 − x}, η(5, x) − η(1, x − 1) − ǫ);
– (C4, label 6) ({x − 1, 10 − x}, η(6, x) − η(1, x + 1) − ǫ);
– (C2) ({x, 11 − x}, η(1, x)) and ({x − 1, 10 − x}, η(j, x)) for 2 ≤ j ≤ 6.
In the next part, we show that such pattern can be solved by Positivstellensatz’s.

5.1

Positivstellensatz’s

We fix a linearly-ordered finite set X of variables and a finite set Γ =
|X|
{g1 , . . . , gm } ⊆ R[X] of polynomials. Let JΓ K be the
Vmset of all vectors x ∈ R
satisfying the propositional polynomial predicate i=1 gi ≥ 0. We first define
pre-orderings and sums of squares as follows.
Definition 10 (Sums of Squares). Define Θ to be the set of sums-of-squares,
i.e,
)
( k
X
2
hi | k ∈ N and h1 , . . . , hk ∈ R[X] .
Θ :=
i=1

Definition 11 (Preordering). The preordering generated by Γ is defined by:


m

 X
Y
giwi | ∀w. hw ∈ Θ .
hw ·
PO(Γ ) :=


m
w∈{0,1}

i=1

Remark 4. It is well-known that a real-coefficient polynomial g of degree 2d is a
sum of squares iff there exists a k-dimensional positive semi-definite real square
matrix Q such that g = y T Qy, where k is the number of monomials of degree no
greater than d and y is the column vector of all such monomials (cf. [28, Corollary
7.2.9]). This implies that the problem whether a given polynomial (with real
coefficients) is a sum of squares can be solved by semi-definite programming [25].
Now we present the first Positivstellensatz, called Schmüdgen’s Positivstellensatz.
14

Theorem 4 (Schmüdgen’s Positivstellensatz [46]). Let g ∈ R[X]. If the
set JΓ K is compact and g(x) > 0 for all x ∈ JΓ K, then g ∈ PO(Γ ).
From Schmüdgen’s Positivstellensatz, any polynomial g which is positive on JΓ K
can be represented by
X
hw · g w ,
(‡)
g=
w∈{0,1}m

Qm

where gw := i=1 giwi and hw ∈ Θ for each w ∈ {0, 1}m. To apply Schmüdgen’s
Positivstellensatz, the degrees of those hw ’s are restricted to be no greater than
a fixed natural number. Then from Remark 4 and by equating the coefficients
of the same monomials between the two polynomials, Eq. (‡) results in a system
of linear equalities that involves variables for synthesis of a pRSM and variables
(grouped as 2m square matrices) under semi-definite constraints.
Example 7. Assume that X = {x} and Γ = {1 − x, 1 + x}. Choose the maximal
degree for sums of squares to be 2. Then from Remark 4, the form of Eq. (‡)
can be written as:
  

4 
X
 ai,1,1 ai,1,2
1
1x ·
·
· ui
g=
x
ai,2,1 ai,2,2
i=1

where u1 = 1, u2 = 1 − x, u3 = 1 + x, u4 = 1 − x2 and each matrix (ai,j,k )2×2
(1 ≤ i ≤ 4) is a matrix of variables subject to be positive semi-definite.

Theorem 4 can be further refined by a weaker version of Putinar’s Positivstellensatz.
Theorem 5 (Putinar’s Positivstellensatz [42]). Let g ∈ R[X]. If (i) there
exists some gi ∈ Γ such that the set {x ∈ R|X| | gi (x) ≥ 0} is compact and (ii)
g(x) > 0 for all x ∈ JΓ K, then
(§)

g = h0 +

m
X

hi · g i

i=1

for some sums of squares h0 , . . . , hm ∈ Θ.
Likewise, Eq. (§) results in a system of linear equalities that involves variables for
synthesis of a pRSM and matrices of variables under semi-definite constraints,
provided that an upper bound on the degrees of sums of squares is enforced.
Example 8. Assume that X = {x} and Γ = {1−x2, 0.5−x}. Choose the maximal
degree for sums of squares to be 2. Then the form of Eq. (§) can be written as:
g=

3 
X
i=1

  

 a
1
a
1 x · i,1,1 i,1,2 ·
· ui
x
ai,2,1 ai,2,2
15

where u1 = 1, u2 = 1 − x2 , u3 = 0.5 − x and each matrix (ai,j,k )2×2 (1 ≤ i ≤ 4)
is a matrix of variables subject to be positive semi-definite.
In the following, we introduce a Positivstellensatz entitled Handelman’s Theorem
when Γ consists of only linear (degree one) polynomials. For Handelman’s Theorem, we assume that Γ consists of only linear (degree 1) polynomials and JΓ K
is non-empty. (Note that whether a system of linear inequalities has a solution
is decidable in PTIME [47].)
Definition 12 (Monoid). The monoid of Γ is defined by:
)
( k
Y
hi | k ∈ N0 and h1 , . . . , hk ∈ Γ
.
Monoid(Γ ) :=
i=1

Theorem 6 (Handelman’s Theorem [26]). Let g ∈ R[X] be a polynomial
such that g(x) > 0 for all x ∈ JΓ K. If JΓ K is compact, then
(#)

g=

d
X

ai · u i

i=1

for some d ∈ N, real numbers a1 , . . . , ad ≥ 0 and u1 , . . . , ud ∈ Monoid(Γ ).
To apply Handelman’s theorem, we consider a natural number which serves as a
bound on the number of multiplicands allowed to form an element in Monoid(Γ );
then Eq. (#) results in a system of linear equalities involving a1 , . . . , ad . Unlike
previous Positivstellensatz’s, the form of Handelman’s theorem allows us to construct a system of linear equalities free from semi-definite constraints.
Example 9. Assume that X = {x} and Γ = {1 − x, 1 + x}. Fix the maximal
number of multiplicands in an element of Monoid(Γ ) to be 2. Then the form of
Eq. (#) can be rewritten as
6
X
ai · u i
g=
i=1

where u1 = 1, u2 = 1−x, u3 = 1+x, u4 = 1−x2 , u5 = 1−2x+x2, u6 = 1+2x+x2
and each ai (1 ≤ i ≤ 6) is subject to be a non-negative real number.
5.2

The Algorithm for pRSM Synthesis

Based on the Positivstellensatz’s introduced in the previous part, we present our
algorithm for synthesis of pRSMs. Below, we fix an input probabilistic program
P , an input polynomial invariant I and an input initial configuration (ℓ0 , x0 ) for
P . Let G = (L, ⊥, (X, R), 7→) be the associated CFG of P .
Description of the Algorithm PRSMSynth. We present a succinct description
of the key ideas. The description of the key steps of the algorithm is as follows.
16

1. Template η for a pRSM. The algorithm fix a natural number d as the maximal degree for a pRSM, construct Md as the set of all monomials over X of
degree no greater
Pthan d, and set up a template d-pRSM η such that η(ℓ, ·) is
the polynomial h∈Md ah,ℓ · h where each ah,ℓ is a (distinct) scalar variable
(cf. C1).
2. Bound for Sums of Squares and Monoid Multiplicands. The algorithm fix
a natural number k as the maximal degree for a sum of squares (cf.
Schmüdgen’s and Putinar’s Positivstellensatz) or as the maximal number
of multiplicands in a monoid element (cf. Handelman’s Theorem).
3. RSM-Difference and Terminating-Negativity. From Remark 3, the algorithm
fixes ǫ to be 1 (cf. condition C3) and K to be −1 (cf. condition C4).
4. Computation of pre-expectation preη . With ǫ, K fixed to be resp. 1, −1 in
the previous step, the algorithm computes preη by Definition 7, whose all
involved coefficients are linear combinations from ah,ℓ ’s.
5. Pattern Extraction. The algorithm extracts instances conforming to pattern (†) from C2, C4 and formulae presented in Definition 9, and translates them into systems of linear equalities over variables among ah,ℓ ’s, ǫ,
K, and extra matrices of variables assumed to be positive semi-definite (cf.
Schmüdgen’s and Putinar’s Positivstellensatz) or scalar variables assumed
to be non-negative (cf. Handelman’s Theorem) through Eq. (‡), Eq. (§) and
Eq. (#).
6. Solution via Semidefinite or Linear Programming. The algorithm calls semidefinite programming (for Schmüdgen’s and Putinar’s Positivstellensatz) or
linear programming (for Handelman’s Theorem) in order to check the feasibility or to optimize UB(P ) (cf. Theorem 1 for upper bound of ET(P )) over
all variables among ah,ℓ ’s and extra matrix/scalar variables from Eq. (‡),
Eq. (§) and Eq. (#). Note that the feasibility implies the existence of a
(difference-bounded) d-pRSM; the existence of a d-pRSM in turn implies finite termination, and the existence of a difference-bounded d-pRSM in turn
implies a concentration bound through Theorem 2.
The soundness of our algorithm is as follows, whose proof is in Appendix H.
Theorem 7 (Soundness). Any function η synthesized through the algorithm
PRSMSynth is a valid pRSM.
Remark 5 (Efficiency). It is well-known that for semi-definite programs with
a positive real number R to bound the Frobenius norm of any feasible solution, an approximate solution upto precision ǫ can be computed in polynomial
time in the size of the semi-definite program (with rational numbers encoded
in binary), log R and log ǫ−1 [25]. Thus, our sound approach presents an efficient method for analysis of many probabilistic programs. Moreover, when each
propositional polynomial predicate in the probabilistic program involves only linear polynomials, then the sound form of Handelman’s theorem can be applied,
resulting in feasibility checking of systems of linear inequalities rather than semidefinite constraints. By polynomial-time algorithms for solving systems of linear
17

inequalities [47], our approach is polynomial time (and thus efficient) over such
programs.
Remark 6 (Semi-Completeness). Consider probabilistic programs of the following form: while φ do if ⋆ then P1 else P2 od , where P1 , P2 are single assignments, JφK is compact, and invariants which assign to each label a propositional
polynomial predicate is in DNF form that involves no strict inequality (i.e. no
‘<’ or ‘>’). Upon such inputs, our approach is semi-complete in the sense that
by raising the upper bounds for the degree of a sum of squares and the number of
multiplicands in a monoid element, the algorithm PRSMSynth will eventually
find a pRSM if it exists. This is because Theorem 4 to 6 are “semi-complete”
when JΓ K is compact, as the terminal label can be separately handled by PP(·) so
that only compact Γ ’s for Positivstellensatz’s may be formed, and the difference
between strict and non-strict inequalities does not matter (cf. Remark 3).
Remark 7 (Comparision with our previous result [13]). Our approach using Handelman’s theorem is a strict generalization of the LRSM (linear ranking supermartingale) approach of [13] that uses Farkas’ lemma. For example, our approach
using Handelman’s Theorem applied to affine programs can handle Example 1,
where no LRSM exists (Remark 2).
Remark 8 (New techniques for nonprobabilistic programs). To the best of our
knowledge, Schmüdgen’s Positivstellensatz and Handelman’s Theorem have not
been used for nonprobabilistic programs, and thus our approach presents new
analysis methods even for nonprobabilistic programs (though our approach is
for the more general class of nondeterministic probabilistic programs).
Remark 9 (Key Insights). The key insights of this paper are (i) the need for
pRSMs (cf. Remark 2), (ii) the adaptation of conditional expectation with
pRSMs, (iii) the connection between synthesis of pRSMs and Positivstellensatz’s and (iv) the adoption of semidefinite and linear programming to synthesize
pRSMs.

6

Experimental Results

In this section, we present experimental results for our algorithm through the
semi-definite programming tool SOSTOOLS [3] (that uses SeDuMi [1]) and the
linear programming tool CPLEX [2]. Due to space constraints, the detailed description of the input probabilistic programs are in Appendix I.
Experimental examples and setup. We consider six classical examples of probabilistic programs that exhibit distinct types non-linear behaviours. Our examples are, namely, Logistic Map adopted in [15] (Example 10 in Appendix I)
which was previously handled by Lagrangian relaxation and semi-definite programming whereas our approach is polynomial time using linear programming,
18

Decay that models a sequence of points converging stochastically to the origin
(Example 11 in Appendix I), Random Walk that models a random walk within a
bounded region defined through non-linear curves (Example 12 in Appendix I),
Gambler’s Ruin which is our running example (Example 1), Gambler’s Ruin
Variant (Example 14 in Appendix I) which is a variant of (Example 13), and
Nested Loop (Example 15 in Appendix I) which is a nested loop with stochastic
increments. Except for Gambler’s Ruin Variant and Nested Loop, our approach
is semi-complete for all other examples (cf. Remark 6). In all the examples the
invariants are straightforward and was manually integrated with the input. Since
SOSTOOLS only produces numerical results, we modify C2 to “η(ℓ, x) ≥ 0” to
“η(ℓ, x) ≥ 1” for Putinar’s or Schmüdgen’s Positivstellensatz and check whether
the maximal numerical error of all equalities added to SOSTOOLS is sufficiently small over a bounded region. In our examples, the bounded region is
{(x, y) | x2 + y 2 ≤ 2} (cf. Example 12 and Example 11) and the maximal numerical error should not exceed 1. Note that 1 is also our fixed ǫ in C4, and by
Remark 3, the modification on C2 is not restrictive. Instead, one may also pursue Sylvester’s Criterion (cf. [28, Theorem 7.2.5]) to check membership of sums
of squares through checking whether a square matrix is positive semi-definite or
not. More elegant approaches for numerical problems is a subject of future work.

Experimental results. In Table 2, we present the experimental results, where
‘Method’ means that whether we use either Handelman’s Theorem, Putinar’s
Positivstellensatz or Schmüdgen’s Positivstellensatz to synthesize pRSMs, ‘SOSTOOLS/CPLEX’ means the running time for CPLEX/SOSTOOLS in seconds,
’error’ is the maximal numerical error of equality constraints added into SOSTOOLS (when instantiated with the solutions), and η(ℓ0 , ·) is the polynomial
for the initial label in the synthesized pRSM. The synthesized pRSMs (in the
last column) refer to the variables of the program. All numbers except errors
are rounded to 10−4 . For all the examples, our translation to the optimization
problems are linear. We report the running times of the optimization tools and
synthesized pRSMs. The experimental results were obtained on Intel Core i72600 machine with 3.4 GHz with 16GB RAM.

Example
Decay
Random Walk
Example
Gambler’s Ruin
Gambler’s Ruin V.
Logistic Map
Nested Loop

Method SOSTOOLS error
η(ℓ0 , ·)
Putinar
0.1248s ≤ 10−9 5282.3435x2 + 5282.3435y 2 + 1
Schmüdgen 0.7176s ≤ 10−7
−300x2 − 300y 2 + 601
Method
CPLEX
η(ℓ0 , ·)
Handelman ≤ 10−2 s
33x − 3x2
Handelman ≤ 10−2 s
−21 + 100x − 70y − 100x2 + 100xy
−2
Handelman ≤ 10 s
1000500.7496x
Handelman ≤ 2 · 10−2 s
48 + 160n + (m − x)(800n + 240)
Table 2. Experimental Results

19

For all the examples we consider except Logistic Map, their almost-sure termination cannot be answered by previous approaches. For the Logistic-Map example,
our reduction is to linear programming whereas existing approaches [15,48]
reduce to semidefinite programming.

7

Conclusion and Future Work

In this paper, we extended linear ranking supermartingale (LRSM) for probabilistic programs proposed in [11,13] to polynomial ranking supermartingales
(pRSM) for nondeterministic probabilistic programs. We developed the notion
of (difference bounded) pRSM and proved that it is sound for almost-sure and
finite termination, as well as for concentration bound (Theorem 1 and Theorem 2). Then we developed an efficient (sound but not complete) algorithm
for synthesizing pRSMs through Positivstellensatz’s (cf. Sect. 5.1), proved its
soundness (Theorem 7) and argued its semi-completeness (Remark 6) over an
important class of programs. Finally, our experiments demonstrate the effectiveness of our synthesis approach over various classical probabilistic of programs,
where LRSMs do not exist (cf. Example 1 and Remark 2). Directions of future
work are to explore (a) more elegant methods for numerical problems related to
semi-definite programming, and (b) other forms of RSMs for more general class
of probabilistic programs.

Acknowledgement We thank anonymous referees for valuable comments.
We also thank Hui Kong for his help on SOSTOOLS. The research was
partly supported by Austrian Science Fund (FWF) NFN Grant No S11407N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), ERC Advanced
Grant ( 267989: QUAREM), and Natural Science Foundation of China (NSFC)
under Grant No. 61532019.

References
1. SeDuMi 1.3. http://sedumi.ie.lehigh.edu/ (2008)
2. IBM ILOG CPLEX Optimizer Interactive Optimizer Community Edition 12.6.3.0. http://www-01.ibm.com/software/integration/optimization/cplexoptimizer/ (2010)
3. SOSTOOLS v3.00. http://www.cds.caltech.edu/sostools/ (2013)
4. Babic, D., Cook, B., Hu, A.J., Rakamaric, Z.: Proving termination of nonlinear
command sequences. Formal Asp. Comput. 25(3), 389–403 (2013)
5. Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)
6. Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer,
2nd edn. (2006)
7. Billingsley, P.: Probability and Measure. Wiley, 3rd edn. (1995)

20

8. Bournez, O., Garnier, F.: Proving positive almost-sure termination. In:
Giesl, J. (ed.) Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3467, pp. 323–337. Springer (2005),
http://dx.doi.org/10.1007/978-3-540-32033-3_24
9. Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International
Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings.
Lecture Notes in Computer Science, vol. 3576, pp. 491–504. Springer (2005)
10. Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In:
Cousot [17], pp. 113–129
11. Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th
International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 511–526. Springer
(2013)
12. Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic
programs through positivstellensatz’s. In: CAV (2016)
13. Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic analysis
of qualitative and quantitative termination problems for affine probabilistic programs. In: Bodı́k, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 327–342. ACM (2016),
http://doi.acm.org/10.1145/2837614.2837639
14. Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi,
W. (eds.) 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. Lecture Notes in Computer Science, vol. 2031, pp. 67–81.
Springer (2001)
15. Cousot, P.: Proving program invariance and termination by parametric abstraction,
Lagrangian relaxation and semidefinite programming. In: Cousot [17], pp. 1–24
16. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static
analysis of programs by construction or approximation of fixpoints. In: Graham,
R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM
Symposium on Principles of Programming Languages, Los Angeles, California,
USA, January 1977. pp. 238–252. ACM (1977)
17. Cousot, R. (ed.): Verification, Model Checking, and Abstract Interpretation, 6th
International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3385. Springer (2005)
18. Dubhashi, D., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press, New York, NY, USA, 1st edn.
(2009)
19. Durrett, R.: Probability: Theory and Examples (Second Edition). Duxbury Press
(1996)
20. Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs
using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13,
2012 Proceedings. Lecture Notes in Computer Science, vol. 7358, pp. 123–138.
Springer (2012)

21

21. Farkas, J.: A fourier-féle mechanikai elv alkalmazásai (Hungarian). Mathematikaiés
Természettudományi Értesitö 12, 457–472 (1894)
22. Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: Soundness, completeness,
and compositionality. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the
42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 489–501. ACM
(2015)
23. Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer
Science 19, 19–33 (1967)
24. Foster, F.G.: On the stochastic matrices associated with certain queuing processes.
The Annals of Mathematical Statistics 24(3), pp. 355–360 (1953)
25. Grötschel, M., Lovasz, L., Schrijver, A.: Geometric Algorithms and Combinatorial
Optimization. Springer-Verlag Berlin Heidelberg (1993)
26. Handelman, D.: Representing polynomials by positive linear functions on compact
convex polyhedra. Pacific J. Math. 132, 35–62 (1988)
27. Hoeffding, W.: Probability inequalities for sums of bounded random variables.
Journal of the American Statistical Association 58(301), 13–30 (1963)
28. Horn, R.A., Johnson, C.R.: Matrix Analysis. Cambridge University Press, 2nd edn.
(2013)
29. Howard, H.: Dynamic Programming and Markov Processes. MIT Press (1960)
30. Hungerford, T.W.: Algebra. Springer (1974)
31. Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially
observable stochastic domains. Artificial intelligence 101(1), 99–134 (1998)
32. Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: A survey.
Journal of Artificial Intelligence Research 4, 237–285 (1996)
33. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. D. Van Nostrand
Company (1966)
34. Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics 25(6), 1370–1381 (2009)
35. Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided
Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July
14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 585–
591. Springer (2011)
36. McIver, A., Morgan, C.: Developing and reasoning about probabilistic programs
in pGCL. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software
Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised
Lectures. Lecture Notes in Computer Science, vol. 3167, pp. 123–155. Springer
(2004), http://dx.doi.org/10.1007/11889229_4
37. McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005)
38. Monniaux, D.: An abstract analysis of the probabilistic termination of
programs. In: Cousot, P. (ed.) Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2126, pp. 111–126. Springer (2001),
http://dx.doi.org/10.1007/3-540-47764-0_7
39. Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press,
New York, NY, USA (1995)
40. Paz, A.: Introduction to probabilistic automata (Computer science and applied
mathematics). Academic Press (1971)

22

41. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and
Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2937, pp.
239–251. Springer (2004)
42. Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ.
Math. J. 42, 969–984 (1993)
43. Rabin, M.: Probabilistic automata. Information and Control 6, 230–245 (1963)
44. Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic
programs: inferring whole program properties from finitely many paths. In: PLDI.
pp. 447–458 (2013)
45. Scheiderer, C.: Positivity and sums of squares: A guide to recent results. The IMA
Volumes in Mathematics and its Applications 149, 271–324 (2008)
46. Schmüdgen, K.: The K-moment problem for compact semi-algebraic sets. Math.
Ann. 289, 203–206 (1991)
47. Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience series
in discrete mathematics and optimization, Wiley (1999)
48. Shen, L., Wu, M., Yang, Z., Zeng, Z.: Generating exact nonlinear ranking functions
by symbolic-numeric hybrid method. J. Systems Science & Complexity 26(2), 291–
301 (2013)
49. Sohn, K., Gelder, A.V.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Proceedings of the Tenth ACM SIGACTSIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31,
1991, Denver, Colorado, USA. pp. 216–226. ACM Press (1991)
50. Tarski, A.: A decision method for elementary algebra and geometry. In: Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 24–84. Texts and
Monographs in Symbolic Computation, Springer Vienna (1951)
51. Williams, D.: Probability with Martingales. Cambridge University Press (1991)
52. Yang, L., Zhou, C., Zhan, N., Xia, B.: Recent advances in program verification
through computer algebra. Frontiers of Computer Science in China 4(1), 1–16
(2010), http://dx.doi.org/10.1007/s11704-009-0074-7

23

A

Propositional Polynomial Predicates

Formally, the set of propositional polynomial predicates over X is defined as the
smallest set satisfying the following conditions:
1.
2.
3.
4.

each polynomial constraint over X is a propositional polynomial predicate;
both true and false are propositional polynomial predicates;
if φ is a propositional polynomial predicate, then so is ¬φ;
if φ, ψ are propositional polynomial predicates, then so are φ ∧ ψ and φ ∨ ψ.

The satisfaction relation |= between real vectors x and propositional polynomial
predicates φ is defined by:
–
–
–
–
–

B

x |= true and x 6|= false for all vectors x;
x |= g1 ⋊
⋉ g2 iff g1 (x) ⋊
⋉ g2 (x) ;
x |= ¬φ iff x 6|= φ ;
x |= φ ∧ ψ iff x |= φ and x |= ψ ;
x |= φ ∨ ψ iff x |= φ or x |= ψ .

Probabilistic Programs: Detailed Syntax

Let X and R be the disjoint countable collections of program and sampling
variables, respectively. We assume that each sampling variable r be associated
with a one-dimensional cumulative distribution function Υr and a non-empty
bounded interval suppr in R such that Υr (sup suppr ) = 1 and Υr (inf suppr ) = 0,
and the sampled values for r fall in suppr with probability 1 (this is the rigorous
condition of the boundedness of the sampling variables).

The Syntax. The syntax of probabilistic programs is given by the grammar in
Figure 3. The expressions hpvar i, hrvar i and hpvarlist i range over X , R and finite sequences of program variables, respectively. The expressions hexpri, hrexpr i
and hrexprlisti may be evaluated to any polynomial with variables in X , any
polynomial with variables in X ∪ R and any finite list of polynomials with variables in X ∪ R, respectively. The assignment statement hpvarlisti ’:=’ hrexprlisti
specifies simultaneous update of program variables in hpvarlisti by polynomial
hrexprlisti in sequel; we thus assume that each instance of hpvarlisti will contain
distinct program variables and the length of each instance of hpvarlisti will always be equal to the corresponding instance of hrexprlisti. From the assignment
statement one observes that sampling variables can only be used in the RHS of
an assignment. Sequential composition, if-branch and while-loop are indicated
by semicolon, the keyword if and the keyword while, respectively. Moreover,
hbexpri may be evaluated to any propositional polynomial predicate.
24

The “if-then-else” Statement. The guard hndbexpri of each if-then-else statement
is either a keyword ⋆ representing demonic resolution of non-determinism, or a
keyword prob(p) (p ∈ (0, 1) being a number given in decimal representation)
representing the probabilistic choice that the if-branch is executed with probability p and the then-branch with probability 1−p, or a propositional polynomial
predicate, in which case the statement represents a standard deterministic conditional branching.

hstmti ::= hpvarlisti ’:=’ hrexprlisti
| ’if ’ hndbexpr i ’then’ hstmti ’else’ hstmti ’fi’
| ’while’ hbexpr i ’do’ hstmti ’od’
| hstmti ’;’ hstmti | ’skip’
hexpr i ::= hconstanti | hpvar i
| hexpr i ’∗’ hexpr i
| hexpr i ’+’ hexpr i | hexpr i ’−’ hexpr i
hrexpr i ::= hconstant i | hpvar i | hrvar i
| hrexpr i ’∗’ hrexpr i
| hrexpr i ’+’ hrexpr i | hrexpr i ’−’ hrexpr i
hpvarlisti ::= hpvar i ’,’ hpvarlisti | hpvar i
hrexprlisti ::= hrexpr i ’,’ hrexprlisti | hrexpr i
hliterali ::= hexpr i ’≤’ hexpr i | hexpr i ’≥’ hexpr i
hpolyexpr i ::= hliterali | hliterali ’and’ hpolyexpr i
hbexpr i ::= hpolyexpr i | hpolyexpr i ’or’ hbexpr i
hndbexpr i ::= ’⋆’ | ’prob(p)’ | hbexpr i
Fig. 3. Syntax of Probabilistic Programs

C

Transformation from Programs to CFGs

Below we fix a set X of program variables and a set R of sampling variables.
We also fix two linear orders on X and R under which X = {x1 , . . . , x|X| } and
R = {r1 , . . . , r|X| }.
25

We recall that a valuation of program variables is a vector x ∈ R|X| interpreted
in the way that the actual value held by a program variable xi (1 ≤ i ≤ |X|) is
x[i]; similarly, a valuation of sampling variables is a vector r ∈ R|R| such that
the sampled value held by ri is r[i]. Every update function f in a CFG can then
be viewed as a tuple (f1 , . . . , f|X| ), where each fi is of type R|X| × R|R| → R. We
use the following succinct notation for special update functions: by id we denote
the 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 any k functions g1 , . . . , gk : R|X| × R|R| → R
and any sequence n1 , . . . , nk of k distinct numbers in {1, . . . , |X|}, we denote by
[{xnj }k1 /{gj }k1 ] the update function f such that fnj (x, r) = gj (x, r) for 1 ≤ j ≤ k
and fi (x, r) = x[i] whenever i 6∈ {n1 , . . . , nk }.
From Probabilistic Programs to CFGs. To every probabilistic program P with
programs variables from X and sampling variables from R, we construct a CFG
GP inductively on the structure of P . The CFG GP has X and resp. R as its
set of program and resp. sampling variables. For each program P , the CFG GP
out
involves two distinguished labels, namely ℓin
P and ℓP , that intuitively represent
the label assigned to the first statement to be executed in P and the terminal
label of P , respectively. The inductive construction is as follows.
1. Asssignments and Skips. For P = xn1 , . . . , xnk := E1 , . . . , Ek or resp. P =
skip, the CFG GP consists of a new assignment labels ℓin
P and a new terminal
out
out
k
k
in
],
ℓ
)
or resp. (ℓin
/{E
}
}
label ℓout
,
and
a
transition
(ℓ
,
[{x
j 1
nj 1
P
P , id, ℓP ),
P
P
where we treat each Ej as a function through direct evaluation of variables.
2. Sequential Statements. For P = Q1 ; Q2 , we take the disjoint union of the
in
in
in
CFGs GQ1 , GQ2 , while redefining ℓout
Q1 to be ℓQ2 and putting ℓP = ℓQ1 and
out
ℓout
P = ℓQ2 .
3. While Statements. For P = while φ do Q od, we add a new terminal lain
out
out
bel ℓout
P , change ℓQ to a branching label, add transitions (ℓQ , φ, ℓQ ) and
out
in
out
out
(ℓQ , ¬φ, ℓP ), and define ℓP := ℓQ .
4. If Statements. For P = if B then Q1 else Q2 fi, we consider different cases
on B: if B is some prob(p), then we add a new probabilistic label ℓin
P toin
in
in
gether with two transitions (ℓin
,
p,
ℓ
)
and
(ℓ
,
1
−
p,
ℓ
);
if
B
is
some
P
Q1
P
Q2
propositional polynomial predicate φ then we add a new branching label ℓin
P
in
in
in
′
together with transitions (ℓin
P , φ, ℓQ1 ) and (ℓP , ¬φ, ℓQ2 ); otherwise, B = ‘⋆
in
in
and we add a new demonic label ℓin
P together with transitions (ℓP , ⋆, ℓQ1 )
in
in
and (ℓP , ⋆, ℓQ2 ). In any of the cases above, we also add a new terminal label
out
out
out
ℓout
P and identify both ℓQ1 and ℓQ2 with ℓP .

D

The Semantics: Detailed Description

The behaviour of a probabilistic program P accompanied with its CFG G =
(L, ⊥, (X, R), 7→) under a scheduler σ is described as follows. The program starts
in the initial configuration (ℓ0 , x0 ). Then in each step i (i ∈ N0 ), given the current
26

configuration (ℓi , xi ), the next configuration (ℓi+1 , xi+1 ) is determined by the
following procedure:
1. a valuation r i of the sampling variables is sampled according to the joint
distribution of the cumulative distributions {Υr }r∈R and independent of
all previously-traversed configurations (including (ℓi , xi )), all previous samplings on R and previous executions of probabilistic branches;
2. if ℓi ∈ Ld and c0 , . . . , ci is the finite path traversed so far (i.e., c0 = (ℓ0 , x0 )
and ci = (ℓi , xi )) with σ(c0 , . . . , ci ) = (ℓi , ⋆, ℓ′ ), then (ℓi+1 , xi+1 ) is set to be
(ℓ′ , xi );
3. if ℓi ∈ Lp and (ℓi , p, ℓ1 ), (ℓi , 1−p, ℓ2) are namely the two transitions in 7→ with
source label ℓi , then with a Bernoulli experiment independent of all previous
samplings, probabilistic branches and traversed configurations, (ℓi+1 , xi+1 )
is set to be (i) (ℓ1 , xi ) with probability p and (ii) (ℓ2 , xi ) with probability
1 − p;
4. if ℓi ∈ Lc and (ℓi , φ, ℓ1 ), (ℓi , ¬φ, ℓ2 ) are namely the two transitions in 7→ with
source label ℓi , then (ℓi+1 , xi+1 ) is set to be (i) (ℓ1 , xi ) when xi |= φ and
(ii) (ℓ2 , xi ) when xi |= ¬φ;
5. if ℓi ∈ La and (ℓi , f, ℓ′ ) is the only transition in 7→ with source location ℓi ,
then (ℓi+1 , xi+1 ) is set to be (ℓ′ , f (xi , ri ));
6. if ℓi = ⊥ then (ℓi+1 , xi+1 ) is set to be (ℓi , xi ).

E

Proof of Lemma 1 and Theorem 1

Lemma 1. Let η : L⊥ × R|X| → R be a function such that each η(ℓ, ·) (for
all ℓ ∈ L⊥ ) is a polynomial function over X, and σ be any scheduler. Let the
stochastic process {Xn }n∈N0 be defined by: Xn := η(θn , xn ). Then for all n ∈ N0 ,
we have Eσ (Xn+1 | Hn ) ≤ preη (θn , xn ).
Proof. For all n ∈ N0 , from the syntax and semantics of probabilistic program
we have
Xn+1 = 1θn =⊥ · Xn + Yp + Yd + Yc + Ya
where the terms are described below.


X
X
1θn =ℓ ·
(1Zℓ =i · η(ℓZℓ =i , xn ))
Yp :=
ℓ∈Lp

i∈{0,1}

where each random variable Zℓ is the Bernoulli random variable for the decision
of the probabilistic branch and ℓZℓ =0 , ℓZℓ =1 are the corresponding target labels
from ℓ in 7→. (Note that all Zℓ ’s are independent of Hn .) In other words, Yp
describes the semantics of statements with probabilistic labels.
X
[1θn =ℓ · η(ℓ′ , fℓ (xn , r n ))]
Ya :=
ℓ∈La

27

where (ℓ, fℓ , ℓ′ ) is the only transition in 7→ with source label ℓ, describing the
semantics of statements with assignment labels.
X
X 

Yc :=
1θn =ℓ∧xn |=φ · η(ℓ′′ , xn )
ℓ∈Lc (ℓ,φ,ℓ′′ )∈7→

which describes the semantics of statements with branching labels.
 h 

i
X
1θn =ℓ · η tgt σ {(θk , xk )}0≤k≤n , xn
Yd :=
ℓ∈Ld

h 
i
where tgt σ {(θk , xk )}0≤k≤n
is the target label of the transition


σ {(θk , xk )}0≤k≤n , describing the semantics of demonic labels. Then from
properties of conditional expectation [51, Page 88], one obtains:
Eσ (Xn+1 | Hn ) = 1θn =⊥ · Xn + Yp′ + Ya′ + Yc + Yd

(see below for details). This can be seen as follows. From the fact that 1θn =⊥ ·Xn ,
Yd , Yc are measurable in Hn , we have Eσ (1θn =⊥ · Xn | Hn ) = 1θn =⊥ · Xn and
similarly for Yd , Yc . For Yp and Ya we need their conditional expectation as Yp′
and Ya′ defined below:


X
X
1θn =ℓ ·
(Pσ (Zℓ = i) · η(ℓZℓ =i , xn ))
Yp′ :=
ℓ∈Lp

i∈{0,1}

and

Ya′ :=

X

[1θn =ℓ · ER (gℓ , xn )]

ℓ∈La

where gℓ equals the function (x, r) 7→ η(ℓ′ , fℓ (x, r)). Note that the fact that
ER (gℓ , xn ) is well-defined is because we consider polynomial functions (i.e.,
pRSMs).
Note that the case for Ya′ is derived from the fact that each η(ℓ′ , ·) is a polynomial
over X and r n is independent of Hn . Now by definition,
1θn 6∈Ld · preη (θn , xn ) = 1θn =⊥ · Xn + Yp′ + Ya′ + Yc
and
Yd ≤ 1θn ∈Ld · preη (θn , xn ) .
⊓
⊔

Then the result follows.

Remark 10. In the proof of the above result, which generalizes the existing proof
from LRSM to pRSM, the crucial property of pRSM we use is for assignments
(locations in La ) where we used the well-definedness of ER (gℓ , xn ) due to polynomials. For more general RSMs if the well-definedness of ER (gℓ , xn ) can be
ensured then our proof ensures that the above result holds as well.
28

To prove Theorem 1, one also needs an important property which states that an
RSM falls below zero almost surely.
Proposition 1. [22,13] Let {Xn }n∈N0 be an RSM w.r.t a filtration {Fn }n∈N0
and constants K, ǫ (cf. Definition 6). Let Z be the random variable defined by
Z := min{n ∈ N0 | Xn < 0} with min ∅ := ∞, denoting the first time n that the
RSM drops below 0. Then P(Z < ∞) = 1 and E(Z) ≤ E(X0ǫ)−K .
Now the proof for Theorem 1 is as follows.
Theorem 1. If there exists a d-pRSM η w.r.t (P, I) with constants ǫ, K (cf.
Definition 8), then P is a.s. terminating and ET(P ) ≤ UB(P ) := η(ℓ0 ,xǫ0 )−K .
Proof. Let η be a d-pRSM and {Xn }n∈N0 be the stochastic process defined in
Lemma 1. By Lemma 1, C4 and the fact that K ≤ −ǫ, {Xn }n∈N0 is a rankingsupermartingale (w.r.t {Hn }n∈N ). Then by C2, C3 and Proposition 1,
ET(P ) = sup Eσ (TP ) ≤
σ

η(ℓ0 , x0 ) − K
.
ǫ
⊓
⊔

F

Proof of Theorem 2

To prove Theorem 2, we need the following concentration inequality.
Theorem 8 (Hoeffding’s Inequality [27,13]). Let {Xn }n∈N be a supermartingale w.r.t 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
for all n ∈ N and λ > 0.

− Pn

2λ2

k=2

(bk −ak )2

Now we fix a difference-bounded d-pRSM η w.r.t [a, b]. Recall that Xn :=
η(θn , xn ). Define the stochastic process {Yn }n∈N by:
Yn = Xn + ǫ · (min{TP , n} − 1) .
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.
29

Proof. Consider the following random variable:
Un = min{TP , n + 1} − min{TP , n} ,
and observe that this is equal to 1TP >n . From the properties of conditional
expectation [51, Page 88] and the facts that (i) the event TP > n is measurable
in Fn (which implies that E(1TP >n | Fn ) = 1TP >n ); and (ii) Xn ≥ 0 iff TP > n
(cf. conditions C2 and C3), we have
E(Yn+1 | Fn ) − Yn = E(Xn+1 | Fn ) − Xn + ǫ · E(Un | Fn )
= E(Xn+1 | Fn ) − Xn + ǫ · E(1TP >n | Fn )
= E(Xn+1 | Fn ) − Xn + ǫ · 1TP >n
≤ −ǫ · 1Xn ≥0 + ǫ · 1TP >n
=0 .
Note that the inequality above is due to the fact that Xn is a ranking supermartingale. Moreover, since TP ≤ n implies θn = ℓout
and Xn+1 = Xn we have
P
that (Xn+1 − Xn ) = 1TP >n · (Xn+1 − Xn ). Hence we have
Yn+1 − Yn = Xn+1 − Xn + ǫ · Un
= (Xn+1 − Xn ) + ǫ · 1TP >n
= 1TP >n · (Xn+1 − Xn + ǫ) .
Hence Yn+1 − Yn ∈ [a + ǫ, b + ǫ].

⊓
⊔

Proof (of Theorem 2). Let W0 := Y1 = η(ℓ0 , x0 ). Fix any demonic strategy σ. By
−

2λ2

Hoeffing’s Inequality, for all λ > 0, we have P(Yn −W0 ≥ λ) ≤ e (n−1)(b−a)2 . Note
that TP > n iff Xn ≥ 0 by conditions C2 and C3 of pRSM. Let α = ǫ(n−1)−W0
and α
b = ǫ(min{n, TP } − 1) − W0 . Note that with the conjunct TP > n we have
that α and α
b coincide. Thus, for P(TP > n) = P(Xn ≥ 0 ∧ TP > n) we have
P(Xn ≥ 0 ∧ TP > n) = P((Xn + α ≥ α) ∧ (TP > n))
= P((Xn + α
b ≥ α) ∧ (TP > n))
≤ P((Xn + α
b ≥ α))
= P(Yn − Y1 ≥ ǫ(n − 1) − W0 )
≤e

−

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

for all n > Wǫ0 + 1. The first equality is obtained by simply adding α on both
sides, and the second equality uses that because of the conjunct TP > n we have
min{n, TP } = n which ensures α = α
b. The first inequality is obtained by simply
dropping the conjunct TP > n. The following equality is by definition, and the
final inequality is an application of Hoeffding’s Inequality.
⊓
⊔
Remark 11. The above result holds for general difference-bounded RSMs and
does not rely on the fact that it is a pRSM.
30

G

Proof for Theorem 3

Theorem 3. The problem whether a (difference-bounded) d-pRSM w.r.t (P, I)
exists is decidable.
Proof. Let M be the set ofPall monomials of degree no greater than d. Let a
template for a d-pRSM be h∈M ah · h, where ah are scalar variables to be resolved. Then it is straightforward that conditions C1-C4 can be directly encoded
as formulae in the first-order theory of reals which is first existentially quantified over the variables ah , K, ǫ and then universally quantified over the vector
variable x. The conditions for difference-bounded pRSMs can also be encoded
as formulae which are firstly existentially quantified over the scalar variables
a, b and then universally quantified over vector variable x. Thus, the existence
a (difference-bounded) d-pRSM is reduced to the validity of a formula in the
first-order theory of reals, which is decidable [50,6].
⊓
⊔

H

Proof of Theorem 7

Theorem 7. Any function η synthesized through the algorithm PRSMSynth
is a valid pRSM.
Proof. To prove the soundness we observe that Steps 1-3 of the algorithm are
basically instantiation of the template and obtaining the coefficients. Step 4 is the
pre-expectation computation based on the definition. The crucial step is Step 5
and Step 6. The soundness of Step 5 and Step 6 follows from the soundness
of Positivstellensatz’s (cf. Theorem 4 to 6) regardless of the compactness of
JΓ K: either Eq. (‡), Eq. (§) or Eq. (#) guarantees that formula (†) holds with
‘g(x) > 0’ replaced by ‘g(x) ≥ 0’. It ensures that the synthesized pRSM is indeed
a pRSM.
⊓
⊔

I

Experimental Details

In the following description of the programs, we use “a ≤ f ≤ b” for an abbreviation of “a ≤ f ∧f ≤ b”, and “(xn1 , . . . , xnk )T := (En1 , . . . , Enk )T ” as a compact
form for assignment “xn1 , . . . , xnk := En1 , . . . , Enk ”. We also use UNIF(a, b) to
denote the uniform distribution on [a, b]. Besides, the invariants are written in
a bracketed fashion [. . . ] and are put directly after the labels they are attached
to. In all our examples the invariants are straightforward to obtain directly from
the program.
Example 10 (Logistic Map). Consider the logistic-map example adopted in [15].
The program is depicted in Fig. 4.
31

[0 ≤ a ≤ 1 ∧ 0 ≤ x ≤ 1]
while 0 ≤ a ≤ 0.999 ∧ 0.001 ≤ x ≤ 1 do
[ 0 ≤ a ≤ 0.999 ∧ 0.001 ≤ x ≤ 1 ]
x := a ∗ x ∗ (1 − x)
od
Fig. 4. Logistic Map

Example 11 (Decay). Consider a decay example in Fig. 5 which is a discretized
randomized version of the system of differential equations x′ = −x + y, y ′ =
−x − y; the ODE describes the exponential decay of any initial value to the
origin.

[ x2 + y 2 ≤ 2 ]
while 0.1 ≤ x2 + y 2 ≤ 1 do
2
2
[ 0.1

 ≤ x + y ≤ 1 ]

x
UNIF(0.98, 1) ∗ x + 0.01 ∗ y
:=
y
UNIF(0.98, 1) ∗ y − 0.01 ∗ x
od
Fig. 5. Decay

Example 12 (Random Walk). Consider a demonic random-walk example in
Fig. 6 which mimics a random walk within a bounded region; the region is
defined through two non-linear parabola curves instead of linear constraints.

[ x2 + y 2 ≤ 2 ]
while x2 + y ≤ 1 ∧ x2 − y ≤ 1 do
[ x2+ y 
≤ 1 ∧ x2 − y ≤ 1 ]


x
x + UNIF(−0.1, 0.1)
:=
y
y + UNIF(−0.1, 0.1)
od
Fig. 6. Random Walk

Example 13 (Gambler’s Ruin). Finally, we consider the gambler’s ruin in Example 1 with invariants given in Example 4.
32

Example 14 (Gambler’s Ruin Variant). Consider a variant of Example 13 depicted in Fig. 7. Note that this example is another affine program that also does
not admit a linear ranking supermartingale.
Example 15 (Nested Loop). Consider the example in Fig. 8. The example is a
nested loop with two independent loop-control variables.

[ 0.7 ≤ x ≤ y + 0.3 ]
while 1 ≤ x ≤ y do
[1 ≤ x ≤ y]
i f ⋆ do
[1 ≤ x ≤ y]
x := x + UNIF(−0.3, 0.3)
else
[1 ≤ x ≤ y]
i f prob ( 0 . 5 ) do
[1 ≤ x ≤ y]
x := x + 0.1
else
[1 ≤ x ≤ y]
x := x − 0.1
fi
fi
od
Fig. 7. Gambler’s Ruin Variant

33

[ x ≤ m + 0.2 ∧ n ≥ 0 ]
while x ≤ m do
[x ≤ m ∧ n ≥ 0]
y :=0;
[ x ≤ m ∧ y ≤ n + 0.2 ∧ n ≥ 0 ]
while y ≤ n do
[x ≤ m ∧ y ≤ n ∧ n ≥ 0]
y := y + UNIF(−0.1, 0.2)
od ;
[x ≤ m ∧ y ≥ n ∧ n ≥ 0]
x := x + UNIF(−0.1, 0.2)
od
Fig. 8. Nested Loop

34

