{"id":"6cb9ab95-c2d5-47f1-b7ec-7408c187b318","arxiv_id":"2412.08102","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":5,"one_line_summary":"Using Verse and CARLA, the authors compute reachable sets for a simulated VTOL landing system and claim safe landing within a helipad and collision avoidance in five scenarios.","lead":"This paper demonstrates a verification and validation pipeline for a vision-based VTOL air taxi landing system, combining the Verse reachability tool with the CARLA photorealistic simulator. It reports scenario-based safety checks for five landing situations, but the obstacle-avoidance results depend on carefully curated initial conditions.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Safety claim for obstacle scenarios rests on altered initial-condition sampling, not the stated scenario.","rationale":"The single most load-bearing concern is the undisclosed alteration of the initial-condition distribution for the obstacle scenarios. The formal verification claim depends on the premise that the reachability analysis covers the stated initial set. By changing the spawn logic to favor a subset of trajectories, the authors verify a different scenario than the one they describe, so the safety conclusion for Scenarios 3 and 5 does not follow. This is not a minor methodological quibble; it directly undermines the central claim that the autonomous landing system is safe within the range of conditions and constraints described in the evaluation scenarios. The admission in §V.D is explicit, so the concern is grounded in the paper itself rather than an external assumption. A concrete test—rerunning the reachability analysis with the original spawn logic—would settle whether the concern lands. If the reachable set intersects the obstacle, the safety claim for those scenarios is invalid. The reader's weakest_assumption identified the same issue, and the proposed verdict of REJECT is appropriate because the paper's headline safety guarantee does not hold for the scenarios as stated. Other issues, such as the small number of trajectories and manual removal of destabilizing runs, are secondary but reinforce the conclusion that the formal safety claim is not adequately supported.","tokens_in":14410,"tokens_out":4004,"duration_ms":35693,"concrete_test":"Re-run Verse reachability for Scenario 3 (and 5) using the original, unmodified spawn logic: sample initial positions uniformly over the exact ranges specified in §V.B (x∈[−5.5,−3.0], y∈[−1.5,1.5], z∈[73.0,77.0]) without biasing toward one side of the intruder, and check whether the computed reachable set intersects the intruder's bounding box. If it does, the safety claim in §V.D is falsified for the stated scenario. As a robustness check, repeat with 100 trajectories and verify whether the over-approximation still intersects the obstacle.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central safety claim in §V.D—that the reachability analysis shows safe landing and collision avoidance for Scenarios 3 and 5—is unsupported because the initial-condition distribution used for those scenarios was changed after the fact. In §V.B, Scenario 3 specifies that initial positions are sampled uniformly from x∈[−5.5,−3.0], y∈[−1.5,1.5], z∈[73.0,77.0]. However, §V.D admits that 'by modifying the spawn logic, the Minihawk is made to favor a subset of all possible trajectories around the obstacle,' and that with the original spawn logic the reachable set 'would erroneously include the region occupied by the obstacle.' This means the verified reachable set is computed over a different, smaller initial set than the one stated, so the formal guarantee of Eqs. (1)–(2) does not apply to the scenario as described. The authors acknowledge this limitation and mention partitioning the initial set as standard practice, but they do not implement it. Therefore, the headline claim that the system 'is safe and reliable' within the stated scenario ranges overreaches; the obstacle-avoidance verification holds only for the curated subset of trajectories.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper presents a Verification and Validation (V&V) framework for a vision-based autonomous landing system for a MiniHawk VTOL aircraft, combining the Verse reachability tool with a CARLA/Gazebo photorealistic simulation environment. Five scenarios are studied, varying initial-condition uncertainty, landing-point uncertainty, a static intruder obstacle, and the use of YOLOv8-based perception. The paper claims that Verse computes over-approximate reachable sets and that the system satisfies safe landing and collision-avoidance properties in all scenarios. It also outlines a validation methodology intended to address the sim-to-real gap, although no independent validation experiments are reported.","tokens_in":14641,"tokens_out":6779,"duration_ms":70673,"significance":"If the central claims were established, the paper would be a useful demonstration of integrating formal reachability analysis with high-fidelity simulation for VTOL landing, and it is candid about several practical limitations. The authors deserve credit for integrating Verse with CARLA/Gazebo, for defining five test scenarios, and for explicitly disclosing the spawn-logic modification and the small number of trajectories. However, the headline safety claim is not supported by the presented evidence: for the obstacle scenarios the reachable set is computed over a curated subset rather than the declared initial set, and the formal verification guarantee is not quantified. Consequently, the paper's main contribution is not currently established.","major_comments":[{"comment":"The safety claim for Scenarios 3 and 5 is unsupported. Section V.B states that Scenario 3 samples initial positions uniformly from x∈[−5.5,−3.0], y∈[−1.5,1.5], z∈[73.0,77.0], but Section V.D admits that the spawn logic was modified so that the MiniHawk favors a subset of all possible trajectories around the obstacle and that, with the original logic, the reachable set would erroneously include the obstacle region. Therefore the reachable tube used to check conditions (1)–(2) is not an over-approximation of the stated initial-condition set. The verification result can at best be read as covering a curated subset, not the scenario as defined, so the sentence in Section V.D that the system 'is safe and reliable' overreaches the evidence.","section":"§V.D and §V.B"},{"comment":"The probabilistic over-approximation guarantee is not established. The reachable sets are computed from only 10 trajectories per scenario, and the authors state that 'rarely' the MiniHawk simulation can destabilize and that such instances were 'manually identified and removed.' DryVR-style simulation-based reachability yields probably approximately correct over-approximations only under sampling assumptions; discarding trajectories after observing their outcomes introduces selection bias and voids or at least leaves unquantified the formal guarantee. The paper does not report sensitivity constants, confidence levels, or the number of discarded trajectories. Thus even for Scenarios 1, 2, and 4 the formal verification claim is not substantiated at the level the paper asserts.","section":"§V.C and §IV.A"},{"comment":"The validation component is not carried out independently. Section IV.B describes a methodology for validating reachability results through scenario-based testing, and the abstract says the results are validated by 'extensive scenario-based testing,' but no separate validation experiments are reported; the scenario results in Section V are the same simulations used to compute the reachable tubes. This makes the validation circular and does not provide independent evidence about the sim-to-real gap, which the paper itself acknowledges requires hardware-in-the-loop testing and outdoor experiments.","section":"§IV.B and §V"}],"minor_comments":[{"comment":"The word 'Additonally' should be 'Additionally'.","section":"§V.C"},{"comment":"The subsection heading 'Over-approximation in V&V Framework' is misleading because the described spawn-logic modification produces an under-approximation of the declared initial set, not an over-approximation.","section":"§V.D"},{"comment":"The phrase 'ensuring it flies behind the intruding vehicle' indicates that Scenario 3 is a single-behavior case study; this should be stated as a limitation in the abstract and conclusion if the safety claim is retained.","section":"§V.B"},{"comment":"The figures are referenced in the text but no captions or panel legends are visible in the provided manuscript, so the reader cannot tell which color corresponds to the reachable set, the obstacle, or the landing pad.","section":"Figures 8–12"}],"recommendation":"reject","confidential_remarks":"The manuscript is candid and generally well written, but the central verification claim is invalid as stated. I am recommending rejection because the flaw is in the main result, not a local presentation issue: the obstacle scenarios were verified on a curated subset of trajectories, and the formal guarantee is unquantified. A substantially revised manuscript that re-runs the obstacle scenarios with partitioned initial sets and reports proper probabilistic confidence bounds, or one that explicitly narrows the safety claim to the curated subset, could be viable in the future."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a useful integration case study, not a verified safety result for the obstacle scenarios. The authors deserve credit for clearly describing the pipeline and for disclosing the load-bearing caveat in Section V.D, but that caveat means the reachability guarantee for Scenarios 3 and 5 applies to a curated subset of initial states, not to the scenario as stated.\n\nWhat is new: the specific combination of Verse formal reachability with a high-fidelity CARLA+Gazebo MiniHawk landing pipeline, including a YOLOv8 perception module and A* planning, across five scenarios. The per-scenario reachable sets and the discussion of how perception uncertainty changes the final uncertainty radius are legitimate, if incremental, results. The writing is clear and the authors openly discuss dataset size, simulator fidelity, and the need for hardware-in-the-loop testing. That level of transparency is genuinely helpful for people building similar frameworks.\n\nSoft spots, in order of seriousness. First, the obstacle-avoidance verification in Scenarios 3 and 5 is not for the initial condition set described in Section V.B. Section V.D says the spawn logic was modified so the MiniHawk favors a subset of trajectories around the intruder, and that the original spawn logic would make the reachable set erroneously include the obstacle region. This is not a minor implementation detail; it undercuts the formal safety claim for those scenarios. The proposed fix, partitioning the initial set, is mentioned but not implemented. Second, only 10 trajectories per scenario are used, and destabilizing runs were manually removed. That is too little evidence for the probabilistic over-approximation guarantee that Verse/DryVR advertises, and the manual removal should at least be quantified and justified. Third, no code, data, or trained model are shipped, so the results are not independently reproducible. Fourth, the scenario-based validation uses the same simulation pipeline as the reachability analysis, making it a coherence check rather than truly independent validation. Finally, the paper says perception accuracy was evaluated with mAP but gives no numbers; as a reader I cannot assess how trustworthy the vision pipeline is.\n\nProportionate verdict: the framework architecture is sound and the paper is an honest demonstration of how Verse can be attached to a realistic VTOL landing simulator. Its mistake is overstating the strength of the guarantee. This is fixable with a rewritten claims section, a proper initial-set partitioning for the obstacle scenarios, and more trajectories or a clear statistical argument.\n\nFor a reader curious about Verse integration or eVTOL landing V&V, this is worth a look and worth citing as an example, though not as a proven safety certificate. I would send it to peer review because the area matters and the authors have done enough real engineering to deserve a serious referee, with the expectation of major revision.","headline":"An honest, well-scoped integration case study whose headline safety guarantee for the obstacle scenarios does not survive its own admitted change to the initial-state distribution.","tokens_in":15221,"tokens_out":1682,"would_cite":false,"duration_ms":21194,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A vision-based VTOL landing system is verified safe in five simulated urban scenarios.","keywords":["formal verification","reachability analysis","vision-based landing","VTOL air taxi","collision avoidance","high-fidelity simulation","sim-to-real gap"],"falsifier":"Using the paper's original spawn logic for scenario 3 or 5, sample initial conditions uniformly from the stated ranges and recompute the Verse reachtube; if any trajectory or the reachable set intersects the intruder's bounding box, the collision-avoidance claim is refuted.","tokens_in":14212,"feed_emoji":"🚁","tokens_out":5440,"duration_ms":51488,"temperature":0.7,"pith_summary":"This paper asks whether a vision-based autonomous landing system for a vertical take-off and landing air taxi can be shown safe before real-world flight tests. It answers by combining formal reachability analysis with a photorealistic simulation environment: for five urban emergency-landing scenarios, the reachable set of the aircraft stays inside the helipad and avoids obstacles. If this result stands, it supports using high-fidelity simulation as a step toward certifying autonomy for urban air mobility, narrowing but not closing the sim-to-real gap.","feed_headline":"Reachability analysis proves VTOL landing system safe in 5 scenarios","feed_subtitle":"Simulated MiniHawk lands inside the helipad and avoids intruder aircraft across five scenarios.","key_machinery":"The load-bearing object is the reachable set: the union of all positions the MiniHawk could occupy at a given time starting from a set of initial conditions. Verse computes an over-approximation of this set by simulating sampled trajectories in a black-box simulator and inflating them, so that if the over-approximation avoids the obstacle region and lies inside the landing pad, the safety guarantee holds for every trajectory the simulator can produce from those initial conditions. The simulator couples CARLA for photorealistic rendering and sensor images with Gazebo for the MiniHawk's vehicle dynamics.","core_discovery":"The paper establishes, on its own terms, that for five simulated emergency-landing scenarios on a rooftop helipad, the MiniHawk's vision-based landing system satisfies both required safety properties: at the end of the maneuver the reachable set of vehicle positions lies inside the landing pad, and along the way the reachable set never touches an obstacle. The evidence is an over-approximated reachable tube computed by the hybrid-system verification tool Verse from simulated trajectories, plus scenario testing with a photorealistic urban environment. The paper states directly that, within the range of conditions and constraints described across the evaluation scenarios, the autonomous landing system is safe and reliable.","pith_inferences":["Pith inference: the paper's own limitation note implies that the obstacle-avoidance guarantee depends on the curated spawn sampling for scenarios 3 and 5; re-running with the original spawn logic could make the reachable set falsely include the obstacle region, so the safety claim is best read as conditional on representative trajectory sampling.","Pith inference: a natural next experiment is to partition the initial-condition set and compute the union of reachable tubes per partition, a remedy the paper names but does not implement; this would test whether the curated sampling hides a real collision risk.","Pith inference: because the reachability analysis uses only 10 trajectories per scenario, the probabilistic accuracy of the over-approximation depends on that sample size; increasing trial counts would tighten the guarantee."],"forward_implications":["A safety claim for a vision-based landing stack can be obtained entirely in simulation, before any hardware flight test.","The same reachability pipeline transfers to new landing scenarios by changing the initial-condition set, obstacle layout, and perception setup.","Perception uncertainty in scenarios 4 and 5 does not push the reachable set outside the landing pad, so the system tolerates bounded detection error.","The formal result covers static intruder aircraft, not moving ones; dynamic-intruder scenarios are left to future work."],"supporting_citations":[{"why":"Supplies the Verse library used to model the hybrid system and compute over-approximated reachable sets.","marker":"[14]"},{"why":"Provides the DryVR simulation-based reachability algorithm that Verse implements for the over-approximation.","marker":"[31]"},{"why":"Provides the CARLA photorealistic urban simulation environment used for perception and scenario rendering.","marker":"[12]"},{"why":"Gives the MiniHawk-VTOL design and dynamic model that the simulation and landing system are built around.","marker":"[19]"},{"why":"Supplies the Gazebo physics simulator that computes the MiniHawk's pose in the integrated pipeline.","marker":"[42]"},{"why":"Extends the CARLA aerial-vehicle simulation approach and connects it to verifiable safe vertical landing, which this paper builds on.","marker":"[13]"}],"fun_headline_variants":["Formal proof secures air taxi landings in 5 scenarios","Reachability analysis verifies VTOL landing safety","Simulation and formal methods validate air taxi landings","Safety proven for vision-based VTOL landing in 5 cases"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The obstacle-avoidance safety result depends on the assumption that the curated subset of spawn trajectories used in scenarios 3 and 5 represents all behaviors the landing system could exhibit from the stated initial conditions.","fun_headline_variants_meta":{"raw":{"variants":["Formal proof secures air taxi landings in 5 scenarios","Reachability analysis verifies VTOL landing safety","Simulation and formal methods validate air taxi landings","Safety proven for vision-based VTOL landing in 5 cases"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000168,"raw_usage":{"total_tokens":1270,"prompt_tokens":967,"completion_tokens":303,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":583,"completion_tokens_details":{"reasoning_tokens":247}},"tokens_in":583,"tokens_out":303,"duration_ms":3669,"temperature":1.0,"reasoning_tokens":247,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T18:13:08.003231+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Using the paper's original spawn logic for scenario 3 or 5, sample initial conditions uniformly from the stated ranges and recompute the Verse reachtube; if any trajectory or the reachable set intersects the intruder's bounding box, the collision-avoidance claim is refuted.","supporting_citations":[{"cited_title":"Verse: A python library for reasoning about multi-agent hybrid system scenarios,","cited_arxiv_id":null,"evidence_quote":"Supplies the Verse library used to model the hybrid system and compute over-approximated reachable sets."},{"cited_title":"DryVR:Data-DrivenVerificationandCompositionalReasoningforAutomotive Systems,","cited_arxiv_id":null,"evidence_quote":"Provides the DryVR simulation-based reachability algorithm that Verse implements for the over-approximation."},{"cited_title":"CARLA: An open urban driving simulator,","cited_arxiv_id":null,"evidence_quote":"Provides the CARLA photorealistic urban simulation environment used for perception and scenario rendering."},{"cited_title":"The Minihawk-VTOL: Design, Modeling, and Experiments of a Rapidly-prototyped Tiltrotor UAV,","cited_arxiv_id":null,"evidence_quote":"Gives the MiniHawk-VTOL design and dynamic model that the simulation and landing system are built around."},{"cited_title":"Synergistic Perception and Control Simplex for Verifiable Safe Vertical Landing,","cited_arxiv_id":null,"evidence_quote":"Extends the CARLA aerial-vehicle simulation approach and connects it to verifiable safe vertical landing, which this paper builds on."}],"review_version":1}