{"id":"8aa92616-5460-4146-87b2-945c9b6d6537","arxiv_id":"2505.23635","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For Markov decision processes over analytic state spaces, the bisimulation pseudometric equals the logical distance of a quantitative modal logic.","lead":"A Markov decision process with a continuous state space is modeled as a coalgebra, and two notions of closeness are defined: the bisimulation pseudometric and the logical distance of a quantitative modal logic. The paper proves they coincide for analytic state spaces, a quantitative Hennessy-Milner theorem.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Expressivity proof relies on an unproved equality of coupling infima: Eq. (14)=(15) requires lifting pushforward couplings along qTh, a disintegration step not established in the paper.","rationale":"The paper's central claim is a quantitative Hennessy-Milner theorem for MDPs over analytic spaces (Corollary 31). The adequacy direction (Theorem 22) is established by a clean structural induction and is not the source of risk. The expressivity direction (Theorem 28) is load-bearing, and its crux is the equality of the two coupling infima in (14) and (15). This step implicitly assumes a lifting theorem for couplings along the theory map qTh, which is a disintegration/regular-conditional-distribution result for perfect measures on countably generated spaces. The paper cites [18, Thm. 6] in a parenthetical but does not state or prove the needed lifting lemma; the surrounding claim about restricting to a standard subspace of [0,1]^L does not by itself justify the equality. This is a genuine proof gap rather than an internal inconsistency. For perfect measures on countably generated spaces, regular conditional distributions are known to exist, so the gap is likely fixable; however, it must be filled before the central claim can be regarded as fully established. I agree with the reader's weakest_assumption and therefore see no reason to change the CONDITIONAL verdict. The proposed concrete test — constructing the lifted coupling from disintegrations, or finding a counterexample where no such lift exists — would settle the concern definitively.","tokens_in":30725,"tokens_out":16723,"duration_ms":155792,"concrete_test":"Formalize the missing lifting step: for ν_1 = qTh_*(m_{x,a}) and ν_2 = qTh_*(m_{y,a}), use [18, Thm. 6] to obtain disintegrations m_{x,a} = ∫ μ_1(t) dν_1(t) and m_{y,a} = ∫ μ_2(s) dν_2(s). For any coupling C' ∈ K(ν_1, ν_2), define C = ∫ μ_1(t) ⊗ μ_2(s) dC'(t,s). Verify that C ∈ K(m_{x,a}, m_{y,a}) and that (qTh × qTh)_*C = C'. If this construction is valid, the equality (14)=(15) holds and the proof gap is closed. If it fails, exhibit a concrete counterexample, e.g., a perfect measure on an analytic space lacking a suitable disintegration along a measurable map to a second-countable space, or a coupling of pushforwards with no lift; such an example would invalidate Theorem 28 and Corollary 31.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In the proof of Theorem 28, the transition from equation (14) to equation (15) replaces the infimum over couplings of the original measures m_{x,a}, m_{y,a} of ∫ dL dc by the infimum over couplings of their pushforwards qTh_*m_{x,a}, qTh_*m_{y,a} of ∫ d~L dc, where d~L is the sup-distance on [0,1]^L. This equality is not immediate: every coupling of the original measures pushes forward to a coupling of the pushforward measures, giving one inequality, but the reverse direction requires that every coupling of the pushforward measures can be lifted to a coupling of the original measures. Such a lifting is equivalent to having regular conditional distributions of m_{x,a} and m_{y,a} along qTh, so that a coupling C' of the pushforwards can be integrated against the product of the disintegrations to produce a coupling C of the original measures. The paper's parenthetical citation of [18, Thm. 6] concerns regular conditional probabilities for perfect measures on countably generated spaces, but no lifting lemma is stated or proved. If no such lifting exists, the expressivity direction bd ≤ dL collapses, even if the metric definition and adequacy are correct. The remaining steps (Kantorovich-Rubinstein duality, Stone-Weierstrass approximation) are comparatively well supported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops bisimulation pseudometrics for Markov reward processes and Markov decision processes whose state spaces are analytic measurable spaces, viewed as coalgebras in the category Ana. The metric is defined as the least fixed point of a functional built from a coupling-based Wasserstein lifting, formalized through a fibration of universally measurable predicates. The paper then introduces a quantitative modal logic with truth, conjunction, negation, scalar addition and subtraction, and one diamond per action; the diamond semantics is a convex combination of the expected value of the formula and the action reward. The main claim, Corollary 31, is that for every MDP in Ana and every discount factor c in [0,1], the bisimulation pseudometric equals the logical distance induced by this language, i.e. a quantitative Hennessy-Milner theorem. Adequacy is proved in Theorem 22, and expressivity is attacked through a general theorem (Theorem 28) assuming topologisability of the theory map and perfectness of the transition measures.","tokens_in":30902,"tokens_out":20942,"duration_ms":217442,"significance":"If the main theorem is correct, this is a valuable contribution to the quantitative coalgebraic semantics of continuous-state MDPs: it replaces Polish-space assumptions with analytic measurable spaces, works with universally measurable predicates rather than lower semi-continuous ones, and provides an expressive quantitative modal logic. The categorical framework, based on two fibrations and a coupling-based lifting, is original, and the adequacy proof is clean and well structured. The paper also gives a self-contained treatment of Kantorovich-Rubinstein duality for perfect measures, which is of independent interest. However, the expressivity proof contains a load-bearing unproved equality of coupling infima and a separate algebraic inconsistency with the discount factor, and the proof of Theorem 13 uses a semicontinuity claim that is not correct as written. These issues are substantial but appear repairable within the manuscript's scope.","major_comments":[{"comment":"The equality of the infimum over couplings of m_{x,a}, m_{y,a} of the integral of dL with the infimum over couplings of their pushforwards along qTh of the integral of d~L is asserted without proof. One inequality is immediate: every coupling of the original measures pushes forward to a coupling of the pushforward measures with the same cost. The reverse direction requires a coupling-lifting lemma: every coupling of qTh_*m_{x,a} and qTh_*m_{y,a} must be obtainable as the pushforward of some coupling of m_{x,a} and m_{y,a}. This is equivalent to the existence of regular conditional distributions of the transition measures along qTh. The parenthetical citation of [18, Thm. 6] does not by itself establish this lifting, and no such lemma is stated or proved in the paper. Since the subsequent argument bounds the pushforward infimum, the direction bd <= dL depends on this step. Please add a complete proof of the equality (or of the needed inequality direction) and verify the required measurability and regularity conditions.","section":"Theorem 28, Eq. (14) to Eq. (15)"},{"comment":"In the proof of Theorem 13, the function f(x,c) = c(d~_x), with d~_x = d_i for x in [i,i+1), is claimed to be upper semicontinuous in x. With the usual topology on [0,Infinity), the preimage f(.,c)^{-1}([0,r)) is a union of half-open intervals of the form [i,i+1), which is not open in general. For example, if c(d_0) >= r and c(d_1) < r, then the point 1 belongs to the preimage but no neighbourhood of 1 is contained in it. Thus the hypotheses of Sion's minimax theorem (Lemma 44) are not satisfied as written. Since Theorem 13 is used both for the existence of the least fixed point (Corollary 16) and in the reduction at the start of the proof of Theorem 28, this proof needs to be repaired or replaced by a valid argument.","section":"Theorem 13, proof using Sion's minimax theorem"},{"comment":"The discount factor is handled inconsistently in the proof of Theorem 28. Lemma 11 gives sigmaMRP_X(d)((m,r),(n,s)) = c * inf_{kappa in K(m,n)} integral d dkappa + (1-c)|r-s|, but Eq. (14) writes the expression as inf over couplings of integral dL dc + c r^a_xy, dropping the leading factor c on the coupling term and replacing the reward coefficient 1-c by c. Moreover, the manipulation in Eq. (18), from sup_phi integral JphiK d(m_{x,a}-m_{y,a}) + c r^a_xy to sup_phi (integral JphiK dm_{x,a} + c r^x_a) - (integral JphiK dm_{y,a} + c r^y_a), is not algebraically valid when r^a_xy = |r^x_a - r^y_a|; the right-hand side can be smaller by 2c|r^x_a - r^y_a|. This makes the chain of inequalities leading to (13) impossible to follow as written and must be corrected.","section":"Theorem 28, Eqs. (14) and (18), discount-factor algebra"}],"minor_comments":[{"comment":"The second pushforward measure is written as qTh(m_{y,a}); it should be qTh_*(m_{y,a}).","section":"Theorem 28, Eq. (15)"},{"comment":"The same symbol c is used both for the discount factor and for an arbitrary coupling in Eqs. (14) and (15); please use different letters, e.g. kappa for couplings, to avoid ambiguity.","section":"Theorem 28, notation"},{"comment":"The companion paper [4] is cited for the fact that the predicate lifting improves universally measurable predicates to Borel predicates, but it is listed as an unpublished manuscript with a placeholder arXiv number. Since this fact is used in the main development, the proof should be included in the appendix or the companion should be made publicly available.","section":"Reference [4]"},{"comment":"The sentence 'Recalling that [0,1] is compact, thus the assumptions of Theorem 29 are fulfilled' is terse; it would be clearer to state explicitly that the relevant index sets are [0,1] with the usual topology and the countable set Sigma with the discrete topology, both second countable Hausdorff.","section":"Lemma 30"},{"comment":"The measurability argument for the function h defined as an infimum over y is compressed into the sentence 'g is nothing but exists_{pr1}(lambda xy. d(x,y)-g(y))'; a few more details or a reference would help the reader verify this step.","section":"Appendix G.2, proof of Lemma 27"},{"comment":"The title of reference [4] contains a typo: 'Henneysey-milner' should be 'Hennessy-Milner'.","section":"Reference [4] title"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is within the scope of CALCO/LIPIcs and the main claim is plausible and interesting. However, the expressivity proof of Theorem 28 has a genuine gap at Eqs. (14)-(15) and an algebraic error involving the discount factor, and the proof of Theorem 13 misuses Sion's minimax theorem. These are load-bearing but appear fixable with additional lemmas and corrections. The unpublished companion paper [4] is cited for a nontrivial measurability fact and should either be made available or the argument should be included. I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The result is real: a quantitative Hennessy-Milner theorem for bisimulation pseudometrics on MDPs over analytic spaces, with rewards baked into the diamond modality. Extending Ferns et al. from Polish to analytic spaces and from lower semicontinuous to universally measurable distances is a genuine advance, and the fibration-based Wasserstein lifting without a complete lattice fibration is a useful piece of infrastructure. The adequacy proof is clean and the appendix is thorough; the Kantorovich-Rubinstein duality lemma and the Stone-Weierstrass variant are given real proofs, not just citations.\n\nThe soft spot is exactly where the stress-test puts it. In Theorem 28, the move from equation (14) to (15) replaces an infimum over couplings of the transition measures by an infimum over couplings of their pushforwards along the theory map. One inequality is free. The reverse requires every coupling on the theory space to lift to a coupling on the state space, which needs a disintegration argument for perfect measures along the theory map. The parenthetical citation to Faden does not state or prove that lifting lemma, and the proof of expressivity collapses if it fails. I think the lemma is true and probably standard for perfect measures on analytic spaces with countably generated target, but the authors need to write it out. This is a load-bearing gap, not a cosmetic one.\n\nAlso, the phrase \"[0,1]^L is second countable\" is imprecise when L is uncountable; in the concrete Corollary 31 the language is countable, so this is annoying rather than fatal, but Theorem 28 as stated should either restrict L or add a second countability hypothesis. The self-citation to an unpublished companion paper with a placeholder identifier should be fixed, though it is cited for a supporting fact rather than the main theorem.\n\nOverall: this deserves a serious referee. I would send it to review and ask for a proof of the coupling-lifting lemma, plus a cleanup of the topological claims. If the lifting lemma goes through, the paper is a solid contribution to the coalgebraic semantics literature.","headline":"A substantial new expressivity result for bisimulation pseudometrics on continuous MDPs, slowed by one unproved coupling-lifting step in Theorem 28.","tokens_in":31513,"tokens_out":3341,"would_cite":true,"duration_ms":38808,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"For continuous Markov decision processes, behavioral distance is exactly logical distance: the paper proves a quantitative Hennessy–Milner theorem for MDPs over analytic state spaces.","keywords":["Markov decision process","analytic space","perfect measure","Wasserstein distance","Kantorovich-Rubinstein duality","quantitative Hennessy-Milner theorem","bisimulation pseudometric","modal logic"],"falsifier":"To refute the expressivity half, one would exhibit an analytic-space MDP, two states $x$ and $y$, an action $a$, and a discount $c$ for which the pushforward measures $qTh_*(m_{x,a})$ and $qTh_*(m_{y,a})$ admit a coupling that is not the image of any coupling of $m_{x,a}$ and $m_{y,a}$; then the step equating equations (14) and (15) collapses, and one can check directly whether $\\mathrm{bd}_c(x,y)>dL_c(x,y)$. Equivalently, a pair of states with identical values on every formula of $L$ but with positive bisimulation distance would refute Corollary 31.","tokens_in":30444,"feed_emoji":"📏","tokens_out":7550,"duration_ms":78985,"temperature":0.7,"pith_summary":"This paper aims to prove a quantitative Hennessy–Milner theorem for Markov decision processes with continuous, analytic state spaces: the bisimulation pseudometric between states, defined as the least fixed point of a Wasserstein-style distance lifting, coincides with the logical distance given by a quantitative modal logic whose formulas test expected transitions and rewards. If the theorem is right, then for any two states in such an MDP, behavioral similarity is exactly indistinguishability by all formulas in that logic, at any fixed discount factor $c\\in[0,1]$. The significance is that this equivalence holds without assuming a Polish topology: the paper works purely measure-theoretically with universally measurable distances and perfect measures, and it derives the bisimulation metric via Kleene's fixed-point theorem rather than contraction arguments. The central result is Corollary 31, for the language $L$ of Lemma 30, with the theory map made topologisable so that Stone–Weierstrass approximation converts logical agreement into metric equality.","feed_headline":"For continuous MDPs, behavioral distance equals logical distance","feed_subtitle":"A modal logic with scalar addition and one diamond per action captures bisimilarity on analytic state spaces.","key_machinery":"The machinery has three load-bearing pieces. First, a fibration of predicates over analytic spaces: $\\mathrm{Pred}(X)$ is the set of universally measurable functions $X\\to[0,1]$, and $\\mathrm{lsPred}(X)$ is the subfibration of lower semi-measurable functions; the direct-image left adjoint exists for Suslin-level predicates, which is what makes the coupling-based lifting possible. Second, the distance lifting $\\sigma_{\\mathrm{MDP}}$ built from the Wasserstein lifting of the Giry functor, $\\hat\\sigma(d)(m,n)=\\inf_{c\\in K(m,n)}\\int d\\,dc$, composed with reward differences by a convex combination with parameter $c$. Third, the theory map $qTh:X\\to [0,1]^L$ sending each state to its vector of formula values; topologisability of $qTh$ lets the proof restrict attention to a standard subspace $A\\subseteq [0,1]^L$ and apply Stone–Weierstrass to approximate short predicates by formulas. The chain is: push the logical distance along the theory map, apply Kantorovich–Rubinstein duality to rewrite the Wasserstein cost as a supremum over short predicates, then approximate those predicates by modal formulas.","core_discovery":"The paper's central claim is that the behavioral distance on a continuous MDP is fully captured by a quantitative modal logic. Concretely, for an MDP coalgebra $\\gamma:(X,\\mathcal{A})\\to B_{\\mathrm{MDP}}(X,\\mathcal{A})$ in the category of analytic spaces, with language $L$ generated by truth, negation, conjunction, scalar addition and subtraction $\\_+r$, $\\_-r$ with $r\\in[0,1]$, and a diamond modality $\\Diamond_a$ for each action $a$, the bisimulation pseudometric $\\mathrm{bd}_c$, defined as the least fixed point of $\\gamma\\circ\\sigma_{\\mathrm{MDP}}$ with discount $c$, equals the logical distance $dL_c(x,y)=\\sup_{\\varphi\\in L}|\\varphi(x)-\\varphi(y)|$. Adequacy ($\\mathrm{bd}\\ge dL$) holds whenever the function symbols are interpreted as nonexpansive functions; expressivity ($\\mathrm{bd}\\le dL$) requires perfect transition measures, a topologisable theory map, and scalar addition in the signature. The proof combines Kantorovich–Rubinstein duality for perfect measures with a Stone–Weierstrass lemma over the compact-open topology on the space of formulas.","pith_inferences":["Beyond the paper's claims: if $\\mathrm{bd}_c=dL_c$ is stable under Lipschitz embeddings, then representation-learning pipelines that map states to formula-value vectors preserve behavioral distances up to the Lipschitz constant; this would give a formal justification for using logical features as state encodings in continuous MDPs.","The unproved disintegration step suggests a targeted stress test: exhibit two perfect measures on an analytic space whose theory-pushforwards admit a coupling that is not the image of any coupling of the original measures; such an example would isolate where the Stone–Weierstrass approximation argument needs a regularity condition beyond analyticity.","A natural extension, which the authors list as future work, would be to replace the compact-open topology on the formula space with a measurable Stone–Weierstrass theorem; if such a theorem existed, the topologisability assumption could likely be dropped from Theorem 28."],"forward_implications":["If Corollary 31 is correct, the bisimulation pseudometric on continuous MDPs is determined by formula evaluations: two states are $\\varepsilon$-close behaviorally exactly when no formula of $L$ separates them by more than $\\varepsilon$.","Because the equality holds for every $c\\in[0,1]$, the discount factor may be set to $0$ or $1$, covering purely reward-based and purely transition-based comparisons, which the contraction-based definition of the earlier bisimulation metric could not handle.","Adequacy holds for any language whose function symbols are nonexpansive, so adding operators such as scalar multiplication or convex combination preserves $\\mathrm{bd}\\ge dL$; expressivity then follows whenever the theory map is topologisable.","The alternative language with a separate reward modality and expected-transition modality is shown to be expressive but not adequate, because truncated addition is not nonexpansive; this explains why the paper's single diamond modality, which mixes the transition expectation and the reward, is needed.","Since the least fixed point is obtained by Kleene iteration, the definition of $\\mathrm{bd}_c$ does not rely on the transition kernel being a contraction, which broadens the class of MDPs for which the metric is defined."],"supporting_citations":[{"why":"Defines continuous-state MDPs and the bisimulation metric that this paper generalises to analytic spaces with universally measurable distances.","marker":"[21]"},{"why":"Supplies the coupling-based lifting construction for endofunctors on Set that is recalibrated here to fibrations over analytic spaces.","marker":"[6]"},{"why":"Gives the general marginal-problem duality that is extended to perfect measures as Lemma 27, the Kantorovich–Rubinstein duality used in the expressivity proof.","marker":"[36]"},{"why":"Cited for the regular conditional probability and disintegration result that justifies replacing couplings of original measures by couplings of their theory-pushforwards in Theorem 28.","marker":"[18]"},{"why":"Provides the measure-theoretic facts about perfect measures, inner regularity, and the Suslin operation used in the proofs of Theorem 13 and the lifting results.","marker":"[23]"},{"why":"Supplies the compact-open topology facts, including Lemma 19, that make the theory map topologisable and the formula space second countable.","marker":"[17]"},{"why":"Used in the proof of Theorem 45 to identify couplings of perfect measures with charges, enabling the minimax argument.","marker":"[35]"},{"why":"Gives the result that perfect measures coincide with charges in the relevant setting, a key step in the omega-cpo-continuity proof.","marker":"[37]"}],"fun_headline_variants":["MDP behavioral distance is captured by modal logic","Analytic MDPs: bisimulation metric equals logical metric","Modal logic fully captures MDP bisimilarity","Distance in MDPs matches modal logic distance","Hennessy-Milner theorem for analytic MDPs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The equality between the bisimulation distance and the logical distance relies on a lifting step: it assumes that whenever the formula-profiles of two states' transition probabilities are paired, that paired profile really comes from pairing the two original random transitions; the paper cites a regularity theorem for this step but gives no proof.","fun_headline_variants_meta":{"raw":{"variants":["MDP behavioral distance is captured by modal logic","Analytic MDPs: bisimulation metric equals logical metric","Modal logic fully captures MDP bisimilarity","Distance in MDPs matches modal logic distance","Hennessy-Milner theorem for analytic MDPs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000577,"raw_usage":{"total_tokens":2701,"prompt_tokens":906,"completion_tokens":1795,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":522,"completion_tokens_details":{"reasoning_tokens":1718}},"tokens_in":522,"tokens_out":1795,"duration_ms":12040,"temperature":1.0,"reasoning_tokens":1718,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T12:43:25.442708+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"To refute the expressivity half, one would exhibit an analytic-space MDP, two states $x$ and $y$, an action $a$, and a discount $c$ for which the pushforward measures $qTh_*(m_{x,a})$ and $qTh_*(m_{y,a})$ admit a coupling that is not the image of any coupling of $m_{x,a}$ and $m_{y,a}$; then the step equating equations (14) and (15) collapses, and one can check directly whether $\\mathrm{bd}_c(x,y)>dL_c(x,y)$. Equivalently, a pair of states with identical values on every formula of $L$ but with positive bisimulation distance would refute Corollary 31.","supporting_citations":[{"cited_title":"Bisimulation metrics for continuous M arkov decision processes","cited_arxiv_id":null,"evidence_quote":"Defines continuous-state MDPs and the bisimulation metric that this paper generalises to analytic spaces with universally measurable distances."},{"cited_title":"A general duality theorem for marginal problems","cited_arxiv_id":null,"evidence_quote":"Gives the general marginal-problem duality that is extended to perfect measures as Lemma 27, the Kantorovich–Rubinstein duality used in the expressivity proof."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Cited for the regular conditional probability and disintegration result that justifies replacing couplings of original measures by couplings of their theory-pushforwards in Theorem 28."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the measure-theoretic facts about perfect measures, inner regularity, and the Suslin operation used in the proofs of Theorem 13 and the lifting results."},{"cited_title":"General topology , volume 6 of Sigma series in pure mathematics","cited_arxiv_id":null,"evidence_quote":"Supplies the compact-open topology facts, including Lemma 19, that make the theory map topologisable and the formula space second countable."},{"cited_title":"Ramachandran and L","cited_arxiv_id":null,"evidence_quote":"Used in the proof of Theorem 45 to identify couplings of perfect measures with charges, enabling the minimax argument."},{"cited_title":"On quasi-compact measures","cited_arxiv_id":null,"evidence_quote":"Gives the result that perfect measures coincide with charges in the relevant setting, a key step in the omega-cpo-continuity proof."}],"review_version":1}