PaperlayerView exact revision on arXiv

Source-linked AI summary

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo

arXiv:1601.01001v2cs.LOcs.PL

TL;DR

Probabilistic programs can exhibit subtle expected run-times, including infinite expected time despite almost-sure termination. The paper develops a wp-style calculus with sound loop-bound rules, connects it to an MDP operational model, and applies it to termination and runtime examples.

  • Problem

    Expected run-time analysis of probabilistic programs is subtle because arbitrarily long runs can coexist with finite expectation, while sequential composition can produce infinite expectation despite almost-sure termination.

  • Method

    The paper introduces ert, a wp-style expected-run-time transformer, together with sound proof rules for upper and lower loop bounds and an operational interpretation using MDPs.

  • Results

    The ert transformer corresponds to expected run-time in the MDP operational model, and the framework analyzes examples including the random walk and coupon collector problem.

  • Takeaways & Limitations

    The framework can determine possibly infinite expected termination times and prove universal positive almost-sure termination, while extending deterministic run-time reasoning conservatively.

  • Takeaways & Limitations

    Inferring loop invariants remains one of the most involved parts of verification, especially when loop bodies are not loop-free; the runtime model is also a design choice adaptable to alternatives.

Abstract

from arXiv · show

This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expected termination time of a probabilistic program and proving positive almost-sure termination - does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run-time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson's approach for reasoning about the run-time of deterministic programs. We analyze the expected run-time of some example programs including a one-dimensional random walk and the coupon collector problem.

1 Introduction

Probabilistic programs can have subtle expected run-times, including infinite expected time despite almost-sure termination. The paper introduces a wp-style calculus and proof rules for analyzing these behaviors soundly.

  • Motivation: Probabilistic programs may have arbitrarily long runs yet finite expected run-time, so termination behavior cannot be characterized by a single diverging execution.The geometric-loop example illustrates this distinction: every finite run length remains possible, while the expected run-time is finite.
  • Motivation: Sequential composition can yield infinite expected run-time even when each component has finite expected run-time and the composite terminates almost surely.The C1; C2 example demonstrates this failure of the classical sequential-composition intuition.
  • Approach: The paper proposes ert, a quantitative wp transformer that computes expected run-time from program structure and a continuation-cost function.Setting the continuation cost to zero gives the expected run-time of the program itself; the calculus conservatively extends Nielson’s deterministic run-time reasoning.
  • Related work: The approach is related to program-verification methods for deterministic run-time bounds and contrasts with prior analyses based on classical probability theory.The paper positions its method as a formal-development alternative to expectation- or martingale-based analyses.
  • Contributions: The authors establish correspondence with an MDP operational model and provide proof rules for upper and lower expected run-time bounds on loops.Applications include a one-dimensional random walk and the coupon collector problem.
  • Contributions: The framework targets possibly infinite expected termination times and universal positive almost-sure termination, a problem stated as harder than universal deterministic halting.The paper claims a sound verification framework handling both positive almost-sure termination and infinite expected run-times.

2 A Probabilistic Programming Language

The paper uses a guarded-command imperative language extended with probabilistic assignments, guards, conditionals, and loops. Its operational conventions assign time costs to constructs and support probabilistic state transitions.

  • Language: The language extends Dijkstra-style guarded commands with probabilistic distribution expressions in assignments and guards.Programs are described by constructs including probabilistic assignments, sequential composition, nondeterministic choice, conditionals, and probabilistic while loops.
  • Examples: The language includes probabilistic examples such as a geometric loop and a tortoise–hare race, illustrating probabilistic guards, distributions, and state updates.The tortoise advances deterministically while the hare makes probabilistic progress until it passes the tortoise.
  • Language: Distribution expressions denote discrete probability distributions, interpreted from program states over values.The notation assigns probabilities to outcomes, such as 1/2·⟨true⟩+1/2·⟨false⟩.
  • Operational semantics: Probabilistic while loops execute their body or terminate according to the guard’s state-dependent probability.Probabilistic guards can simulate geometric behavior with a specified success probability.
  • Operational semantics: The runtime model charges no time for empty and halt, one unit for skip and probabilistic assignments, and an additional unit for evaluating probabilistic guards.The model also treats nondeterministic choice demonically by selecting the branch with greatest run-time.

3 A Calculus of Expected Run–Times

This section defines ert as a continuation-based transformer for expected run-time and establishes its algebraic and fixed-point foundations. It illustrates the calculus on a truncated geometric program and motivates invariant-based loop rules.

  • ert [C] (f) (σ) gives the expected run-time of C from σ, assuming f captures the run-time of the computation following C.
  • The transformer assigns run-time according to program structure, weighting sampled assignments by outcome probabilities and defining loops through least fixed points.
  • The concrete run-time model counts assignments, guard evaluations, and skip statements, but the development can adapt to alternative cost models.
  • Example 2 (Truncated geometric distribution): For the truncated geometric example, Ctrunc has expected run-time 2.5 time units.
  • Direct fixed-point calculation is generally infeasible for loops, motivating invariant-based proof rules for bounding their run-times.
  • Basic properties of the ert transformer: The ert transformer satisfies constant propagation, preservation of ∞, sub-additivity for fully probabilistic programs, and scaling bounds.
  • Continuity of ert makes the characteristic functional continuous, so the Kleene Fixed Point Theorem establishes well-defined expected run-times for loops.

4 An Operational Model for Expected Run–Times

This section models probabilistic programs as operational Markov decision processes whose rewards represent run-time. It proves that the expected reward of the associated MDP exactly matches the ert transformer.

  • The operational MDP of a program: An operational MDP contains program states, actions, transition probabilities, an initial state, and a reward function, with transitions specified by operational rules.
  • Schedulers resolve nondeterministic choices in MDPs by selecting actions based on the sequence of states visited so far.
  • Rewards are positive only for guard evaluations, assignments, and skip statements; other program statements receive zero reward.
  • The operational construction includes termination and sink states so continuations are collected after successful termination but not after reaching halt through the sink.
  • Example 3 (MDP of Ctrunc): For Ctrunc, the operational model has three finite paths corresponding to the probabilistic guard outcomes, and both expected reward and ert equal 5/2.
  • Soundness of the ert transformer: Theorem 2 establishes that ert precisely captures the expected reward of the operational MDP associated with each probabilistic program.

5 Expected Run–Time of Loops

The section develops invariant-based proof rules for approximating expected loop run-times, including exact bounds and programs with infinite expected run-time despite almost-sure termination.

  • Proof-rule families: Two families of invariant-based rules approximate loop run-times: global invariants provide upper bounds, while parametrized invariants provide incremental upper and lower bounds.The rules use upper invariants and lower or upper ω-invariants, with refinement procedures for improving bounds.
  • Global invariants: An upper invariant I satisfying the loop’s characteristic-functional inequality yields an upper bound on the expected run-time.The approach relies on Park’s theorem and applies even when direct least-fixed-point computation is impractical.
  • Global invariants: The global-invariant method is complete: an upper invariant exists that equals the loop’s exact expected run-time, although synthesizing a useful invariant can be difficult.Verification is usually easier for loop-free bodies, while invariant inference remains a major part of the effort.
  • Incremental invariants: Lower and upper ω-invariants approximate executions finishing within increasing iteration bounds, and their limits can establish exact loop run-times.Theorem 6 states that a suitable ω-invariant sequence converges to the exact expected run-time; the rules are therefore complete.
  • Examples: The analyzed program terminates with probability one but has infinite expected run-time, demonstrating that almost-sure termination does not imply finite expected termination time.The section also concludes that the geometric-loop bound is exact and can be derived by combining the lower and upper ω-invariant rules.

6 Run–Time of Deterministic Programs

The ert calculus applies to deterministic programs and matches the tightest run-time bounds derivable through Nielson’s approach. Soundness and completeness results establish this relationship, while guard evaluations remain cost-free in the model.

  • Deterministic fragment: ert is defined for deterministic programs and is compared with Nielson’s Hoare-style run-time calculus.The deterministic fragment excludes probabilistic guards, probabilistic assignments, and nondeterministic choice.
  • Nielson’s system: Nielson’s correctness properties bound execution by k · E evaluated in the initial state, subject to pre- and postconditions.The bound applies to every initial state satisfying the precondition and a terminating execution.
  • Soundness: Theorem 8 proves that ert yields an upper run-time bound whenever a deterministic program has a total-correctness proof.The result is stated for programs and assertions in the deterministic fragment.
  • Model assumptions: The calculus assumes guard evaluations take no time, so its correspondence with run-time bounds cannot be made more precise under that model.The rule system otherwise extends standard total-correctness Hoare reasoning with run-time bounds.
  • Completeness: Theorem 9 shows that every bound derivable in Nielson’s system is matched by ert up to a natural constant factor.This establishes completeness relative to Nielson’s run-time reasoning.
  • Relationship to Nielson: Together, the theorems make ert a conservative extension of Nielson’s deterministic run-time analysis.A deterministic Hoare-logic proof can be transferred by computing ert [C] (0).

7 Case Studies

The ert calculus analyzes three randomized algorithms, deriving infinite expected run-time for the fair one-dimensional random walk and Θ(N · log(N)) for coupon collection. The analyses use loop invariants and expected-run-time transformations for nested probabilistic loops.

  • Case-study scope: The case studies cover a fair one-dimensional random walk, the coupon collector problem, and randomized quicksort.The section applies the ert calculus to three well-known randomized algorithms.
  • One-Dimensional Random Walk: The random walk terminates with probability one but has infinite expected run-time.The calculus derives ert [Crw] (0) = ∞ from a lower invariant whose limit diverges.
  • One-Dimensional Random Walk: The random-walk derivation computes the program’s expected run-time compositionally by analyzing the loop and then substituting the initial state x = 10.The resulting lower and upper bounds coincide at infinity.
  • Coupon Collector: The coupon collector analysis decomposes the program into inner and outer loops and proposes lower and upper ω-invariants for each.The outer-loop invariant is shown to bound the loop from both directions.
  • Coupon Collector: 4 + [N > 0] · 2N · (2 + H_N−1) is the derived coupon collector run-time expression.H_N−1 is the (N−1)-th harmonic number.
  • Coupon Collector: Θ(N · log(N)) is the coupon collector’s expected run-time.This follows because harmonic numbers grow asymptotically like the natural logarithm.

8 Conclusion

The paper concludes that its wp-style ert calculus provides sound and complete loop-bound rules for probabilistic expected run-times and positive almost-sure termination. It also preserves Nielson’s deterministic reasoning while supporting established randomized case studies.

  • Main contribution: The calculus provides sound and complete rules for both upper and lower expected run-time bounds of loops.The rules are applied to examples including the coupon collector problem.
  • Practical proof development: The authors report that correct loop invariants were often guessed from a few loop unrollings despite invariant discovery being generally challenging.They therefore regard the proof rules as natural and widely applicable.
  • Foundational properties: The approach is a conservative extension of Nielson’s deterministic run-time method and is sound with respect to a simple operational model.This connects probabilistic expected-run-time reasoning to established deterministic analysis.

A Omitted Proofs

The omitted proofs establish algebraic properties of ert by structural induction, including compositionality, monotonicity-related bounds, and behavior on loops and probabilistic assignments. These derivations support the calculus rules used in the main text.

  • Proof strategy: The proofs use induction on program structure, with atomic programs as the base cases and compound constructs as induction steps.The induction covers sequential composition, choice, conditionals, loops, and probabilistic assignment.
  • Probabilistic assignment: For probabilistic assignment, adding a constant to the continuation adds the same constant to ert.The argument uses linearity of expectation and distributions of total mass 1.
  • Structural rules: For sequential composition, ert distributes continuation costs through nested transformers, yielding the composition rule.The proof applies monotonicity and the induction hypothesis to both components.
  • Loop rules: Loop proofs rely on characteristic functionals, least fixed points, and fixed-point induction.The omitted derivations establish the required inequalities for loop transformers.

A.7 Proof of Theorem 2

The appendix proves that ert matches the operational expected reward for probabilistic programs. The proof reduces loops to bounded unrollings and establishes the result by structural induction.

  • Bounded while loops: Bounded while loops connect finite unrollings to the loop characteristic functional through induction and Kleene’s Fixed Point Theorem.This supplies the preparation needed to relate the loop’s ert to its operational semantics.
  • Loop decomposition: The loop decomposition rewrites while(ξ){C} as a conditional executing C followed by the loop again, or empty when ξ is false.This decomposition supports the characteristic-functional and operational reasoning used in the soundness proof.
  • Soundness of ert: Theorem 2 establishes soundness: ert[C](f)(σ) equals the operational expected reward for every program, state, and post-expectation.The proof proceeds by induction on program structure, with the while case relying on Lemmas 5 and 6.
  • Structural induction: The proof handles sequential composition, conditionals, nondeterministic choice, assignments, empty, skip, and halt through corresponding operational cases.Each case matches the compositional ert rule to the expected reward of the associated operational model.

A.8 ert of Deterministic Programs

For deterministic programs, ert inherits the existing reasoning approach: ordinary total-correctness proofs imply expected-runtime proofs, while deterministic ert proofs can be bounded by a natural multiple of the original expression.

  • Sequential composition: For sequential composition, ert[C1; C2](0) decomposes into the runtime of C1 plus the runtime of C2 after executing C1.This compositional identity is used to transfer deterministic proof obligations to expected-runtime obligations.
  • Soundness: ⊢{ P } C { ⇓Q } implies ⊢E { P } C { ert [C] (0) ⇓Q } for deterministic programs.This establishes soundness of the expected-runtime calculus as an extension of deterministic reasoning.
  • Proof strategy: The deterministic soundness proof proceeds by induction over program structure, covering sequential composition, conditionals, and loops.The loop case uses a ranking-style assertion R(z) and expected-runtime side conditions.
  • Completeness: Completeness with respect to Nielson states that any deterministic ert proof using expression E yields a natural-number multiple k bounding ert[C](0).The bound holds for every state satisfying P.

B.1 Invariant Verification for the Random Walk

The random-walk analysis verifies a lower invariant for the loop and uses harmonic-number growth to show that its expected runtime diverges.

  • Invariant verification: The proposed sequence is a lower ω-invariant when it satisfies the characteristic-functional inequalities for every n ≥ 0.The verification begins with F(0) ⪰ I_0 and establishes F(I_n) ⪰ I_{n+1}.
  • Recurrence conditions: The recurrence construction uses boundary conditions such as a_n,k = 0 whenever k > n and an explicit zero extension for negative indices.These conditions support the recursive invariant equations.
  • Invariant verification: a_n,0 ≥ 1 + H_floor(n/2) for all n ≥ 2, where H_m is the m-th Harmonic number.This lower bound is the key step toward proving lim n→∞ a_n,0 = ∞.

B.2 Invariant Verification for the Inner Loop of the Coupon Collector Algorithm

For the coupon collector’s inner loop, the analysis expresses ert through a characteristic functional and verifies a proposed ω-invariant using the loop’s probabilistic update structure.

  • Characteristic functional: The inner-loop runtime is defined as the least fixed point of its characteristic functional F_f(X).The functional is then expanded using the loop body’s conditional and uniform-sampling behavior.
  • Invariant verification: The proposed Jf_n is intended to serve as both a lower and an upper ω-invariant for the inner loop.The verification starts by checking F_f(0) = Jf_0 and then proceeds to the invariant inequalities.
  • Probabilistic update: The loop functional distinguishes the case cp[i] = 0 from cp[i] ≠ 0 and incorporates the uniform update i :≈ Unif[1 . . . N].This case split determines whether the post-expectation is retained or updated through a sampled coupon index.

B.3 Invariant Verification for the Outer Loop of the Coupon Collector Algorithm

The section verifies that the proposed sequence I_n forms both lower and upper ω-invariants for the coupon collector algorithm's outer loop. The proof computes the characteristic functional, establishes the base case H(0) = I_0, and shows H(I_n) = I_{n+1} before taking the limit.

  • Characteristic functional: The characteristic functional H is evaluated on the loop's run-time expression and the transformed state with x decreased and cp[i] updated.The calculation uses substitutions x/x −1 and cp[i]/1 within the loop body.
  • Coupon collector setup: The calculation also invokes a relationship between collected and missing coupons in the coupon collector analysis.This relationship is introduced as useful for the subsequent reasoning.
  • Invariant verification: The proof aims to show that I_n is both a lower and an upper ω-invariant for the outer loop.This is the stated goal before applying Theorem 5.
  • Invariant verification: The base case is established as H(0) = I_0, followed by the inductive relation H(I_n) = I_{n+1}.The displayed derivation repeatedly rewrites H(Y) and concludes with the successor relation.
  • Limit argument: The argument concludes by bounding the loop functional between the limit of I_n and the limiting invariant I.The stated chain is n→∞ I_n ⪯ ert[C_out](0) ⪯ lim n→∞ I_n = I.
Loading 1601.01001v2…