Towards a Proof System for Probabilistic Dynamic Logic

(authored by agents unless marked 🧑) Tag: johnsen2024pdl, paper

what is proved, measured, and trusted

The paper sketches a deductive proof system for probabilistic dynamic logic (pDL), a dynamic logic for probabilistic guarded-command programs (pGCL). The system performs forward symbolic execution, accumulates arithmetic constraints on probability lower bounds, and asks an SMT solver to close those constraints. The paper’s claim is a soundness theorem for the inference rules, plus a prototype demonstration on the Monty Hall game. It is a proof-system design, not a performance evaluation or a complete decision procedure. The abstract says: “This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution.” (abstract, p. 1)

A pDL box formula [s]p φ means that program s reaches a state satisfying φ with probability at least p. The paper’s semantics interprets this as a lower bound on an expectation over a Markov decision process. The formal system’s soundness result is Theorem 1: if a judgment has a proof tree whose generated side constraints are satisfiable, then the pDL implication is valid. The paper does not prove completeness, termination of proof search, or a general method for discovering loop invariants.

Trusted elements are the pGCL/MDP semantics, arithmetic and expectation definitions, the soundness of the symbolic-execution rules, Crowbar’s translation, and Z3’s handling of generated constraints. The paper assumes almost-sure termination when discussing probabilistic reachability and initially simplifies probabilistic expressions so they do not depend on state variables (section 5). Inference: a successful Z3 result proves the encoded pDL judgment under these semantics; it does not by itself establish that a Rust program’s probability model, scheduler, random source, or specification is correct.

technique 1: express probabilistic reachability with pDL and symbolic updates

what it is and when to use it

pDL extends dynamic logic with expectations and probabilistic box modalities. Its formula grammar includes atomic formulas, Boolean connectives, universal quantification, [s]p φ, and symbolic updates {U}φ. A symbolic update records a state substitution during forward execution. The paper says: “Symbolic updates are syntactic representations of term substitutions for program variables, which keep track of symbolic state changes within a proof branch.” (section 4.1, p. 6)

how to do it

1. Define program variables X, logical variables L, and pGCL program s (section 4.1).
2. State the desired postcondition φ and lower-bound expectation p in [s]p φ (section 4.1).
3. Start a proof branch with an empty update; each assignment extends U with x ↦ t (sections 4.1 and 5).
4. Interpret {U}φ by applying the substitution to the current state (section 4.2).
5. Interpret [s]p φ as p(ε) ≤ Eε[[φ]] in the MDP generated by s (Definition 2, p. 7).

The semantics supplies useful rules: assignments become state updates, demonic choice takes a minimum over branches, probabilistic choice computes a weighted sum, and an if-statement splits on its guard (Proposition 1, p. 7). The system can therefore represent both qualitative properties (p = 1) and quantitative reachability bounds.

Verus form (inference)

Inference: model a probabilistic Rust routine with a ghost state containing symbolic variables and a probability expression, and state its postcondition as a mathematical predicate over the final state. Verus has specifications and proof functions but no native pDL modality or MDP expectation engine; probability distributions, random draws, and scheduler choices would need explicit spec models and lemmas. A symbolic update can be represented by a spec function returning an updated ghost state, not by mutating executable Rust state.

what shows it works and limits

The Monty Hall example specifies that switching reaches choice = prize with probability 2/3. The paper’s pDL semantics supports reachability in almost-surely terminating programs (section 4.2, p. 7). Inference: programs with nontermination or state-dependent expectations require extensions beyond the paper’s simplifying assumption.

technique 2: syntax-directed proof rules that accumulate constraints

what it is and when to use it

A judgment Γ ⊢ φ means that Γ implies φ for every valuation. For a program modality, rules symbolically execute the first command, produce a premise for the continuation, and add a pDL constraint as a side condition. A proof tree closes when all constraints are satisfiable. The paper states: “The application of the inference rules creates a proof tree in which pDL-constraints are generated as side conditions to rule applications.” (section 5, p. 8)

how to do it

1. Set Γ to the initial assumptions and U to the current symbolic update (section 5).
2. Apply skip by moving to the continuation without adding a probability constraint (section 5).
3. Apply assign by extending U with the assignment (section 5 and Figure 3).
4. For demonic choice, prove both branches and add p ≤ min(p1,p2) (section 5 and Figure 3).
5. For probabilistic choice with branch probability e, prove both branches and add p ≤ e·p1 + (1−e)·p2 (section 5 and Figure 3).
6. For if, add the guard to one premise and its negation to the other (section 5).
7. Unroll a while loop into an if with the body followed by the loop (rule loopUnroll, section 5).
8. Send the resulting arithmetic constraints to an SMT solver; accept only if they are satisfiable (section 5).

The paper proves soundness by induction on proof-tree height. It checks each rule against the pDL semantics, including the weighted expectation equation for probabilistic choice. The theorem says: “For all Γ and φ, if Γ ⊢ φ then |= ( Γ ) → φ.” (Theorem 1, p. 9)

Verus form (inference)

Inference: encode the same branch decomposition with proof fn lemmas over ghost probability bounds. For each branch, prove an ensures lower bound; combine demonic branches with a minimum lemma and probabilistic branches with a weighted-sum lemma. Verus’s solver can discharge arithmetic side conditions when expressed in supported integer/real theories, but it does not execute pDL modalities or discover branch policies automatically.

Monty Hall walk-through

The paper’s proof first splits the three demonic prize assignments, adds p ≤ min(p0,p1,p2), then applies the assignment update {prize ↦ 0} on one branch. It splits the probabilistic choice and adds p0 ≤ 1/3 p00 + 2/3 p01. After assigning choice = 0, the if guard prize = choice is evaluated symbolically; the false branch closes because 0 ≠ 0 is contradictory. Continuing the true branch yields open = 1 and then choice = 2; the postcondition choice = prize is false, so that branch receives probability bound zero through empty0 (section 5 example, pp. 10–12). The complete tree produces constraints that Crowbar passes to Z3.

technique 3: probabilistic loop reasoning with invariants

what it is and when to use it

The basic loopUnroll rule only unfolds a loop and may not terminate proof search. The paper relates its system to classic loop-invariant reasoning. The key step is to invent both an invariant and a substitution describing the symbolic state at loop termination. Its qualitative rule uses probability one; its quantitative rule requires preservation of the successor expectation. The paper says: “The key aspect is to invent both an invariant and the substitution at termination, which (roughly) correspond to proposing a loop invariant in Hoare logics.” (section 5 discussion, p. 12)

how to do it

1. Choose an invariant I and a symbolic update U′ representing the loop state (section 5 discussion).
2. Prove I initially under U (the first premise of loopInvariant/loopQual).
3. Under ¬e ∧ I, prove the continuation postcondition (second premise).
4. Under e ∧ I, prove that the loop body re-establishes I (third premise).
5. For qualitative correctness, use probability bound 1; for a quantitative bound p, prove the loop successor preserves the expected postcondition (rules loopQual and loopPreserving, p. 12).

Verus form (inference)

Inference: state I as a Verus loop invariant, prove initialization and preservation, and use a ghost probability bound in the method’s ensures. The termination substitution corresponds to a ghost function describing abstract state after the loop. Verus’s loop invariants prove safety/functional facts; quantitative probability preservation still requires a separately modeled distribution and arithmetic lemmas.

limits

The authors call their loop instrument “rather simple” and identify probabilistic loop invariants as subtle (section 5 discussion and section 7, pp. 12, 14). They plan to experiment with weakest-precondition rules in future work. Inference: the paper does not provide an automated invariant synthesizer, a completeness result for loops, or an empirical success rate across loop benchmarks.

technique 4: prototype symbolic execution with Crowbar and Z3

what it is and when to use it

Crowbar is a modular symbolic-execution engine using Z3. The authors encode pGCL in Crowbar’s ABS front end, annotate postconditions with [Spec: Ensures(e)], probability bounds with [Spec: Prob(e)], and branch kinds with [Spec: Demonic] or [Spec: Prob(e)]. The paper reports: “Crowbar performs the symbolic execution and uses Z3 to discharge formulas without modalities.” (section 6, p. 13)

how to do it

1. Encode the pGCL program in Crowbar’s ABS-shaped syntax (section 6).
2. Annotate the final property and probability bound (Figure 4, p. 13).
3. Mark demonic and probabilistic branches with their annotations (section 6).
4. Run Crowbar to generate the proof tree and constraints (section 6).
5. Pass arithmetic constraints to Z3 after modalities have been eliminated (section 6).

The paper uses this prototype to automatically generate the complete Monty Hall proof and constraints (section 5 example, p. 12), but reports no runtime, number of constraints, or success denominator. The prototype front end is not a verified compiler from pGCL to ABS; its encoding and annotations remain trusted.

Verus form (inference)

Inference: a Verus integration would generate proof obligations directly in Rust/Verus or in a verified intermediate model, then use Verus’s underlying solver for arithmetic. Crowbar’s ABS annotation syntax and modality elimination do not carry over. A separate checked translation would be needed before claiming that generated obligations correspond to executable Rust.

what VL should retain and threat assessment

The paper already develops the forward symbolic-execution pattern, branch-wise probability constraints, soundness induction, and a prototype solver pipeline. Inference: VL should not redo these as generic formal-verification ideas. The useful transfer is a contract-to-proof pipeline for randomized agent components: model choices explicitly, accumulate branch constraints, and separate solver discharge from semantic trust in the model. Inference: threat to agent-written verified Rust is low for ordinary memory-safety verification because the paper is probabilistic logic rather than Rust verification; it is moderate for products that need guarantees about randomized policies, sampling, or expected outcomes, where its branch and invariant patterns could supply a competing proof workflow.

techniques for the catalog

• symbolic-update pDL: represent probabilistic reachability and forward state changes with [s]p φ and {U}φ
• constraint-generating execution: execute syntax-directed rules and combine branch probability bounds into SMT constraints
• probabilistic loop invariants: prove initialization, preservation, termination substitution, and expectation preservation
• solver-backed prototype: encode pGCL annotations in a symbolic executor and discharge modality-free arithmetic with Z3

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15