{"id":"f483021c-b601-4891-b6e3-564c0a951d4b","arxiv_id":"2508.19186","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"A custom, tiny model checker on a Raspberry Pi robot generates multi-step obstacle avoidance plans in real time, outperforming a one-step reactive controller in cul-de-sac and playground trials.","lead":"This paper puts a small model checking routine inside a low-powered robot's loop to plan several avoidance moves ahead, and on real trials it avoided cul-de-sacs faster than a one-step reactive controller. The planning runs in under 22 milliseconds on a Raspberry Pi with a 2D LiDAR, using no pre-computed map.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Safety Theorem 5.2 is undercut by Eq. 15: P_shield's upper bound is vΔt+ε, not d_safe+vΔt+ε, so a disturbance just beyond one step's travel enters P_safe before being flagged.","rationale":"I read the paper's central claim as two-part: (i) a bespoke on-board model checker can generate multi-step obstacle-avoidance plans under real-time constraints, and (ii) two properties hold, including that no disturbance can enter the safe zone. Part (i) is supported by the reported latencies, the memory profiling, and the comparative runs; the small sample in Scenario 2 and unreported parameter values are real weaknesses but not the most load-bearing. Part (ii) is the load-bearing formal support for 'collision free navigation is guaranteed,' and Theorem 5.2 is the only proof of that guarantee. The proof is invalid under the stated definitions: Eq. 15's upper bound is one step of travel from the origin, not one step beyond the safe-zone radius. The proof silently changes vΔt+ε into d_safe+vΔt+ε. This is the kind of defect that can be settled by re-deriving the inequality and by checking the released code. I do not think this changes the reader's CONDITIONAL verdict: the empirical contribution appears real, but the safety guarantee must either be corrected in Eq. 15 or explicitly downgraded to an empirical/assumption-dependent claim. My agreement is partial because the reader's weakest_assumption emphasizes lateral error and static abstraction, while I am pointing to a precise offset error in the shield definition; the reader's rationale does mention a sign error, so this is overlapping rather than identical.","tokens_in":26923,"tokens_out":7314,"duration_ms":74712,"concrete_test":"Re-derive Theorem 5.2 from Eq. 15 as written with the numerical counterexample above (x0 = vΔt+ε+0.5·d_safe). If the model permits this initial condition, the computation shows penetration of P_safe in one step, contradicting the theorem. Then inspect the released implementation (zenodo/15382644) for the actual P_shield construction: if the code uses d_safe+vΔt+ε as the upper bound, the paper's Eq. 15 is a typo and the theorem can be repaired; if the code matches the printed bound, the safety guarantee is false. An additional empirical check: place a calibration obstacle at distance x in (vΔt+ε, d_safe+vΔt+ε) in front of the robot and record whether the robot stops/plans only after the obstacle is inside the safe zone.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim 'collision free navigation is guaranteed' rests on Theorem 5.2. The proof assumes that if a disturbance was not in P_shield at t-1, then D+_x > d_safe + vΔt + ε. That inference is not licensed by Eq. 15, which defines P_shield as {o | d_safe < min(o_x) ≤ vΔt+ε ∧ ...}. The stated upper bound gives only D+_x > vΔt+ε (or D+_x ≤ d_safe). Place a stationary disturbance at x0 = vΔt+ε+δ with 0<δ<d_safe, y=0. It is outside P_shield as written. After one straight-task step of length vΔt+ε, its relative x is δ, which is inside P_safe (Eq. 14). Thus the safe zone can be penetrated before the shield ever flags the disturbance. To make the theorem go through, the longitudinal interval in Eq. 15 must be (d_safe, d_safe+vΔt+ε], not (d_safe, vΔt+ε]. This is a concrete algebraic/definitional error in the only formal argument for the safety guarantee. A separate but related gap is Theorem 5.2's explicit assumption that lateral error is negligible; that would need experimental support even after Eq. 15 is corrected.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a custom, on-board model-checking planner for a low-cost differential-drive robot with 2D LiDAR. It abstracts closed-loop obstacle-avoidance tasks into spatial partitions, constructs a 15-state disturbance-focused transition system, and uses an NFA for an LTL property to generate multi-step plans by counterexample search via forward depth-first search. Two scenarios (cul-de-sac, playground) compare planning against a one-step reactive baseline using trajectory length, collisions, latency, and memory. Reported processing latency is below 22 ms, with zero collisions for the model-checking method in the collected runs. Two informal theorems claim that the robot cannot get trapped in a corner and that no disturbance can enter the safe zone.","tokens_in":27276,"tokens_out":10608,"duration_ms":107700,"significance":"If the claims hold, the paper is a useful instructional case study showing that a small, purpose-built model checker can run on a low-powered robot in real time. Strengths include the deposited code (Zenodo link), the clear empirical setup, measured latency/memory data, zero collisions in the reported runs, and a transparent LTL/NFA formulation. The main safety theorem, however, is not correct as stated, and the unconditional \"collision free navigation is guaranteed\" phrasing in §5.5 and §7 overstates the support provided. The paper is also honest about its limitations (static environments, no target-driven behavior, specific hardware), which is welcome. The contribution is modest in scope but potentially publishable after the formal guarantee is repaired and the empirical claims are tempered.","major_comments":[{"comment":"P_shield is defined with upper bound vΔt+ε, not d_safe+vΔt+ε. The proof then infers that a disturbance not in P_shield at t−1 satisfies D+_x > d_safe+vΔt+ε; this is not licensed. A stationary disturbance at x0 = vΔt+ε+δ with 0<δ<d_safe, y=0 lies outside P_shield as written, yet after one straight step its relative x-coordinate is δ, inside P_safe (Eq. 14). Thus the safe zone can be penetrated before the shield flags the disturbance. The fix is to define P_shield's longitudinal interval as (d_safe, d_safe+vΔt+ε] and to correct the proof's algebra to D+_x − (vΔt+ε) > d_safe. Since the unconditional safety claim in §5.5 and §7 rests on Theorem 5.2, this is load-bearing.","section":"§5.4.2, Eq. (15) and Theorem 5.2"},{"comment":"The proof assumes that lateral error is negligible, but no lateral tracking-error measurement is reported and the platform is acknowledged to have a strong right veer (§5.2.1). With differential-drive servos, a few centimeters of lateral drift can move a disturbance into P_shield's lateral band while its x-coordinate is outside the required interval; the proof has no margin for this. Please either provide empirical lateral-error data and set the shield's lateral tolerance accordingly, or state the theorem as conditional on zero lateral error and remove the unconditional \"collision free navigation is guaranteed\" in §5.5 and §7.","section":"§5.4.2, Theorem 5.2 and §5.5"},{"comment":"The statement uses \"subsequence,\" but the proof only rules out the adjacent ordered pair ⟨T_L,T_R⟩ (and has a typo, repeating ⟨T_L,T_R⟩ twice). The distinction matters: Fig. 9 admits paths such as T_L, T_S, T_R, T0 (via s1→s3→s5), so if \"subsequence\" is read in the standard non-contiguous sense, the theorem is false as stated. If the intended claim is that avoid tasks never occur consecutively, state this explicitly and repair the proof. If the stronger non-contiguous claim is intended, a different argument is needed.","section":"§5.4.1, Theorem 5.1"}],"minor_comments":[{"comment":"The numeric values of parameters dsafe, dmax, dmin, β, L+tol, v, and ε are never reported. A parameter table would greatly improve reproducibility, even though code is available.","section":"§4.2 and §5"},{"comment":"The condition \"D_L_y ∈ P_L < d_min ∧ D_R_y ∈ P_R > −d_min\" is malformed; it should express that the nearest lateral disturbance in each direction is within d_min. Also, Algorithm 2, line 4 uses Δ_y while the input is Δ_L/R.","section":"Algorithm 3, line 19"},{"comment":"The edge label \"T / T0 S / T0 S\" in Fig. 9 is garbled, and some edges have ambiguous labels. Please define all edge labels explicitly in the caption or text.","section":"Fig. 9 and Definition 1"},{"comment":"The baseline method is not fully specified. In particular, it is unclear whether the baseline uses the same safe-zone and P_shield logic or only a single task feedback loop; this matters for interpreting the collision counts.","section":"§5.1"},{"comment":"The use of min(o_x) in P_shield is inconsistent with the pointwise definitions in Eqs. (3)–(12); using o_x would be clearer.","section":"Eq. (15)"},{"comment":"The playground scenario reports only two comparisons, apparently one run per method per comparison. The paper should state the number of runs explicitly and avoid generalizing \"reliably avoids collisions\" from this small sample.","section":"§5.3.2"}],"recommendation":"major_revision","confidential_remarks":"The paper's core novelty is modest — the \"model checking\" in the loop is a small DFS over a hand-built 15-state graph — but the empirical demonstration on a real low-power robot is solid enough to be worth publishing after the Theorem 5.2 definitional error is fixed. The framing in the introduction and Section 6 should also be tempered to avoid overclaiming against general-purpose model checking. The code deposit and the explicit limitations are good scholarly practice."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read on arXiv:2508.19186. The real contribution is empirical: a purpose-built model checker running on a Raspberry Pi, planning multi-step obstacle avoidance in under 22 ms, with shipped code and a sensible comparison against a one-step reactive baseline. I buy the latency and the trajectory results. In the cul-de-sac, the planner gets out and the baseline gets stuck; in both playground comparisons the planner produced fewer collisions. That is a genuine first (to my knowledge) for on-board real-time model checking for planning, and it's a useful case study for the formal-methods-in-robotics crowd.\n\nThe formal wrapping, though, is shakier than the abstract suggests. The stress-test concern about Theorem 5.2 lands. Eq. 15 defines P_shield as d_safe < min(o_x) <= vΔt+ε, but the proof requires the upper bound to be d_safe + vΔt + ε. As written, a disturbance sitting just beyond one step's travel is outside P_shield and enters P_safe after one straight step, so the claim \"no disturbance can enter the safe zone\" doesn't follow from the equations. That's a concrete fix—just correct the interval in Eq. 15—but until it's fixed, the safety guarantee is unsupported. The theorem also just assumes zero lateral error, which is an empirical claim needing at least a sensitivity check. Theorem 5.1 is less concerning: it's true because the transition system has no TL/TR alternation edges, which is a design property of the model rather than a verified fact about the world. And the key parameters (dsafe, dmax, dmin, beta) are never reported, which hurts reproducibility even with the code on Zenodo.\n\nTo be fair, the paper is honest about several limitations itself: no target-driven behavior, single hardware platform, static environments, small playground sample. The second scenario is two comparisons, so I'd treat it as illustrative.\n\nBottom line: solid engineering demonstration, overstated guarantees. It deserves peer review—the idea and the system are worth discussing—but the authors should fix Eq. 15, soften \"guaranteed\" to \"empirically supported under stated assumptions,\" and report the parameter values. I'd send it to a robotics venue with formal-methods reviewers, not to a pure verification venue.\n\nFor me: I'd bring it to reading group, but I don't see myself citing it in the next year.","headline":"Real, working on-board model-checking planner; the empirical claim holds, but the safety proof has a concrete definitional gap and the no-corner-trap theorem is true by construction.","tokens_in":27735,"tokens_out":2723,"would_cite":false,"duration_ms":28043,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that a purpose-built model checker can generate multi-step obstacle-avoidance plans on a low-powered robot in about 10 ms with no precomputed data, and that two safety properties—no corner trapping and collision-free navig","keywords":["model checking","reactive planning","obstacle avoidance","closed-loop control","LTL","LiDAR abstraction","real-time planning","mobile robots"],"falsifier":"Measure actual lateral displacement over a 200 ms straight-driving step on the real platform; if it is large enough that a LiDAR point could cross the safe-zone boundary between observations, the safe-zone guarantee fails. Alternatively, instrument the executed task sequence in a corridor designed to provoke left-right alternation; any executed pair ⟨T_L, T_R⟩ or ⟨T_R, T_L⟩ would falsify the no-corner-trapping theorem.","tokens_in":26845,"feed_emoji":"🤖","tokens_out":8747,"duration_ms":84983,"temperature":0.7,"pith_summary":"Model checking is normally an offline verification tool; this paper turns it into an on-board planner. The authors claim that a small, purpose-built checker can run on a Raspberry Pi-class robot, take the current 2D LiDAR snapshot, reason three or four closed-loop actions ahead, and output an obstacle-avoidance plan in about 10 milliseconds—well inside the 100 ms real-time deadline. The central trick is to abstract each closed-loop \"task\" (turn left, turn right, drive straight) into a static spatial partition, so the future can be represented by a 15-state transition system and a plan is just a counterexample to an LTL property. If the claims hold, reactive robots can be both fast and explainable, avoiding the corner-trapping failure of one-step reactive controllers without needing precomputed maps.","feed_headline":"Model checker on a low-power robot plans escapes in 10 ms","feed_subtitle":"Counterexamples become multi-step avoidance plans; tests show zero collisions where one-step reactive control failed.","key_machinery":"The load-bearing object is the disturbance-focused transition system (Definition 1), a 15-state egocentric model whose states are valued at runtime from sensor data. The abstraction renders closed-loop task outcomes as static geometry: LiDAR points are shifted by offsets Δ+ and Δ_L/R to simulate proximal detection and lateral displacement, then filtered into lateral partitions P_L/P_R and longitudinal partitions P_+/P_− (Algorithms 1–2). The planner checks the LTL property φ = ¬(safe U (safe ∧ horizon)) by forming the product of the transition system with a two-state NFA; an accepting path found by forward depth-first search is a safe task sequence, and the shortest such sequence without con","core_discovery":"The central claim is that real-time multi-step planning can be achieved by running model checking inside the robot's control loop. The authors define a disturbance-focused transition system of 15 states whose valuations are computed at runtime from LiDAR observations: obstacles are translated by fixed offsets to predict what the robot will sense after each closed-loop task, and lateral and longitudinal partitions decide whether a straight task has a finite or infinite horizon. Planning is formulated as finding a counterexample to the LTL property ¬(safe U (safe ∧ horizon)), using a two-state NFA and forward depth-first search, so the counterexample path is the robot's plan. In a cul-de-sac s","pith_inferences":["I would extend the safety claim cautiously: because dsafe, dmax, dmin, and beta are never given numerical values, the informal proofs should be read as conditional on parameter choices; measuring the actual values on the platform would turn them into testable quantitative predictions.","The rigid-translation abstraction suggests an immediate stress test on surfaces with slip or camber; if lateral error over a 200 ms step is not negligible relative to dsafe, the safe-zone guarantee probably needs an explicit error bound rather than an assumption.","A natural generalisation is target-driven navigation: the paper deliberately omits localisation, but its own discussion notes SLAM can add hundreds of milliseconds, so adding goal-directed behaviour while preserving the latency budget is an open problem.","The architecture could be reused as a fast receding-horizon planner in dynamic environments by re-running the checker every control step, but the static-environment assumption in Section 4.2.2 must first be relaxed."],"forward_implications":["If the central claim is right, on-board model checking can meet hard real-time constraints on a low-powered device: mean latency around 10 ms in the cul-de-sac and at most 21.61 ms for four-step plans, both well below the 100 ms deadline.","The collision counts in both scenarios (0 for model checking versus 3 and 6 for the one-step baseline) imply that multi-step reasoning prevents a class of collisions that purely reactive control does not.","Because the transition system has no transitions producing alternating left/right pairs, the robot cannot exhibit the corner-trapping behaviour that motivates the paper, regardless of the static environment.","The shield-partition theorem implies that, absent lateral error, the robot will always act before a disturbance reaches its safe zone during straight driving—so the safety property is structural, not merely observed.","With estimated model-checking memory of about 2.9 KB, the planner leaves most of the Raspberry Pi's RAM free, so the approach is practical for energy-constrained platforms and needs no offline pre-computation."],"supporting_citations":[{"why":"Baier and Katoen's monograph supplies the LTL grammar, NFA semantics, and product-transition-system construction that the planning-as-counterexample method is built on.","marker":"[2]"},{"why":"The SPIN/Unity overtaking planner whose roughly 3 second compilation-and-communication lag is the concrete bottleneck this paper's bespoke on-board checker is designed to remove.","marker":"[48]"},{"why":"The extended overtaking planner with memoisation that this work adapts, providing the closed-loop planning baseline and the motivation for faster model checking.","marker":"[47]"},{"why":"Prior closed-loop multi-step planning on a low-powered robot using a physics engine, which grounds the \"core knowledge\" and attention framing this paper adopts.","marker":"[34]"},{"why":"Earlier real-time safe-navigation work in unstructured partially observable environments that checks single trajectories without planning, the gap the paper fills.","marker":"[7]"},{"why":"Online strategy synthesis with Uppaal Stratego taking 0.04–6.99 seconds, used as a comparison point for the speed of the purpose-built checker.","marker":"[37]"}],"fun_headline_variants":["Robot's onboard model checker plans escapes in real time","Model checking on a low-power robot enables multi-step avoidance","Real-time model checking makes robot obstacle avoidance safer","Low-power robot uses model checking to plan around obstacles","Counterexamples become plans: onboard model checking for robots"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"Everything rests on the assumption that the robot's immediate future can be predicted by rigidly shifting the current LiDAR cloud forward or sideways by fixed offsets, with lateral error effectively zero, in an environment that does not change.","fun_headline_variants_meta":{"raw":{"variants":["Robot's onboard model checker plans escapes in real time","Model checking on a low-power robot enables multi-step avoidance","Real-time model checking makes robot obstacle avoidance safer","Low-power robot uses model checking to plan around obstacles","Counterexamples become plans: onboard model checking for robots"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000751,"raw_usage":{"total_tokens":3193,"prompt_tokens":774,"completion_tokens":2419,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":2343}},"tokens_in":518,"tokens_out":2419,"duration_ms":17183,"temperature":1.0,"reasoning_tokens":2343,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T15:53:14.252496+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Measure actual lateral displacement over a 200 ms straight-driving step on the real platform; if it is large enough that a LiDAR point could cross the safe-zone boundary between observations, the safe-zone guarantee fails. Alternatively, instrument the executed task sequence in a corridor designed to provoke left-right alternation; any executed pair ⟨T_L, T_R⟩ or ⟨T_R, T_L⟩ would falsify the no-corner-trapping theorem.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The SPIN/Unity overtaking planner whose roughly 3 second compilation-and-communication lag is the concrete bottleneck this paper's bespoke on-board checker is designed to remove."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Prior closed-loop multi-step planning on a low-powered robot using a physics engine, which grounds the \"core knowledge\" and attention framing this paper adopts."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Earlier real-time safe-navigation work in unstructured partially observable environments that checks single trajectories without planning, the gap the paper fills."},{"cited_title":"Lehmann, A","cited_arxiv_id":null,"evidence_quote":"Online strategy synthesis with Uppaal Stratego taking 0.04–6.99 seconds, used as a comparison point for the speed of the purpose-built checker."}],"review_version":1}