We report on ongoing research eforts aimed at algebraic symbolic analysis of running time in probabilistic programs. We represent (sub-)probability distributions via generating functions and interpret loops as fixed-points in metric spaces. Probabilistic Programming (PP) [24, 4] is concerned with formal tools to define and analyze probabilistic models programmatically. Applications of PP include the modeling of randomized algorithms, probabilistic graphical models such as Bayesian networks, cognitive and decision-making models, and security protocols [26, 30, 35, 1, 32, 27]. Analyzing probabilistic programs is intrinsically challenging: even in the restricted setting where only a coin-flipping primitive is available, computing the expected value of a variable at program termination is as hard as solving the universal halting problem, while computing higher moments (such as variances) is provably harder; see [28] and references therein. In this communication, we report on ongoing research eforts aimed at symbolic or exact, as opposed to simulation-based [37, 16], analysis of probabilistic programs, in the spirit of works such as [4, 28, 6, 38, 29, 5]. Our focus is on termination and running time analysis [28, 6, 38]. We adopt a denotational perspective in the spirit of Kozen [31]: we interpret programs as transformers of functionals - maps from initial states to (sub)-probability distributions on running time, represented via generating functions [8, 28, 29] (Section 2.1). Our approach departs from previous work in a few key respects. In particular, we work in a metricspace setting (over generating functions and functionals), where fixed points needed to interpret loops are shown to exist and be unique leveraging the Banach fixed-point theorem [ 2] (Section 2.2). Compared to a traditional order-theoretic framework, based on the Knaster-Tarski or Kleene fixed-point theorems [40], our approach appears to be more streamlined. In particular, the uniqueness and convergence rate guaranteed by Banach theorem suggest novel promising approximation and algebraic techniques for symbolic analysis, which we will illustrate through a simple example (Section 3).
Related and Further Work The semantics of probabilistic programs, starting with the seminal work of Kozen [31] and the monograph by McIver and Morgan [33], is by now a well-established topic. Other semantics for discrete probabilistic while-programs are discussed in the aforementioned references; see also [33, 21, 25, 7, 5, 39, 22, 36]. A generating function approach has been considered in [28], and analysis techniques have been put forward for a class of programs with rational generating functions. Here we target a broader class of programs, with possibly non-rational (algebraic) generating functions. A diferent approach based on invariants and theorem proving is discussed in [ 20, 6]. The investigations discussed here are part of a broader research agenda, aimed at developing flexible, compositional formal methods applicable across diverse, probability-related domains, including dynamical systems with safety-related aspects [10, 9, 11, 12, 13, 15], information leakage and security [19, 18], distributed systems with notions of failure and recovery [14], randomized model counting and testing [17, 34].
Let sD denote the set of sub-probability generating functions (gf) in the variable . These are functions of
the complex variable of the form () = ∑︀∞=0 such that ∈ [0, 1] and (
sD(, ) := 2− min{≥ 0:̸=}
with the convention that min ∅ = +∞ and 2−∞ = 0. Note that, for any integer ≥ 0, sD(, ) ≤ 2−
if () − () = (), convening that (∞) = 0. It is a standard fact that (sD, sD) forms a
complete1 metric space. Fix an integer ≥ 1 — representing the number of program variables. We
let F := { : Z → sD} be the set of functionals from Z to sD. In what follows, we will let
= (1, ..., ) range over Z. We lift the complete metric space structure of sD to F by defining
the following distance for 1, 2 ∈ F:
(
With this notion of distance, (F, F) is in turn a complete metric space. We shall denote by 0 (resp. 1) the functional that assigns the constant gf () = 0 (resp. constant () = 1) to any ∈ Z. The convex combination of two or more functionals, say (for ∈ [0, 1]), 1 + (1 − )2 := . ( 1() + (1 − )2() ), is still a functional in F. Likewise, for any predicate : Z → {0, 1}, the linear combination, (¬) · 1 + · 2 := . ( (1 − ()) · 1() + () · 2() ), is still in F. In what follows, we shall omit the index and write just F whenever is understood from the context.
Probabilistic programs [4, 24] extend ordinary programs in the sense that they allow probabilistic choice between blocks of instructions. We consider here the probabilistic Guarded Command Language pGCL of [33], which focuses on discrete probability distributions, represented by guarded choices. We do not consider nondeterminism at this stage. We also do not consider observe() statements, which can be encoded using fail variables like in [38]. Programs are built from integer variables 1, ..., , for a fixed ≥ 1. We let range over predicates, that is functions Z → {0, 1}, and ℎ over functions Z → Z.
::=skip | :=ℎ | 1 : 1 □ · · · □ : | if 1 else 2 | 1; 2 | while Here, 1, . . . , represents a probability distribution, hence we require ∑︀=1 = 1 and ≥ 0 ∀ ∈ {1, . . . , }. In the sequel, we will let = (1, . . . , ) denote the entire variables tuple and sometimes, slightly abusing notation, also a tuple in Z.
runtime through iteration counting. Intuitively, we can think of a hidden counter in our program that gets incremented each time an iteration of a while-loop is executed. We are interested in the final value of this counter, say . Since is probabilistic, and may or may not terminate, for each given input, represents a sub-probability distribution on the set of naturals 0, 1, 2,... Natural questions about are: What is the probability of termination? What are the expected value of and its standard deviation,
given termination? Or even: what is the probability that deviates from its expected value by more than a given amount?
In what follows, we define a semantics of programs, in which [[ ]] is represented by a functional section, as well as of the following abbreviations, where ℎ : Z transformer. Formally, for each probabilistic program , [[ ]] takes each ∈ F into a ′ ∈ F, that is [[ ]] : F → F. In what follows, we shall make use of the operations over F introduced in the previous → Z. [ℎ()/] := . (1, ..., − 1, ℎ(), +1, ...) · := . · (()).
In the semantic clauses one should think of as the ‘continuation’ of — what is executed after terminates. In the clause for the while loop, the formal variable ‘marks’, in the parlance of generating functions, the number of loop iterations; fix (·) denotes the fixed-point operator.
• Skip: [[skip]]() = . • Assignment: [[ := ℎ]]() = [ℎ()/]. • Composition: [[1; 2]]() = [[1]]([[2]]()). • Probabilistic Choice: [[1 : 1 □ · · · □ : ]]() = ∑︀=1 · [[]](). • Conditional: [[if 1 else 2]]() = · [[1]]() + (¬) · [[2]]().
as follows: for each ∈ F • While Loop: [[while ]]() = fix(Ψ,,), where Ψ,, : F → F is the transformer defined Ψ,,( ) := (¬) · + · · [[ ]]( ) . (* ) = * . The unique * is denoted by fix ( ).
space (, ), a function : → is a contraction on if there is a constant ∈ [0, 1) s.t. for all
1, 2 ∈ we have ( (1), (2)) ≤ · (1, 2). The Banach fixed point theorem states that if (, )
is a nonempty, complete metric space and is a contraction on , then there is a unique * ∈ s.t.
in (
Theorem 1 (fixed-points) . For each program , predicate and ∈ F, the functional Ψ,, defined 21 . As a consequence of the The semantics of is a functional {[ ]} ∈ F, defined as
{[ ]} := [[ ]](
For each ∈ Z, {[ ]}() is a sub-probability gf which, for the sake of compact notation, we will
denote by {[ ]}; wanting to make the argument of {[ ]} explicit, we will write this as {[ ]}(). So
[]{[ ]}() is the probability that with input terminates in precisely iterations; {[ ]}(
Example 1. Fix = 1 and write 1 = . Consider the program
(
︂( [ < 0]1 + [ ≥ 0](︀ 1 3 {[ ]}− 1 + {[ ]}+1 2 3 ︀) ︂) .
(
of {[ ]}(). This will be elaborated in the next section.
Approximations Based on Banach Fixed Point Theorem As mentioned in the Introduction, one appealing feature of Banach fixed-point theorem, compared to order-theoretic ones (Knaster-Tarski, Kleene,...), is that it immediately implies uniqueness. Moreover, it makes easy it to assess the quality of approximations given by finite iterations of Ψ. We elaborate on these points below.
⊑: for each 1, 2 ∈ sD, say 1 = ∑︀≥ 0 and 2 = ∑︀≥ 0 , we let 1 ⊑ 2 if and only ≤ for each ≥ 0. The bottom element of this partial order is 0, the constant zero gf. The partial order (sD, ⊑) is lifted to a partial order (F, ⊑) on F point-wise: 1 ⊑ 2 if and only if for each ∈ Z, we have 1() ⊑ 2() in sD. Letting again 0 denote the constant zero gf, the least element of this partial order is 0 := . 0. The following result highlights an important property of our semantics. Theorem 2 (monotonicity). For each , , , Ψ,, : F → F is monotonic w.r.t. (F, ⊑).
Let us now fix generic program = while , and consider the corresponding transformer Ψ,,.
We focus on = 1, as used in our semantics (
1 −
· F(0, Ψ(0))
where is the contraction constant. In our case ≤
2− 1, in the light of the definition of F, cf. (
Ψ(
3 ⎩ 0 if < 0 if = 0 otherwise.
Ψ(
2 ⎪⎪⎩ 09 ⎧ 1 if < 0 if = 0 if = 1 otherwise.
Continuing this way, one can see that, say for = 0:
{[ ]}0() = 31 + 227 3 + 2483 5 + 214807 7 + 19262843 9 + (11) . (
such that ⊒ fix(Ψ), or even s.t. Ψ() ⊑ , then the iterates form a descending chain3: ⊒ Ψ() ⊒ · · · Ψ()() ⊒ · · · ⊒ fix(Ψ) ={[ ]}.
Ideally, and the subsequent iterates, should provide tighter and tighter upper bounds on such quantities
as: {[ ]}(
∑︀ ≥ 0 = .
1 ; techniques based on templates [6] seem promising. {[ ]} in the above sense. How to efectively find an informative is a subject of our ongoing research; = ≥ for all ∈ Z: A Connection With Directed Lattice Paths
A rather diferent approach to the analysis of
probabilistic programs is expressing the behaviour of a loop, whenever possible, in terms of directed lattice
paths [3]. Basically, these are random walks in the Z line, starting from an arbitrary position ∈ Z, with
left and right jumps of fixed magnitude and probability. In the cases that interest us, a walk terminates
as soon as it reaches a negative value. Indeed, given a loop program = while ≥
of values taken on by the iteration variable can be seen as such a path. For our running example, a
0 , a sequence
terminating execution corresponds to either a zero length path from < 0, or to path starting from
0, ending at = 0 without ever going below 0 — this is called an excursion in [3] — followed
by a final step, corresponding to an execution of the body’s loop where the branch := − 1 is taken,
with probability 1/3. More precisely, let () denote the generating function of excursions starting at
, with jumps in {− 1, +1} and associated weights {1/3, 2/3} (note that () = 0 for < 0). Then
{[ ]}() = [ < 0]1 + [ ≥ 0]
︂( 1
3 · ()
︂)
(
There exist consolidated techniques to work out algebraic characterizations of generating functions for directed lattice paths. For the case in question, applying the techniques of [3], one easily obtains, () = 3
︃( 1 3
4
·
−
√
9
− 82 )︃+1
which leads to:
{[ ]}() =
︃( 1 3
4
·
−
√
9
− 82 )︃+1
. (
For instance, for ≥
0, we have {[ ]}(
approximation approach discussed in the previous paragraph. In fact, we conjecture that the directed lattice approach applies to a class of programs that generalizes the Constant Probability programs considered in [23].
Acknowledgments