{"id":"371fcf5a-c066-4583-8abd-8bc1118bc6db","arxiv_id":"2511.13460","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new SMC method approximates Pareto fronts of multi-objective MDP queries by sampling strategies, with a statistically sound lower bound and an asymptotic confidence band.","lead":"This paper introduces the first statistical model checking approach for multi-objective Pareto queries on Markov decision processes, using lightweight strategy sampling to approximate tradeoff fronts with statistical guarantees. It matters because it extends simulation-based verification to settings where exhaustive multi-objective model checking blows up in state space, e.g. large control and scheduling problems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 2's overapproximation guarantee rests on a false inference and an incorrect distance bound: box containment does not make the optimistic-corner hull an overapproximation, and the stated precision √(2dε²) is arithmetically wrong.","rationale":"The reader's verdict is CONDITIONAL and identifies ideal LSS as the weakest assumption. That is a fair scope limitation, and the paper discloses it. However, the most load-bearing concern for the central asymptotic claim is internal to Lemma 2: the proof sketch does not establish the stated overapproximation conclusion, and the precision value it gives is wrong. These are not merely presentational issues; they affect the exact guarantee advertised in the abstract ('confidence band in the long run'). The ideal-LSS assumption concerns whether all Pareto-optimal strategies are ever sampled; the precision/conainment gap concerns what happens even when they are sampled and their boxes are correct. Since the latter is a definite mathematical inconsistency in the theorem statement, it is more decisive for correctness risk. The concern does not overturn the paper's contribution: Lemma 1's underapproximation guarantee appears sound, the fixed-budget algorithms are reasonable, and Lemma 2's high-level idea (sample all strategies eventually, then optimistically bounded boxes surround the front) is salvageable by replacing 'overapproximation' with 'δ-neighbourhood overapproximation' and fixing δ to 2√d·ε. Hence the verdict stays CONDITIONAL: the asymptotic band claim needs correction and clarification before acceptance, but the core approach is not invalidated.","tokens_in":23369,"tokens_out":17731,"duration_ms":189220,"concrete_test":"Analytically re-derive the distance underlying Lemma 2. For each dimension i, the CI has half-width ε, so the pessimistic corner p and optimistic corner o of a box satisfy |p_i − o_i| = 2ε. The Euclidean distance is sqrt(Σ_i (2ε)²) = 2√d·ε, not √(2dε²). Then, with d=2, take a single Pareto-optimal strategy with true mean μ=(0.5,0.5) and box [0.4,0.6]²; the optimistic-corner hull is the singleton {(0.6,0.4)}, which does not contain μ, demonstrating that C̄ is not an overapproximation unless expanded by the box diagonal. If both checks reproduce, Lemma 2's precision bound must be corrected and its proof must explicitly state the δ-neighbourhood formulation.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central asymptotic claim is Lemma 2: with probability γ, C and C̄ converge to an under- and overapproximation with precision √(2dε²). The proof sketch contains two problems. First, from 'all Pareto-optimal strategies have been sampled and their boxes contain the true means' it concludes 'thus C̄ is an overapproximation.' This does not follow: C̄ is the convex hull of the optimistic corners of the boxes. A true mean μ_i lying inside box B_i is generally not equal to the optimistic corner o_i, and a convex hull of a few corner points need not contain μ_i. For example, with one Pareto-optimal strategy, C̄ is the singleton {o_i}, which does not contain μ_i. What the argument can show is only that the δ-neighbourhood of C̄ is an overapproximation, for δ equal to the maximal box diagonal — a qualification the lemma statement blurs. Second, the stated precision is arithmetically incorrect. Each CI has half-width ε per dimension, so the pessimistic and optimistic corners of one box differ by 2ε per coordinate; the Euclidean distance is sqrt(d·(2ε)²) = 2√d·ε, not √(2dε²). For d=2 this is 2√2·ε ≈ 2.83ε, not 2ε. Thus the quantitative 'confidence band' claim in the abstract is not supported as written, even granting the disclosed ideal-LSS assumption. The ideal-LSS limitation (Section 2) is real but explicitly acknowledged; the precision and containment gap is an internal mathematical inconsistency in the paper's key lemma.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents the first statistical model checking (SMC) method for multi-objective Pareto queries on Markov decision processes. It uses lightweight strategy sampling (LSS) to generate random memoryless deterministic strategies, evaluates them by SMC for all objectives simultaneously, and constructs under- and over-approximations of the true Pareto front from confidence boxes. An incremental scheme (Alg. 1) is claimed to almost surely converge to a statistically sound confidence band under ideal LSS, and three fixed-budget algorithms (WVR, FIB, FSB) with several strategy-selection heuristics are proposed to obtain close underapproximations in finite time. The methods are implemented in the Modest Toolset's modes simulator and evaluated on 34 benchmark models, including some too large for the Storm model checker.","tokens_in":23715,"tokens_out":9642,"duration_ms":97594,"significance":"If the main theorems are correct, the paper delivers a genuinely novel capability: SMC-based multi-objective verification with statistical guarantees and constant memory, extending earlier LSS-based single-objective tools. The underapproximation result (Lemma 1) is defensible, and the fixed-budget algorithms with a separate bias-free evaluation phase are a sound and useful engineering contribution. The experimental comparison with Storm demonstrates scalability on models beyond PMC's reach, and the implementation and benchmark set are valuable. However, the central asymptotic claim — the long-run confidence band of the incremental scheme — has flaws in Lemma 2 that need correction before the paper's advertised contribution is reliable.","major_comments":[{"comment":"The overapproximation claim is not justified by the proof sketch. It argues that once all Pareto-optimal strategies are sampled and their boxes contain the true means, C̄ is an overapproximation. But C̄ is the convex hull of the optimistic corners o_i, and a true mean μ_i inside box B_i is generally not equal to o_i. The convex hull of a finite set of optimistic corners need not contain μ_i; for a single Pareto-optimal strategy, C̄={o_1} does not contain μ_1. The argument can only support that a δ-neighbourhood of C̄ is an overapproximation, with δ equal to the maximal distance between a true mean and its optimistic corner (at most 2√d ε). The lemma and the abstract's 'confidence band' statement must be revised accordingly.","section":"Section 3.1, Lemma 2(2)"},{"comment":"The stated precision √(2dε²) is arithmetically incorrect. Each CI has half-width ε per dimension, so the pessimistic and optimistic corners of one box differ by 2ε in each coordinate; the Euclidean distance is √(d·(2ε)²) = 2√d ε, not √(2dε²). For d=2, the paper's formula gives 2ε, whereas the correct value is 2√2 ε. This quantitative bound appears in the central convergence claim, so it must be corrected and propagated consistently through the abstract and any derived statements.","section":"Section 3.1, Lemma 2(2)"},{"comment":"The phrase 'almost surely converge to an under- and overapproximation with probability γ' conflates two different probability spaces. The almost-sure part is over LSS strategy sampling under ideal LSS, while γ is the simultaneous confidence over simulation randomness. The proof sketch does not separate the two, nor does it define the mode of set convergence (e.g., Hausdorff distance). A rigorous statement is needed, especially because the 'when not interrupted' clause is an infinite-time statement while the CI correctness is per-batch and only gives probability γ. This is not merely cosmetic; it affects what the convergence claim actually guarantees.","section":"Section 3.1, Lemma 2"}],"minor_comments":[{"comment":"The abstract's 'almost surely converges' should be qualified with 'under ideal LSS.' Section 2 explicitly acknowledges the 32-bit identifier cap as a practical limitation, but the abstract and conclusion omit this condition, which is essential for the long-run guarantee.","section":"Section 2 and Abstract"},{"comment":"The SMC interface is used inconsistently: Alg. 1 line 6 passes a precision ε as third argument, while Alg. 2 line 3 and Alg. 4 line 4 pass a run count n or ⌊n/|Σ|⌋. Please define the SMC parameter convention explicitly and align the pseudo-code.","section":"Algorithms 2–5"},{"comment":"Line 5 says 'select w ... between C(stat), C(stat)', which appears to be a typo for C(stat) and C̄(stat). Also, the expression 'λ σ.w·x̂^σ' in line 6 is unclear; define the dot product and the role of λ.","section":"Algorithm 3"},{"comment":"The tables report counts of models where one setting 'strictly outperformed all others,' but no statistical significance measure is given, and only three seeds are used. A brief note on the variability (e.g., standard deviation or a paired test) would strengthen the comparative claims.","section":"Experimental evaluation, Tables 2–4"}],"recommendation":"major_revision","confidential_remarks":"The paper is likely of interest to the QEST/CAV community, and the underapproximation algorithms appear to be a solid contribution. However, the headline asymptotic result—the simultaneous confidence band—is currently stated with a false containment inference and an incorrect precision bound. These are fixable with a reformulation to a δ-neighbourhood statement and corrected arithmetic, so I do not recommend rejection. The ideal-LSS assumption is a significant gap between theory and practice, and the authors should be encouraged to state it prominently rather than as a side remark. Overall, I would support publication after the main theorem is repaired and the presentation clarified."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Punchline: first real SMC approach to equal-priority multi-objective Pareto queries, and the underapproximation machinery is sound; but Lemma 2's overapproximation/convergence claim has a genuine gap and a wrong bound, so the abstract's 'confidence band' promise is not supported. It deserves a serious referee, but needs major revision on that lemma.\n\nWhat's new and good. The idea of using LSS with 32-bit strategy identifiers, computing confidence boxes for all objectives from the same runs, and taking convex hulls of pessimistic corners to get a statistical lower bound on the Pareto front — with constant memory in state-space size — is genuinely new. Lemma 1 is sound: a simultaneous-γ-correct family of boxes makes the hull of pessimistic corners an underapproximation with probability γ. The three fixed-budget heuristics (WVR, FIB, FSB) are sensible, and the experiments on 34 models / 1836 configurations show the tool producing nontrivial fronts on models where Storm's multi-objective PMC crashes. The related-work survey is careful and the 'first' claim looks justified.\n\nThe soft spots. Lemma 2 is the load-bearing problem. Its proof sketch infers that once all Pareto-optimal strategies have been sampled and their boxes contain the true means, the hull of optimistic corners is an overapproximation. That's not a valid inference: a box containing its mean does not make the mean an element of the hull of the box's optimistic corner. With a single Pareto-optimal strategy, the overapprox hull is just that corner, not the true mean. What the argument actually yields is that a δ-neighbourhood of that hull is an overapproximation, with δ the maximal box diagonal. Second, the precision bound √(2dε²) is arithmetically wrong: the corner-to-corner distance of a box of half-width ε is 2√d·ε, so the number should be 2√d ε. For d=2 that's about 2.83ε, not 2ε. So the quantitative band claim in the abstract is not established. The 'almost surely converge' wording also conflates the a.s. strategy sampling (which requires ideal LSS, disclosed as impractical) with the probability-γ CI guarantee. On the experimental side, three seeds and no error bars is thin for ranking heuristics, though it doesn't invalidate the main tool message.\n\nWho it's for. This paper is a meaningful addition for the SMC and quantitative-verification community; the underapproximation technique is the durable contribution. I would send it to peer review, with the clear expectation that the authors repair or carefully weaken Lemma 2, correct the bound, and recalibrate the abstract's claims. The fixed-budget algorithms and the evaluation are good enough to stand on their own once that is done.","headline":"First real SMC for equal-priority multi-objective Pareto queries; underapproximation part is sound, but the asymptotic confidence-band lemma has a genuine hole and a wrong bound — worth reviewing but needs major revision to that lemma.","tokens_in":24214,"tokens_out":8773,"would_cite":true,"duration_ms":74568,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q87"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces the first statistical model checking approach for multi-objective Pareto queries, using random sampling of strategies to approximate the tradeoff frontier in Markov decision processes.","keywords":["multi-objective model checking","statistical model checking","Pareto front","Markov decision processes","lightweight strategy sampling","confidence band","probabilistic verification","simulation-based verification"],"falsifier":"Construct a small MDP whose Pareto-optimal strategies form a set that the LSS hash function never generates from any 32-bit identifier, and run the incremental scheme: if the over-approximation does not converge to the true front within the claimed precision √(2d ε²), the ideal-LSS assumption fails. Alternatively, count the effective number of distinct strategies the hash function can produce; if it is less than the true strategy space, convergence cannot be guaranteed.","tokens_in":23253,"feed_emoji":"📊","tokens_out":4401,"duration_ms":38164,"temperature":0.7,"pith_summary":"The paper establishes that multi-objective Pareto queries—finding optimal tradeoffs among several probability or reward objectives in a Markov decision process—can be answered statistically without exploring the model's state space. The authors propose a scheme that samples control strategies at random via lightweight strategy sampling, evaluates each with simulation runs, and forms an under-approximation of the Pareto front from the pessimistic corners of per-strategy confidence boxes. In the long run, the scheme also yields an over-approximation, so the two enclose the true front in a statistically guaranteed band. They also offer three fixed-budget heuristics for finding a close under-approximation in finite time. A sympathetic reader would care because this brings simulation-based verification to the multi-objective setting, where exhaustive methods fail on large state spaces.","feed_headline":"First statistical method finds Pareto fronts in MDPs","feed_subtitle":"Simulation-based approach bounds the true tradeoff front from both sides, without state-space explosion.","key_machinery":"The central mechanism is lightweight strategy sampling (LSS), which represents each memoryless deterministic strategy by a 32-bit integer identifier and chooses actions via a hash function of identifier and state, enabling constant-memory strategy representation. Strategy identifiers are sampled uniformly, and for each sampled strategy, simulation runs produce a d-dimensional confidence box around the sample mean. The convex hull of the boxes' pessimistic corners forms the under-approximation; the hull of optimistic corners forms the over-approximation. Simultaneous correctness of all boxes is ensured by distributing the error budget α across strategies and dimensions via the union bound (Bo","core_discovery":"For an MDP with d objectives, randomly sampling memoryless deterministic strategies and evaluating them by statistical model checking yields a statistically sound under-approximation C of the true Pareto front with confidence γ. When sampling continues indefinitely under ideal lightweight strategy sampling, the under- and over-approximations almost surely converge to a simultaneous confidence band with precision √(2d ε²), enveloping the true front. In finite time, fixed-budget heuristics that discard unpromising strategies and reallocate runs to promising ones produce close under-approximations, outperforming exhaustive methods on models whose state space grows too large for conventional pro","pith_inferences":["If the confidence band claim holds in practice, engineers could certify both performance and risk simultaneously: the upper bound guards against overestimating achievable tradeoffs, while the lower bound gives a safe set of strategies.","The strategy-selection heuristics suggest a natural connection to multi-objective reinforcement learning; a testable extension is whether combining the incremental scheme with RL-style value approximation could reduce the number of simulation runs needed to reach a given precision.","The reliance on 32-bit identifiers implies that for very large strategy spaces, the theoretical convergence may be obstructed by practical hashing collisions; moving to larger identifiers or structured sampling could restore the guarantee."],"forward_implications":["Multi-objective verification becomes feasible for models with state spaces too large for exhaustive probabilistic model checking, since the method is constant-memory in the state space size.","The incremental scheme provides, for the first time, a statistical confidence band around the true Pareto front, giving both lower and upper bounds in the limit.","Fixed-budget variants give statistically guaranteed lower bounds, which is useful for one-shot analyses where only a limited simulation budget is available.","The approach extends beyond MDPs to any model class supported by LSS, such as Markov automata and probabilistic timed automata, potentially broadening its applicability."],"fun_headline_variants":["Pareto front via light sampling in MDPs","Statistical sampling finds multi-objective tradeoffs","First SMC for Pareto queries with sampling","Sampling-based Pareto bounds for large MDPs","Lightweight strategy sampling for Pareto fronts"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The asymptotic over-approximation guarantee depends on the assumption that uniformly sampling 32-bit strategy identifiers eventually produces every memoryless deterministic strategy with probability one; in practice the finite identifier space and the hash function may never sample some Pareto-optimal strategies, so the over-approximation may never close.","fun_headline_variants_meta":{"raw":{"variants":["Pareto front via light sampling in MDPs","Statistical sampling finds multi-objective tradeoffs","First SMC for Pareto queries with sampling","Sampling-based Pareto bounds for large MDPs","Lightweight strategy sampling for Pareto fronts"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000165,"raw_usage":{"total_tokens":1046,"prompt_tokens":660,"completion_tokens":386,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":404,"completion_tokens_details":{"reasoning_tokens":330}},"tokens_in":404,"tokens_out":386,"duration_ms":4076,"temperature":1.0,"reasoning_tokens":330,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T21:47:31.227384+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a small MDP whose Pareto-optimal strategies form a set that the LSS hash function never generates from any 32-bit identifier, and run the incremental scheme: if the over-approximation does not converge to the true front within the claimed precision √(2d ε²), the ideal-LSS assumption fails. Alternatively, count the effective number of distinct strategies the hash function can produce; if it is less than the true strategy space, convergence cannot be guaranteed.","supporting_citations":[],"review_version":1}