{"id":"7228d9b5-8a21-48b8-b422-fce4ccf3431c","arxiv_id":"2411.14371","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":6,"one_line_summary":"A POMDP-based synthesis and verification pipeline can generate recurrent, energy-minimizing cleaning strategies for small robot collectives, but the soundness of the probabilistic abstraction used is left unproven.","lead":"The authors present a workflow for synthesizing recurrent cleaning schedules for teams of battery-driven robots, using partially observable Markov decision processes and the PRISM model checker. The paper is a case study in making formal controller synthesis practical for tasks that combine optimization, safety, and recurrence under uncertainty.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Safety 'under uncertainty' is verified on the deterministic induced model Mσ, but no soundness proof connects Mσ to the stochastic POMDP M; the deferred abstraction condition in Section 3.6 goes in the opposite direction from what such a transfer would require.","rationale":"The reader's conditional verdict is appropriate: the paper is a transparent case study with a plausible pipeline, but the headline guarantee outstrips what is formally shown. My stress-test agrees with the reader's weakest assumption—the relationship between M, M′, and Mσ is not soundness-established—and sharpens it: the property the paper leaves for future work (Section 3.6) has the inequality direction reversed for transferring the verified safety property CT from Mσ to the stochastic M. This matters because the conclusion says 'guarantees under uncertainty', and the uncertainty is encoded in M, while the verification is performed on the deterministic Mσ. The paper does not hide this limitation—it is explicitly deferred—so the work remains a useful case study and guidance contribution. However, the central claim as stated in the abstract and conclusion should be read as 'guarantees for the induced deterministic counter model', not for the stochastic POMDP, unless the missing soundness condition is supplied in the correct direction. This does not change the reader's CONDITIONAL verdict; it reinforces why the condition is necessary. I set verdict_should_be to UNCHANGED because my concern is the same load-bearing gap the reader identified, and the conditional recommendation already reflects it. I mark agreement as partial because I add a technical correction about the direction of the deferred abstraction check rather than merely endorsing the reader's formulation.","tokens_in":14813,"tokens_out":10713,"duration_ms":117918,"concrete_test":"For the one-robot and two-robot instances in Section 4, export the synthesized strategy σ from PRISM and build the induced DTMC on the original stochastic POMDP M (Boolean contamination flags, actions fixed by σ as a function of time, positions, and charges). For each room R_i, compute P=? [F R_i.d=true] over horizon T in this DTMC, and compare with the counter trajectory of the single Mσ path: identify any R_i with P>0 while R_i.d < R_i.threshold along the Mσ path. If such a room exists, CT verified on Mσ does not transfer to M, and the Section 3.6 abstraction condition, even if checked, would not support the claimed guarantee in the required direction. If no such room exists, the gap is at least not empirically visible on these instances, but a formal implication is still absent.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central guarantee is that the pipeline produces strategies that are safe and recurrent 'under uncertainty', i.e., in the stochastic POMDP M. But the actual verification in Section 3.7/Table 2 checks CT, BC, FR, ωC, and UT on Mσ, a deterministic, fully observable, single-path model derived from the counter-based M′. No theorem or proof shows that a property verified on Mσ holds in M. The paper explicitly defers exactly this: Section 3.6 says a future-work property is to check whether the probabilities of contamination flags being set in M are greater than or equal to the probabilities of the corresponding counters in M′/Mσ reaching their thresholds. This is the wrong inequality for lifting CT from Mσ to M: to conclude from 'counter never reaches threshold' (probability 0 on the single Mσ path) that the stochastic model is safe, one would need P_M(flag=true) ≤ P_{Mσ}(counter≥threshold), not ≥. With the stated ≥ direction, M can have positive probability of a contamination flag even when the deterministic counter path is safe. Thus the claim 'recurrence and safety guarantees under uncertainty' is not established for the stochastic model; if the intended guarantee is only for the deterministic counter model M′, then the 'under uncertainty' wording overstates what is verified.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a case study for synthesising robust controllers of robot collectives with recurrent cleaning tasks. The authors build a reward-enhanced POMDP M in PRISM, in which robot positions, battery levels, time, and Boolean contamination flags are modelled, and partial observability hides the contamination flags from the strategy. PRISM synthesises a deterministic, memoryless strategy σ by minimising a weighted reward over a finite horizon T (Eq. 3). The strategy is then applied to a deterministic, counter-based model M′ to obtain an induced model Mσ, on which the PLTL requirements FR, ωR, ωC, BC, CT, and UT from Table 2 are verified. The paper reports synthesised schedules for one and two robots, a parameter study over grid resolution, contamination probability, and penalty weight, and argues for the scalability of the pipeline, including a 12-hour schedule for 3 robots and 11 rooms. The conclusion claims 'recurrence and safety guarantees on the resulting strategies under uncertainty'.","tokens_in":15233,"tokens_out":7628,"duration_ms":70503,"significance":"The paper is a transparent and practically oriented case study. Its strengths are the concrete benchmark, the clear separation of synthesis and verification, the careful discussion of model-size and parameter trade-offs, and the explicit acknowledgement of the main limitation in Section 3.6. If the transfer from Mσ back to M were established, the approach would be a useful recipe for applying POMDP synthesis to recurrent collective tasks at a scale beyond toy examples. As it stands, however, the central guarantee is not supported: the verification results are for a deterministic, fully observable induced model, while the claimed guarantee concerns stochastic behaviour under uncertainty. The abstraction property suggested in Section 3.6 has the wrong inequality direction for that transfer, so the conclusion overstates what is established.","major_comments":[{"comment":"The paper verifies CT, BC, UT, and the recurrence properties on the deterministic induced model Mσ, but the central claim is that the resulting strategy is safe and recurrent 'under uncertainty' in the stochastic POMDP M. Section 3.6 defers to future work the property that 'the probabilities of the contamination flags set in M are greater than or equal to the hypothetical probabilities of the corresponding counters in M′ and, thus, Mσ, reaching their thresholds.' This inequality has the wrong direction for the safety transfer. To infer from the verified property P≤0[F Ri.d ≥ Ri.threshold] on the single path of Mσ that M cannot reach the contamination threshold, one would need P_M(Rj.d=true) ≤ P_{Mσ}(Rj.d ≥ Rj.threshold); with the stated ≥ direction, M can have positive probability of a contamination flag even when the deterministic counter path is safe. Hence the guarantees claimed in the Conclusion for the stochastic model are not established. The authors should either prove a correct conservative-abstraction relation between M and Mσ for the relevant events, or restrict the guarantee to the deterministic model Mσ and revise the wording of the Conclusion accordingly.","section":"Section 3.6 (and Section 6)"},{"comment":"The recurrence verification is performed for a region ω whose thresholds are chosen after examining the synthesised strategy (Section 4.1: 'We identified ω manually by examining the generated strategy'; Section 4.2: 'verifying a list of probable ωs'). This turns the 'correct recurrent' classification in Figure 7 into a search for a post-hoc witness rather than an independent check. The paper acknowledges this difficulty in Section 5 ('Selecting the Recurrence Area ω'), but the text in Section 4.2 and the Conclusion should qualify the recurrence claim: it is conditional on a manually selected ω, and no argument is given that ω covers all states from which σ is intended to be applicable. A strategy verified only from a hand-picked ω does not by itself establish the recurrence requirement ω → F≤T ω in Formula (2).","section":"Section 4.2 and Section 3.7"},{"comment":"The synthesis query minimises a weighted reward in which the safety requirements are encoded as finite penalties a_lot and a_bit rather than as hard constraints. The statement in Section 3.3 that 'the penalty for constraints is chosen such that it is not possible to offset the penalty of an invalid state by the reduced penalty for a less energy-consuming strategy' is not proved. Without a bound on the maximum energy-reward difference among strategies that satisfy Table 2, a strategy minimising Eq. (3) is not known to be energy-optimal among the admissible strategies. The paper should either provide such a bound or explicitly state that 'optimal' means optimal with respect to the hand-tuned reward function, not optimal among the verified safe and recurrent strategies.","section":"Section 3.3 and Section 3.5 (Eq. 3)"}],"minor_comments":[{"comment":"The requirement identifiers are inconsistent: Section 3.3 uses ωC for the battery-threshold requirement, while Table 2 uses ωR for that requirement and ωC for the contamination-threshold requirement. Please align the naming.","section":"Table 2 and Section 3.3"},{"comment":"The phrase 'all shortest sequences of transitions with non-zero probability' is undefined: a contamination flag in M can be set along paths of different lengths, and M′ contains no probabilities, so 'non-zero probability' does not directly apply to sequences in M′.","section":"Section 3.6"},{"comment":"The axis label 'cumulative propability' is misspelled, and the caption mentions only blue and green markers while the text refers to incorrect strategies shown in red; please make the colour coding visible and consistent in the figure and caption.","section":"Figure 7"},{"comment":"The phrase 'quasi-LTL, that is, ACTL* allowing only one universal quantifier at the outermost level' is imprecise: the PLTL properties in Table 2 use probabilistic operators P≤0 and P≥1, which are not literally ACTL* formulas. A brief clarification of the intended logic fragment would help.","section":"Section 3.7"}],"recommendation":"major_revision","confidential_remarks":"The paper sits between an engineering case study and a formal-methods contribution. The main risk is the overclaim in the Conclusion: the verification is performed on a deterministic induced model, while the guarantee is stated for the stochastic POMDP. Because the paper itself identifies the missing abstraction condition, I see this as addressable by a major revision rather than a rejection. The authors should either supply a soundness argument for the specific models and strategies considered, or visibly weaken the claims to what is actually verified."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe thing to know: this is a genuinely useful case study of a POMDP-based synthesis workflow for recurrent robot cleaning tasks, with a clever trick of hiding stochastic contamination behind observability to keep the belief space small, and then verifying on a deterministic induced model. The engineering is solid and the paper is admirably transparent about its limitations. But the central claim that the resulting strategies provide 'recurrence and safety guarantees under uncertainty' is not established by the verification.\n\nThe new contribution is the specific pipeline: synthesize in PRISM on a POMDP with boolean contamination flags, then extract the deterministic Mσ with integer counters and check PLTL properties there. The case study results—partition-based strategies, the parameter maps in Figure 7—are concrete and give practical guidance on grid resolution and penalty weights. The paper also does a good job of discussing scalability, e.g., the 3-robot, 11-room, 12-hour schedule in 15 hours.\n\nThe soft spot is real. Section 3.6 explicitly defers the quantitative soundness proof connecting the boolean flags in M to the integer counters in Mσ. The paper suggests checking whether P_M(flag set) ≥ P_{Mσ}(counter ≥ threshold). But to lift a safety property like 'counter never reaches threshold' (probability 0 on the single Mσ path) to a corresponding safety property in M, you need the opposite inequality: P_M(flag) ≤ P_{Mσ}(counter). With the stated direction, a strategy verified on Mσ could still have positive probability of contamination reaching threshold in M. So the 'under uncertainty' guarantee is really only a guarantee for the deterministic counter model. This is not a fatal flaw for the case study, but it needs to be fixed or the claims softened.\n\nMinor concerns: the recurrence region ω is selected after looking at the synthesized strategy, so there is some circularity in the evaluation; the parameter choices in Section 4.2 are manually tuned; and the evaluation is on a small, simplified layout. None of these kill the paper.\n\nWho is this for? Researchers working on POMDP-based synthesis for multi-robot planning, especially those using PRISM. It deserves a serious referee—the pipeline is novel and the practical guidance is valuable—but the referee should push for either a soundness proof for the abstraction or a careful restatement of what is actually verified.","headline":"A transparent and genuinely useful POMDP synthesis case study whose central 'guarantees under uncertainty' claim is not fully established because the verified deterministic model's abstraction relation to the stochastic model is unproven, and the paper's suggested future-work inequality points the wrong way.","tokens_in":15637,"tokens_out":4363,"would_cite":true,"duration_ms":39166,"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 a two-stage pipeline—POMDP strategy synthesis followed by verification of the induced deterministic model—can produce recurrent, energy-optimal, safe cleaning schedules for robot collectives under uncertainty.","keywords":["robot collectives","POMDP strategy synthesis","probabilistic model checking","recurrent tasks","safety verification","cleaning robots","partial observability"],"falsifier":"Run the synthesised strategy σ on the original stochastic POMDP M, or on a high-resolution Monte Carlo simulation of it, and record for each room the maximum contamination counter reached; if any room reaches its threshold R_j.threshold although the model checker's verification of Mσ reports the contamination-safety property CT as satisfied, the abstraction is unsound. A sharper test is to compute, for a single room, the probability under σ that the boolean flag R_j.d becomes true in M and compare it with the probability under σ that the counter R_j.d reaches R_j.threshold in M; if the latter ever exceeds the former, the flags are not a conservative quantitative abstraction.","tokens_in":14650,"feed_emoji":"🤖","tokens_out":10186,"duration_ms":87553,"temperature":0.7,"pith_summary":"The paper claims that a two-stage pipeline can produce correct-by-construction controllers for robot collectives with recurrent tasks: first synthesise a strategy on a small partially observable stochastic model (a POMDP) that hides room contamination, then apply that strategy to a non-probabilistic model with integer contamination counters and verify recurrence and safety properties with a standard model checker. The running case study is a team of battery-driven cleaning robots that must keep rooms below contamination thresholds, never fully discharge, and avoid rooms while they are occupied. If the pipeline works as claimed, cleaning schedules for public buildings could be generated automatically and certified against hygiene and safety requirements despite uncertainty about contamination levels. The paper reports synthesising and verifying a 12-hour schedule for 3 robots and 11 rooms in 15 hours.","feed_headline":"Robot cleaning schedules synthesised and verified in 15 hours","feed_subtitle":"A two-stage pipeline turns a stochastic model into a certified cleaning schedule for robot teams.","key_machinery":"The central mechanism is the strategy-induced deterministic model Mσ. After the model checker's grid-based belief-MDP approximation synthesises a memoryless deterministic POMDP strategy σ, the paper builds Mσ by replacing boolean contamination flags with integer counters, removing all probabilistic branching, and pruning every action not selected by σ at the corresponding time step, leaving a single-path model that can be checked with ordinary probabilistic model checking. The same reward structure does double duty: heavy penalties encode hard constraints that synthesis cannot handle as temporal-logic formulas, while smaller penalties and separate rewards steer the search toward energy-efficient, utilisation-compliant schedules.","core_discovery":"On the paper's own terms, the central claim is that weighted, partially observable stochastic models and POMDP strategy synthesis can provide recurrence and safety guarantees for optimally coordinated robot collectives under uncertainty. The method encodes four requirements—robots return to start with sufficient charge, batteries never empty, contamination never exceeds thresholds, and no cleaning during room utilisation—partly as penalties in the reward structure because PLTL constraints cannot be used directly in synthesis, and partly as PLTL properties checked after synthesis. The strategy is synthesised by minimising a sum of penalty, energy-consumption, and utilisation rewards up to a fixed horizon T, with contamination flags hidden from the strategy so it must be robust to the accumulation of contamination probability. Then the strategy is transferred to a deterministic integer-counter model Mσ and verified against recurrence and safety formulas; the paper presents a 3-robot, 11-room case where the resulting 12-hour schedule is verified in this way.","pith_inferences":["Beyond what the paper claims, the deferred soundness check can be settled directly: simulate σ on the original POMDP and compare, room by room, the probability that the boolean flag becomes true with the probability that the integer counter reaches its threshold.","The border-region observation suggests an automated tuning loop that searches the penalty/probability parameter space for strategies whose verified recurrence set borders non-recurrence, where the paper found optimal strategies.","The modest synthesis times relative to the 24-hour schedule make the pipeline a plausible online re-planning tool for daily utilisation-plan changes, not just a one-shot schedule generator."],"forward_implications":["Cleaning schedules for multi-robot teams can be generated and certified against recurrence (all robots back at start, charged, contamination below threshold) and safety (no empty batteries, no threshold overrun, no cleaning during occupancy).","The case-study numbers suggest the pipeline is practical at moderate scale: 3 robots, 11 rooms, 12-hour horizon, about 690,000 belief states and 11.8 million transitions, with synthesis and verification completed in 15 hours.","Parameter studies show a region of favourable settings (cumulative contamination probability around 40% and contamination penalty around 300) and that increasing grid resolution yields lower-energy strategies, placing optimal recurrent strategies near the border between recurrent and non-recurrent behaviour.","The same modelling pattern transfers to other spatio-temporal recurrent tasks, such as firefighting drone patrols, geriatric care monitoring, and general patrolling."],"supporting_citations":[{"why":"Supplies the POMDP formalism and the grid-based belief-MDP approximation used for strategy synthesis.","marker":"[13]"},{"why":"Documents the model checker's POMDP strategy synthesis and property-checking commands used in both pipeline stages.","marker":"[14]"},{"why":"Shows minimal-energy POMDP strategy synthesis for robot object-finding, the starting point the paper extends from reachability to recurrent response properties.","marker":"[4]"},{"why":"Provides multi-objective MDP synthesis with bounded co-safe LTL properties that the paper contrasts with its bounded response property support.","marker":"[9]"}],"fun_headline_variants":["Certified 12-hour cleaning schedules from POMDP synthesis","Verified robust robot cleaning schedules in 12 hours","POMDP synthesis yields verified cleaning schedules for robots","Recurrent task controllers for robot collectives verified","Robust robot cleaning strategies synthesised and verified"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The verified safety of the deterministic schedule transfers back to the original stochastic model, which requires that a room's boolean contamination flag in the POMDP is at least as likely to be set as the room's integer contamination counter is to reach its threshold; the paper does not prove this and leaves it to future work.","fun_headline_variants_meta":{"raw":{"variants":["Certified 12-hour cleaning schedules from POMDP synthesis","Verified robust robot cleaning schedules in 12 hours","POMDP synthesis yields verified cleaning schedules for robots","Recurrent task controllers for robot collectives verified","Robust robot cleaning strategies synthesised and verified"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00053,"raw_usage":{"total_tokens":2532,"prompt_tokens":904,"completion_tokens":1628,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":520,"completion_tokens_details":{"reasoning_tokens":1553}},"tokens_in":520,"tokens_out":1628,"duration_ms":10434,"temperature":1.0,"reasoning_tokens":1553,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:15:13.403763+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the synthesised strategy σ on the original stochastic POMDP M, or on a high-resolution Monte Carlo simulation of it, and record for each room the maximum contamination counter reached; if any room reaches its threshold R_j.threshold although the model checker's verification of Mσ reports the contamination-safety property CT as satisfied, the abstraction is unsound. A sharper test is to compute, for a single room, the probability under σ that the boolean flag R_j.d becomes true in M and compare it with the probability under σ that the counter R_j.d reaches R_j.threshold in M; if the latter ever exceeds the former, the flags are not a conservative quantitative abstraction.","supporting_citations":[{"cited_title":"Real-Time Systems 53(3), p","cited_arxiv_id":null,"evidence_quote":"Supplies the POMDP formalism and the grid-based belief-MDP approximation used for strategy synthesis."},{"cited_title":"Available at http: //www.prismmodelchecker.org/manual/","cited_arxiv_id":null,"evidence_quote":"Documents the model checker's POMDP strategy synthesis and property-checking commands used in both pipeline stages."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows minimal-energy POMDP strategy synthesis for robot object-finding, the starting point the paper extends from reachability to recurrent response properties."},{"cited_title":"In: Automated Planning and Scheduling (ICAPS), 27th Int","cited_arxiv_id":null,"evidence_quote":"Provides multi-objective MDP synthesis with bounded co-safe LTL properties that the paper contrasts with its bounded response property support."}],"review_version":1}