How long, O Bayesian network,
will I sample thee?

arXiv:1802.10433v1 [cs.PL] 28 Feb 2018

A program analysis perspective on
expected sampling times.
(arXiv extended version)
Kevin Batz, Benjamin Lucien Kaminski,
Joost-Pieter Katoen, and Christoph Matheja
RWTH Aachen University

Abstract. Bayesian networks (BNs) are probabilistic graphical models
for describing complex joint probability distributions. The main problem
for BNs is inference: Determine the probability of an event given observed
evidence. Since exact inference is often infeasible for large BNs, popular
approximate inference methods rely on sampling.
We study the problem of determining the expected time to obtain a single
valid sample from a BN. To this end, we translate the BN together with
observations into a probabilistic program. We provide proof rules that
yield the exact expected runtime of this program in a fully automated
fashion. We implemented our approach and successfully analyzed various
real–world BNs taken from the Bayesian network repository.
Keywords: Probabilistic Programs, Expected Runtimes, Weakest Preconditions, Program Verification

1

Introduction

Bayesian networks (BNs) are probabilistic graphical models representing joint
probability distributions of sets of random variables with conditional dependencies. Graphical models are a popular and appealing modeling formalism, as
they allow to succinctly represent complex distributions in a human–readable
way. Bayesian Networks have been intensively studied at least since 1985 [42]
and have a wide range of applications including machine learning [23], speech
recognition [49], sports betting [10], gene regulatory networks [17], diagnosis of
diseases [26], and finance [38].
Probabilistic programs are programs with the key ability to draw values at random. Seminal papers by Kozen from the 1980s consider formal semantics [31]
as well as initial work on verification [46,32]. McIver & Morgan [34] build on
this work to further weakest–precondition style verification for imperative probabilistic programs.

2

The interest in probabilistic programs has been rapidly growing in recent
years [19,22]. Part of the reason for this déjà vu is their use for representing
probabilistic graphical models [30] such as BNs. The full potential of modern
probabilistic programming languages like Anglican [47], Church [20], Figaro [43],
R2 [39], or Tabular [21] is that they enable rapid prototyping and obviate the
need to manually provide inference methods tailored to an individual model.
Probabilistic inference is the problem of determining the probability of an event
given observed evidence. It is a major problem for both BNs and probabilistic
programs, and has been subject to intense investigations by both theoreticians
and practitioners for more than three decades; see [30] for a survey. In particular,
it has been shown that for probabilistic programs exact inference is highly undecidable [27], while for BNs both exact inference as well as approximate inference
to an arbitrary precision are NP–hard [11,12]. In light of these complexity–
theoretical hurdles, a popular way to analyze probabilistic graphical models as
well as probabilistic programs is to gather a large number of independent and
identically distributed (i.i.d. for short) samples and then do statistical reasoning
on these samples. In fact, all of the aforementioned probabilistic programming
languages support sampling based inference methods.
Rejection sampling is a fundamental approach to obtain valid samples from BNs
with observed evidence. In a nutshell, this method first samples from the joint
(unconditional) distribution of the BN. If the sample complies with all evidence,
it is valid and accepted; otherwise it is rejected and one has to resample.
Apart from rejection sampling, there are more sophisticated sampling techniques, which mainly fall in two categories: Markov Chain Monte Carlo (MCMC)
and importance sampling. But while MCMC requires heavy hand–tuning and
suffers from slow convergence rates on real–world instances [30, Chapter 12.3],
virtually all variants of importance sampling rely again on rejection sampling
[30,48].
A major problem with rejection sampling is that for poorly conditioned data,
this approach might have to reject and resample very often in order to obtain
just a single accepting sample. Even worse, being poorly conditioned need not be
immediately evident for a given BN, let alone a probabilistic program. In fact,
Gordon et al. [22, p. 177] point out that
“the main challenge in this setting [i.e. sampling based approaches] is
that many samples that are generated during execution are ultimately
rejected for not satisfying the observations.”
If too many samples are rejected, the expected sampling time grows so large that
sampling becomes infeasible. The expected sampling time of a BN is therefore a
key figure for deciding whether sampling based inference is the method of choice.
How long, O Bayesian network, will I sample thee? More precisely, we use techniques from program verification to give an answer to the following question:

3
S=0 S=1
R=0

a

1−a

R=1

0.2

0.8

R=0 R=1
S

R

a

1−a

G=0 G=1

G

S = 0, R = 0 0.01

0.99

S = 0, R = 1 0.25

0.75

S = 1, R = 0

0.9

0.1

S = 1, R = 1

0.2

0.8

Fig. 1. A simple Bayesian network.

Given a Bayesian network with observed evidence, how long does it take
in expectation to obtain a single sample that satisfies the observations?
As an example, consider the BN in Figure 1 which consists of just three nodes
(random variables) that can each assume values 0 or 1. Each node X comes
with a conditional probability table determining the probability of X assuming
some value given the values of all nodes Y that X depends on (i.e. X has an
incoming edge from Y ), see Appendix A.1 for detailed calculations. For instance,
the probability that G assumes value 0, given that S and R are both assume 1,
is 0.2. Note that this BN is paramterized by a ∈ [0, 1].
Now, assume that our observed evidence is the event G=0 and we apply rejection sampling to obtain one accepting sample from this BN. Then our approach
will yield that a rejection sampling algorithm will, on average, require
200a2 − 40a − 460
89a2 − 69a − 21
guard evaluations, random assignments, etc. until it obtains a single sample that
complies with the observation G=0 (the underlying runtime model is discussed
in detail in Section 3.3). By examination of this function, we see that for large
ranges of values of a the BN is rather well–behaved: For a ∈ [0.08, 0.78] the
expected sampling time stays below 18. Above a = 0.95 the expected sampling
time starts to grow rapidly up to 300.
While 300 is still moderate, we will see later that expected sampling times of
real–world BNs can be much larger. For some BNs, the expected sampling time
even exceeded 1018 , rendering sampling based methods infeasible. In this case,
exact inference (despite NP–hardness) was a viable alternative (see Section 6).
Our approach. We apply weakest precondition style reasoning a lá McIver &
Morgan [34] and Kaminski et al. [29] to analyze both expected outcomes and
expected runtimes (ERT) of a syntactic fragment of pGCL, which we call the
Bayesian Network Language (BNL). Note that since BNL is a syntactic fragment

4

of pGCL, every BNL program is a pGCL program but not vice versa. The main restriction of BNL is that (in contrast to pGCL) loops are of a special form that prohibits undesired data flow across multiple loop iterations. While this restriction
renders BNL incapable of, for instance, counting the number of loop iterations1 ,
BNL is expressive enough to encode Bayesian networks with observed evidence.
For BNL, we develop dedicated proof rules to determine exact expected values
and the exact ERT of any BNL program, including loops, without any user–
supplied data, such as invariants [34,29], ranking or metering functions [18],
(super)martingales [7,8,9], etc.
As a central notion behind these rules, we introduce f –i.i.d.–ness of probabilistic loops, a concept closely related to stochastic independence, that allows us to rule out undesired parts of the data flow across loop iterations. Furthermore, we show how every BN with observations is translated into a BNL
program, such that
(a) executing the BNL program corresponds to sampling from the conditional
joint distribution given by the BN and observed data, and
(b) the ERT of the BNL program corresponds to the expected time until a sample
that satisfies the observations is obtained from the BN.
As a consequence, exact expected sampling times of BNs can be inferred by
means of weakest precondition reasoning in a fully automated fashion. This can
be seen as a first step towards formally evaluating the quality of a plethora of
different sampling methods (cf. [30,48]) on source code level.
Contributions. To summarize, our main contributions are as follows:
– We develop easy–to–apply proof rules to reason about expected outcomes
and expected runtimes of probabilistic programs with f –i.i.d. loops.
– We study a syntactic fragment of probabilistic programs, the Bayesian network language (BNL), and show that our proof rules are applicable to every
BNL program; expected runtimes of BNL programs can thus be inferred.
– We give a formal translation from Bayesian networks with observations to
BNL programs; expected sampling times of BNs can thus be inferred.
– We implemented a prototype tool that automatically analyzes the expected
sampling time of BNs with observations. An experimental evaluation on
real–world BNs demonstrates that very large expected sampling times (in
the magnitude of millions of years) can be inferred within less than a second;
This provides practitioners the means to decide whether sampling based
methods are appropriate for their models.
Outline. We discuss related work in Section 2. Syntax and semantics of the
probabilistic programming language pGCL are presented in Section 3. Our proof
rules are introduced in Section 4 and applied to BNs in Section 5. Section 6
reports on experimental results and Section 7 concludes.
1

An example of a program that is not expressible in BNL is given in Example 1.

5

2

Related Work

While various techniques for formal reasoning about runtimes and expected outcomes of probabilistic programs have been developed, e.g. [24,6,5,16,37], none
of them explicitly apply formal methods to reason about Bayesian networks on
source code level. In the following, we focus on approaches close to our work.
Weakest preexpectation calculus. Our approach builds upon the expected runtime calculus [29], which is itself based on work by Kozen [31,32] and McIver and
Morgan [34]. In contrast to [29], we develop specialized proof rules for a clearly
specified program fragment without requiring user–supplied invariants. Since
finding invariants often requires heavy calculations, our proof rules contribute
towards simplifying and automating verification of probabilistic programs.
Ranking supermartingales. Reasoning about almost–sure termination is often
based on ranking (super)martingales (cf. [7,9]). In particular, Chatterjee et al. [8]
consider the class of affine probabilistic programs for which linear ranking supermartingales exist (Lrapp); thus proving (positive2 ) almost–sure termination
for all programs within this class. They also present a doubly–exponential algorithm to approximate ERTs of Lrapp programs. While all BNL programs lie
within Lrapp, our proof rules yield exact ERTs as expectations (thus allowing
for compositional proofs), in contrast to a single number for a fixed initial state.
Bayesian networks and probabilistic programs. Bayesian networks are a — if
not the most — popular probabilistic graphical model (cf. [3,30] for details) for
reasoning about conditional probabilities. They are closely tied to (a fragment
of) probabilistic programs. For example, Infer.NET [35] performs inference by
compiling a probabilistic program into a Bayesian network. While correspondences between probabilistic graphical models, such as BNs, have been considered in the literature [36,20,22], we are not aware of a formal soudness proof for
a translation from classical BNs into probabilistic programs including conditioning.
Conversely, some probabilistic programming languages such as Church [20],
Stan [25], and R2 [39] directly perform inference on the program level using sampling techniques similar to those developed for Bayesian networks. Our approach
is a step towards understanding sampling based approaches formally: We obtain
the exact expected runtime required to generate a sample that satisfies all observations. This may ultimately be used to evaluate the quality of a plethora of
proposed sampling methods for Bayesian inference (cf. [30,48]).

3

Probabilistic Programs

We briefly present the probabilistic programming language that is used throughout this paper. Since our approach is embedded into weakest-precondition style
2

Positive almost–sure termination means termination in finite expected time [4].

6

approaches, we also recap calculi for reasoning about both expected outcomes
and expected runtimes of probabilistic programs.
3.1

The Probabilistic Guarded Command Language

We enhance Dijkstra’s Guarded Command Language [14,13] by a probabilistic construct, namely a random assignment. We thereby obtain a probabilistic
Guarded Command Language (for a closely related language, see [34]).
Let Vars be a finite set of program variables. Moreover, let Q be the set of
rational numbers, and let D (Q) be the set of discrete probability distributions
over Q. The set of program states is given by Σ = { σ | σ : Vars → Q }.
A distribution expression µ is a function of type µ : Σ → D (Q) that takes a
program state and maps it to a probability distribution on values from Q. We
denote by µσ the distribution obtained from applying σ to µ.
The probabilistic guarded command language (pGCL) is given by the grammar
C

−→

(effectless program)
(endless loop)

skip
| diverge
| x :≈ µ
| C; C

(random assignment)
(sequential composition)

| if (ϕ) {C} else {C}
| while (ϕ) {C}

(conditional choice)
(while loop)

| repeat {C} until (ϕ) ,

(repeat–until loop)

where x ∈ Vars is a program variable, µ is a distribution expression, and ϕ is a
Boolean expression guarding a choice or a loop. A pGCL program that contains
neither diverge, nor while, nor repeat − until loops is called loop–free.
For σ ∈ Σ and an arithmetical expression E over Vars, we denote by σ(E)
the evaluation of E in σ, i.e. the value that is obtained by evaluating E after
replacing any occurrence of any program variable x in E by the value σ(x).
Analogously, we denote by σ(ϕ) the evaluation of a guard ϕ in state σ to either
true or false. Furthermore, for a value v ∈ Q we write σ [x 7→ v] to indicate that
we set program variable x to value v in program state σ, i.e.3
(
v,
if y = x
σ [x 7→ v] = λ y
σ(y), if y 6= x .

.

We use the Iverson bracket notation to associate with each guard its according
indicator function. Formally, the Iverson bracket [ϕ] of ϕ is thus defined as the
function [ϕ] = λ σ σ(ϕ).

.

3

.

We use λ–expressions to construct functions: Function λX ǫ applied to an argument
α evaluates to ǫ in which every occurrence of X is replaced by α.

7

Let us briefly go over the pGCL constructs and their effects: skip does not
alter the current program state. The program diverge is an infinite busy loop,
thus takes infinite time to execute. It returns no final state whatsoever.
The random assignment x :≈ µ is (a) the only construct that can actually
alter the program state and (b) the only construct that may introduce random
behavior into the computation. It takes the current program state σ, then samples a value v from probability distribution µσ , and then assigns v to program
variable x. An example of a random assignment is
x :≈ 1/2 · h5i + 1/6 · hy + 1i + 1/3 · hy − 1i .
If the current program state is σ, then the program state is altered to either
σ [x 7→ 5] with probability 1/2, or to σ [x 7→ σ(y) + 1] with probability 1/6, or to
σ [x 7→ σ(y) − 1] with probability 1/3. The remainder of the pGCL constructs are
standard programming language constructs.
In general, a pGCL program C is executed on an input state and yields a
probability distribution over final states due to possibly occurring random assignments inside of C. We denote that resulting distribution by JCKσ . Strictly speaking, programs can yield subdistributions, i.e. probability distributions whose total
mass may be below 1. The “missing” probability mass represents the probability
of nontermination. Let us conclude our presentation of pGCL with an example:
Example 1 (Geometric Loop). Consider the program Cgeo given by
x :≈ 0; c :≈ 1/2 · h0i + 1/2 · h1i;
while (c = 1) {x :≈ x + 1; c :≈ 1/2 · h0i + 1/2 · h1i}
This program basically keeps flipping coins until it flips, say, heads (c = 0). In
x it counts the number of unsuccessful trials.4 In effect, it almost surely sets
c to 0 and moreover it establishes a geometric distribution on x. The resulting
distribution is given by
JCgeo Kσ (τ ) =
3.2

ω
X

[τ = σ [c, x 7→ 0, n]] ·

n=0

1
.
2n+1

△

The Weakest Preexpectation Transformer

We now present the weakest preexpectation transformer wp for reasoning about
expected outcomes of executing probabilistic programs in the style of McIver
& Morgan [34]. Given a random variable f mapping program states to reals, it
allows us to reason about the expected value of f after executing a probabilistic
program on a given state.
4

This counting is also the reason that Cgeo is an example of a program that is not
expressible in our BNL language that we present later.

8

Expectations. The random variables the wp transformer acts upon are taken
from a set of so-called expectations, a term coined by McIver & Morgan [34]:
Definition 1 (Expectations). The set of expectations E is defined as

.
E = f f : Σ → R∞
≥0

We will use the notation f [x/E] to indicate the replacement of every occurrence of x in f by E. Since x, however, does not actually occur in f , we more
formally define f [x/E] = λσ f (σ [x 7→ σ(E)]).
A complete partial order ≤ on E is obtained by point–wise lifting the canonical
total order on R∞
≥0 , i.e.

.

f1  f2

∀σ ∈ Σ :

iff

f1 (σ) ≤ f2 (σ) .

Its least element is given by λσ 0 which we (by slight abuse of notation) also
denote by 0. Suprema are constructed pointwise, i.e. for S ⊆ E the supremum
sup S is given by sup S = λσ supf ∈S f (σ).

.

.

We allow expectations to map only to positive reals, so that we have a complete
partial order readily available, which would not be the case for expectations of
type Σ → R ∪ {−∞, +∞}. A wp calculus that can handle expectations of such
type needs more technical machinery and cannot make use of this underlying
natural partial order [28]. Since we want to reason about ERTs which are by
nature non–negative, we will not need such complicated calculi.
Notice that we use a slightly different definition of expectations than McIver
& Morgan [34], as we allow for unbounded expectations, whereas [34] requires
that expectations are bounded. This however would prevent us from capturing
ERTs, which are potentially unbounded.
Expectation Transformers. For reasoning about the expected value of f ∈ E
after execution of C, we employ a backward–moving weakest preexpectation
transformer wpJCK : E → E, that maps a postexpectation f ∈ E to a preexpectation wp JCK (f ) ∈ E, such that wp JCK (f ) (σ) is the expected value of f after
executing C on initial state σ. Formally, if C executed on input σ yields final
distribution JCKσ , then the weakest preexpectation wp JCK (f ) of C with respect
to postexpectation f is given by
Z
f dJCKσ ,
(1)
wp JCK (f ) (σ) =
Σ

R

where we denote by A h dν the expected value of a random variable h : A → R∞
≥0
with respect to a probability distribution ν : A → [0, 1]. Weakest preexpectations
can be defined in a very systematic way:
Definition 2 (The wp Transformer [34]). The weakest preexpectation transformer wp : pGCL → E → E is defined by induction on all pGCL programs according to the rules in Table 1. We call Ff (X) = [¬ϕ] · f + [ϕ] · wp JCK (X)
the wp–characteristic functional of the loop while (ϕ) {C} with respect to postexpectation f . For a given wp–characteristic function Ff , we call the sequence
{Ffn (0)}n∈N the orbit of Ff .

9
C

wp JCK (f )

skip

f

diverge

0

x :≈ µ

λσ

if (ϕ) {C1 } else {C2 }

[ϕ] · wp JC1 K (f ) + [¬ϕ] · wp JC2 K (f )

C1 ; C2

wp JC1 K (wp JC2 K (f ))
′

.R

Q

λv

. f [x/v] dµ

σ

. [¬ϕ] · f + [ϕ] · wp JC K (X)
′

while (ϕ) {C }

lfp X

repeat {C ′ } until (ϕ)

wp JC ′ ; while (¬ϕ) {C ′ }K (f )

Table 1. Rules for the wp–transformer.

Let us briefly go over the definitions in Table 1: For skip the program state is
not altered and thus the expected value of f is just f . The program diverge
will never yield any final state. The distribution over the final states yielded by
diverge is thus the null distribution ν0 (τ ) = 0, that assigns probability 0 to
every state.
R Consequently,
P the expected value of f after execution of diverge is
given by Σ f dν0 = τ ∈Σ 0 · f (τ ) = 0.
The rule for the random assignment x :≈ µ is a bit more technical: Let the
current program state be σ. Then for every value v ∈ Q, the random assignment
assigns v to x with probability µσ (v), where σ is the current program state. The
value of f after assigning v to x is f (σ [x 7→ v]) = f [x/v](σ) and therefore the
expected value of f after executing the random assignment is given by
Z
X

µσ (v) · f [x/v](σ) =
λv f [x/v](σ) dµσ .
v∈Q

Q

.

Expressed as a function of σ, the latter yields precisely the definition in Table 1.
The definition for the conditional choice if (ϕ) {C1 } else {C2 } is not surprising: if the current state satisfies ϕ, we have to opt for the weakest preexpectation
of C1 , whereas if it does not satisfy ϕ, we have to choose the weakest preexpectation of C2 . This yields precisely the definition in Table 1.
The definition for the sequential composition C1 ; C2 is also straightforward:
We first determine wp JC2 K (f ) to obtain the expected value of f after executing
C2 . Then we mentally prepend the program C2 by C1 and therefore determine
the expected value of wp JC2 K (f ) after executing C1 . This gives the weakest
preexpectation of C1 ; C2 with respect to postexpectation f .
The definition for the while loop makes use of a least fixed point, which is
a standard construction in program semantics. Intuitively, the fixed point iteration of the wp–characteristic functional, given by 0, Ff (0), Ff2 (0), Ff3 (0), . . .,
corresponds to the portion the expected value of f after termination of the loop,
that can be collected within at most 0, 1, 2, 3, . . . loop guard evaluations. The
Kleene Fixed Point Theorem [33] ensures that this iteration converges to the

10

least fixed point, i.e.
sup Ffn (0) = lfp Ff = wp Jwhile (ϕ) {C}K (f ) .

n∈N

By inspection of the above equality, we see that the least fixed point is exactly the
construct that we want for while loops, since supn∈N Ffn (0) in principle allows the
loop to run for any number of iterations, which captures precisely the semantics
of a while loop, where the number of loop iterations is — in contrast to e.g. for
loops — not determined upfront.
Finally, since repeat {C} until (ϕ) is syntactic sugar for C; while (ϕ) {C},
we simply define the weakest preexpectation of the former as the weakest preexpectation of the latter. Let us conclude our study of the effects of the wp
transformer by means of an example:
Example 2. Consider the following program C:
c :≈ 1/3 · h0i + 2/3 · h1i;
if (c = 0) {x :≈ 1/2 · h5i + 1/6 · hy + 1i + 1/3 · hy − 1i} else {skip}
Say we wish to reason about the expected value of x + c after execution of the
above program. We can do so by calculating wp JCK (x + c) using the rules in
Table 1. This calculation in the end yields wp JCK (x + c) = 3y + 26/18 The
expected valuation of the expression x + c after executing C is thus 3y + 26/18.
Note that x + c can be thought of as an expression that is evaluated in the final
states after execution, whereas 3y + 26/18 must be evaluated in the initial state
before execution of C.
△

Healthiness Conditions of wp. The wp transformer enjoys some useful properties, sometimes called healthiness conditions [34]. Two of these healthiness
conditions that we will heavily make use of are given below:
Theorem 1 (Healthiness Conditions for the wp Transformer [34]). For
all C ∈ pGCL, f1 , f2 ∈ E, and a ∈ R≥0 , the following holds:
1.
2.
3.3

wp JCK (a · f1 + f2 ) = a · wp JCK (f1 ) + wp JCK (f2 )
wp JCK (0) = 0

(linearity)
(strictness)

The Expected Runtime Transformer

While for deterministic programs we can speak of the runtime of a program on
a given input, the situation is different for probabilistic programs: For those we
instead have to speak of the expected runtime (ERT). Notice that the ERT can
be finite (even constant) while the program may still admit infinite executions.
An example of this is the geometric loop in Example 1.
A wp–like transformer designed specifically for reasoning about ERTs is the
ert transformer [29]. Like wp, it is of type ertJCK : E → E and it can be shown that

11
C

ert JCK (f )

skip

1+f

diverge

∞

x :≈ µ

1 + λσ

if (ϕ) {C1 } else {C2 }
C1 ; C2

1 + [ϕ] · ert JC1 K (f ) + [¬ϕ] · ert JC2 K (f )

ert JC1 K ert JC2 K (f )

while (ϕ) {C ′ }

lfp X

repeat {C ′ } until (ϕ)

ert JC ′ ; while (¬ϕ) {C ′ }K (f )

.R

Q

λv

. f [x/v] dµ

σ

. 1 + [¬ϕ] · f + [ϕ] · ert JC K (X)
′

Table 2. Rules for the ert–transformer.

ert JCK (0) (σ) is precisely the expected runtime of executing C on input σ. More
generally, if f : Σ → R∞
≥0 measures the time that is needed after executing C
(thus f is evaluated in the final states after termination of C), then ert JCK (f ) (σ)
is the expected time that is needed to run C on input σ and then let time f
pass. For a more in–depth treatment of the ert transformer, see [29, Section 3].
The transformer is defined as follows:
Definition 3 (The ert Transformer [29]). The expected runtime transformer
ert : pGCL → E → E is defined by induction on all pGCL programs according to
the rules given in Table 2. We call Ff (X) = 1 + [¬ϕ]·f + [ϕ] ·wp JCK (X) the ert–
characteristic functional of the loop while (ϕ) {C} with respect to postexpectation
f . As with wp, for a given ert–characteristic function Ff , we call the sequence
{Ffn (0)}n∈N the orbit of Ff . Notice that
ert Jwhile (ϕ) {C}K (f ) = lfp Ff = sup {Ffn (0)}n∈N .
The rules for ert are very similar to the rules for wp. The runtime model we
assume is that skip statements, random assignments, and guard evaluations
for both conditional choice and while loops cost one unit of time. This runtime
model can easily be adopted to count only the number of loop iterations or only
the number of random assignments, etc. We conclude with a strong connection
between the wp and the ert transformer, that is crucial in our proofs:
Theorem 2 (Decomposition of ert [40]). For any C ∈ pGCL and f ∈ E,
ert JCK (f ) = ert JCK (0) + wp JCK (f ) .

4

Expected Runtimes of i.i.d. Loops

We derive a proof rule that allows to determine exact ERTs of independent
and identically distributed loops (or i.i.d. loops for short). Intuitively, a loop

12
10

×

while (x − 5)2 + (y − 5)2 ≥ 25 {


x :≈ Unif[0 . . . 10];

5

×
×

×

×

×
×

×
×

×

y :≈ Unif[0 . . . 10]

×

×
×

}

×
5

×
×
10

Fig. 2. An i.i.d. loop sampling a point within a circle uniformly at random using
rejection sampling. The picture on the right–hand side visualizes the procedure: In
each iteration a point (×) is sampled. If we obtain a point within the white area inside
the square, we terminate. Otherwise, i.e. if we obtain a point within the gray area
outside the circle, we resample.

is i.i.d. if the distributions of states that are reached at the end of different
loop iterations are equal. This is the case whenever there is no data flow across
different iterations. In the non–probabilistic case, such loops either terminate
after exactly one iteration or never. This is different for probabilistic programs.
As a running example, consider the program Ccircle in Figure 2. Ccircle samples a point within a circle with center (5, 5) and radius r = 5 uniformly at
random using rejection sampling. In each iteration, it samples a point (x, y) ∈
[0, . . . , 10]2 within the square (with some fixed precision). The loop ensures that
we resample if a sample is not located within the circle. Our proof rule will allow
us to systematically determine the ERT of this loop, i.e. the average amount of
time required until a single point within the circle is sampled.
Towards obtaining such a proof rule, we first present a syntactical notion
of the i.i.d. property. It relies on expectations that are not affected by a pGCL
program:
Definition 4. Let C ∈ pGCL and f ∈ E. Moreover, let Mod (C) denote the set
of all variables that occur on the left–hand side of an assignment in C, and let
Vars (f ) be the set of all variables that “occur in f ”, i.e. formally
x ∈ Vars (f )

iff

∃ σ ∃ v, v ′ :

f (σ [x 7→ v]) 6= f (σ [x 7→ v ′ ]) .

Then f is unaffected by C, denoted f 6⋓ C, iff Vars (f ) ∩ Mod (C) = ∅.
We are interested in expectations that are unaffected by pGCL programs because
of a simple, yet useful observation: If g 6⋓ C, then g can be treated like a constant
w.r.t. the transformer wp (i.e. like the a in Theorem 1 (1)). For our running example Ccircle (see Figure 2), the expectation f = wp JCbody K ([x + y ≤ 10]) is unaffected by the loop body Cbody of Ccircle . Consequently, we have wp JCbody K (f ) =
f · wp JCbody K (1) = f . In general, we obtain the following property:
Lemma 1 (Scaling by Unaffected Expectations). Let C ∈ pGCL and f, g ∈
E. Then g 6⋓ C implies wp JCK (g · f ) = g · wp JCK (f ).

Proof. By induction on the structure of C. See Appendix A.2.

⊓
⊔

13

We develop a proof rule that only requires that both the probability of the guard
evaluating to true after one iteration of the loop body (i.e. wp JCK ([ϕ])) as well
as the expected value of [¬ϕ] · f after one iteration (i.e. wp JCK ([¬ϕ] · f )) are
unaffected by the loop body. We thus define the following:
Definition 5 (f –Independent and Identically Distributed Loops). Let
C ∈ pGCL, ϕ be a guard, and f ∈ E. Then we call the loop while (ϕ) {C}
f –independent and identically distributed (or f –i.i.d. for short), if both
wp JCK ([ϕ]) 6⋓ C

wp JCK ([¬ϕ] · f ) 6⋓ C .

and

Example 3. Our example program Ccircle (see Figure 2) is f –i.i.d. for all f ∈ E.
This is due to the fact that
wp JCbody K



48
6 Cbody
⋓
(x − 5)2 + (y − 5)2 ≥ 25
=
121

(by Table 1)

and (again for some fixed precision p ∈ N \ {0})

 
wp JCbody K (x − 5)2 + (y − 5)2 > 25 · f

10p 10p

1 XX i
( /p − 5)2 + (j/p − 5)2 > 25 · f [x/(i/p), y/(j/p)] 6⋓ Cbody . △
·
=
121 i=0 j=0

Our main technical Lemma is that we can express the orbit of the wp–characteristic
function as a partial geometric series:
Lemma 2 (Orbits of f –i.i.d. Loops). Let C ∈ pGCL, ϕ be a guard, f ∈ E
such that the loop while (ϕ) {C} is f –i.i.d, and let Ff be the corresponding wp–
characteristic function. Then for all n ∈ N \ {0}, it holds that
Ffn (0)

= [ϕ] · wp JCK ([¬ϕ] · f ) ·

n−2
X
i=0

i

wp JCK ([ϕ])

!

+ [¬ϕ] · f .

Proof. By use of Lemma 1, see Appendix A.3.
Using this precise description of the wp orbits, we now establish proof rules for
f –i.i.d. loops, first for wp and later for ert.
Theorem 3 (Weakest Preexpectations of f –i.i.d. Loops). Let C ∈ pGCL,
ϕ be a guard, and f ∈ E. If the loop while (ϕ) {C} is f –i.i.d., then
wp Jwhile (ϕ) {C}K (f ) = [ϕ] ·
where we define

0
0

:= 0.

wp JCK ([¬ϕ] · f )
+ [¬ϕ] · f ,
1 − wp JCK ([ϕ])

14

Proof. We have
wp Jwhile (ϕ) {C}K (f )
= sup Ffn (0)

(by Definition 2)

n∈N

= sup [ϕ] · wp JCK ([¬ϕ] · f ) ·
n∈N

= [ϕ] · wp JCK ([¬ϕ] · f ) ·

ω
X

n−2
X

i=0

i=0

i

wp JCK ([ϕ])
i

wp JCK ([ϕ])

!

!

+ [¬ϕ] · f (by Lemma 2)

+ [¬ϕ] · f .

(†)

The preexpectation (†) is to be evaluated in some state σ for which we have two
cases: The first case P
is when wp JCK ([ϕ]) (σ) < 1. Using the closed form of the
1
geometric series, i.e. ω
i=0 q = 1−q if |q| < 1, we get
[ϕ] (σ) · wp JCK ([¬ϕ] · f ) (σ) ·

ω
X
i=0

i

wp JCK ([ϕ]) (σ)

!

+ [¬ϕ] (σ) · f (σ)
(† instantiated in σ)

wp JCK ([¬ϕ] · f ) (σ)
= [ϕ] (σ) ·
+ [¬ϕ] (σ) · f (σ) .
1 − wp JCK ([ϕ]) (σ)
(closed form of geometric series)
The second case is when wp JCK ([ϕ]) (σ) = 1. This case is technically slightly
more involved. The full proof can be found in Appendix A.4
⊓
⊔
We now derive a similar proof rule for the ERT of an f –i.i.d. loop while (ϕ) {C}.
Theorem 4 (Proof Rule for ERTs of f –i.i.d. Loops). Let C ∈ pGCL, ϕ
be a guard, and f ∈ E such that all of the following conditions hold:
1. while (ϕ) {C} is f –i.i.d.
2. wp JCK (1) = 1 (loop body terminates almost–surely).
3. ert JCK (0) ⋓
6 C (every iteration runs in the same expected time).
Then for the ERT of the loop while (ϕ) {C} w.r.t. postruntime f it holds that
ert Jwhile (ϕ) {C}K (f ) = 1 +
where we define

0
0

:= 0 and

a
0

[ϕ] · (1 + ert JCK ([¬ϕ] · f ))
+ [¬ϕ] · f ,
1 − wp JCK ([ϕ])

:= ∞, for a 6= 0.

Proof. We first prove
ert Jwhile (ϕ) {C}K (0) = 1 + [ϕ] ·

1 + ert JCK (0)
.
1 − wp JCK ([ϕ])

(‡)

15

To this end, we propose the following expression as the orbit of the ert–characteristic function of the loop w.r.t. 0:
!
n−1
n
X
X
i
i
n
wp JCK ([ϕ])
wp JCK ([ϕ]) +
F0 (0) = 1 + [ϕ] · ert JCK (0) ·
i=0

i=0

For a verification that the above expression is indeed the correct orbit, we refer to
the rigorous proof of this theorem located in Appendix A.5. Now, analogously to
the reasoning in the proof of Theorem 3 (i.e. using the closed form of the geometric series and case distinction on whether wp JCK ([ϕ]) < 1 or wp JCK ([ϕ]) = 1),
we get that the supremum of this orbit is indeed the right–hand side of (‡). To
complete the proof, consider the following:
ert Jwhile (ϕ) {C}K (f )
= ert Jwhile (ϕ) {C}K (0) + wp Jwhile (ϕ) {C}K (f )
= 1 + [ϕ] ·

= 1 + [ϕ] ·

5

(by Theorem 2)

1 + ert JCK (0)
wp JCK ([¬ϕ] · f )
+ [ϕ] ·
+ [¬ϕ] · f
1 − wp JCK ([ϕ])
1 − wp JCK ([ϕ])
(by (‡) and Theorem 3)

1 + ert JCK ([¬ϕ] · f )
+ [¬ϕ] · f
1 − wp JCK ([ϕ])

(by Theorem 2)
⊓
⊔

A Programming Language for Bayesian Networks

So far we have derived proof rules for formal reasoning about expected outcomes
and expected run-times of i.i.d. loops (Theorems 3 and 4). In this section, we apply these results to develop a syntactic pGCL fragment that allows exact computations of closed forms of ERTs. In particular, no invariants, (super)martingales
or fixed point computations are required.
After that, we show how BNs with observations can be translated into pGCL
programs within this fragment. Consequently, we call our pGCL fragment the
Bayesian Network Language. As a result of the above translation, we obtain a
systematic and automatable approach to compute the expected sampling time
of a BN in the presence of observations. That is, the expected time it takes to
obtain a single sample that satisfies all observations.
5.1

The Bayesian Network Language

Programs in the Bayesian Network Language are organized as sequences of
blocks. Every block is associated with a single variable, say x, and satisfies
two constraints: First, no variable other than x is modified inside the block, i.e.
occurs on the left–hand side of a random assignment. Second, every variable
accessed inside of a guard has been initialized before. These restrictions ensure
that there is no data flow across multiple executions of the same block. Thus,
intuitively, all loops whose body is composed from blocks (as described above)
are f –i.i.d. loops.

16

Definition 6 (The Bayesian Network Language). Let Vars = {x1 , x2 , . . .}
be a finite set of program variables as in Section 3. The set of programs in
Bayesian Network Language, denoted BNL, is given by the grammar
C

−→

Seq

|

Seq

−→

Seq; Seq

Bx i

−→

xi :≈ µ

repeat {Seq} until (ψ)
|
|

Bx 1

|

Bx 2

|

|

C; C

...

if (ϕ) {xi :≈ µ} else {Bxi }
(rule exists for all xi ∈ Vars)

where xi ∈ Vars is a program variable, all variables in ϕ have been initialized
before, and Bxi is a non–terminal parameterized with program variable xi ∈ Vars.
That is, for all xi ∈ Vars there is a non–terminal Bxi . Moreover,
Pnψ is an arbitrary
guard and µ is a distribution expression of the form µ =
j=1 pj · haj i with
aj ∈ Q for 1 ≤ j ≤ n.
Example 4. Consider the BNL program Cdice :
x1 :≈ Unif[1 . . . 6]; repeat {x2 :≈ Unif[1 . . . 6]} until (x2 ≥ x1 )
This program first throws a fair die. After that it keeps throwing a second die
until its result is at least as large as the first die.
△
For any C ∈ BNL, our goal is to compute the exact ERT of C, i.e. ert JCK (0).
In case of loop–free programs, this amounts to a straightforward application of
the ert calculus presented in Section 3. To deal with loops, however, we have to
perform fixed point computations or require user–supplied artifacts, e.g. invariants, supermartingales, etc. For BNL programs, on the other hand, it suffices to
apply the proof rules developed in Section 4. As a result, we directly obtain an
exact closed form solution for the ERT of a loop. This is a consequence of the
fact that all loops in BNL are f –i.i.d., which we establish in the following.
By definition, every loop in BNL is of the form repeat {Bxi } until (ψ), which
is equivalent to Bxi ; while (¬ψ) {Bxi }. Hence, we want to apply Theorem 4 to
that while loop. Our first step is to discharge the theorem’s premises:
Lemma 3. Let Seq be a sequence of BNL–blocks, g ∈ E, and ψ be a guard.
Then:
1. The expected value of g after executing Seq is unaffected by Seq. That is,
wp JSeqK (g) 6⋓ Seq.
2. The ERT of Seq is unaffected by Seq, i.e. ert JSeqK (0) 6⋓ Seq.
3. For every f ∈ E, the loop while (¬ψ) {Seq} is f –i.i.d.
Proof. 1. is proven by induction on the length of the sequence of blocks Seq and
2. is a consequence of 1., see Appendix A.6. 3. follows immediately from 1. by
instantiating g with [¬ψ] and [ψ] · f , respectively.
⊓
⊔
We are now in a position to derive a closed form for the ERT of loops in BNL.

17

Theorem 5. For every loop repeat {Seq} until (ψ) ∈ BNL and every f ∈ E,
ert Jrepeat {Seq} until (ψ)K (f ) =

1 + ert JSeqK ([ψ] · f )
.
wp JSeqK ([ψ])

Proof. Let f ∈ E. Moreover, recall that repeat {Seq} until (ψ) is equivalent
to the program Seq; while (¬ψ) {Seq} ∈ BNL. Applying the semantics of ert
(Table 2), we proceed as follows:
ert Jrepeat {Seq} until (ψ)K (f ) = ert JSeqK (ert Jwhile (¬ψ) {Seq}K (f ))
Since the loop body Seq is loop–free, it terminates certainly, i.e. wp JSeqK (1) = 1
(Premise 2. of Theorem 4). Together with Lemma 3.1. and 3., all premises of Theorem 4 are satisfied. Hence, we obtain a closed form for ert Jwhile (¬ψ) {Seq}K (f ):


[¬ψ] · (1 + ert JSeqK ([ψ] · f ))
= ertJSeqK
1+
+ [ψ] · f
1 − wp JSeqK ([¬ψ])
|
{z
}
=:g

By Theorem 2, we know ert JSeqK (g) = ert JSeqK (0) + wp JCK (g) for any g. Thus:


[¬ψ] · (1 + ert JSeqK ([ψ] · f ))
= ert JSeqK (0) + wpJSeqK
1+
+ [ψ] · f
1 − wp JSeqK ([¬ψ])
|
{z
}
g

Since wp is linear (Theorem 1 (2)), we obtain:

= ert JSeqK (0) + wp JSeqK (1) + wp JSeqK ([ψ] · f )
{z
}
|
= 1


[¬ψ] · (1 + ert JSeqK ([ψ] · f ))
+ wp JSeqK
1 − wp JSeqK ([¬ψ])

By a few simple algebraic transformations, this coincides with:


1 + ert JSeqK ([ψ] · f )
= 1 + ert JSeqK (0) + wp JSeqK ([ψ] · f ) + wp JSeqK [¬ψ] ·
1 − wp JSeqK ([¬ψ])

Let R denote the fraction above. Then Lemma 3.1. and 2. implies R 6⋓ Seq. We
may thus apply Lemma 1 to derive wp JSeqK ([¬ψ] · R) = wp JSeqK ([¬ψ]) · R. Hence:
= 1 + ert JSeqK (0) + wp JSeqK ([ψ] · f ) + wp JSeqK ([¬ψ]) ·

1 + ert JSeqK ([ψ] · f )
1 − wp JSeqK ([¬ψ])

Again, by Theorem 2, we know that ert JSeqK (g) = ert JSeqK (0) + wp JSeqK (g) for
any g. Thus, for g = [ψ] · f , this yields:
= 1 + ert JSeqK ([ψ] · f ) + wp JSeqK ([¬ψ]) ·

1 + ert JSeqK ([ψ] · f )
1 − wp JSeqK ([¬ψ])

Then a few algebraic transformations lead us to the claimed ERT:
=

1 + ert JSeqK ([ψ] · f )
.
wp JSeqK ([ψ])

⊓
⊔

18

Note that Theorem 5 holds for arbitrary postexpectations f ∈ E. This enables
compositional reasoning about ERTs of BNL programs. Since all other rules of the
ert–calculus for loop–free programs amount to simple syntactical transformations
(see Table 2), we conclude that
Corollary 1. For any C ∈ BNL, a closed form for ert JCK (0) can be computed
compositionally.
Example 5. Theorem 5 allows us to comfortably compute the ERT of the BNL
program Cdice introduced in Example 4:
x1 :≈ Unif[1 . . . 6]; repeat {x2 :≈ Unif[1 . . . 6]} until (x2 ≥ x1 )
For the ERT, we have
ert JCdice K (0)

= ert Jx1 :≈ Unif[1 . . . 6]K (ert Jrepeat {. . .} until ([x2 ≥ x1 ])K (0)) (Table 2)


1 + ert Jx2 :≈ Unif[1. . .6]K ([x2 ≥ x1 ])
(Thm. 5)
= ert Jx1 :≈ Unif[1. . .6]K
wp Jx1 :≈ Unif[1. . .6]K ([x2 ≥ x1 ])
P
X
1 + 1≤j≤6 1/6 · [j ≥ i]
1/6 ·
P
=
(Table 2)
1
1≤j≤6 /6 · [j ≥ i]
1≤i≤6

= 3.45 .
5.2

△

Bayesian Networks

To reason about expected sampling times of Bayesian networks, it remains to
develop a sound translation from BNs with observations into equivalent BNL
programs. Before we present a formal translation, let us briefly recall BNs. A
BN is a probabilistic graphical model that is given by a directed acyclic graph.
Every node is a random variable and a directed edge between two nodes expresses
a probabilistic dependency between these nodes.
As a running example, consider the BN depicted in Figure 3 (inspired by [30])
that models the mood of students after taking an exam. The network contains
four random variables. They represent the difficulty of the exam (D), the level
of preparation of a student (P ), the achieved grade (G), and the resulting mood
(M ). For simplicity, let us assume that each random variable assumes either 0
or 1. The underlying dependencies express that the mood of a student depends
on the achieved grade which, in turn, depends on the difficulty of the exam and
the amount of preparation before taking it. Every node is accompanied by a
conditional probability table that provides the probabilities of a node given the
values of all the nodes it depends upon. We can then use the BN to answer
queries such as ”What is the probability that a student is well–prepared for an
exam (P = 1), but ends up with a bad mood (M = 0)?”
In order to translate BNs into equivalent BNL programs, we need a formal
representation first. Technically, we consider extended BNs in which nodes may

19
D=0 D=1
0.6

P =0 P =1

Preparation

Difficulty

0.4

0.7

0.3

G=0 G=1
D = 0, P = 0 0.95

0.05

D = 1, P = 1 0.05

0.95

D = 0, P = 1

0.5

0.5

D = 1, P = 0

0.6

0.4

Grade

M =0 M =1
Mood

G=0

0.9

0.1

G=1

0.3

0.7

Fig. 3. A Bayesian network

additionally depend on inputs that are not represented by nodes in the network. This allows us to define a compositional translation without modifying
conditional probability tables.
Towards a formal definition of extended BNs, we use the following notation.
A tuple (s1 , . . . , sk ) ∈ S k of length k over some set S is denoted by s. The
empty tuple is ε. Moreover, for 1 ≤ i ≤ k, the i-th element of tuple s is given by
s(i). To simplify the presentation, we assume that all nodes and all inputs are
represented by natural numbers.
Definition 7. An extended Bayesian network, EBN for short, is a tuple B =
(V, I, E, Vals, dep, cpt), where
V ⊆ N and I ⊆ N are finite disjoint sets of nodes and inputs.
E ⊆ V × V is a set of edges such that (V, E) is a directed acyclic graph.
Vals is a finite set of possible values that can be assigned to each node.
dep : V → (V ∪I)∗ is a function assigning each node v to an ordered sequence
of dependencies. That is, dep(v) = (u1 , . . . , um ) such that ui < ui+1
(1 ≤ i < m). Moreover, every dependency uj (1 ≤ j ≤ m) is either an input,
i.e. uj ∈ I, or a node with an edge to v, i.e. uj ∈ V and (uj , v) ∈ E.
– cpt is a function mapping each node v to its conditional probability table
cpt[v]. That is, for k = |dep(v)|, cpt[v] is given by a function of the form

–
–
–
–

cpt[v] : Valsk → Vals → [0, 1]

such that

X

cpt[v](z)(a) = 1.

z∈Valsk ,a∈Vals

Here, the i-th entry in a tuple z ∈ Valsk corresponds to the value assigned to
the i-th entry in the sequence of dependencies dep(v).
A Bayesian network (BN) is an extended BN without inputs, i.e. I = ∅. In
particular, the dependency function is of the form dep : V → V ∗ .

20

Example 6. The formalization of our example BN (Figure 3) is straightforward.
For instance, the dependencies of variable G are given by dep(G) = (D, P )
(assuming D is encoded by an integer less than P ). Furthermore, every entry
in the conditional probability table of node G corresponds to an evaluation
of the function cpt[G]. For example, if D = 1, P = 0, and G = 1, we have
cpt[G](1, 0)(1) = 0.4.
△
In general, the conditional probability table cpt determines the conditional probability distribution of each node v ∈ V given the nodes and inputs it depends
on. Formally, we interpret an entry in a conditional probability table as follows:
Pr (v = a | dep(v) = z) = cpt[v](z)(a) ,
where v ∈ V is a node, a ∈ Vals is a value, and z is a tuple of values of length
|dep(v)|. Then, by the chain rule, the joint probability of a BN is given by the
product of its conditional probability tables (cf. [3]).
Definition 8. Let B = (V, I, E, Vals, dep, cpt) be an extended Bayesian network.
Moreover, let W ⊆ V be a downward closed5 set of nodes. With each w ∈ W ∪ I,
we associate a fixed value w ∈ Vals. This notation is lifted pointwise to tuples of
nodes and inputs. Then the joint probability in which nodes in W assume values
W is given by


Y
Y
Pr (W = W ) =
cpt[v](dep(v))(v) .
Pr v = v | dep(v) = dep(v) =
v∈W

v∈W

The conditional joint probability distribution of a set of nodes W , given observations on a set of nodes O, is then given by the quotient Pr(W =W )/Pr(O=O).
For example, the probability of a student having a bad mood, i.e. M = 0, after
getting a bad grade (G = 0) for an easy exam (D = 0) given that she was
well–prepared, i.e. P = 1, is
Pr (D=0, G=0, M =0, P =1)
Pr (P =1)
0.9 · 0.5 · 0.6 · 0.3
=
= 0.27 .
0.3

Pr (D=0, G=0, M =0 | P =1) =

5.3

From Bayesian Networks to BNL

We now develop a compositional translation from EBNs into BNL programs.
Throughout this section, let B = (V, I, E, Vals, dep, cpt) be a fixed EBN. Moreover, with every node or input v ∈ V ∪ I we associate a program variable xv .
We proceed in three steps: First, every node together with its dependencies
is translated into a block of a BNL program. These blocks are then composed
into a single BNL program that captures the whole BN. Finally, we implement
conditioning by means of rejection sampling.
5

W is downward closed if v ∈ W and (u, v) ∈ E implies u ∈ E.

21

Step 1: We first present the atomic building blocks of our translation. Let v ∈ V
be a node. Moreover, let z ∈ Vals|dep(v)| be an evaluation of the dependencies of
v. That is, z is a tuple that associates a value with every node and input that
v depends on (in the same order as dep(v)). For every node v and evaluation of
its dependencies z, we define a corresponding guard and a random assignment:
^
xdep(v)(i) = z(i)
guardB (v, z) =
1≤i≤|dep(v)|

assignB (v, z) = xv :≈

X

cpt[v](z)(a) · hai

a∈Vals

Note that dep(v)(i) is the i-th element from the sequence of nodes dep(v).
Example 7. Continuing our previous example (see Figure 1), assume we fixed
the node v = G. Moreover, let z = (1, 0) be an evaluation of dep(v) = (S, R).
Then the guard and assignment corresponding to v and z are given by:
guardB (G, (1, 0)) = xD = 1 ∧ xP = 0, and
assignB (G, (1, 0)) = xG :≈ 0.6 · h0i + 0.4 · h1i.

△

We then translate every node v ∈ V into a program block that uses guards
to determine the rows in the conditional probability table under consideration.
After that, the program samples from the resulting probability distribution using
the previously constructed assignments. In case a node does neither depend on
other nodes nor input variables we omit the guards. Formally,

assignB (v, ε)
if |dep(v)| = 0









if (guardB (v, z1 )) {




assignB (v, z1 )}
blockB (v) =
else {if (guardB (v, z2 )) { if |dep(v)| = k > 0





and Valsk = {z1 , . . . , zm } .
assignB (v, z2 )}





. . .} else {



assignB (v, zm )} . . .}

Remark 1. The guards under consideration are conjunctions of equalities between variables and literals. We could thus use a more efficient translation of
conditional probability tables by adding a switch-case statement to our probabilistic programming language. Such a statement is of the form
switch(x) { case a1 : C1 case a2 : C2 . . . default : Cm } ,

where x is a tuple of variables, and a1 , . . . am−1 are tuples of rational numbers of
the same length as x. With respect to the wp semantics, a switch-case statement is syntactic sugar for nested if-then-else blocks as used in the above
translation. However, the runtime model of a switch-case statement requires

22

just a single guard evaluation (ϕ) instead of potentially multiple guard evaluations when evaluating nested if-then-else blocks. Since the above adaption
is straightforward, we opted to use nested if-then-else blocks to keep our
programming language simple and allow, in principle, more general guards. △
Step 2 The next step is to translate a complete EBN into a BNL program. To
this end, we compose the blocks obtained from each node starting at the roots
of the network. That is, all nodes that contain no incoming edges. Formally,
roots(B) = {v ∈ VB | ¬∃u ∈ VB : (u, v) ∈ EB } .
After translating every node in the network, we remove them from the graph,
i.e. every root becomes an input, and proceed with the translation until all nodes
have been removed. More precisely, given a set of nodes S ⊆ V , the extended
BN B \ S obtained by removing S from B is defined as
B \ S = (V \ S, I ∪ S, E \ (V × S ∪ S × V ), dep, cpt) .
With these auxiliary definitions readily available, an extended BN B is translated
into a BNL program as follows:


if roots(B) = {r1 , . . . , rm } = V
blockB (r1 ); . . . ; blockB (rm )
BNL(B) =
blockB (r1 ); . . . ; blockB (rm ); if roots(B) = {r1 , . . . , rm } $ V


BNL(B \ roots(B))

Step 3 To complete the translation, it remains to account for observations. Let
cond : V → Vals ∪ {⊥} be a function mapping every node either to an observed
value in Vals or to ⊥. The former case is interpreted as an observation that node
v has value cond(v). Otherwise, i.e. if cond(v) = ⊥, the value of node v is not
observed. We collect all observed nodes in the set O = {v ∈ V | cond(v) 6= ⊥}.
It is then natural to incorporate conditioning into our translation by applying
rejection sampling: We repeatedly execute a BNL program until every observed
node has the desired value cond(v). In the presence of observations, we translate
the extended BN B into a BNL program as follows:
!
^
BNL(B, cond) = repeat {BNL(B)} until
xv = cond(v)
v∈O

Example 8. Consider, again, the BN B depicted in Figure 3. Moreover, assume
we observe P = 1. Hence, the conditioning function cond is given by cond(P ) = 1
and cond(v) = ⊥ for v ∈ {D, G, M }. Then the translation of B and cond, i.e.
BNL(B, cond), is the BNL program Cmood depicted in Figure 4.
△
Since our translation yields a BNL program for any given BN, we can compositionally compute a closed form for the expected simulation time of a BN. This
is an immediate consequence of Corollary 1.

23

1

10

repeat {

} else {

2

xD :≈ 0.6 · h0i + 0.4 · h1i;

11

3

xP :≈ 0.7 · h0i + 0.3 · h1i

12

};

4

if (xD = 0 ∧ xP = 0) {

13

if (xG = 0) {

5
6
7
8
9

xG :≈ 0.95 · h0i + 0.05 · h1i
} else if (xD = 1 ∧ xP = 1) {
xG :≈ 0.05 · h0i + 0.95 · h1i
} else if (xD = 0 ∧ xP = 1) {
xG :≈ 0.5 · h0i + 0.5 · h1i

xG :≈ 0.6 · h0i + 0.4 · h1i

14
15

xM :≈ 0.9 · h0i + 0.1 · h1i
} else {

16
17
18

xM :≈ 0.3 · h0i + 0.7 · h1i
}
} until (xP = 1)

Fig. 4. The BNL program Cmood obtained from the BN in Figure 3.

We still have to prove, however, that our translation is sound, i.e. the conditional joint probabilities inferred from a BN coincide with the (conditional)
joint probabilities from the corresponding BNL program. Formally, we obtain
the following soundness result.
Theorem 6 (Soundness of Translation). Let B = (V, I, E, Vals, dep, cpt) be
a BN and cond : V → Vals ∪ {⊥} be a function determining the observed nodes.
For each node and input v, let v ∈ Vals be a fixed value associated with v. In
particular, we set v = cond(v) for each observed node v ∈ O. Then



V
^
Pr v∈V v = v





V
xv = v
wp JBNL(B, cond)K
=
.
Pr o∈O o = o
v∈V \O

Proof. Without conditioning, i.e. O = ∅, the proof proceeds by induction on the
number of nodes of B. With conditioning, we additionally apply Theorems 3
and 5 to deal with loops introduced by observed nodes. See Appendix A.7. ⊓
⊔

Example 9 (Expected Sampling Time of a BN). Consider, again, the BN B in
Figure 3. Moreover, recall the corresponding program Cmood derived from B
in Figure 4, where we observed P = 1. By Theorem 6 we can also determine
the probability that a student who got a bad grade in an easy exam was well–
prepared by means of weakest precondition reasoning. This yields
wp JCmood K ([xD = 0 ∧ xG = 0 ∧ xM = 0])
=

Pr (D = 0, G = 0, M = 0, P = 1)
= 0.27 .
Pr (P = 1)

Furthermore, by Corollary 1, it is straightforward to determine the expected
time to obtain a single sample of B that satisfies the observation P = 1:
ert JCmood K (0) =

1 + ert JCloop-body K (0)
= 23.4 + 1/15 = 23.46̄ .
wp JCloop-body K ([P = 1])

△

24

6

Implementation

We implemented a prototype in Java to analyze expected sampling times of
Bayesian networks. More concretely, our tool takes as input a BN together with
observations in the popular Bayesian Network Interchange Format.6 The BN is
then translated into a BNL program as shown in Section 5. Our tool applies the
ert–calculus together with our proof rules developed in Section 4 to compute the
exact expected runtime of the BNL program.
The size of the resulting BNL program is linear in the total number of rows
of all conditional probability tables in the BN. The program size is thus not the
bottleneck of our analysis. As we are dealing with an NP–hard problem [11,12],
it is not surprising that our algorithm has a worst–case exponential time complexity. However, also the space complexity of our algorithm is exponential in
the worst case: As an expectation is propagated backwards through an if–clause
of the BNL program, the size of the expectation is potentially multiplied. This
is also the reason that our analysis runs out of memory on some benchmarks.
We evaluated our implementation on the largest BNs in the Bayesian Network Repository [45] that consists — to a large extent — of real–world BNs
including expert systems for, e.g., electromyography (munin) [2], hematopathology diagnosis (hepar2) [41], weather forecasting (hailfinder) [1], and printer
troubleshooting in Windows 95 (win95pts) [44, Section 5.6.2]. For a evaluation
of all BNs in the repository, see Appendix.
All experiments were performed on an HP BL685C G7. Although up to 48
cores with 2.0GHz were available, only one core was used apart from Java’s
garbage collection. The Java virtual machine was limited to 8GB of RAM.
Our experimental results are shown in Table 3. The number of nodes of the
considered BNs ranges from 56 to 1041. For each Bayesian network, we computed
the expected sampling time (EST) for different collections of observed nodes
(#obs). Furthermore, Table 3 provides the average Markov Blanket size, i.e.
the average number of parents, children and children’s parents of nodes in the
BN [42], as an indicator measuring how independent nodes in the BN are.
Observations were picked at random. Note that the time required by our
prototype varies depending on both the number of observed nodes and the actual
observations. Thus, there are cases in which we run out of memory although the
total number of observations is small.
In order to obtain an understanding of what the EST corresponds to in actual execution times on a real machine, we also performed simulations for the
win95pts network. More precisely, we generated Java programs from this network analogously to the translation in Section 5. This allowed us to approximate
that our Java setup can execute 9.714 · 106 steps (in terms of EST) per second.
For the win95pts with 17 observations, an EST of 1.11·1015 then corresponds
to an expected time of approximately 3.6 years in order to obtain a single valid
sample. We were additionally able to find a case with 13 observed nodes where
6

http://www.cs.cmu.edu/~ fgcozman/Research/InterchangeFormat/

25

our tool discovered within 0.32 seconds an EST that corresponds to approximately 4.3 million years. In contrast, exact inference using variable elimination
was almost instantaneous. This demonstrates that knowing expected sampling
times upfront can indeed be beneficial when selecting an inference method.

7

Conclusion

We presented a syntactic notion of independent and identically distributed probabilistic loops and derived dedicated proof rules to determine exact expected outcomes and runtimes of such loops. These rules do not require any user–supplied
information, such as invariants, (super)martingales, etc.
Moreover, we isolated a syntactic fragment of probabilistic programs that
allows to compute expected runtimes in a highly automatable fashion. This fragment is non–trivial: We show that all Bayesian networks can be translated into
programs within this fragment. Hence, we obtain an automated formal method
for computing expected simulation times of Bayesian networks. We implemented
this method and successfully applied it to various real–world BNs that stem
from, amongst others, medical applications. Remarkably, our tool was capable
of proving extremely large expected sampling times within seconds.
There are several directions for future work: For example, there exist subclasses of BNs for which exact inference is in P, e.g. polytrees. Are there analogies
for probabilistic programs? Moreover, it would be interesting to consider more
complex graphical models, such as recursive BNs [15].

References
1. Abramson, B., Brown, J., Edwards, W., Murphy, A., Winkler, R.L.: Hailfinder: A
Bayesian System for Forecasting Severe Weather. International Journal of Forecasting 12(1), 57–71 (1996)
2. Andreassen, S., Jensen, F.V., Andersen, S.K., Falck, B., Kjærulff, U., Woldbye, M.,
Sørensen, A., Rosenfalck, A., Jensen, F.: MUNIN: An Expert EMG Assistant. In:
Computer–aided Electromyography and Expert Systems, pp. 255–277. Pergamon
Press (1989)
3. Bishop, C.: Pattern Recognition and Machine Learning. Springer (2006)
4. Bournez, O., Garnier, F.: Proving Positive Almost–Sure Termination. In: RTA.
LNCS, vol. 3467, pp. 323–337. Springer (2005)
5. Brázdil, T., Kiefer, S., Kucera, A., Vareková, I.H.: Runtime Analysis of Probabilistic Programs with Unbounded Recursion. J. Comput. Syst. Sci. 81(1), 288–310
(2015)
6. Celiku, O., McIver, A.: Compositional Specification and Analysis of Cost–based
Properties in Probabilistic Programs. In: FM. LNCS, vol. 3582, pp. 107–122.
Springer (2005)
7. Chakarov, A., Sankaranarayanan, S.: Probabilistic Program Analysis with Martingales. In: CAV. LNCS, vol. 8044, pp. 511–526. Springer (2013)
8. Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic Analysis of
Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In: POPL. pp. 327–342. ACM (2016)

26
9. Chatterjee, K., Novotný, P., Zikelic, D.: Stochastic Invariants for Probabilistic
Termination. In: POPL. pp. 145–160. ACM (2017)
10. Constantinou, A.C., Fenton, N.E., Neil, M.: pi–football: A Bayesian Network Model
for Forecasting Association Football Match Outcomes. Knowl.–Based Syst. 36,
322–339 (2012)
11. Cooper, G.F.: The Computational Complexity of Probabilistic Inference Using
Bayesian Belief Networks. Artif. Intell. 42(2-3), 393–405 (1990)
12. Dagum, P., Luby, M.: Approximating Probabilistic Inference in Bayesian Belief
Networks is NP–Hard. Artif. Intell. 60(1), 141–153 (1993)
13. Dijkstra, E.W.: Guarded Commands, Nondeterminacy and Formal Derivation of
Programs. Communications of the ACM 18(8), 453–457 (1975)
14. Dijkstra, E.W.: A Discipline of Programming. Prentice–Hall (1976)
15. Etessami, K., Yannakakis, M.: Recursive Markov Chains, Stochastic Grammars,
and Monotone Systems of Nonlinear Equations. JACM 56(1), 1:1–1:66 (2009)
16. Fioriti, L.M.F., Hermanns, H.: Probabilistic Termination: Soundness, Completeness, and Compositionality. In: POPL. pp. 489–501. ACM (2015)
17. Friedman, N., Linial, M., Nachman, I., Pe’er, D.: Using Bayesian Networks to
Analyze Expression Data. In: RECOMB. pp. 127–135. ACM (2000)
18. Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower Runtime Bounds
for Integer Programs. In: IJCAR 2016. pp. 550–567 (2016)
19. Goodman, N.D.: The Principles and Practice of Probabilistic Programming. In:
POPL. pp. 399–402. ACM (2013)
20. Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.:
Church: A Language for Generative Models. In: UAI. pp. 220–229. AUAI Press
(2008)
21. Gordon, A.D., Graepel, T., Rolland, N., Russo, C.V., Borgström, J., Guiver, J.:
Tabular: A Schema–Driven Probabilistic Programming Language. In: POPL. pp.
321–334. ACM (2014)
22. Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic Programming. In: Future of Software Engineering. pp. 167–181. ACM (2014)
23. Heckerman, D.: A Tutorial on Learning with Bayesian Networks. In: Innovations
in Bayesian Networks, Studies in Computational Intelligence, vol. 156, pp. 33–82.
Springer (2008)
24. Hehner, E.C.R.: A Probability Perspective. Formal Aspects of Computing 23(4),
391–419 (2011)
25. Hoffman, M.D., Gelman, A.: The No–U–turn Sampler: Adaptively Setting Path
Lengths in Hamiltonian Monte Carlo. Journal of Machine Learning Research 15(1),
1593–1623 (2014)
26. Jiang, X., Cooper, G.F.: A Bayesian Spatio–temporal Method for Disease Outbreak
Detection. JAMIA 17(4), 462–471 (2010)
27. Kaminski, B.L., Katoen, J.: On the Hardness of Almost–Sure Termination. In:
MFCS. LNCS, vol. 9234, pp. 307–318. Springer (2015)
28. Kaminski, B.L., Katoen, J.: A Weakest Pre–expectation Semantics for Mixed–sign
Expectations. In: LICS (2017)
29. Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest Precondition Reasoning for Expected Run–times of Probabilistic Programs. In: ESOP. LNCS, vol.
9632, pp. 364–389. Springer (2016)
30. Koller, D., Friedman, N.: Probabilistic Graphical Models - Principles and Techniques. MIT Press (2009)
31. Kozen, D.: Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22(3), 328–
350 (1981)

27
32. Kozen, D.: A Probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985)
33. Lassez, J.L., Nguyen, V.L., Sonenberg, L.: Fixed Point Theorems and Semantics:
A Folk Tale. Information Processing Letters 14(3), 112–116 (1982)
34. McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2004)
35. Minka, T., Winn, J.: Infer.NET (2017), http://infernet.azurewebsites.net/,
Accessed online October 17
36. Minka, T., Winn, J.M.: Gates. In: NIPS. pp. 1073–1080. Curran Associates (2008)
37. Monniaux, D.: An Abstract Analysis of the Probabilistic Termination of Programs.
In: SAS. LNCS, vol. 2126, pp. 111–126. Springer (2001)
38. Neapolitan, R.E., Jiang, X.: Probabilistic Methods for Financial and Marketing
Informatics. Morgan Kaufmann (2010)
39. Nori, A.V., Hur, C., Rajamani, S.K., Samuel, S.: R2: An Efficient MCMC Sampler
for Probabilistic Programs. In: AAAI. pp. 2476–2482. AAAI Press (2014)
40. Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about Recursive
Probabilistic Programs. In: LICS. pp. 672–681. ACM (2016)
41. Onisko, A., Druzdzel, M.J., Wasyluk, H.: A Probabilistic Causal Model for Diagnosis of Liver Disorders. In: Proceedings of the Seventh International Symposium
on Intelligent Information Systems (IIS–98). pp. 379–387 (1998)
42. Pearl, J.: Bayesian Networks: A Model of Self–activated Memory for Evidential
Reasoning. In: Proc. of CogSci. pp. 329–334 (1985)
43. Pfeffer, A.: Figaro: An Object–oriented Probabilistic Programming Language.
Charles River Analytics Technical Report 137, 96 (2009)
44. Ramanna, S., Jain, L.C., Howlett, R.J.: Emerging paradigms in machine learning.
Springer (2013)
45. Scutari, M.: Bayesian Network Repository. URL http://www.bnlearn.com (2017)
46. Sharir, M., Pnueli, A., Hart, S.: Verification of Probabilistic Programs. SIAM J.
Comput. 13(2), 292–314 (1984)
47. Wood, F., van de Meent, J., Mansinghka, V.: A New Approach to Probabilistic
Programming Inference. In: AISTATS. JMLR Workshop and Conference Proceedings, vol. 33, pp. 1024–1032. JMLR.org (2014)
48. Yuan, C., Druzdzel, M.J.: Importance Sampling Algorithms for Bayesian Networks: Principles and Performance. Mathematical and Computer Modelling 43(910), 1189–1207 (2006)
49. Zweig, G., Russell, S.J.: Speech Recognition with Dynamic Bayesian Networks. In:
AAAI/IAAI. pp. 173–180. AAAI Press / The MIT Press (1998)

28

BN

#obs

earthquake #nodes:
0
cancer
#nodes:
0
survey
#nodes:
0
asia
#nodes:
0
sachs
#nodes:
0
insurance #nodes:
0
alarm
#nodes:
0
barley
#nodes:
0
hailfinder #nodes:
0
hepar2
#nodes:
0
win95pts #nodes:
0
7
pathfinder #nodes:
0
5
andes
#nodes:
0
5
pigs
#nodes:
0
5
munin
#nodes:
0
5

Time

EST

#obs

Time

EST

5, #edges: 4, avg. Markov Blanket: 2.00
0.09 8.000 · 100
2
0.23 9.276 · 101
5, #edges: 4, avg. Markov Blanket: 2.00
0.09 8.000 · 100
2
0.22 1.839 · 101
6, #edges: 6, avg. Markov Blanket: 2.67
0.09 1.000 · 101
2
0.21 2.846 · 102
8, #edges: 8, avg. Markov Blanket: 2.50
0.26 1.400 · 101
2
0.25 3.368 · 102
11, #edges: 17, avg. Markov Blanket: 3.09
0.13 2.000 · 101
3
0.24 7.428 · 102
27, #edges: 52, avg. Markov Blanket: 5.19
0.17 5.200 · 101
3
0.31 5.096 · 103
37, #edges: 46, avg. Markov Blanket: 3.51
0.14 6.200 · 101
2
MO —
48, #edges: 84, avg. Markov Blanket: 5.25
0.46 8.600 · 101
2
0.53 5.246 · 104
56, #edges: 66, avg. Markov Blanket: 3.54
0.23 9.500 · 101
5
0.63 5.016 · 105
70, #edges: 123, avg. Markov Blanket: 4.51
0.22 1.310 · 102
1
1.84 1.579 · 102
76, #edges: 112, avg. Markov Blanket: 5.92
0.20 1.180 · 102
1
0.36 2.284 · 103
12
0.42 3.973 · 107
0.91 1.876 · 106
135, #edges: 200, avg. Markov Blanket: 3.04
0.37 217
1
0.53 1.050 · 104
MO —
7
5.44 ∞
223, #edges: 338, avg. Markov Blanket: 5.61
0.46 3.570 · 102
1
MO —
1.41 9.862 · 103
7
0.99 8.904 · 104
441, #edges: 592, avg. Markov Blanket: 3.66
0.57 7.370 · 102
1
0.74 2.952 · 103
5
0.85 1.260 · 10
7
1.02 1.511 · 106
1041, #edges: 1397, avg. Markov Blanket: 3.54
1.29 1.823 · 103
1
1.47 3.648 · 104
1.43 ∞
9
1.79 1.824 · 1016

#obs

Time

EST

4

0.24

1.857 · 102

5

0.20

5.639 · 102

5

0.22

9.113 · 103

6

0.25

8.419 · 104

6

2.72

5.533 · 107

5

0.91

1.373 · 105

6

40.47

3.799 · 105

5

MO

—

9

0.46

9.048 · 106

2

MO

—

3
17

0.36
61.73

4.296 · 105
1.110 · 1015

3
7

31.31
480.83

2.872 · 104
∞

3
9

1.66
0.90

5.251 · 103
6.637 · 105

3
8

0.88
MO

2.362 · 103
—

3
10

1.37
65.64

1.824 · 107
1.153 · 1018

Table 3. Experimental results. Time is in seconds. MO denotes out of memory.

29

A
A.1

Appendix
Calculation for Expected Sampling Time of Example Network

Let B denote the Bayesian Network shown in Figure 1. We denote the nodes
by R, S, and G, respectively. Since we want to condition G to value 0, let
cond(G) = 0, cond(R) = ⊥, and cond(S) = ⊥. According to the translation
from Bayesian Networks to BNL programs presented in Section 5.1, we obtain
the following program BNL(B, cond):
repeat{
// translation of node R, denoted blockB (R, cond)
xR :≈ a · h0i + (1 − a) · h1i;
// translation of node S, denoted blockB (S, cond)
if (xR = 0) {
xS :≈ a · h0i + (1 − a) · h1i
} else {
xS :≈ 0.2 · h0i + 0.8 · h1i};
// translation of node G, denoted blockB (G, cond)
if (xS = 0 ∧ xR = 0) {
xG :≈ 0.01 · h0i + (0.99 · h1i
} else if (xS = 0 ∧ xR = 1) {
xG :≈ 0.25 · h0i + (0.75 · h1i
} else if (xS = 1 ∧ xR = 0) {
xG :≈ 0.9 · h0i + (0.1 · h1i
} else {
xG :≈ 0.2 · h0i + (0.8 · h1i}
}until (xG = 0) //condition node G to value 0
Thus we have
ert JBNL(B, cond)K (0)

= ert Jrepeat {blockB (R, cond); blockB (S, cond); blockB (G, cond)} until (xG = 0)K (0) .

Let C denote the body of the above loop. Theorem 5 then yields
ert Jrepeat {C} until (xG = 0)K (0) =

1 + ert JCK (0)
.
wp JCK ([xG = 0])

We first compute ert JCK (0) = ert JblockB (R, cond); blockB (S, cond); blockB (G, cond)K (0).
We have
ert JblockB (G, cond)K (0) = 2 + [xS 6= 0 ∨ xR 6= 0] · (1 + [xS 6= 0 ∨ xR 6= 0]) ,

30

thus
18
+ [xR = 0] ·
ert JblockB (S, cond)K (ert JblockB (G, cond)K (0)) =
5



2
− 2a
5



,

and finally
ert JCK (0)

= ert JblockB (R, cond)K (ert JblockB (S, cond)K (ert JblockB (G, cond)K (0)))
2
18
= − 2a2 + a +
.
5
5

Next, we determine wp JCK ([xG = 0]) and therefore calculate
wp JblockB (G, cond)K ([xG = 0]) = 0.01 · [xS = 0 ∧ xR = 0] + 0.25 · [xS = 0 ∧ xR = 1]

+ 0.9 · [xS = 1 ∧ xR = 0] + 0.2 · [xS = 1 ∧ xR = 1] ,

and
wp JblockB (S, cond)K (wp JblockB (G, cond)K (0))


89
69
21
,
+ [xR = 0] · −
a+
=
100
100
100
thus we finally obtain
wp JCK ([xG = 0])
= wp JblockB (R, cond)K (wp JblockB (S, cond)K (wp JblockB (G, cond)K ([xG = 0])))
89 2
69
21
= −
a +
a+
.
100
100
100
Overall, by applying some simple algebra, we get
ert Jrepeat {C} until (xG = 0)K (0) =
A.2

200a2 − 40a − 460
.
89a2 − 69a − 21

Proof of Lemma 1

Proof. By induction on the structure of C. As the induction base we have the
atomic programs:
skip: We have
wp JskipK (g · f ) = g · f = g · wp JskipK (f ) .

(by Table 1)

empty: Analogous to skip.
diverge: We have
wp JdivergeK (g · f ) = 0 = g · wp JdivergeK (f ) .

(by Table 1)

31

x :≈ µ: We have
Z

.
Z
= λσ .

. (f · g)[x/v] dµ

λv . f [x/v] · g dµ


= g · λσ

Z

wp Jx :≈ µK (g · f ) = λσ

λv

Q

σ

(by Table 1)

σ

Q

.

λv
Q

.

= g · wp Jx :≈ µK (f ) .

(g 6⋓ (x :≈ µ) by assumption)


f [x/v] dµσ

As the induction hypothesis we now assume that for arbitrary but fixed C1 , C2 ∈
pGCL and all f, g ∈ E with g 6⋓ C1 and g 6⋓ C2 it holds that both
wp JC1 K (g · f ) = g · wp JC1 K (f )
and
wp JC2 K (g · f ) = g · wp JC2 K (f ) .
if (ϕ) {C1 } else {C2 }: We have
wp Jif (ϕ) {C1 } else {C2 }K (g · f )
= [ϕ] · wp JC1 K (g · f ) + [¬ϕ] · wp JC2 K (g · f )

= [ϕ] · g · wp JC1 K (f ) + [¬ϕ] · wp JC2 K (g · f )
= [ϕ] · g · wp JC1 K (f ) + [¬ϕ] · g · wp JC2 K (f )

(by Table 1)
(g ⋓
6 C1 and I.H. on C1 )
(g ⋓
6 C2 and I.H. on C2 )

= g · ([ϕ] · wp JC1 K (f ) + [¬ϕ] · wp JC2 K (f ))
= g · wp Jif (ϕ) {C1 } else {C2 }K (f ) .

(by Table 1)

C1 ; C2 : We have
wp JC1 ; C2 K (g · f ) = wp JC1 K (wp JC2 K (g · f ))

= wp JC1 K (g · wp JC2 K (f ))
= g · wp JC1 K (wp JC2 K (f ))

(by Table 1)
(g ⋓
6 C2 and I.H. on C2 )
(g ⋓
6 C1 and I.H. on C1 )

= g · wp JC1 ; C2 K (f ) .

(by Table 1)

while (ϕ) {C1 }: This case is more involved. Recall that
wp Jwhile (ϕ) {C1 }K (h) = sup Fhn (0)

(2)

n∈N

holds for all h ∈ E. Thus we show
n
Fg·f
(0) = g · Ffn (0)

(3)

32

for all n ∈ N, which implies the desired result. We proceed by induction on n.
Induction base n = 0. We have
Ff0·g (0) = 0 = g · 0 = g · Ff0 (0) .
Induction Hypothesis: Equation 3 holds for some arbitrary but fixed n ∈ N.
Induction Step n 7→ n + 1. We have
!

n+1
Ffn+1
(0)
·g (0) = g · Ff

iff
iff
iff
iff
iff
iff

Ff ·g (Ffn·g (0)) = g · Ff (Ffn (0))


[¬ϕ] · f · g + wp JC1 K Ffn·g (0) = g · [¬ϕ] · f + wp JC1 K Ffn (0)
(by Definition 2)


n
n
wp JC1 K Ff ·g (0) = g · wp JC1 K Ff (0)


wp JC1 K g · Ffn (0) = g · wp JC1 K Ffn (0)
(by I.H.)


n
n
g · wp JC1 K Ff (0) = g · wp JC1 K Ff (0)
(by g 6⋓ C1 and I.H. on C1 )
true .

repeat {ϕ} until (C1 ): We have
wp Jrepeat {C1 } until (ϕ)K (g · f )

= wp JC1 ; while (ϕ) {C1 }K (g · f )
= wp JC1 K (wp Jwhile (ϕ) {C1 }K (g · f ))

(by Table 1)

= wp JC1 K (g · wp Jwhile (ϕ) {C1 }K (f ))

(see case while (ϕ) {C1 })

= g · wp JC1 K (wp Jwhile (ϕ) {C1 }K (f ))
= g · wp Jrepeat {C1 } until (ϕ)K (f ) .

(g 6⋓ C1 and I.H. on C1 )
(by Table 1)
⊓
⊔

A.3

Proof of Lemma 2

Proof. By induction on n. We consider the cases n = 1 and n = 2 as the
induction base. For n = 1, we have
Ff1 (0) = [ϕ] · wp JCK (0) + [¬ϕ] · f
= [ϕ] · 0 + [¬ϕ] · f

(by Definition 2)
(by strictness, see Theorem 1 (2))

= [¬ϕ] · f

(†)

= [ϕ] · 0 + [¬ϕ] · f
= [ϕ] · wp JCK ([¬ϕ] · f ) ·

−1
X
i=0

|

i

wp JCK ([ϕ])
{z

=0

!
}

+ [¬ϕ] · f .

33

For n = 2, we have

Ff2 (0) = [ϕ] · wp JCK Ff1 (0) + [¬ϕ] · f

(by Definition 2)

= [ϕ] · wp JCK ([¬ϕ] · f ) + [¬ϕ] · f

= [ϕ] · wp JCK ([¬ϕ] · f ) ·

0
X

(by †)
i

wp JCK ([ϕ])

i=0

!

{z

|

+ [¬ϕ] · f .

}

=1

Before we perform the inductive step, observe the following equality implied by
Lemma 1, which holds for all n ∈ N:
!
n−2
X
i
wp JCK ([ϕ])
wp JCK [ϕ] · wp JCK ([¬ϕ] · f ) ·
i=0

=

n−2
X

wp JCK [ϕ] · wp JCK ([¬ϕ] · f ) · wp JCK ([ϕ])

n−2
X

wp JCK ([ϕ] · wp JCK ([¬ϕ] · f )) · wp JCK ([ϕ])

n−2
X

wp JCK ([ϕ]) · wp JCK ([¬ϕ] · f ) · wp JCK ([ϕ])

i=0

=

i=0

=

i=0



i



(by linearity, see Theorem 1 (1))
i

(by Lemma 1, wp JCK ([ϕ]) 6⋓ C)
i

= wp JCK ([¬ϕ] · f ) ·

n−1
X
i=1

(by Lemma 1, wp JCK ([¬ϕ] · f ) 6⋓ C)
wp JCK ([ϕ])i

(‡)

As induction hypothesis, we now assume that the lemma holds for some arbitrary
but fixed n ∈ N \ {0}. Then
Ffn+1 (0)

= [ϕ] · wp JCK Ffn (0) + [¬ϕ] · f

= [ϕ] · wp JCK [ϕ] · wp JCK ([¬ϕ] · f ) ·
+ [¬ϕ] · f
= [ϕ] · wp JCK [ϕ] ·wp JCK ([¬ϕ] ·f ) ·
+ [¬ϕ] ·f

= [ϕ] · wp JCK ([¬ϕ] ·f ) ·

n−1
X
i=1

n−2
X

wp JCK ([ϕ])

i=0

n−2
X
i=0

i

wp JCK ([ϕ])

i

wp JCK ([ϕ])

i

!

!

(by Definition 2)
!

+ [¬ϕ] · f

(by I.H.)
!

+ wp JCK ([¬ϕ] ·f )

(by linearity, see Theorem 1 (1))
!
!
+ wp JCK ([¬ϕ] ·f )

+ [¬ϕ] ·f

(by Lemma 1, wp JCK ([¬ϕ] · f ) 6⋓ C, wp JCK ([ϕ]) 6⋓ C, and [ϕ] · [ϕ] = [ϕ])

34

= [ϕ] ·

A.4

n−1
X

wp JCK ([¬ϕ] · f ) ·

i=0

i

wp JCK ([ϕ])

!

+ [¬ϕ] · f .

⊓
⊔

Proof of Theorem 3

Proof. We have
wp Jwhile (ϕ) {C}K (f )
= sup Ffn (0)

(by Definition 2)

n∈N

= sup [ϕ] · wp JCK ([¬ϕ] · f ) ·
n∈N

= [ϕ] · wp JCK ([¬ϕ] · f ) ·

ω
X

n−2
X
i=0

i

wp JCK ([ϕ])
i

wp JCK ([ϕ])

i=0

!

!

+ [¬ϕ] · f (by Lemma 2)

+ [¬ϕ] · f .

(†)

† is to be evaluated in some state σ for which we have two cases: The first case
is
wp JCK ([ϕ]) (σ) < 1. Using the closed form of the geometric series, i.e.
Pwhen
ω
1
q
=
i=0
1−q if |q| < 1, we get
[ϕ] (σ) · wp JCK ([¬ϕ] · f ) (σ) ·
= [ϕ] (σ) ·

ω
X
i=0

i

wp JCK ([ϕ]) (σ)

!

+ [¬ϕ] (σ) · f (σ)
(† instantiated in σ)

wp JCK ([¬ϕ] · f ) (σ)
+ [¬ϕ] (σ) · f (σ) .
1 − wp JCK ([ϕ]) (σ)
(closed form of geometric series)

The second case is when wp JCK ([ϕ]) (σ) = 1. This can only be true if every
state τ that is reachable with non–zero probability by executing C on σ has to
satisfy ϕ. Otherwise, the integral would not add up to exactly 1. Formally,
Z
wp JCK ([ϕ]) (σ) = 1 iff
[ϕ] dJCKσ = 1
Σ

iff ∀ JCKσ (τ ) > 0 =⇒ [ϕ] (τ ) = 1

(‡)

From that, it follows that
wp JCK ([¬ϕ] · f ) (σ) =

Z

Σ

[¬ϕ] · f dJCKσ =
=

Z

ZΣ

Σ

=

Z

Σ

f − [ϕ] · f dJCKσ
f − 1 · f dJCKσ
0 dJCKσ = 0

(by ‡)
(⋆)

35

We then get
[ϕ] (σ) · wp JCK ([¬ϕ] · f ) (σ) ·

ω
X
i=0

i

wp JCK ([ϕ]) (σ)

!

+ [¬ϕ] (σ) · f (σ)
(instantiate † in σ)

= [ϕ] (σ) · 0 · ∞ + [¬ϕ] (σ) · f (σ)
= [ϕ] (σ) · 0 + [¬ϕ] (σ) · f (σ)
0
= [ϕ] (σ) · + [¬ϕ] (σ) · f (σ)
0
wp JCK ([¬ϕ] · f ) (σ)
= [ϕ] (σ) ·
+ [¬ϕ] (σ) · f (σ) .
1 − wp JCK ([ϕ]) (σ)

(by ⋆)
(by 0 · ∞ = 0)
0
0

(by

= 0)

(Case 2)
⊓
⊔

For both cases we get the desired form which completes the proof.
A.5

ert Orbits of f –i.i.d. Loops w.r.t. Postruntime 0

Lemma 4 (ert Orbits of 0–i.i.d. Loops). Let C ∈ pGCL, ϕ be a guard, f ∈ E
such that the loop while (ϕ) {C} is 0–i.i.d., and let F0 be the corresponding ert–
characteristic function. Furthermore, assume
wp JCK (1) = 1

(4)

ert JCK (0) 6⋓ C .

(5)

and
Then the orbit of F0 is given by
F0n (0) = 1 + [ϕ] ·

ert JCK (0) ·

n−1
X
i=0

i

wp JCK ([ϕ])

+

n−2
X
i=0

i

wp JCK ([ϕ])

!

for n ≥ 1.
Proof. By induction on n. For the induction base, we have n = 1:
F0 (0) = 1 + [ϕ] · ert JCK (0)
= 1 + [ϕ] ·

ert JCK (0) ·

0
X
i=0

wp JCK ([ϕ])

i

+

−1
X
i=0

i

wp JCK ([ϕ])

!

The second induction base is n = 2:
F02 (0) = 1 + [ϕ] · ert JCK (1 + [ϕ] · ert JCK (0))
= 1 + [ϕ] · (ert JCK (0) + wp JCK (1 + [ϕ] · ert JCK (0))) (by Theorem 2)
= 1 + [ϕ] · (ert JCK (0) + wp JCK (1) + wp JCK ([ϕ] · ert JCK (0)))
(by linearity, see Theorem 1 (1))

= 1 + [ϕ] · (ert JCK (0) + 1 + wp JCK ([ϕ] · ert JCK (0))) (by Equation 4)

36

= 1 + [ϕ] · (ert JCK (0) + 1 + wp JCK ([ϕ]) · ert JCK (0))
(by Lemma 1, ert JCK (0) 6⋓ C)
!
0
1
X
X
i
i
.
wp JCK ([ϕ])
wp JCK ([ϕ]) +
= 1 + [ϕ] · ert JCK (0) ·
i=0

i=0

Before we prove the induction step, observe the following: Lemma 1 yields
!
n
X
i
wp JCK [ϕ] · ert JCK (0) ·
wp JCK ([ϕ])
i=0

=

n
X

wp JCK [ϕ] · ert JCK (0) · wp JCK ([ϕ])

n
X

wp JCK ([ϕ] · ert JCK (0)) · wp JCK ([ϕ])

n
X

wp JCK ([ϕ]) · ert JCK (0) · wp JCK ([ϕ])

i=0

=

i=0

=

i=0



i



(by linearity, see Theorem 1 (1))
i

(by Lemma 1, wp JCK ([ϕ]) 6⋓ C)
i

= ert JCK (0) ·

n+1
X
i=1

(by Lemma 1, ert JCK (0) 6⋓ C)

i

wp JCK ([ϕ]) .

(6)

Lemma 1 implies further
wp JCK [ϕ] ·
=
=
=

n
X

i=0
n
X

i=0
n+1
X
i=1

n
X
i=0

i

wp JCK ([ϕ])

!



i
wp JCK [ϕ] · wp JCK ([ϕ])
i

wp JCK ([ϕ]) · wp JCK ([ϕ])

(by linearity, see Theorem 1 (1))
(by Lemma 1, wp JCK ([ϕ]) 6⋓ C)

i

wp JCK ([ϕ]) .

(7)

We are now in a position two show that F0 (In ) = In+1 holds. We have
F0n+1 (0)
= 1 + [ϕ] · ert JCK (F0n (0))

= 1 + [ϕ] · (ert JCK (0) + wp JCK (F0n (0)))
= 1 + [ϕ] ·

ert JCK (0)

(by Theorem 2)

37

+ wp JCK 1 + [ϕ] ·

= 1 + [ϕ] ·

ert JCK (0) ·

wp JCK ([ϕ])

n−2
X

+

wp JCK ([ϕ])

i=0

i

!!!

(by I.H. on n)

n−1
X
i=0

wp JCK ([ϕ])

i

+ [ϕ] ·

n−2
X

n−2
X
i=0

i

wp JCK ([ϕ])

i

wp JCK ([ϕ])

i=0

ert JCK (0) + wp JCK (1) + wp JCK [ϕ] · ert JCK (0) ·
+ wp JCK [ϕ] ·

= 1 + [ϕ] ·

i=0

i

ert JCK (0)

+ wp JCK 1 + [ϕ] · ert JCK (0) ·
= 1 + [ϕ] ·

n−1
X

!!

n−1
X
i=0

!!
i

wp JCK ([ϕ])

(by linearity, see Theorem 1 (1))
!
n−1
X
i
wp JCK ([ϕ])
ert JCK (0) + 1 + wp JCK [ϕ] · ert JCK (0) ·
i=0

+ wp JCK [ϕ] ·
= 1 + [ϕ] ·

n−1
X
i=1

A.6

n−2
X
i=0

wp JCK ([ϕ])i

ert JCK (0) ·

n
X
i=0

n
X
i=1

wp JCK ([ϕ])

!

wp JCK ([ϕ])

n
X
i=1

!!

(by Equation 4)
i

wp JCK ([ϕ])

i

ert JCK (0) + 1 + ert JCK (0) ·
+

= 1 + [ϕ] ·

i=0

i

wp JCK ([ϕ])

ert JCK (0) + 1 + ert JCK (0) ·
+ wp JCK [ϕ] ·

= 1 + [ϕ] ·

n−2
X

!!

(by Equation 6)

wp JCK ([ϕ])i
(by Equation 7)

i

+

n−1
X
i=0

i

wp JCK ([ϕ])

!

.

⊓
⊔

Proof of Lemma 3

Proof of Lemma 3.1
Proof. We prove a stronger statement: For all sequences Seq ∈ BNL and all g ∈ E
it holds that
Vars (wp JSeqK (g)) = Vars (g) \ Mod (Seq) .
(8)

It then follows that Vars (wp JSeqK (g)) ∩ Mod (Seq) = ∅ and hence wp JSeqK (g) 6⋓
Seq by definition. Note that every sequence Seq ∈ BNL is of the form Bxi 1 ; . . . ; Bxi n

!

38

for some n ≥ 1, where each Bxi j is a block. Given a program C ∈ pGCL, let
VarsGuard (C) denote the the set of variables occurring in a guard in C. A straightforward induction on the structure of a block Bxi ∈ BNL yields
Vars (wp JBxi K (g)) = (VarsGuard (Bxi ) ∪ Vars (g)) \ Mod (Bxi ) .

(9)

We now proceed by induction on the length of a sequence n.
Induction base. Seq consists of a single block Bxi 1 . Moreover no guard in Bxi 1
contains a variable since no variable is initialized, i.e. VarsGuard (C) = ∅. We thus
have
Vars (wp JSeqK (g)) = Vars (wp JBxi 1 K (g))




= VarsGuard (Bxi ) ∪ Vars (g) \ Mod (Bxi )
=∅

(by Equation 9)

= Vars (g) \ Mod (Bxi ) .
Induction hypothesis. Suppose Equation 8 holds for some arbitrary but fixed sequence Seq of length n and all g ∈ E.
Induction step. We have
y 
q
Vars wp Bxi 1 ; . . . Bxi n ; Bxi n+1 (g)
q
y
q
y 
= Vars wp Bxi 1 ; . . . ; Bxi n wp Bxi n+1 (g)

y 
q
= Vars wp Bxi n+1 (g) \ Mod Bxi 1 ; . . . ; Bxi n .
Further, Equation 9 yields
y 
q
Vars wp Bxi n+1 (g) =

(by Table 1)
(by I.H.)




VarsGuard Bxi n+1 ∪ Vars (g) \ Mod Bxi n+1 .

Recall that every variable occurring in a guard in Bxi n+1 must be initialized,
that is


VarsGuard Bxi n+1 ⊆ Mod Bxi 1 ; . . . ; Bxi n .

Overall, the aforementioned facts and some simple set algebra yields
y 
q
Vars wp Bxi 1 ; . . . Bxi n ; Bxi n+1 (g)

= Vars (g) \ Mod Bxi 1 ; . . . Bxi n ; Bxi n+1 .
Proof of Lemma 3.2

Proof. We show that Vars (ert JSeqK (0)) = ∅ holds for every sequence Seq ∈ BNL.
This implies ert JSeqK (0) 6⋓ Seq. First observe that since every Seq ∈ BNL is loop–
free, we have
Vars (wp JSeqK (g)) = Vars (ert JSeqK (g)) .
(10)

39

Thus Equation 8 verified in the previous proof yields
Vars (ert JSeqK (0)) = Vars (wp JSeqK (0))

(by Equation 10)

= Vars (0) \Mod (Seq)
=∅

= ∅.
A.7

(by Equation 8)

Proof of Theorem 6

The proof makes use of two technical lemmas that are proven afterwards.
Proof (Proof of Theorem 6). Assume B is a Bayesian network, i.e. I = ∅. Moreover, let σ ∈ Σ. We have to show that
#!
"

V
^
Pr v∈V v = v
.
V
(σ) =
wp JBNL(B, cond)K
xv = v
Pr v∈O v = v
v∈U
Then

wp JBNL(B, cond)K

"

^

xv = v

v∈U

#!

(σ)


V
wp JBNL(B)K [ψ] · v∈U xv = v (σ)
=
wp JBNL(B)K ([ψ]) (σ)
V

wp JBNL(B)K
(σ)
v∈V xv = v
=
wp JBNL(B)K ([ψ]) (σ)

V
Pr v∈V v = v
.
V
=
Pr v∈O v = v

(Lemma 5, see below)
(Definition of ψ)
(Lemma 6, see below)

Lemma 5. Let B be an extended Bayesian network, cond be a conditioning
function, and f ∈ E. We define a shortcut for the guard corresponding to all
observations:
^
ψ=
xv = cond(v)
v∈O

Then, for each σ ∈ Σ, we have

wp JBNL(B, cond)K (f ) (σ) =

wp JBNL(B)K ([ψ] · f ) (σ)
,
wp JBNL(B)K ([ψ]) (σ)

where, again, we define 0/0 = 0.
Proof.
wp JBNL(B, cond)K (f )
= wp Jrepeat {BNL(B)} until (ψ)K (f )

(Definition of BNL(B, cond))

40

= wp JBNL(B); while (¬ψ) {BNL(B)}K (f )

(Table 1)

= wp JBNL(B)K (wp Jwhile (¬ψ) {BNL(B)}K (f ))

(Table 1)

We now distinguish two cases: wp JBNL(B)K ([ψ]) (σ) > 0 and wp JBNL(B)K ([ψ]) (σ) =
0.
For wp JBNL(B)K ([ψ]) (σ) > 0, we proceed as follows:


[¬ψ] · wp JBNL(B)K ([ψ] · f )
+ [ψ] · f
= wp JBNL(B)K
1 − wp JBNL(B)K ([¬ψ])
(Assumption, Theorem 3 (1))


[¬ψ] · wp JBNL(B)K ([ψ] · f )
+ wp JBNL(B)K ([ψ] · f )
= wp JBNL(B)K
1 − wp JBNL(B)K ([¬ψ])
(Theorem 1 (2))
wp JBNL(B)K ([ψ] · f )
+ wp JBNL(B)K ([ψ] · f )
1 − wp JBNL(B)K ([¬ψ])
(Lemma 3 (2) allows to apply Lemma 1)


wp JBNL(B)K ([¬ψ])
(Algebra)
= wp JBNL(B)K ([ψ] · f ) · 1 +
1 − wp JBNL(B)K ([¬ψ])
wp JBNL(B)K ([ψ] · f )
=
(Algebra)
1 − wp JBNL(B)K ([¬ψ])
wp JBNL(B)K ([ψ] · f )
(Theorem 1)
=
wp JBNL(B)K ([ψ])
= wp JBNL(B)K ([¬ψ]) ·

For wp JBNL(B)K ([ψ]) (σ) = 0, we proceed as follows:
= wp JBNL(B)K ([ψ] · f )

(Assumption, Theorem 3 (2))

= 0
=

wp JBNL(B)K ([ψ] · f )
wp JBNL(B)K ([ψ])

where the last step is a consequence of our definition 0/0 = 0 and the following
observations:
1. wp JBNL(B)K ([ψ]) (σ) = 0 holds by assumption.
2. wp JBNL(B)K ([ψ] · f ) (σ) = 0 holds. This shown analogously to the the proof
of Theorem 3, below equation (‡).
Lemma 6. Let B be an extended Bayesian network, cond be a conditioning function, and f ∈ E. Let I = {u1 , . . . , uk } be the set of inputs of B. Moreover, let u =
(u1 , . . . , uk ) be the canonically ordered tuple of inputs, i.e. u1 < u2 < . . . < uk .
We denote the corresponding tuple of variables by xu = (xu1 , . . . , xuk ). Then,
for every set M ⊆ V , we have
#!
"
!
^
X
^
[xu = y] · Pr
v=v | u=y
=
wp JBNL(B)K
xv = v
v∈M

y∈Valsk

v∈M

41

Proof. By induction on the numberVof nodes n of the extended Bayesian network
B. To improve readability, let ϕ = v∈M xv = v.
I.B. For n = 1, B contains exactly one node, say w. Let Vals|dep(w)| =
{y1 , . . . , yk }.
wp JBNL(B)K ([ϕ])

= wp JblockB (w)K ([ϕ])


X
Y

=
[¬guardB (w, yℓ )] · [guardB (w, yj )] · wp JassignB (w, yj )K ([ϕ])
1≤j<k

1≤ℓ<j

(apply wp to blockB (w))



=

+

X

1≤j≤k

=

X

Y

1≤ℓ<k



[¬guardB (w, yℓ )] · wp JassignB (w, yk )K ([ϕ])

[u = yj ] · wp JassignB (w, yj )K ([ϕ])

(guards partition Vals|dep(w)| )

[u = yj ] · cpt[w](yj )(w) · [ϕ] [xw /w]

1≤j≤k

=

X

(Definition of assignB (w, .), Table 1)
[u = yj ] · Pr (w = w | dep(w) = yj ) · [ϕ] [xw /w] (Definition of cpt)

1≤j≤k

=

X

[u = yj ] · Pr (w = w | dep(w) = yj ) .

(ϕ = true or ϕ = (w = w))

1≤j≤k

I.S. Now consider an extended Bayesian network B whose (smallest) root is w.
We distinguish two cases: w ∈ M and w ∈
/ M . First, assume w ∈
/ M . Then
wp JBNL(B)K ([ϕ])
= wp JblockB (w); BNL(B ′ )K ([ϕ])

(Construction of BNL(B))

= wp JblockB (w)K (wp JBNL(B ′ )K ([ϕ]))


(Table 1)


!

^
 X

= wp JblockB (w)K 
[u = yj ] · Pr
v = v | u = yj 


1≤j≤k

v∈M
{z
}
|
= g
!
X
^
=
[u = yj ] · Pr
v = v | u = yj
1≤j≤k

(I.H.)

v∈M

(wp JblockB (w)K (g) = g as blockB (w) does not modify variables in g.)

Now assume w ∈ M , and Vals|dep(w)| = {z1 , . . . , zm }. Then
wp JBNL(B)K ([ϕ])

42

= wp JblockB (w); BNL(B ′ )K ([ϕ])

(Construction of BNL(B))

′

= wp JblockB (w)K (wp JBNL(B )K ([ϕ]))


(Table 1)






X
^




v = v | w = a, u′ = yj′ 
= wp JblockB (w)K 
w = a ∧ u′ = yj′ · Pr 


v∈M\{w}

1≤j≤k′ ,a∈Vals
{z
}
|


= g

(I.H.)

=

X

1≤j<k′




1≤ℓ<j



=

Y

+

Y

1≤ℓ<k′

X 

1≤j≤m



[¬guardB (w, zℓ )] · [guardB (w, zj )] · wp JassignB (w, zj )K (g)

(apply wp to blockB (w))



[¬guardB (w, zℓ )] · wp JassignB (w, zk )K (g)


xdep(w) = zj · wp JassignB (w, zj )K (g)

(guards partition Vals|I| and actually all rationals due to else at the end of each block.)
X 

=
xdep(w) = zj · cpt[w](zj )(w) · g[xw /w]
1≤j≤m

(Definition of assignB (w, .))

=

X 



xdep(w) = zj · Pr (w = w | dep(w) = zj ) · g[xw /w]

1≤j≤m

=

X 



xdep(w) = zj · Pr (w = w | dep(w) = zj )

1≤j≤m

·

X

1≤i≤k′

=

X 

(Definition of cpt[w](zj )(w))



[u′ = yi′ ] · Pr 

xdep(w) = zj

1≤j≤m

^

v∈M\{w}

 X

=

1≤j≤m



v = v | w = w, u′ = yi′ 

[u′ = yi′ ] ·

(Algebra)

1≤i≤k′



Pr (w = w | dep(w) = zj ) · Pr 

X 

(Definition of g)

xdep(w) = zj

 X

1≤i≤k′

^

v∈M\{w}

[u′ = yi′ ] · Pr



v = v | w = w, u′ = yi′ 

^

v∈M

v = v | dep(w) = zj , u′ = yi′

!

(Chain rule)

43

=

X

[u = yi ] · Pr

1≤i≤k

=

^

v∈M

v = v | u = yi

!

(All inputs of B, i.e. u are given by dep(w) and inputs of B ′ , i.e. u′ )
!
^
X
[u = y] · Pr
v=v |u=y .

y∈Valsk

v∈M

