Pith. sign in

REVIEW 3 major objections 5 minor 44 references

Multiobjective Preexpectation Reasoning for Probabilistic Programs

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper shows that the almost-achievable trade-offs of a probabilistic program form exactly the least fixed point of a Bellman operator on convex value sets, computed by a syntactic transformer.

desk verdict A serious multiobjective preexpectation calculus that is mostly sound, but the operational soundness theorem is a sketch rather than a proof, and the whole paper leans on it. read the letter →

arxiv 2608.13268 v1 pith:OIGJECWS submitted 2026-08-13 cs.PL cs.LO

Lena Verscht , Hannah Mertens , Kevin Batz , Sebastian Junges , Benjamin Lucien Kaminski , Joost-Pieter Katoen This is my paper · ORCID
classification cs.PLcs.LO MSC 68Q5568Q6068Q8790C29
keywords multiobjectivepreexpectationParetofrontprobabilisticprogramsweakestconvexHoarepowerdomainstrategysynthesisscalarizationMarkovdecisionprocesses
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Probabilistic programs with nondeterministic choices model planning problems where a strategy resolves the nondeterminism to optimize expected outcomes. This paper asks not for the best value of a single objective but for the whole set of value vectors simultaneously achievable by randomizing over program refinements, and it proves that this set is computable by a program-level transformer, the multiobjective preexpectation transformer $\mathrm{mop}$, a conservative extension of weakest preexpectations. $\mathrm{mop}$ maps a tuple of postexpectations to an element of the convex Hoare powerdomain, supports invariant-based loop proofs, and for $n=1$ collapses to the classical weakest preexpectation. The load-bearing result is that $\mathrm{mop}$ coincides with the Scott closure of the achievable vectors and, operationally, with the least fixed point of a generalized Bellman operator on the induced countable-state MDP. A sympathetic reader should care because this gives a deductive, syntax-directed calculus for Pareto-front reasoning over infinite-state MDPs, together with rules for synthesizing the witnessing mixed determinizations.

What carries the argument

The central object is the convex Hoare powerdomain $\mathbb{H}$: nonempty, downward-closed, convex-closed, and Scott-closed subsets of $\mathbb{R}^n_{\ge 0}$, used to represent the region under the Pareto front. The multiobjective preexpectation transformer $\mathrm{mop}$ lifts each weakest-preexpectation rule to this domain; for loops it takes the least fixed point of the characteristic function $\Phi_{\mathrm{mop}}(X) = [\neg\varphi]\cdot F \oplus [\varphi]\cdot \mathrm{mop}[\![C']\!](X)$. Two identities carry the argument: scalarization ($\mathrm{wp}$ of the weighted sum $w\cdot f$ is the maximum of $w\cdot x$ over the $\mathrm{mop}$ set) and halfspace reconstruction (the $\mathrm{mop}$ set is the intersection of the supporting halfspaces over all weight vectors). Its operational counterpart is the generalized Bellman operator $\Phi_M^{\mathrm{Pareto}}$ on multivalue functions, whose least fixed point over the program's MDP coincides with $\mathrm{mop}$.

What would settle it

Take the program that in round $i$ either terminates with reward vector $(1-2^{-i}, 2^i)$ or continues. Compute $\mathrm{mop}[\![C]\!](\mathrm{dwc}(\{(x,y)\}))$ and compare it with the halfspace intersection $\bigcap_{w\in W}\{x \mid w\cdot x \le \mathrm{wp}[\![C]\!](w\cdot f)(\sigma)\}$. If the two sets differ at the point $(1,\infty)$, or if $\max\{w\cdot x \mid x\in \mathrm{mop}[\![C]\!](\mathrm{dwc}(\{f\}))(\sigma)\}$ differs from $\mathrm{wp}[\![C]\!](w\cdot f)(\sigma)$ for a single weight $w$, the compactness foundation behind the scalarization theorems is refuted.

Watch

Extended reading notes

Core claim

The paper's own formulation of the central claim is Corollary 10.7: for every program $C$, tuple of postexpectations $f$, and state $\sigma$, $\mathrm{mop}[\![C]\!](\mathrm{dwc}(\{f\}))(\sigma) = \mathrm{cl}(\mathrm{Ach}^{C,f}_\sigma)$, i.e. the transformer returns exactly the Scott closure of the set of value vectors achievable by mixed determinizations, and the maximal elements of this set are the Pareto front. This is obtained through operational soundness (Theorem 10.6): $\mathrm{mop}$ is the least fixed point of a generalized Bellman operator on convex sets of reward vectors over the countable-state, finite-action MDP induced by the program, with no finite-state assumption. The companion identities are scalarization (Theorem 7.1), $\mathrm{wp}[\![C]\!](w\cdot f)(\sigma)=\max\{w\cdot x \mid x\in \mathrm{mop}[\![C]\!](\mathrm{dwc}(\{f\}))(\sigma)\}$, and halfspace reconstruction (Theorem 7.3), $\mathrm{mop}[\![C]\!](\mathrm{dwc}(\{f\}))(\sigma)=\bigcap_{w\in W}\{x \mid w\cdot x\le \mathrm{wp}[\![C]\!](w\cdot f)(\sigma)\}$. From these the paper derives sufficient conditions for exact synthesis of Pareto-optimal mixed determinizations and a Straszewicz-style guarantee that every extreme point can be approximated arbitrarily closely by synthesized witnesses.

Load-bearing premise

The load-bearing premise is that every element of the convex Hoare powerdomain is compact in the extended nonnegative orthant with the convention $0\cdot\infty=0$, so along any weight direction a maximum is attained and any point outside the set can be separated by a supporting halfspace; if that compactness fails, the scalarization equality, the halfspace characterization, and the descending fixpoint iteration lose their foundation.

Editorial extensions

If this is right

  • For any point in the multiobjective preexpectation, some mixed determinization realizes the point up to arbitrarily small error; if the set of determinization values is Scott closed, exact realization follows.
  • Weighted-sum optimization is complete for exposed Pareto points, and every non-exposed extreme point can be approached arbitrarily closely by synthesized determinizations.
  • The calculus conservatively extends weakest preexpectations: with a single objective, mop returns the downward closure of the ordinary wp value.
  • Multiobjective invariants give sound loop proofs: superinvariants bound the least fixed point from above; subinvariants bound it from below under demonic almost-sure termination with bounded objectives or demonic certain termination; and lower omega-invariants give lower bounds without side conditions.
  • The equality with the Bellman operator transfers multiobjective MDP verification to countable-state, finite-action MDPs at program level, bypassing the finite-state restriction of earlier multiobjective MDP work.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Multiobjective refutation could be reduced to single-objective proof obligations: to show a point is not achievable it suffices to find one weight vector whose supporting halfspace excludes it, and each such obligation is a standard wp query.
  • The paper reports that key invariants were machine-proposed and machine-checked while some loop calculations are delegated as straightforward; this points to invariant discovery, not the calculus, as the practical bottleneck, and automation of convex-Hoare invariant search is the natural next step.
  • Because mixed determinizations use only finitely supported distributions, synthesized strategies remain executable as initial coin flips; moving to infinite mixtures would need a continuity result outside the current rules.
  • The framework is built around reachability-style expectations, so translating discounted or long-run average objectives into bounded reachability rewards over an expanded state space is a plausible route to extend the calculus.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper develops a multiobjective preexpectation transformer, mop, for probabilistic programs with nondeterminism. mop maps a tuple of postexpectations to an element of the convex Hoare powerdomain: the set of simultaneously achievable value vectors, downward closed, convex, and Scott closed. The authors prove basic healthiness properties, invariant-based loop rules for upper and lower bounds, a scalarization theorem relating mop to classical weakest preexpectations via weighted sums, and conditions for synthesizing mixed determinizations that realize Pareto-optimal trade-offs. They then relate mop to a generalized Bellman operator on the operational MDP semantics of pGCL and claim an exact correspondence for countable-state, finite-action MDPs without finite-state restrictions. Three case studies (robot, casino, queue) illustrate the calculus with closed-form Pareto fronts.

Significance. If the main soundness theorem is fully established, the paper would be a substantial contribution: it provides a program-level, deductive calculus for multiobjective strategy synthesis over infinite-state MDPs, conservatively extending classic weakest preexpectations and connecting to the finite-state multiobjective MDP literature. The scalarization result (Theorem 7.1) and the halfspace characterization (Theorem 7.3) are elegant and well developed, and the case studies give explicit, checkable closed forms. The paper is also honest about its limitations in Section 12. However, the headline equivalence between mop and almost-achievable values, Corollary 10.7, rests on Theorem 10.6, which is currently asserted rather than proved; this gap is load-bearing and must be closed before the central claim can be accepted. The compactness concern raised in the stress-test note is, on inspection, addressed by the footnote to Theorem 7.1: the directed-set argument there does establish topological closedness of downward-closed Scott-closed sets in Rbar^n, so I do not base my recommendation on that point.

major comments (3)
  1. [Section 10.3, Theorem 10.6] The central operational soundness theorem is not actually proved. The proof consists of two sentences: the direction mopJ C K(F)(σ) ⊒ (lfp Φ_O)((C,σ)) is claimed by 'essentially showing' that mopJ C K(F) is a fixed point of the Bellman operator, and the converse is said to follow 'via induction on the program structure, using a compositionality lemma for sequential composition' that is never stated. This is not a presentation issue: Corollary 10.7 and Lemma 10.8, which are the paper's main characterization of the achievable set, are direct consequences of Theorem 10.6. The cited scalar analogue [Batz et al. 2024b, Theorem 6] does not cover Minkowski sums with probabilities, convex and Scott closures in the Hoare powerdomain, or intermediate configurations such as (C1#C2, σ) and loop unfoldings. Please supply the full proof, including an explicit compositionality lemma, the loop case, and the verification that the Bellman operator's action-enabledness matches the guarded-choice semantics at every state.
  2. [Section 6, Theorem 6.7] The descending fixpoint iteration theorem for molp is not established. The proof itself states that the required ω-co-continuity 'is not routine', defers nested loops to 'a Park-style argument', and claims that closure points involving ∞-components are handled by 'reduc[ing] to the bounded sublattices via finite caps' without giving that reduction. Since Lemma 6.8, and consequently Lemmas 6.9 and 6.10 and the lower-bound rules Theorems 6.11 and 6.12, all depend on Theorem 6.7, the lower-bound loop reasoning is currently conditional. Either provide a complete proof of ω-co-continuity, or explicitly mark these rules as relying on an unproved conjecture and adjust the claims in Section 6 accordingly.
  3. [Section 9, Theorem 9.3 and Section 10.2, Lemma 10.3] The reductions between memoryful and memoryless schedulers and between mixed determinizations and schedulers are only sketched. The proof of Theorem 9.3 lists four high-level steps but does not define the schedulers ρ_k, the finite-state fragments M_k^⊥, or the precise reward preservation argument when passing from the finite fragment back to the full countable MDP. Lemma 10.3 similarly asserts the correspondence 'by induction on the program structure' and 'by the reverse construction' without giving the construction. These results feed directly into Corollary 10.5 and hence into Corollary 10.7, so they need to be written out in enough detail to be checked.
minor comments (5)
  1. [Section 6, Lemmas 6.9 and 6.10] The headings 'Eqivalence of Fixpoints I/II' contain a typo; both should read 'Equivalence'.
  2. [Section 8.1, footnote 4] The claim that the invariant was 'proposed by Anthropic's Claude Fable 5 and subsequently verified in Lean' is unsupported and irrelevant to the mathematical content; either provide a reproducible artifact or remove the claim.
  3. [Section 8.1, formula for L_k(t,g)] The displayed formula for L_k(t,g) ends with a stray '.𝑠' that appears to be a typographical artifact.
  4. [Section 5.3, Theorem 5.8] The proof of basic healthiness is very brief; in particular, the well-definedness of the least fixed point for loops in the convex Hoare powerdomain deserves a few more sentences, since it is not entirely routine.
  5. [Section 4, Lemma 4.4] The proof of Lemma 4.4 is omitted. A short argument showing that dwc(Pareto) = cl(Ach) would be helpful, as the lemma is used in Lemma 7.7.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: mop, Ach, and the Bellman operator are independently defined, and the central equality is a proven soundness correspondence rather than an assumed input.

full rationale

The paper's derivation chain is self-contained in the sense required for a circularity finding. The multiobjective preexpectation transformer mop is defined syntactically (Definition 5.5, Table 2) as a lifting of the classical wp rules to the convex Hoare powerdomain; the set of achievable points Ach is defined separately via weakest preexpectations of mixed determinizations (Definition 4.1); and the MDP-side Bellman operator is defined over operational semantics (Definition 9.6). The advertised equality mopJ𝐶K(dwc({𝑓}))(𝜎) = cl(Ach^{𝐶,𝑓}_𝜎) is not baked into any of these definitions. It is derived through independent intermediate results: the scalarization equality (Theorem 7.1) is proven by induction on programs, the halfspace representation (Theorem 7.3) follows by a separating-hyperplane argument, and the operational correspondence (Corollary 10.7) combines the Bellman fixed-point characterization (Theorem 9.7), the determinization-to-scheduler correspondence (Lemma 10.3), and the equivalence of closures (Corollary 10.5). The paper does rely on co-authored prior work, especially [Batz et al. 2024a] for single-objective programmatic strategy synthesis and [Batz et al. 2024b, Theorem 6] as a proof template for soundness, but these citations are parameter-free, do not include the multiobjective target result, and are not used to define mop or the achievable set. The proof of Theorem 10.6 is compressed into a short sketch and is arguably a correctness or presentation risk; however, a missing or abbreviated proof is not the same as a circular reduction, and none of the quoted steps equates the conclusion with an input by construction. No fitted parameters, renamed empirical patterns, or author-imported uniqueness claims appear. Therefore the appropriate finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No physical or empirical entities are introduced. The mop transformer and mixed determinizations are defined constructively over existing powerdomain constructions and program syntax, not postulated to explain observations. The only unusual external assertion, the Lean verification footnote, is not an entity but an unverified claim about verification.

assumptions (5)
  • standard math R-bar_geq0 with the order topology is compact, and every Hoare powerdomain element is a closed subset; continuous functions on compact sets attain maxima.
    Used in Theorem 7.1 and Theorem 7.3 to justify the existence of maxima and separating halfspaces; if this topology fails, the scalarization equality breaks.
  • standard math Separating hyperplane theorem for disjoint closed convex sets with one compact, Caratheodory's theorem, and Straszewicz's theorem on exposed points.
    Used in Sections 7.3 and 7.4 for representing the achievable region and for approximate synthesis of non-exposed extreme points.
  • standard math Cantor's intersection theorem for decreasing sequences of nonempty compact sets.
    Used in Theorem 6.7 and Lemma 6.8 to commute Minkowski sums and suprema with descending intersections in the Hoare powerdomain.
  • domain assumption The operational MDP of pGCL has countable states and finite actions, and memoryless schedulers suffice for almost-achievable rewards.
    Bridges the program-level mop transformer to the MDP Bellman operator in Theorems 9.3, 9.7 and 10.6; assumes Forejt et al. 2011 Proposition 6 applies to finite-state fragments of the operational MDP.
  • domain assumption The standard weakest preexpectation semantics wp and the programmatic strategy synthesis results of Batz et al. 2024a are correct.
    The paper builds on these for single-objective optimal determinizations and upper/lower bound completeness, citing Theorems 2.5 and 6.7 of that prior work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Multiobjective Preexpectation Reasoning for Probabilistic Programs." pith.science (2026). https://pith.science/paper/OIGJECWS

@misc{pith2026260813268,
  author       = {Pith},
  title        = {Pith review of: Multiobjective Preexpectation Reasoning for Probabilistic Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OIGJECWS}},
  note         = {Machine review of arXiv:2608.13268}
}
read the original abstract

Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective setting, optimizing several outcomes at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that randomize over non-probabilistic determinizations. We prove the transformer and synthesis rules sound against an operational MDP semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using various case studies.

Figures

Figures reproduced from arXiv: 2608.13268 by the authors.

Figure 1
Figure 1. Nondeterministic program𝐶robot as well as two determinizations maximizing [𝑝 ≥ 𝑔] and 𝑡, respectively. • Building on this transformer, we lift invariant-based loop reasoning to the multiobjective setting, for both upper and lower bounds (Section 6). • We discuss when it is possible to synthesize a determinization realizing a given specification, and show how to do so (Section 7). • We establish an exact corresponden… view at source ↗
Figure 2
Figure 2. Illustration of Pareto front (in red) for the program [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Calculus annotations for a simple program with respect to the multiobjective expectation dwc({(𝑥, 𝑦)}). Read bottom to top [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (17 more)
Figure 4
Figure 4. Figure 4: Rules defining the determinization relation [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Illustration of the Pareto front (blue) lying in between the achievable (green) and the unachievable (white) points for a fixed state 𝜎 and 𝑛 = 2. The Pareto front for each state 𝜎 is precisely the set of nondominated achievable points, i.e., those lying on the boundar…
Figure 6
Figure 6. Figure 6: Annotations for the computation of mop J𝐶runK(dwc({(𝑥, 𝑦)})) for Example 5.7. 5.3 Healthiness Conditions Healthiness conditions are routine results in predicate transformer semantics to characterize well￾behaved operators and ensure compatibility with the underlying or…
Figure 7
Figure 7. Figure 7: Illustrations of the relation between mop and wp for weighted sums. This set contains all vectors whose weighted sum 𝑤 · 𝑥 is no larger than the optimal weighted sum achievable by the program 𝐶. Theorem 7.1 implies that for any 𝑦 ∈ R 𝑛 ≥0 which is not included in the h…
Figure 8
Figure 8. Figure 8: Nondeterministic program 𝐶circ and a determinization 𝐶 𝑤1 circ optimal for 𝑤1 · (𝑥, 𝑦), achieving 𝜏 ′ 1 . to the same supporting face. Hence, if the face is a singleton (which, by definition, means that 𝑝 is exposed), we are done. Unfortunately, not every extreme point…
Figure 9
Figure 9. Figure 9: Illustration of mop J𝐶circK(dwc({(𝑥, 𝑦)})), including target points 𝜏1 and 𝜏2 for synthesis [PITH_FULL_IMAGE:figures/full_fig_p032_9.png]
Figure 10
Figure 10. Figure 10: Further determinizations of 𝐶circ from Figure 8a, both optimal for 𝑤2 · (𝑥, 𝑦). Assume we want to synthesize a determinization achieving the point 𝜏1 = [PITH_FULL_IMAGE:figures/full_fig_p033_10.png]
Figure 11
Figure 11. Figure 11: Nondeterministic program 𝐶robot as well as two determinizations achieving Pareto optimal points 𝑉1 and 𝑉2, respectively. The reason is that 𝜏2 is not exposed: the face containing 𝜏2 also contains all points on the line from (1, 0) to (1, 1). Consequently, the determin…
Figure 12
Figure 12. Figure 12: Illustration of mop J𝐶robotK(dwc({(𝑡, [𝑝 ≥ 𝑔])})) for several initial states 𝜎. The x-axis shows 𝑡 and the y-axis shows [𝑝 ≥ 𝑔]. the last two cells, because that sprint is free. 𝑉3’s larger expected leftover is earned solely by failing earlier more often. Expected lef…
Figure 13
Figure 13. Figure 13: Illustration of the weight vectors needed to achieve [PITH_FULL_IMAGE:figures/full_fig_p038_13.png]
Figure 14
Figure 14. Figure 14: Annotations for computing mop J𝐶casinoK(dwc({(𝑖, 𝑛)})) We again prove an exact fixpoint of the characteristic function using rules for lower and upper bounds. The invariant we will use is 𝐼 = [𝑐 = 0] · dwc({(𝑖, 𝑛)}) ⊕ [𝑐 = 1] · Ä 𝑚∈N dwc 𝑖 + 3 − 2 𝑚+1 3𝑚 ,  2 3 𝑚…
Figure 15
Figure 15. Figure 15: Annotations for computing mop of the loop body of 𝐶casino and invariant 𝐼. and the winnings become 𝑛 + 𝑚 with probability 2 3 𝑚 . The Scott and convex closed union over 𝑚 ∈ N captures all possible numbers of successful gambling rounds. To prove this invariant correct…
Figure 16
Figure 16. Figure 16: Illustration of mop J𝐶casinoK(dwc({(𝑖, 𝑛)})) for any initial state. Moreover, all extreme points are exposed, so pure determinizations achieve all exposed extreme points; mixed determinizations realize the intervening points on the boundary. Notably, this also applies…
Figure 17
Figure 17. Figure 17: The program 𝐶queue. 𝑎 = 0.3 𝑎 = 0.5 𝑎 = 0.7 𝑒 𝑝 0.5 1 1.5 1.7 1.8 1.9 2 [PITH_FULL_IMAGE:figures/full_fig_p042_17.png]
Figure 18
Figure 18. Figure 18: mop J𝐶queueK(dwc({(𝑒, 𝑝)})) for initial states where 𝑁 = 𝑇 = 2, depending on 𝑎. Darker green corresponds to higher initial values of the arrival probability 𝑎. The result depends heavily on the initial values of 𝑇 and 𝑁. For simplicity, we focus on initial states wher…
Figure 19
Figure 19. Figure 19: MDP M1 discussed in Example 9.2. States without label are assumed to have reward (0, 0). Given rew: 𝑇 → R 𝑛 ≥0 , we define the function ExpRew𝜌 JMK (rew) : 𝑆init → R 𝑛 ≥0 , which maps an initial state 𝑠init to its expected (reachability-)reward ExpRew[𝑘] M,rew 𝑠init,𝜌…
Figure 20
Figure 20. Figure 20: Rules defining the small-step execution relation [PITH_FULL_IMAGE:figures/full_fig_p047_20.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 25 canonical work pages

  1. [1]

    1995.Domain theory

    Samson Abramsky and Achim Jung. 1995.Domain theory. Oxford University Press, Inc., USA, 1–168. https://dl.acm.org/ doi/10.5555/218742.218744 Pranav Ashok, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger, and Tobias Winkler

    work page arXiv 1995

  2. [5]

    9035), Christel Baier and Cesare Tinelli (Eds.)

    Proceedings (Lecture Notes in Computer Science, Vol. 9035), Christel Baier and Cesare Tinelli (Eds.). Springer, 256–271. https://doi.org/10.1007/978-3-662-46681-0_22 Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, and Tobias Winkler. 2024a. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs.Proc. ACM Program. Lang.8, P...

    work page doi:10.1007/978-3-662-46681-0_22 2024

  3. [9]

    Markov Decision Processes with Multiple Long-Run Average Objectives. InFSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4855), Vikraman Arvind and Sanjiva Prasad (Eds.). Springer, 473–484. https://doi...

    work page doi:10.1007/978-3-540-77050-3_39 2007

  4. [12]

    8054), Kaustubh R

    Proceedings (Lecture Notes in Computer Science, Vol. 8054), Kaustubh R. Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro R. D’Argenio (Eds.). Springer, 322–337. https://doi.org/10.1007/978-3-642-40196-1_28 Patrick Cousot and Michael Monerau

    doi:10.1007/978-3-642-40196-1_28

  5. [14]

    7211), Helmut Seidl (Ed.)

    Proceedings (Lecture Notes in Computer Science, Vol. 7211), Helmut Seidl (Ed.). Springer, 169–193. https://doi.org/10.1007/978-3-642-28869-2_9 Ankush Das, Di Wang, and Jan Hoffmann

    work page doi:10.1007/978-3-642-28869-2_9

  6. [16]

    Methods Comput

    Multi-Objective Model Checking of Markov Decision Processes.Log. Methods Comput. Sci.4, 4 (2008). https://doi.org/10.2168/LMCS-4(4:8)2008 Kousha Etessami and Emanuel Martinov

    doi:10.2168/lmcs-4(4:8)2008 2008

  7. [17]

    In Reachability Problems - 14th International Conference, RP 2020, Paris, France, October 19-21, 2020, Proceedings (Lecture Notes in Computer Science, Vol

    Qualitative Multi-objective Reachability for Ordered Branching MDPs. In Reachability Problems - 14th International Conference, RP 2020, Paris, France, October 19-21, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12448), Sylvain Schmitz and Igor Potapov (Eds.). Springer, 67–82. https://doi.org/10.1007/978-3- 030-61739-4_5 Owain Evans, Andreas ...

    doi:10.1007/978-3- 2020

  8. [20]

    6605), Parosh Aziz Abdulla and K

    Proceedings (Lecture Notes in Computer Science, Vol. 6605), Parosh Aziz Abdulla and K. Rustan M. Leino (Eds.). Springer, 112–127. https://doi.org/10.1007/978-3-642-19835-9_11 Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker

    doi:10.1007/978-3-642-19835-9_11

Show all 44 references
  1. [21]

    InAutomated Technology for Verification and Analysis - 10th International Symposium, ATV A 2012, Thiruvananthapuram, India, October 3-6,

    Pareto Curves for Probabilistic Model Checking. InAutomated Technology for Verification and Analysis - 10th International Symposium, ATV A 2012, Thiruvananthapuram, India, October 3-6,

    2012

  2. [22]

    7561), Supratik Chakraborty and Madhavan Mukund (Eds.)

    Proceedings (Lecture Notes in Computer Science, Vol. 7561), Supratik Chakraborty and Madhavan Mukund (Eds.). Springer, 317–332. https://doi.org/10.1007/978-3-642-33386-6_25 Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen

    doi

  3. [23]

    ACM Program

    Aiming low is harder: induction for lower bounds in probabilistic program verification.Proc. ACM Program. Lang.4, POPL (2020), 37:1–37:28. https: //doi.org/10.1145/3371105 Mordechai I. Henig

    2020 doi

  4. [27]

    Methods Comput

    Mixed powerdomains for probability and nondeterminism.Log. Methods Comput. Sci.13, 1 (2017). https://doi.org/10.23638/LMCS-13(1:2)2017 Dexter Kozen

    2017 doi

  5. [30]

    InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S

    Bounded expectations: resource analysis for probabilistic programs. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 496–512. ...

    2018

  6. [32]

    Comput.23, 4 (2011), 493–517

    Enhancement of Sandwich Algorithms for Approximating Higher-Dimensional Convex Pareto Sets.INFORMS J. Comput.23, 4 (2011), 493–517. https://doi.org/10.1287/IJOC.1100. 0419 R. Tyrrell Rockafellar. 1970.Convex Analysis. Princeton University Press. Diederik Roijers and Shimon Whi...

    2011 doi

  7. [34]

    InAutomata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings (Lecture Notes in Computer Science, Vol

    Power Domains and Predicate Transformers: A Topological View. InAutomata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings (Lecture Notes in Computer Science, Vol. 154), Josep Díaz (Ed.). Springer, 662–675. https://doi.org/10.1007/BFB...

    1983 doi

  8. [40]

    InPLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N

    Central moment analysis for cost accumulators in probabilistic programs. InPLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 559–573. htt...

    2021

  9. [41]

    CoRRabs/2006.14010 (2020)

    Raising Expectations: Automating Expected Cost Analysis with Types. CoRRabs/2006.14010 (2020). arXiv:2006.14010 https://arxiv.org/abs/2006.14010 54 Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, and Joost-Pieter Katoen Kazuki Watanabe and...

    2020 arXiv

  10. [42]

    InProceedings of the 35th International Joint Conference on Artificial Intelligence and the 29th European Conference on Artificial Intelligence (IJCAI-ECAI 2026)

    Automated Safety Verification of Posterior Distributions of Probabilistic Programs. InProceedings of the 35th International Joint Conference on Artificial Intelligence and the 29th European Conference on Artificial Intelligence (IJCAI-ECAI 2026). To appear. D.J White

    2026

  11. [299]

    2002.1029838 Di Wang, Jan Hoffmann, and Thomas W

    https://doi.org/10.1109/LICS. 2002.1029838 Di Wang, Jan Hoffmann, and Thomas W. Reps

    2002 arXiv

  12. [1955]

    Math.5, 2 (1955), 285–309

    A lattice-theoretical fixpoint theorem and its applications.Pacific J. Math.5, 2 (1955), 285–309. Regina Tix

    1955

  13. [1979]

    InAbstract Software Specifications, 1979 Copenhagen Winter School, January 22 - February 2, 1979, Proceedings (Lecture Notes in Computer Science, Vol

    Dijkstras Predicate Transformers & Smyth’s Power Domaine. InAbstract Software Specifications, 1979 Copenhagen Winter School, January 22 - February 2, 1979, Proceedings (Lecture Notes in Computer Science, Vol. 86), Dines Bjørner (Ed.). Springer, 527–553. https://doi.org/10.1007...

    1979 doi

  14. [1982]

    Multi-objective infinite-horizon discounted Markov decision processes.J. Math. Anal. Appl.89, 2 (1982), 639–647. https://doi.org/10.1016/0022-247X(82)90122-6 Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti

    1982 doi

  15. [1983]

    Control Optim.21, 3 (May 1983), 490–499

    Vector-Valued Dynamic Programming.SIAM J. Control Optim.21, 3 (May 1983), 490–499. https://doi.org/10.1137/0321030 Claire Jones. 1990.Probabilistic non-determinism. Ph. D. Dissertation. University of Edinburgh, UK. https://hdl.handle.net/ 1842/413 Multiobjective Preexpectation...

    1983 doi

  16. [1985]

    A Probabilistic PDL.J. Comput. Syst. Sci.30, 2 (1985), 162–178. https://doi.org/10.1016/0022- 0000(85)90012-1 Annabelle McIver and Carroll Morgan. 2005.Abstraction, Refinement and Proof for Probabilistic Systems. Springer. https: //doi.org/10.1007/B138392 Carroll Morgan, Annab...

    1985 doi

  17. [1993]

    https://doi.org/10.1016/0377- 2217(93)90192-P Valeriu Soltan

    Approximating the noninferior set in multiobjective linear programming problems.European Journal of Operational Research68, 3 (1993), 356–373. https://doi.org/10.1016/0377- 2217(93)90192-P Valeriu Soltan. 2019.Lectures on Convex Sets. World Scientific. https://doi.org/10.1142/...

    1993 doi

  18. [1996]

    Probabilistic Predicate Transformers.ACM Trans. Program. Lang. Syst.18, 3 (1996), 325–353. https://doi.org/10.1145/229542.229547 James R. Munkres. 2000.Topology(2nd ed.). Prentice Hall, Upper Saddle River, NJ. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann

    1996

  19. [1998]

    InWorkshop on Domains IV 1998, Haus Humboldtstein, Remagen-Rolandseck, Germany, October 2-4, 1998 (Electronic Notes in Theoretical Computer Science, Vol

    Convex power constructions for continuous d-cones. InWorkshop on Domains IV 1998, Haus Humboldtstein, Remagen-Rolandseck, Germany, October 2-4, 1998 (Electronic Notes in Theoretical Computer Science, Vol. 35), Dieter Spreen, Ralf Greb, Holger Schulz, and Michel P. Schellekens ...

    1998 doi

  20. [2002]

    In17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings

    The Powerdomain of Indexed Valuations. In17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society,

    2002

  21. [2006]

    InSTACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23-25, 2006, Proceedings (Lecture Notes in Computer Science, Vol

    Markov Decision Processes with Multiple Objectives. InSTACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23-25, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3884), Bruno Durand and Wolfgang Thomas (Eds.). Spr...

    2006 doi

  22. [2007]

    https://doi.org/10.1007/S11225-007-9052-Y Krishnendu Chatterjee

    Continuous Lattices and Domains.Stud Logica86, 1 (2007), 137–138. https://doi.org/10.1007/S11225-007-9052-Y Krishnendu Chatterjee

    2007 doi

  23. [2008]

    InMachine Learning, Proceedings of the Twenty-Fifth International Conference (ICML 2008), Helsinki, Finland, June 5-9, 2008 (ACM International Conference Proceeding Series, Vol

    Learning all optimal policies with multiple criteria. InMachine Learning, Proceedings of the Twenty-Fifth International Conference (ICML 2008), Helsinki, Finland, June 5-9, 2008 (ACM International Conference Proceeding Series, Vol. 307), William W. Cohen, Andrew McCallum, and ...

    2008

  24. [2009]

    Predicate transformers for extended probability and non-determinism.Math. Struct. Comput. Sci.19, 3 (2009), 501–539. https://doi.org/10.1017/S0960129509007555 Klaus Keimel and Gordon D. Plotkin

    2009 doi

  25. [2011]

    Quantitative Multi- objective Verification for Probabilistic Systems. InTools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011,...

    2011

  26. [2012]

    Probabilistic Abstract Interpretation. InProgramming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1,

    2012

  27. [2013]

    8087), Krishnendu Chatterjee and Jirí Sgall (Eds.)

    Proceedings (Lecture Notes in Computer Science, Vol. 8087), Krishnendu Chatterjee and Jirí Sgall (Eds.). Springer, 266–277. https://doi.org/10.1007/978-3-642-40313-2_25 Taolue Chen, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. 2013b. Synthesis for Multi-objecti...

    doi

  28. [2015]

    Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. InTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS ...

    2015

  29. [2017]

    https://agentmodels.org

    Modeling Agents with Probabilistic Programs. https://agentmodels.org. Accessed: 2026-8-12. Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

    2026

  30. [2018]

    ACM65, 5 (2018), 30:1–30:68

    Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.J. ACM65, 5 (2018), 30:1–30:68. https://doi.org/10.1145/ 3208102 Klaus Keimel and Gordon D. Plotkin

    2018

  31. [2020]

    Approximating Values of Generalized-Reachability Stochastic Games. InLICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 102–115. https://doi.o...

    2020

  32. [2021]

    InComputer Aided Verification - 33rd International Conference, CA V 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture Notes in Computer Science, Vol

    Latticed k-Induction with an Application to Probabilistic Programs. InComputer Aided Verification - 33rd International Conference, CA V 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 12760), Alexandra Silva and K. Rustan M....

    2021 doi

  33. [2022]

    ACM Program

    Weighted programming: a programming paradigm for specifying mathematical models.Proc. ACM Program. Lang.6, OOPSLA1 (2022), 1–30. https://doi.org/10.1145/3527310 52 Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, and Joost-Pieter Katoen Kev...

    2022 doi

  34. [2023]

    ACM Program

    Probabilistic Resource-Aware Session Types.Proc. ACM Program. Lang.7, POPL (2023), 1925–1956. https://doi.org/10.1145/3571259 Edsger W. Dijkstra. 1976.A Discipline of Programming. Prentice-Hall. https://dl.acm.org/doi/book/10.5555/550359 Kousha Etessami, Marta Z. Kwiatkowska, ...

    2023 doi

  35. [2025]

    ACM Program

    A Demonic Outcome Logic for Randomized Nondeterminism.Proc. ACM Program. Lang.9, POPL (2025), 539–568. https://doi.org/10.1145/3704855

    2025 doi

  36. [2026]

    https://doi.org/10

    Caesar: A Deductive Verifier for Probabilistic Programs.CoRRabs/2605.15827 (2026). https://doi.org/10. 48550/ARXIV.2605.15827 arXiv:2605.15827 Michael B. Smyth

    2026 doi arXiv

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.