{"id":"67e95cc9-e08f-41d1-b7be-960e0b1ec05d","arxiv_id":"2411.11803","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new abstraction model, odIMDP, stores transition probabilities as products of per-dimension interval bounds, cutting memory and conservatism in stochastic controller synthesis.","lead":"This paper introduces a way to verify and control stochastic (noisy) systems by simplifying them into a new kind of compact probabilistic model, called an odIMDP. The model stores only per-dimension probability ranges instead of full transition tables, cutting memory needs by orders of magnitude and enabling 7-dimensional examples that prior tools cannot handle.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Abstract claims an optimal odIMDP strategy is computed via linear problems, but Eqn. (15) is a relaxation and Section 8 admits exact solution of Eqn. (14) is open; optimality is therefore unsupported.","rationale":"The paper's central contribution has two parts: a structural representation that saves memory and tightens lower bounds, and an algorithm that computes an optimal strategy for the abstraction. The first part is well supported by Theorem 4.3, Proposition 6.2, and the empirical tables; the memory complexity and guaranteed improvement over the product-interval IMDP construction are concrete and credible. The second part is not supported: Eqn. (15) is an explicitly relaxing approximation of Eqn. (14), and Section 8 says the exact multilinear problem is open. The abstract nevertheless promises an optimal strategy computed by solving linear problems. This is not a mere wording issue, because Problem 2.3 is stated as an optimization problem and the reader's strongest claim repeats 'optimal strategy.' The reader's rationale already lists the overclaim as a concern, but the reader's weakest_assumption singles out independence of noise across dimensions. I agree independence is a real applicability restriction and the authors acknowledge it; it is less damaging because diagonal-covariance Gaussian mixtures can approximate correlated noise with enough components, and the mixture-of-odIMDP construction in Section 5.2 is sound. The optimality overclaim is more load-bearing because it is contradicted by the paper's own limitation statement and affects the headline claim. A small exact-vs-relaxed comparison would settle whether the overclaim is harmless in practice or, as is likely, the relaxation is strict. The verdict should remain CONDITIONAL: the memory and tightness contributions stand, but the optimality statement needs to be corrected and the exactness gap documented for the final version.","tokens_in":25724,"tokens_out":11665,"duration_ms":131910,"concrete_test":"Implement a small odIMDP with two marginals of three states each (e.g., the Fig. 2/Fig. 6 instance) and compute both the exact pessimistic Bellman update by solving Eqn. (14) over all vertex combinations of the two interval ambiguity sets, and the relaxed update W from Eqn. (15). Run both value iterations to obtain policies, then evaluate the relaxed policy under the exact Eqn. (14) minimization. If the exact robust value of the relaxed policy is strictly below the exact optimal robust value, the algorithm is not computing an optimal odIMDP strategy and the abstract's optimality claim must be retracted or qualified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Problem 2.3 asks for a strategy maximizing the concrete reach-avoid probability, and the abstract states that 'an optimal control strategy for an odIMDPs can be computed by solving a set of linear problems.' The algorithm actually presented in Section 6 solves Eqn. (15), a divide-and-conquer relaxation of the exact pessimistic Bellman update in Eqn. (14). Theorem 6.1 proves only that W_k,s,a is a lower bound on the exact minimization over the product ambiguity set; it does not prove equality, and strict inequality is generic because Eqn. (15) lets the adversary choose the marginal for dimension i after seeing the prefixes of dimensions 1,...,i-1, which is more adversarial power than a single product distribution. The paper's own Section 8 states: 'exactly and efficiently solving the multi-linear problem of Eqn.(14) is still an open problem for which we employed relaxations.' That admitted relaxation contradicts the abstract's optimality claim: the strategy maximizing W is not shown to maximize the exact robust value in Eqn. (12), let alone to solve Problem 2.3 for the concrete system. The memory-complexity and reduced-conservatism claims relative to the product-interval IMDP construction remain intact, but the paper's advertised optimal synthesis result is not supported by the presented mathematics.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces orthogonally decoupled Interval Markov Decision Processes (odIMDPs), a subclass of robust MDPs whose transition ambiguity sets factor as products of marginal interval ambiguity sets. It shows how Gaussian and Gaussian-mixture stochastic systems with diagonal-covariance noise can be abstracted compositionally to odIMDPs, storing only marginal probability bounds and reducing memory from O(|S|^2|A|) to O(2|S||A| n |S|^{1/n}). The paper proposes a divide-and-conquer linear-programming value iteration for odIMDPs and proves (Theorem 4.3 and Proposition 6.2) that the resulting lower bounds are contained in and at least as tight as the interval bounds obtained by multiplying marginal bounds. It reports experiments on benchmarks up to 7D showing substantial memory and tightness improvements over IMDP/MDP-based tools.","tokens_in":25931,"tokens_out":9783,"duration_ms":90094,"significance":"If the claims hold, the memory-complexity improvement and the tightened ambiguity sets are valuable contributions to abstraction-based verification, because memory is a known bottleneck and the framework scales to 6D/7D systems on standard hardware. The theoretical comparisons (Theorem 4.3, Theorem 6.1, Proposition 6.2) are parameter-free derivations, and the empirical evaluation is extensive. The main reservation is that the advertised 'optimal' synthesis is not actually achieved; the algorithm computes a sound lower bound via a relaxation, which is still useful but is a weaker claim.","major_comments":[{"comment":"The abstract claims that 'an optimal control strategy for an odIMDP can be computed by solving a set of linear problems,' but the algorithm presented in Section 6 solves the recursive relaxation in Eq. (15), which is only a lower bound on the exact pessimistic Bellman update in Eq. (14). Theorem 6.1 proves only an inequality, and Section 8 explicitly states that exactly solving Eq. (14) is open. Therefore the strategy maximizing W_{k,s,a} is optimal for the relaxed problem, not for the odIMDP robust value in Eq. (12) or for Problem 2.3 on the concrete system. This overstatement should be corrected in the abstract and in the list of contributions.","section":"Abstract and Section 6 (Eqs. (14)-(15))"},{"comment":"The proof of Proposition 6.2 asserts that if each marginal of a distribution lies in the corresponding interval set, then the joint probabilities lie between the products of the marginal bounds. That implication is false for arbitrary joint distributions; it holds for the distribution generated by Eq. (15) only because that distribution is built from conditional factors chosen recursively, not because of marginal containment alone. The proof should be rewritten to argue directly from the recursive construction, e.g., by showing that the sequentially defined minimizing distribution has conditional factors in the marginal sets and therefore satisfies the product bounds. As written, the proof is not valid.","section":"Section 6, Proposition 6.2"},{"comment":"The correctness proof is a single sentence referring to [29, Theorem 4], and the computation of the upper bound \\hat{V}_\\pi^H is not specified for odIMDPs. The text says 'the case min follows similarly,' but it does not give the analogous over-approximation update. Please provide the explicit upper-bound value iteration for odIMDPs and state the precise conditions under which [29, Theorem 4] applies to the relaxed values W_{k,s,a} used in the lower-bound computation.","section":"Section 6.1, Theorem 6.3"}],"minor_comments":[{"comment":"The phrase 'an odIMDPs' is grammatically incorrect; the abbreviation should be used as a singular noun: 'an odIMDP.'","section":"Throughout"},{"comment":"The notation \\hat{V}_\\pi^H is introduced but never explicitly defined. Please define it as the value obtained by replacing the inner minimization in Eq. (13) with a maximization, and state clearly that it is an upper bound on the satisfaction probability.","section":"Section 6"},{"comment":"In Eq. (16), the notation W^{k,0}_{r,s,a} should be explicitly defined as the value computed by Eq. (15) for the r-th component odIMDP, so that the mixture extension is unambiguous.","section":"Section 5.2, Eq. (16)"},{"comment":"The columns 'Min δ', 'Max δ', and 'Mean δ' should be accompanied by a note under the table defining δ = V_odIMDP - V_other, with positive values indicating that the odIMDP method yields a higher satisfaction probability. The text defines this, but a table note would improve readability.","section":"Table 3"},{"comment":"The memory figures for odIMDPs at large |S| (e.g., 59.5 GB for 360k states) are substantial; a brief remark pointing this out would temper the scalability narrative and inform readers about the trade-off between memory and tightness.","section":"Table 4"}],"recommendation":"major_revision","confidential_remarks":"The paper's central theoretical contributions—the memory-complexity bound, Theorem 4.3, and the tightness comparison—are sound and valuable. The main problem is the overclaimed optimality result, which is contradicted by the paper's own relaxation and acknowledgment in Section 8. This is fixable by rewriting the abstract and contribution statements. The proof of Proposition 6.2 also needs repair, as the current argument is invalid as written. The reliance on [29, Theorem 4] for Theorem 6.3 is acceptable but should be made more explicit. Overall, the paper is a good fit for HSCC and warrants revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth your time. The core idea is genuinely new: by abstracting each dimension's transition probabilities into marginal interval ambiguity sets, the authors define a product-form robust MDP (odIMDP) that needs only O(n|S|^(1+1/n)) memory per action instead of O(|S|^2). That is a real asymptotic improvement, and the paper proves it cleanly. Theorem 4.3 shows the odIMDP ambiguity set is strictly contained in the naive interval-product IMDP, and Proposition 6.2 shows their divide-and-conquer Bellman update is no more conservative than the standard IMDP lower bound. The experiments back this up: on 6D/7D linear systems baseline IMDP tools run out of memory while odIMDP finishes with lower bounds above 0.95. The memory and tightness claims are solid.\n\nThe soft spot is the abstract. It says an optimal control strategy for an odIMDP can be computed by solving a set of linear problems. That is not what the paper proves. Equation (15) is a relaxation of the exact multilinear minimization in Eq. (14); Theorem 6.1 only gives a lower bound, and the authors admit in Section 8 that exactly solving Eq. (14) is open. The strategy synthesized from the relaxation is not shown to maximize the robust value in Eq. (12), let alone solve Problem 2.3 for the concrete system. So the optimality statement is unsupported as written. It does not sink the main contribution—a tight, memory-efficient lower bound is still valuable—but it needs to be fixed before acceptance.\n\nTwo smaller issues. First, correctness of the concrete abstraction (Theorem 6.3) is deferred to the authors' earlier Theorem 4 in [29]. That is a legitimate citation, but the paper does not fully prove its own soundness; a reader must fetch the earlier proof. Second, there is no code or data artifact. The experiments run their own IntervalMDP.jl package, but without a released implementation the 4682x memory numbers are hard to verify independently. That is a reproducibility gap, not a correctness flaw.\n\nThis paper is for anyone doing abstraction-based synthesis for stochastic systems with independent noise across dimensions. The odIMDP model and the recursion in Eq. (15) are worth citing. I would send it to review—the core result deserves referee time—but I would insist the optimality claim be scaled back and ideally the code be released.","headline":"Genuinely new abstraction class with real memory/tightness gains, but the abstract's optimality claim outruns the mathematics; fix that and this is a solid paper.","tokens_in":26533,"tokens_out":2613,"would_cite":true,"duration_ms":23433,"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":"The paper claims that stochastic systems with independent per-dimension noise can be verified by storing only marginal probability bounds, cutting memory from quadratic to near-linear in the grid size while tightening reach-avoid…","keywords":["orthogonally decoupled interval Markov decision processes","robust value iteration","probabilistic reach-avoid","abstraction-based controller synthesis","compositional abstraction","stochastic systems","marginal probability bounds","scalable verification"],"falsifier":"Run a high-accuracy Monte Carlo simulation of the 6D linear benchmark under the odIMDP-optimal policy and check whether the empirical reach-avoid probability falls below the paper's reported guaranteed lower bound of 0.958; a violation would contradict Theorem 6.3.","tokens_in":25474,"feed_emoji":"🎯","tokens_out":8246,"duration_ms":72487,"temperature":0.7,"pith_summary":"This paper introduces a new class of robust Markov models, orthogonally decoupled Interval Markov Decision Processes (odIMDPs), in which every transition's uncertain probability distribution is a product of independent interval bounds, one per state dimension. The central claim is that for stochastic systems whose noise is independent across dimensions, this product structure makes the abstraction compositional: one stores only the marginal probability bounds of the original system, reducing memory from $2|S|^2|A|$ to $2|S||A|\\, n\\sqrt[n]{|S|}$ scalar values. The paper further claims that an optimal control strategy for an odIMDP can be computed by a divide-and-conquer sequence of linear programs, and that the strategy, mapped back to the concrete system, yields guaranteed lower and upper bounds on the reach-avoid probability that are never more conservative than the standard IMDP approach. If correct, this makes formal controller synthesis with probabilistic guarantees practical on 6D and 7D systems on ordinary CPU hardware, where existing abstraction-based tools run out of memory or time out.","feed_headline":"Per-dimension noise bounds make 7D stochastic verification practical","feed_subtitle":"Storing only marginal probabilities cuts memory by orders of magnitude and tightens reach-avoid guarantees.","key_machinery":"The load-bearing object is the odIMDP: a robust Markov decision process whose state space is a product $S=S_1\\times\\cdots\\times S_n$ and whose transition ambiguity set for each source-action pair is $\\Gamma_{s,a}=\\bigotimes_{i=1}^n \\Gamma^i_{s,a}$, an independent interval ambiguity set per dimension. This product form is what lets the abstraction store only the marginal bounds, because the joint transition probability is the product of marginal probabilities. The synthesis algorithm works on the same structure: instead of one large multilinear minimization over all joint distributions, it recursively applies O-maximization one marginal at a time (equation (15)), producing a sound lower bound at linear-programming cost. The correctness argument runs through Theorem 6.3, which lifts the abstract strategy to the concrete system via the region map and transfers the value interval.","core_discovery":"The central discovery is that encoding interval uncertainty in product form is not a lossy simplification of the usual IMDP but a strictly tighter model. Theorem 4.3 shows that the product ambiguity set $\\Gamma = \\bigotimes_{i=1}^n \\Gamma^i$ is contained in the interval ambiguity set obtained by multiplying the marginal bounds, so some distributions admitted by the multiplied intervals cannot be factored as products of marginals and are correctly excluded. Theorem 6.1 proves that the recursive divide-and-conquer bound $W^k_{s,a}$ computed one marginal at a time is a sound lower bound on the true pessimistic value iteration, and Proposition 6.2 proves it is at least as large as the bound obtained by the standard IMDP relaxation. Theorem 6.3 then guarantees that any strategy synthesized on the odIMDP, applied to the concrete system through the region map $J(x)=s$, gives an interval $[V^H_\\pi(J(x_0)), \\hat V^H_\\pi(J(x_0))]$ that contains the true reach-avoid probability. On the experimental side, the paper reports that this construction completes 6D and 7D verification tasks with guaranteed lower bounds above 0.95, at memory reductions of roughly 4,700x and 30,000x compared with the parallel IMDP baseline.","pith_inferences":["Editorial inference: the memory savings grow with dimension $n$, so combining odIMDP abstractions with model-order reduction or dimension-wise refinement could plausibly push formal synthesis beyond 7D, where the paper's approach still spends about 13,900 seconds of certification time on the 7D case.","Editorial inference: the product ambiguity set is strictly smaller than the multiplied-interval set, which suggests that per-dimension adaptive grids can refine each marginal independently without destroying the product structure; the paper notes that heterogeneous non-grid partitioning is currently incompatible.","Editorial inference: the recursive value iteration is exponential in the number of marginals, so for high-dimensional systems with many states per dimension, an alternative that solves the multilinear problem (14) directly, or with a tighter relaxation, would be needed; the paper explicitly leaves exact solution of (14) open.","Editorial inference: for systems with correlated noise, one could try a preliminary decorrelating coordinate transform so that the diagonal-covariance assumption holds approximately; the paper restricts itself to the exactly independent case."],"forward_implications":["Memory for the abstraction drops from $2|S|^2|A|$ to $2|S||A|\\,n\\sqrt[n]{|S|}$ scalars, which is what lets 6D and 7D grids fit in main memory.","For the same partition of the state space, the odIMDP lower bound on reach-avoid probability is guaranteed to be at least as high as the bound from an IMDP built by multiplying marginal intervals (Proposition 6.2).","The synthesized switching strategy $\\pi_x(x,k)=\\pi(J(x),k)$ comes with a certificate interval that provably contains the true reach-avoid probability of the original stochastic system (Theorem 6.3).","Systems with Gaussian-mixture transition kernels are handled by abstracting each mixture component separately and optimizing over the uncertain component weights, extending the same guarantees to non-Gaussian but independent noise.","The reported experiments show the approach is 5--80x faster to abstract on 2D benchmarks and at least two orders of magnitude faster above 3D, while producing tighter lower bounds than both interval-based baselines on most benchmarks."],"supporting_citations":[{"why":"supplies the interval-bound construction for transition probabilities that the Gaussian abstraction step builds on.","marker":"[3]"},{"why":"provides the standard IMDP abstraction-and-correctness template that odIMDPs extend and the benchmark for efficiency comparison.","marker":"[14]"},{"why":"defines bounded-parameter MDPs/IMDPs and the O-maximization routine used inside the divide-and-conquer recursion.","marker":"[20]"},{"why":"supplies IMDP value iteration and the O-maximization algorithm used to solve each marginal linear program.","marker":"[28]"},{"why":"provides the dynamic-programming proof template that Theorem 6.3 uses to transfer abstract strategies to the concrete system.","marker":"[29]"},{"why":"provides the parallel value-iteration implementation used to run both the odIMDP and baseline IMDP experiments.","marker":"[37]"},{"why":"provides the MDP-based comparison baseline and the car-parking benchmark used in the scaling study.","marker":"[51]"},{"why":"provides the parallel IMDP abstraction baseline and several benchmark models used in the experimental comparison.","marker":"[56]"}],"fun_headline_variants":["Marginal-only abstraction cuts memory 30,000x for 7D control","Product-form intervals tighten reach-avoid guarantees","Compositional IMDP scales to 7D with 30,000x less memory","Sound synthesis for 7D stochastic systems via marginal bounds","Structural IMDP abstraction slashes memory and conservatism"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method rests on the assumption that the noise is independent across state dimensions (each Gaussian in the transition mixture has diagonal covariance), so each transition probability factors into a product of per-dimension marginals; if the noise is correlated, the product form and the guarantees collapse.","fun_headline_variants_meta":{"raw":{"variants":["Marginal-only abstraction cuts memory 30,000x for 7D control","Product-form intervals tighten reach-avoid guarantees","Compositional IMDP scales to 7D with 30,000x less memory","Sound synthesis for 7D stochastic systems via marginal bounds","Structural IMDP abstraction slashes memory and conservatism"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000253,"raw_usage":{"total_tokens":1620,"prompt_tokens":1055,"completion_tokens":565,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":671,"completion_tokens_details":{"reasoning_tokens":476}},"tokens_in":671,"tokens_out":565,"duration_ms":5553,"temperature":1.0,"reasoning_tokens":476,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:09:22.929885+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a high-accuracy Monte Carlo simulation of the 6D linear benchmark under the odIMDP-optimal policy and check whether the empirical reach-avoid probability falls below the paper's reported guaranteed lower bound of 0.958; a violation would contradict Theorem 6.3.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the interval-bound construction for transition probabilities that the Gaussian abstraction step builds on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the standard IMDP abstraction-and-correctness template that odIMDPs extend and the benchmark for efficiency comparison."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"defines bounded-parameter MDPs/IMDPs and the O-maximization routine used inside the divide-and-conquer recursion."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies IMDP value iteration and the O-maximization algorithm used to solve each marginal linear program."},{"cited_title":"IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes","cited_arxiv_id":"2401.04068","evidence_quote":"provides the parallel value-iteration implementation used to run both the odIMDP and baseline IMDP experiments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the MDP-based comparison baseline and the car-parking benchmark used in the scaling study."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the parallel IMDP abstraction baseline and several benchmark models used in the experimental comparison."}],"review_version":1}