{"id":"1932e660-09ca-4a45-a394-39ce4e55ce4b","arxiv_id":"2411.16564","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For MDPs with possibly infinite rewards, the minimal and maximal total expected rewards equal the least fixed points of the corresponding Bellman operators.","lead":"This paper proves that expected total rewards in Markov decision processes can be characterized as least fixed points, even when rewards and expected values are allowed to be infinite. This matters because infinite expected runtimes arise naturally in probabilistic programs, and a clean fixed point foundation makes weakest preexpectation calculi sound and easier to reuse.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Circular citation in Thm 3.1 proof is a repairable reference slip: the single-action MC case follows from Thm 3.2, so the central claim is not undermined.","rationale":"The reader's weakest assumption correctly locates the self-reference in the proof of Theorem 3.1: the chain for Inequality 7 invokes 'Theorem 3' for the induced Markov chain M(S'). I agree that the written proof is formally circular. But the circularity is only apparent because Theorem 3.2 is proven earlier in the same appendix and independent of Theorem 3.1; it applies to M(S') as a single-action MDP, giving lfp Phi^max_{M(S')} rew = MaxER(M(S'),rew) = ER(M(S'),rew). I checked that Theorem 3.2 itself uses only Kleene's theorem, Lemma 2.2, and commutation of suprema, and does not depend on Lemma 7 or Theorem 3.1. The construction of S' via Lemma 7 is independent of Theorem 3. Thus a one-line correction of the citation suffices. No deeper issue with the sup-inf exchange was found; the argument via Lemma 7 and the induced Markov chain is the standard way to justify it, and the finite-branching, nonnegative-reward setting supports the equality. The operational soundness proofs in Section 9 rely on Theorem 3, so they inherit the same minor citation issue but are otherwise consistent. I therefore recommend keeping the conditional verdict: the paper is correct in substance but needs a small revision to make the proof of Theorem 3.1 self-contained and to fix the ambiguous reference.","tokens_in":57,"tokens_out":16961,"duration_ms":223330,"concrete_test":"Re-derive the step in Appendix A.5, Inequality 7, of Theorem 3.1, replacing the reference 'Theorem 3' in the chain 'ER(M(S'),s,rew) = lfp Phi_{M(S')} rew' with 'Theorem 3.2'. Verify that Theorem 3.2 applies to the single-action induced Markov chain M(S') because MaxER(M(S'),s,rew) = ER(M(S'),s,rew), and hence lfp Phi^max_{M(S')} rew = ER(M(S'),s,rew). If this derivation is valid, the circularity is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof of Theorem 3.1 in Appendix A.5 (Inequality 7) contains the step 'ER(M(S'),s,rew) = lfp Phi_{M(S')} rew (Theorem 3)' inside the proof of Theorem 3. As written, this is a circular self-reference: the theorem being proved is invoked for the induced Markov chain M(S'). However, this does not amount to a real gap, because Theorem 3.2 was already proven independently in the same appendix and applies to any MDP, including the single-action MDP M(S'). Since M(S') has exactly one enabled action per state, MaxER(M(S'),s,rew) = ER(M(S'),s,rew), so Theorem 3.2 yields lfp Phi^max_{M(S')} rew = ER(M(S'),s,rew). Thus replacing the citation 'Theorem 3' by 'Theorem 3.2' repairs the proof. The central claim of the paper (Theorem 3) is therefore supported; the only issue is a citation/reference ambiguity that should be corrected in a revision.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":32732,"tokens_out":10260,"duration_ms":102811,"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":[{"comment":"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.","section":"Appendix A.3, Lemma 7"},{"comment":"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.","section":"Appendix A.3, Lemma 7"}],"minor_comments":[{"comment":"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.","section":"Section 5"},{"comment":"The introductory sentence “an application to operational semantics of probabilistic semantics” appears to contain a typo; it should read “probabilistic programs.”","section":"Section 8.1"},{"comment":"The rule for final configurations appears to be typeset as “(⇓, σ) N,1 → ⊥⊥ N,1 → ⊥”; it should be a single transition “(⇓, σ) N,1 → ⊥.”","section":"Figure 5, rule 1"},{"comment":"The abstract contains the misspelling “probabilisitic”; it should be “probabilistic.”","section":"Abstract"},{"comment":"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.","section":"References"},{"comment":"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.","section":"Section 9, Theorem 5"}],"recommendation":"major_revision","confidential_remarks":"The circular step in Appendix A.5 is a citation slip rather than a substantive mathematical error, and the ill-typed definition in Lemma 7 is obvious to repair. If the authors replace the internal reference to Theorem 3 with Theorem 3.2 in the proof of Inequality (7) and correct Lemma 7, I expect the proof of Theorem 3 to go through. The festschrift-style framing, including the non-technical quotations and the unusual reference entries, should be normalized if this is intended for a regular journal issue."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does what it says: it gives least-fixed-point characterizations of minimal and maximal total expected rewards for MDPs with extended nonnegative rewards, allowing infinite expected values. That genuinely removes a restriction that matters for probabilistic program verification, where expected runtimes are often infinite. The max case is a clean supremum-swap argument; the min case is harder and handled with a constructed optimal memoryless scheduler. The application to soundness of dwp/awp calculi for pGCL is a nice payoff, and the examples in the paper make the fixed-point behavior comprehensible.\n\nThe reader flagged a circular proof in Theorem 3.1's appendix: the step for the induced Markov chain M(S') cites 'Theorem 3' while proving Theorem 3. I checked the surrounding text, and the stress-test note is right. Theorem 3.2 is proved first, independently, and it applies to any MDP, including the single-action Markov chain M(S'). Since max and min Bellman operators coincide on a Markov chain, Theorem 3.2 alone yields lfp Phi_{M(S')} = ER(M(S'), s, rew). So the citation should be to Theorem 3.2, and the argument goes through as written. It is a reference slip, not a logical gap. The reader's conditional verdict is stricter than the paper deserves on this point.\n\nOther soft spots are minor. The healthiness properties for dwp/awp are imported from the authors' earlier work [31], which is fine since those are established results, not fitted claims. The paper also leaves open whether the supremum over memoryless schedulers equals the maximal expected reward when infinite rewards are allowed; that is disclosed honestly as an open question. The J-P framing is a bit unusual but does not affect the technical content.\n\nThe math is careful, the definitions are standard, and the examples are illustrative rather than decorative. This is a useful reference for anyone working on weakest preexpectation calculi or infinite-state MDP verification. I would bring it to a reading group and would cite it. It deserves serious peer review; the only required change is correcting the internal reference in the proof of Theorem 3.1.","headline":"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.","tokens_in":33305,"tokens_out":2643,"would_cite":true,"duration_ms":28887,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["Markov decision processes","expected rewards","least fixed points","Bellman operators","weakest preexpectations","probabilistic programs","infinite-state MDPs","infinite rewards"],"falsifier":"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'.","tokens_in":40,"feed_emoji":"🎲","tokens_out":11354,"duration_ms":230889,"temperature":0.7,"pith_summary":"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.","feed_headline":"Expected rewards are least fixed points, even infinite ones","feed_subtitle":"A Bellman-operator result grounds weakest-preexpectation proofs for unbounded loops and infinite expected runtimes.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the classical positive-bounded and negative-model fixed-point theorems whose finiteness assumptions this paper removes.","marker":"[41]"},{"why":"Supplies the standard definitions of MDPs, schedulers, path probabilities, and reachability rewards that the paper follows.","marker":"[1]"},{"why":"Supplies the reachability-reward fixed-point characterizations, its Lemma 2.8 and Theorem 2.9, that this paper's Lemma 2 and Theorem 3 extend to total expected rewards.","marker":"[4]"},{"why":"Supplies the continuity of addition, multiplication, minima, and maxima on extended non-negative reals used in Theorem 2.","marker":"[17]"},{"why":"Supplies Park induction, used to bound least fixed points in Lemmas 3, 4, and 7.","marker":"[39]"},{"why":"Supplies the Kleene fixed point theorem and the omega-continuity setup used to express least fixed points as suprema of iterates from zero.","marker":"[50]"},{"why":"Supplies the expected-runtime weakest-precondition calculus whose treatment of loops and nondeterminism is adapted to reward-collecting programs.","marker":"[31]"},{"why":"Supplies the original weakest-preexpectation calculus on which the demonic and angelic transformers are built.","marker":"[37]"},{"why":"Supplies Bellman's optimality equations, the equation system whose least solution is the paper's subject.","marker":"[13]"},{"why":"Supplies the prior soundness result for bounded expectations without reward statements, which Theorem 6 generalizes.","marker":"[20]"}],"fun_headline_variants":["Infinite rewards still fit least fixed point theorem","Least fixed points hold for MDPs with infinite expected rewards","Bellman equations solved even when rewards are infinite","Generalizing least fixed point theorems to infinite MDP rewards","MDP expected rewards: least fixed points without finiteness"],"cache_read_input_tokens":35456,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Infinite rewards still fit least fixed point theorem","Least fixed points hold for MDPs with infinite expected rewards","Bellman equations solved even when rewards are infinite","Generalizing least fixed point theorems to infinite MDP rewards","MDP expected rewards: least fixed points without finiteness"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000475,"raw_usage":{"total_tokens":2366,"prompt_tokens":961,"completion_tokens":1405,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":577,"completion_tokens_details":{"reasoning_tokens":1327}},"tokens_in":577,"tokens_out":1405,"duration_ms":8894,"temperature":1.0,"reasoning_tokens":1327,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:58:41.410420+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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'.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the reachability-reward fixed-point characterizations, its Lemma 2.8 and Theorem 2.9, that this paper's Lemma 2 and Theorem 3 extend to total expected rewards."},{"cited_title":"Springer Publishing Company, Incorporated, 1st edn","cited_arxiv_id":null,"evidence_quote":"Supplies the continuity of addition, multiplication, minima, and maxima on extended non-negative reals used in Theorem 2."},{"cited_title":"Machine Intelli- gence 5 (1969)","cited_arxiv_id":null,"evidence_quote":"Supplies Park induction, used to bound least fixed points in Lemmas 3, 4, and 7."},{"cited_title":"initial segments","cited_arxiv_id":null,"evidence_quote":"Supplies the Kleene fixed point theorem and the omega-continuity setup used to express least fixed points as suprema of iterates from zero."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the expected-runtime weakest-precondition calculus whose treatment of loops and nondeterminism is adapted to reward-collecting programs."},{"cited_title":"Monographs in Computer Science, Springer (2005)","cited_arxiv_id":null,"evidence_quote":"Supplies the original weakest-preexpectation calculus on which the demonic and angelic transformers are built."},{"cited_title":"Indiana University Mathematics Jour- nal 6, 679–684 (1957),https://api.semanticscholar.org/CorpusID:123329493","cited_arxiv_id":null,"evidence_quote":"Supplies Bellman's optimality equations, the equation system whose least solution is the paper's subject."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the prior soundness result for bounded expectations without reward statements, which Theorem 6 generalizes."}],"review_version":1}