Pith. sign in

REVIEW 2 major objections 6 minor 56 references

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)

T0 review · 2 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read This paper proves that minimal and maximal total expected rewards in Markov decision processes are exactly the least fixed points of the Bellman operators, even when rewards are infinite, and uses this to prove weakest-preexpectation…

desk verdict A solid generalization of Puterman's least-fixed-point characterizations to infinite rewards; the apparent circularity in Thm 3.1 is just a fixable citation slip. read the letter →

arxiv 2411.16564 v1 pith:U35Z66R2 submitted 2024-11-25 cs.LO cs.PL

Kevin Batz , Benjamin Lucien Kaminski , Christoph Matheja , Tobias Winkler This is my paper · ORCID
classification cs.LOcs.PL
keywords MarkovdecisionprocessesexpectedrewardsleastfixedpointsBellmanoperatorsweakestpreexpectationsprobabilisticprogramsinfinite-stateMDPsinfinite
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

The paper proves that minimal and maximal total expected rewards in Markov decision processes are exactly the least fixed points of their Bellman operators, with no finiteness restriction on rewards or expected rewards. Earlier characterizations of this kind existed for finite-state, positive-bounded, and negative models, but all assumed rewards are finite; a one-dimensional random walk already has infinite expected runtime, so those assumptions block probabilistic program verification. The theorem is then used to prove two weakest-preexpectation calculi, demonic and angelic, sound with respect to an operational MDP semantics for a probabilistic guarded command language with reward statements. A sympathetic reader should care because this supplies the missing fixed-point foundation for modular, compositional reasoning about expected costs and runtimes of unbounded-loop probabilistic programs.

What carries the argument

The min-Bellman and max-Bellman operators, defined by $\Phi^\min_{M,\mathrm{rew}}(v) = \lambda s.\, \mathrm{rew}(s) + \min_{a \in Act(s)} \sum_{s'} P(s,a,s')\,v(s')$ and analogously with $\max$, act on the complete lattice of value functions $S \to \mathbb{R}^\infty_{\ge 0}$ under the pointwise order. They are $\omega$-continuous because addition, multiplication, minima, and maxima are continuous on extended non-negative reals, so by the Kleene fixed point theorem their least fixed points are the suprema of iterates starting from zero. Lemma 2 identifies the $n{+}1$-st iterate with the $n$-step-bounded expected reward, and Theorem 3 passes to the limit; for the min case, Lemma 7's optimal memoryless scheduler makes the supremum/infimum swap valid.

What would settle it

A concrete check is to iterate $\Phi^\min_{M,\mathrm{rew}}$ from zero on the MDP of Figure 1 with $r > 0$: the theorem predicts convergence to $\mathrm{MinER} = 2$, and if any state's limiting value differs from $\mathrm{MinER}$, Theorem 3.1 fails; equally concrete is reading Appendix A.5 to see whether the equality used for the induced Markov chain is justified only by an internal invocation of 'Theorem 3'.

Watch

Extended reading notes

Core claim

The central claim is Theorem 3: for every MDP $M = (S, Act, P)$ with countable state space and every reward function $\mathrm{rew} : S \to \mathbb{R}^\infty_{\ge 0}$, the equalities $\operatorname{lfp} \Phi^\min_{M,\mathrm{rew}} = \lambda s.\, \mathrm{MinER}(M, s, \mathrm{rew})$ and $\operatorname{lfp} \Phi^\max_{M,\mathrm{rew}} = \lambda s.\, \mathrm{MaxER}(M, s, \mathrm{rew})$ hold. The maximal case follows by commuting two suprema; the minimal case requires swapping a supremum and an infimum, which is justified by constructing a memoryless scheduler that realizes the optimal choice at every state. A by-product is that uniformly min-optimal memoryless schedulers always exist, while max-optimal schedulers need not. The paper presents the result as a generalization of known least-solution theorems, with the only substantive relaxation being allowance of infinite rewards and infinite expected rewards.

Load-bearing premise

The load-bearing premise is that the theorem already holds for the one-action Markov chains induced by memoryless schedulers; the proof of Theorem 3.1 in the appendix appeals to 'Theorem 3' for exactly that case, so if the single-action case is not proved separately, the minimization half is not established as written.

Editorial extensions

If this is right

  • Weakest-preexpectation calculi for the reward language are sound with respect to the operational MDP semantics, including programs whose expected rewards are infinite.
  • Reachability probabilities are recovered as a special case by adding a sink and a 0/1 reward, so the least-fixed-point characterization applies to them unchanged.
  • For minimization, a memoryless uniformly optimal scheduler always exists, so the infimum in the definition of minimal expected reward is actually a minimum.
  • For maximization, optimal schedulers can fail to exist, so the characterization is a statement about suprema, not necessarily attained maxima.
  • Expected runtimes of probabilistic programs, which can be infinite even when termination is almost sure, are now covered by the fixed-point characterization.

Reading between the lines

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

  • An editor's inference: if the circularity in Appendix A.5 is repaired, the same least-fixed-point template should carry over to weakest-preexpectation calculi for conditioning, mixed-sign expectations, or amortized costs.
  • An editor's inference: the min/max asymmetry suggests that tool builders can rely on the least-fixed-point equation for minimization, but for maximization they should verify scheduler existence before interpreting the fixed point as an attained value.
  • An editor's inference: a natural next step is to examine signed or negative rewards, where the least-fixed-point characterization can fail and greatest fixed points become the relevant object.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 6 minor

Summary. The paper studies Markov decision processes with countably infinite state spaces, finite action sets, finitely branching transitions, and rewards taking values in the extended nonnegative reals. It defines minimal and maximal total expected rewards via path sums under schedulers, proves that the min- and max-Bellman operators are continuous, and states the main theorem (Theorem 3) asserting that the least fixed points of these operators coincide with minimal and maximal expected rewards. The paper then proves existence of a memoryless uniformly min-optimal scheduler and applies the fixed-point characterization to prove soundness of demonic and angelic weakest-preexpectation calculi for a probabilistic guarded command language with rewards against an operational MDP semantics.

Significance. If the main theorem is established, the paper provides a clean and useful generalization of classical least-fixed-point characterizations to nonnegative extended rewards, covering infinite-state MDPs with infinite expected rewards, which arise naturally in probabilistic program verification. The application to dwp/awp soundness is valuable, and the paper is largely self-contained, with detailed proofs for Lemma 2, Theorem 2, and the max case of Theorem 3.2. However, the proof of the min case contains a circular citation, so the central theorem is not proven as written and the contribution needs revision before it can be accepted.

major comments (2)
  1. [Appendix A.3, Lemma 7] The step “ER(M(S′), s, rew) = lfp Φ_{M(S′)} rew (Theorem 3)” occurs inside the proof of Theorem 3.1 and invokes the very theorem being proved. As written, this is circular and leaves Theorem 3.1 unproved. The gap is repairable: since M(S′) has exactly one enabled action per state, Theorem 3.2, which is proved independently in the same appendix, applies and gives lfp Φ^max_{M(S′)} rew = MaxER(M(S′), s, rew) = ER(M(S′), s, rew). The citation should be changed to Theorem 3.2 and the equality with the unique expected reward should be stated explicitly. This is a genuine load-bearing issue because Theorem 3.1, and hence Theorem 4 and the soundness proofs of Section 9, depend on it.
  2. [Appendix A.3, Lemma 7] The definition of the scheduler S reads S(s) = rew(s) + argmin_{a∈Act(s)} Σ_{s′∈Succs^a(s)} P(s,a,s′)·(lfp Φ^min_{M,rew})(s′), which is ill-typed: rew(s) is a reward value and cannot be added to an action. The intended definition is clearly S(s) = argmin_{a∈Act(s)} Σ ... with the stated tie-breaking rule. This should be corrected, since Lemma 7 is used in the proof of Theorem 3.1 and in Section 7.
minor comments (6)
  1. [Section 5] In the paragraph introducing partial orders, the sentence “v is ‘larger’ than u, in that all entries of u are component-wise larger than v” is backwards; it should say that all entries of v are at least as large as the corresponding entries of u.
  2. [Section 8.1] The introductory sentence “an application to operational semantics of probabilistic semantics” appears to contain a typo; it should read “probabilistic programs.”
  3. [Figure 5, rule 1] The rule for final configurations appears to be typeset as “(⇓, σ) N,1 → ⊥⊥ N,1 → ⊥”; it should be a single transition “(⇓, σ) N,1 → ⊥.”
  4. [Abstract] The abstract contains the misspelling “probabilisitic”; it should be “probabilistic.”
  5. [References] References [44] and [48] appear to be satirical or placeholder entries whose titles do not match the cited sources (the Rifleman’s Creed and stochastic Petri nets, respectively); they should be replaced by accurate citations or removed.
  6. [Section 9, Theorem 5] Theorem 5 states the healthiness properties without proof and attributes them to [31]; since Section 9 uses these properties to justify the definition of the loop semantics, a proof sketch or a more precise reference would improve self-containedness.

Circularity Check

1 steps flagged · score 4.0 of 10

Repairable self-reference in the proof of Theorem 3.1: the equality chain for the induced Markov chain cites 'Theorem 3' while proving Theorem 3, but the needed special case is independently covered by already-proved Theorem 3.2.

  1. self citation load bearing [Appendix A.5, proof of Theorem 3, proof of Inequality (7)]
    "= ER (M(S′), s, rew) (Definition 6.2) = lfp Φ_{M(S′)} rew (Theorem 3) = lfp Φ^min_M rew (Lemma 7)"

    This equality chain occurs inside the proof of Theorem 3 and is used to establish Inequality (7), the non-trivial half of the min/max exchange needed for Theorem 3.1. The displayed step '= lfp Φ_{M(S′)} rew (Theorem 3)' invokes the very theorem being proved, applied to the induced Markov chain M(S′). As written, the proof of Theorem 3.1 therefore depends on the theorem's conclusion for a special case. The circularity is repairable because Theorem 3.2, proved earlier in the same appendix, is independent and, for the single-action MDP M(S′), it gives exactly the same equality; however, the manuscript does not say this and instead cites the full 'Theorem 3' as if it were already available.

full rationale

The central fixed-point characterization is not fitted, renamed, or obtained from a prior by-construction definition: Theorem 2 (continuity) and Lemma 2 (step-bounded iteration) are proved directly, and the max case of Theorem 3 is derived by commuting suprema. The only genuinely circular-looking step is the internal self-reference in the proof of Theorem 3.1, where the equality 'lfp Φ_{M(S′)} rew (Theorem 3)' is used to justify Inequality (7). This is load-bearing in the proof as written, but it is not a deep circularity: Theorem 3.2 was already proved without using Theorem 3.1, and since M(S′) has exactly one enabled action per state, Theorem 3.2 directly yields lfp Φ_{M(S′)} rew = ER(M(S′), s, rew). Replacing the citation 'Theorem 3' by 'Theorem 3.2' repairs the proof. The healthiness properties in Theorem 5 are cited from the authors' prior work [31], but that is an externally published result and is not the paper's central fixed-point contribution, so it does not amount to load-bearing circularity. I therefore score the paper 4: one self-referential proof step with independent content behind the central claim.

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

No fitted constants or invented entities. The central result rests on standard fixed point theory, on the order-theoretic treatment of extended nonnegative reals, and on one ad hoc unproved special case: the lfp characterization for induced Markov chains, which is exactly where the proof of Theorem 3.1 becomes circular.

assumptions (6)
  • standard math Knaster-Tarski and Kleene fixed point theorems.
    Used in Section 5 to establish existence and iterative approximation of least fixed points of Bellman operators and characteristic functions.
  • standard math Supremum-based countable summation over extended nonnegative reals, following Wilkins [49].
    Section 3 defines expected rewards using this sum, relying on its independence from enumeration order.
  • domain assumption MDPs are finitely branching with countable state spaces and finite action sets.
    Definition 1; needed for Bellman operators to involve finite sums and for path sets to remain countable.
  • standard math Arithmetic on R^infty_{\ge 0} with 0*infinity = infinity*0 = 0 is order-continuous for addition, multiplication, min, and max.
    Theorem 2.1 uses this, citing Droste, Kuich, Vogler [17, Chapter 1], to prove continuity of the Bellman operators.
  • domain assumption Monotonicity and continuity of dwp and awp transformers from Kaminski et al. [31].
    Theorem 5 is cited from prior work by the same research group and not proved in this paper.
  • ad hoc to paper Theorem 3 holds for induced Markov chains M(S') with one enabled action per state.
    Invoked as 'Theorem 3' inside the proof of Theorem 3.1 in Appendix A.5; no independent proof or reference is supplied, causing a circular step in the main proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)." pith.science (2026). https://pith.science/paper/U35Z66R2

@misc{pith2026241116564,
  author       = {Pith},
  title        = {Pith review of: J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/U35Z66R2}},
  note         = {Machine review of arXiv:2411.16564}
}
read the original abstract

Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result about MDPs is that their minimal and maximal expected rewards satisfy Bellmann's optimality equations. For various classes of MDPs - notably finite-state MDPs, positive bounded models, and negative models - expected rewards are known to be the least solution of those equations. However, these classes of MDPs are too restrictive for probabilistic program verification. In particular, they assume that all rewards are finite. This is already not the case for the expected runtime of a simple probabilisitic program modeling a 1-dimensional random walk. In this paper, we develop a generalized least fixed point characterization of expected rewards in MDPs without those restrictions. Furthermore, we demonstrate how said characterization can be leveraged to prove weakest-preexpectation-style calculi sound with respect to an operational MDP model.

Figures

Figures reproduced from arXiv: 2411.16564 by the authors.

Figure 1
Figure 1. Example MDP with infinite state space. Omitted probabilities are 1. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. An MDP where no max-optimal scheduler exist at any state [PITH_FULL_IMAGE:figures/full_fig_p020_2.png] view at source ↗
Figure 3
Figure 3. An example pGCL program. We assume that r ∈ Q∞ ≥0 is a constant. 8.2 Operational MDP Semantics of pGCL Towards defining the operational MDP semantics of pGCL, we define a small￾step execution relation à la Plotkin [40]. We mainly follow the presentation from [11] with adaptions from [5]. We define the (countable) set of configurations as Conf = (pGCL ∪ {⇓}) × States ∪ {⊥} . Configurations are denoted by c and variat… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: A reachable fragment of pGCL’s operational MDP O for the loop from [PITH_FULL_IMAGE:figures/full_fig_p024_4.png]
Figure 5
Figure 5. Figure 5: Rules defining the small-step execution relation [PITH_FULL_IMAGE:figures/full_fig_p025_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

56 extracted references · 54 canonical work pages

  1. [31]

    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition rea- soning for expected runtimes of randomized algorithms. J. ACM65(5), 30:1–30:68 (2018)

    work page 2018

  2. [1]

    MIT Press (2008)

    Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)

    2008

  3. [2]

    Discrete Mathematics98(1), 75–79 (1991)

    Baranga, A.: The contraction principle as a particular case of Kleene’s fixed point theorem. Discrete Mathematics98(1), 75–79 (1991)

    work page 1991

  4. [3]

    Cambridge University Press (2020)

    Barthe, G., Katoen, J.P., Silva, A.: Foundations of probabilistic programming. Cambridge University Press (2020)

    work page 2020

  5. [4]

    Batz, K.: Automated Deductive Verification of Probabilistic Programs. Ph.D. the- sis, RWTH Aachen University, Germany (202?), [submitted; to be defended]

    work page

  6. [5]

    Batz,K.,Biskup,T.J.,Katoen,J.P.,Winkler,T.:Programmaticstrategysynthesis: Resolving nondeterminism in probabilistic programs. Proc. ACM Program. Lang. 8(POPL), 2792–2820 (2024)

    work page 2024

  7. [6]

    In: TACAS

    Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Prob- abilistic program verification via inductive synthesis of inductive invariants. In: TACAS. LNCS, vol. 13994, pp. 410–429. Springer (2023) 34 K. Batz et al

    work page 2023

  8. [7]

    In: CAV (2)

    Batz, K., Chen, M., Kaminski, B.L., Katoen, J., Matheja, C., Schröer, P.: Latticed k-induction with an application to probabilistic programs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 524–549. Springer (2021)

    work page 2021

Show all 56 references
  1. [8]

    In: CAV (2)

    Batz, K., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C., Schröer, P.: PrIC3: Property directed reachability for MDPs. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 512–538. Springer (2020)

    2020

  2. [9]

    In: ESOP

    Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. In: ESOP. Lecture Notes in Computer Science, vol. 10801, pp. 186–213. Springer (2018)

    2018

  3. [10]

    Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang.5(POPL), 1–30 (2021)

    2021

  4. [11]

    Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C., Noll, T.: Quantitative separa- tion logic: A logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. 3(POPL), 34:1–34:29 (2019)

    2019

  5. [12]

    Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C., Verscht, L.: A calculus for amortized expected runtimes. Proc. ACM Program. Lang.7(POPL), 1957–1986 (2023)

    2023

  6. [13]

    Indiana University Mathematics Jour- nal 6, 679–684 (1957),https://api.semanticscholar.org/CorpusID:123329493

    Bellman, R.: A Markovian decision process. Indiana University Mathematics Jour- nal 6, 679–684 (1957),https://api.semanticscholar.org/CorpusID:123329493

    1957

  7. [14]

    In: LICS

    Dahlqvist, F., Silva, A., Smith, W.: Deterministic stream-sampling for probabilistic programming: semantics and verification. In: LICS. pp. 1–13. IEEE (2023)

    2023

  8. [15]

    In: CAV (2)

    Dehnert, C., Junges, S., Katoen, J., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: CAV (2). Lecture Notes in Computer Science, vol. 10427, pp. 592–600. Springer (2017)

    2017

  9. [16]

    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of pro- grams. Commun. ACM18(8), 453–457 (1975)

    1975

  10. [17]

    Springer Publishing Company, Incorporated, 1st edn

    Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata. Springer Publishing Company, Incorporated, 1st edn. (2009)

    2009

  11. [18]

    Goswami, K.K.: Design for dependability: A simulation-based approach. Ph.D. thesis, University of Illinois at Urbana-Champaign (1993)

    1993

  12. [19]

    In: QEST

    Gretz, F., Katoen, J., McIver, A.: Prinsys – On a quest for probabilistic loop invariants. In: QEST. LNCS, vol. 8054, pp. 193–208. Springer (2013)

    2013

  13. [20]

    Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation se- mantics for the probabilistic guarded command language. Perform. Evaluation73, 110–132 (2014)

    2014

  14. [21]

    Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci.735, 111–131 (2018)

    2018

  15. [22]

    Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: Induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL), 37:1–37:28 (2020)

    2020

  16. [23]

    In: CAV (2)

    Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 488–511. Springer (2020)

    2020

  17. [24]

    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    1969

  18. [25]

    In: MFPS

    Jansen, N., Kaminski, B.L., Katoen, J., Olmedo, F., Gretz, F., McIver, A.: Condi- tioning in probabilistic programming. In: MFPS. Electronic Notes in Theoretical Computer Science, vol. 319, pp. 199–216. Elsevier (2015)

    2015

  19. [26]

    Kaminski, B.L.: Advanced Weakest Precondition Calculi for Probabilistic Pro- grams. Ph.D. thesis, RWTH Aachen University, Germany (2019) J-P: MDP. FP. PP. 35

    2019

  20. [27]

    In: MFCS (1)

    Kaminski, B.L., Katoen, J.P.: On the hardness of almost-sure termination. In: MFCS (1). Lecture Notes in Computer Science, vol. 9234, pp. 307–318. Springer (2015)

    2015

  21. [28]

    In: LICS

    Kaminski, B.L., Katoen, J.: A weakest pre-expectation semantics for mixed-sign expectations. In: LICS. pp. 1–12. IEEE Computer Society (2017)

    2017

  22. [29]

    Acta Informatica56(3), 255–285 (2019)

    Kaminski, B.L., Katoen, J.P., Matheja, C.: On the hardness of analyzing proba- bilistic programs. Acta Informatica56(3), 255–285 (2019)

    2019

  23. [30]

    In: ESOP

    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition rea- soning for expected run-times of probabilistic programs. In: ESOP. Lecture Notes in Computer Science, vol. 9632, pp. 364–389. Springer (2016)

    2016

  24. [32]

    Annales de la Societe Polonaise de Mathematique6, 133–134 (1928)

    Knaster, B.: Un théorème sur les functions d’ensembles. Annales de la Societe Polonaise de Mathematique6, 133–134 (1928)

    1928

  25. [33]

    In: FOCS

    Kozen, D.: Semantics of probabilistic programs. In: FOCS. pp. 101–114. IEEE Computer Society (1979)

    1979

  26. [34]

    In: STOC

    Kozen, D.: A probabilistic PDL. In: STOC. pp. 291–297. ACM (1983)

    1983

  27. [35]

    Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci.30(2), 162–178 (1985)

    1985

  28. [36]

    In: Computer Performance Evaluation / TOOLS

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Computer Performance Evaluation / TOOLS. Lecture Notes in Com- puter Science, vol. 2324, pp. 200–204. Springer (2002)

    2002

  29. [37]

    Monographs in Computer Science, Springer (2005)

    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Sys- tems. Monographs in Computer Science, Springer (2005)

    2005

  30. [38]

    McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost- sure termination. Proc. ACM Program. Lang.2(POPL), 33:1–33:28 (2018)

    2018

  31. [39]

    Machine Intelli- gence 5 (1969)

    Park, D.: Fixpoint induction and proofs of program properties. Machine Intelli- gence 5 (1969)

    1969

  32. [40]

    Plotkin, G.D.: The origins of structural operational semantics. J. Log. Algebraic Methods Program. 60-61, 3–15 (2004)

    2004

  33. [41]

    Wiley Series in Probability and Statistics, Wiley (1994)

    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Pro- gramming. Wiley Series in Probability and Statistics, Wiley (1994)

    1994

  34. [42]

    In: CAV (1)

    Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 643–661. Springer (2018)

    2018

  35. [43]

    In: POPL

    Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL. pp. 154–165. ACM (2002)

    2002

  36. [44]

    Marine Corps Chevron (1942)

    Rupertus, W.H.: On the supervisory control of distributed high-performance com- puting systems in engineering. Marine Corps Chevron (1942)

    1942

  37. [45]

    Proceedings of the American Mathematical Society22(3), 704–710 (1969)

    Santos, E.S.: Probabilistic turing machines and computability. Proceedings of the American Mathematical Society22(3), 704–710 (1969)

    1969

  38. [46]

    Schröer, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A deductive ver- ification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052–2082 (2023)

    2023

  39. [47]

    Pacific Jour- nal of Mathematics5(2) (1955)

    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Jour- nal of Mathematics5(2) (1955)

    1955

  40. [48]

    WIT Transactions on Information and Communication Technologies11 (1970)

    Westphal, H., Menge, S.: On the supervisory control of distributed high- performance computing systems in engineering. WIT Transactions on Information and Communication Technologies11 (1970)

    1970

  41. [49]

    Section 6: The extended real number system

    Wilkins, D.R.: Course 221: Hilary term 2007. Section 6: The extended real number system. Lecture Notes (2007), https://www.maths.tcd.ie/~dwilkins/Courses/ 221/Extended.pdf, accessed online November 20, 2023 36 K. Batz et al

    2007

  42. [50]

    initial segments

    Winskel, G.: The formal semantics of programming languages – an introduction. Foundation of computing series, MIT Press (1993) A Omitted Proofs and Results on MDPs (Sections 3, 6 and 7) A.1 Alternative Characterization of Expected Rewards We will use the following alternative ...

    1993

  43. [51]

    MinER=n (M, s,rew)

    Φmin n+1 M rew (0) = λs. MinER=n (M, s,rew)

  44. [52]

    consumes

    Φmax n+1 M rew (0) = λs. MaxER=n (M, s,rew) Proof. We prove the claim for the min-Bellman operator by induction onn. The proof for the max-Bellman operator is completely analogous. Base case n = 0. We have Φmin 1 M rew(0) = λs. rew(s) + min a∈Act(s) X s′∈Succsa(s) P (s, a, s′)...

  45. [53]

    MinER (M, s,rew)

    lfp Φmin M rew = λs. MinER (M, s,rew)

  46. [54]

    MaxER (M, s,rew) Proof

    lfp Φmax M rew = λs. MaxER (M, s,rew) Proof. Since the proof of Theorem 3.1 is more involved, we first prove Theo- rem 3.2. For that, consider the following: lfp Φmax M rew = G n∈N Φmax n M rew(0) (Theorem 2.2) = G n∈N λs. MaxER=n (M, s,rew) (Lemma 2.2) = G n∈N λs. sup S∈Sched...

  47. [55]

    Wehave Act(C1, σ) ={N }and C1, σ N,1 − − → ⇓, τ.Hence,also Act(C1 ; C2, σ) = {N } and (C1 ; C2, σ) N,1 − − →(C2, τ)

  48. [56]

    Hence, for every a ∈ Act(C1 ; C2, σ), all configurations in Succsa(C1 ; C2, σ) are of the form(C ′ 1 ; C2, σ′)

    For every a ∈ Act(C1, σ), all configurations in Succsa(C1, σ) are of the form (C ′ 1, σ′). Hence, for every a ∈ Act(C1 ; C2, σ), all configurations in Succsa(C1 ; C2, σ) are of the form(C ′ 1 ; C2, σ′). We proceed by distinguishing these two cases. For the first case, we have ...

Pith tools

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