{"id":"8dccae4b-c3a7-46b5-add1-a0f65b215aa8","arxiv_id":"2411.14168","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"A case study shows multi-machine Hybrid Event-B can model an autonomous incident response system and express a global safety invariant about hazard-data consistency.","lead":"This paper applies the multi-machine Hybrid Event-B formal method to a small autonomous incident response system, modeling a controller, two drones, and three responders as separate machines. It argues the formalism is well suited for specifying safety properties of autonomous systems, though the verification is by hand and not machine-checked.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Controller_Mch case study as written leaves sibling mode events enabled after LaunchDrone1/UpdateDrone1, violating Hybrid Event-B's requirement that each mode event disable all mode events.","rationale":"The reader's verdict is CONDITIONAL, and the main concern I identify does not move that verdict; rather, it sharpens the condition. The reader's weakest_assumption was the unmechanized, self-cited proof-obligation framework from prior work. That is a legitimate concern, but it is external to the case study. The concern I report is internal: even if the framework is entirely sound, the Controller_Mch given in Section 5 violates the framework's own mode/pliant alternation rule quoted in Section 2. The displayed events LaunchDrone1 and LaunchResp1 (and UpdateDrone1 with UpdateResp1) are simultaneously enabled over a shared time window and are not mutually exclusive, so after either fires the other remains enabled. Since mode events do not advance time, the subsequent pliant interval would have zero duration, which the semantics forbids, or the run aborts because both kinds of events are enabled at handover. This is not a disagreement with scientific consensus; it is a concrete, checkable inconsistency between the model and the semantics the paper itself describes. The paper's own limitation statements support the risk: Section 6 admits there is no tool support and that POs are checked by inspection, and Section 5 says liberties are taken with syntax. Those admissions make it plausible that a handover PO was overlooked. The global invariant IncidentResponse_GI is the paper's headline safety property, and it is meaningful only if the project can execute; the stated model cannot. The concern is repairable: by partitioning the launch/update windows into disjoint sub-intervals, or by adding a controller phase variable that forces the events to be mutually exclusive, the model could satisfy the alternation requirement. A repair of this kind should be a condition of acceptance. Therefore the verdict should remain CONDITIONAL, with the condition explicitly including a corrected and, ideally, mechanically checked mode/pliant handover PO for Controller_Mch.","tokens_in":16322,"tokens_out":10416,"duration_ms":95814,"concrete_test":"Formalize Controller_Mch's guards and updates and check the mode-event-disables-all-mode-events PO at two instants: (a) t=0.05, mode=DISPATCH, drones2comd={1,2}, resps2comd={1,2,3}; fire LaunchDrone1 and recompute the enabled controller mode events. (b) t=12.06, mode=UPDATEHAZ, cyclestart=12, drones2comd={1,2}, resps2comd={1,2,3}; fire UpdateDrone1 and recompute the enabled set. If any sibling event (LaunchResp1 in (a); UpdateResp1 or UpdateDrone2 in (b)) remains enabled, the PO fails, confirming the model violates Section 2's alternation requirement. This check can be done by hand or with a small ProB-like enumerator over the finite mode-state components.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Granting the soundness of the multi-machine Hybrid Event-B framework, the presented Controller_Mch does not satisfy the framework's own well-formedness condition stated in Section 2: 'Each mode event execution must enable at least one pliant event and disable all mode events.' In the DISPATCH phase, LaunchDrone1 has guard mode=DISPATCH ∧ 1∈drones2comd ∧ t<δ, and LaunchResp1 has guard mode=DISPATCH ∧ 1∈resps2comd ∧ t<δ. Both are enabled simultaneously at, say, t=0.05. If LaunchDrone1 fires, LaunchResp1's guard remains true because resps2comd is unchanged and t<δ still holds. The same problem occurs in the UPDATEHAZ phase: after UpdateDrone1 fires, UpdateResp1 remains enabled since 1∈resps2comd and the same time-window guard still holds. Because mode events are instantaneous, the next pliant interval would have to be empty, contradicting the non-empty interval semantics described in Section 2; equivalently, at the mode→pliant handover both mode and pliant events are enabled, so the run aborts. Section 6's claim that the POs are 'rather trivial' and can be checked 'by inspection' misses this failing mode/pliant handover PO. The global invariant IncidentResponse_GI is therefore not established for the model as given; the paper's central demonstration rests on a project that, as written, has no valid executions beyond the first mode event.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper argues that multi-machine Hybrid Event-B, an extension of Event-B with real time and continuous pliant events, is suitable for specifying and verifying safety properties of autonomous systems. It surveys the formalism's syntax, refinement, and multi-machine composition, drawing on the author's prior work for the technical semantics and proof obligations. The paper then presents a case study: a controller, two drones, and three responders cooperate to manage a hazardous scenario. The project's global invariant IncidentResponse_GI asserts that outside the delta-wide update windows following scheduled hazard changes, all agents agree on the hazard set. Section 6 claims that the vast majority of proof obligations are trivial and can be checked by inspection, while acknowledging that no tool support exists for Hybrid Event-B.","tokens_in":16613,"tokens_out":6545,"duration_ms":60037,"significance":"If the case study were fully validated, the paper would provide a useful, compact demonstration of how a multi-machine hybrid formalism can express a system-level safety property (distributed agreement on hazard state) and support modular scenario changes by editing one machine and one context. The paper is honest about the lack of tool support and the hand-checked nature of the verification. However, the central demonstration is undermined by an apparent violation of the formalism's own mode/pliant handover condition in the controller machine, and by the absence of any proof sketch for the only global safety property. The claimed suitability of multi-machine Hybrid Event-B is therefore not established as written, although the problems are local and potentially fixable within the scope of the paper.","major_comments":[{"comment":"The controller machine violates the mode/pliant handover condition stated in Section 2. In the DISPATCH phase, LaunchDrone1 has guard `mode = DISPATCH \\land 1 \\in drones2comd \\land t < \\delta` and LaunchResp1 has guard `mode = DISPATCH \\land 1 \\in resps2comd \\land t < \\delta`; both are enabled at the same instant (e.g., t = 0.05 after ActivateController), and firing LaunchDrone1 does not change `mode` or `resps2comd`, so LaunchResp1 remains enabled. The same issue occurs with UpdateDrone1 and UpdateResp1 in the UPDATEHAZ phase. Since Section 2 requires that each mode event 'disable all mode events' and that at mode-to-pliant handover all enabled events be of one kind or the run aborts, a run cannot proceed past the first launch or update under the stated semantics. Section 6's assertion that the handover POs are 'rather trivial' and can be checked 'by inspection' is therefore not credible for this model; the model must either add mutual exclusion guards that make the sibling launch/update events mutually disable one another, or restructure the phases so that each mode event leaves no other mode event enabled.","section":"Section 5, Controller_Mch; Section 2"},{"comment":"The global invariant IncidentResponse_GI is the paper's central safety property, but no derivation or proof obligation is given for it. The paper states that the individual conjuncts such as `hazards = drhazards` were 'not included as invariants of the relevant machines above' and that global invariants are 'intended to be derivable' from the other invariants; it does not show how `hazards = ctrhazards = drhazards = resp1hazards = resp2hazards = resp3hazards` follows from the declared machine and interface invariants, the mode guards, and the update schedule. Because there is no tool support and the POs are unmechanized, the claim that multi-machine Hybrid Event-B is suitable for formalising this safety property is not demonstrated; the paper needs at least a detailed hand-proof sketch of IncidentResponse_GI, including the treatment of the `INITSCHED` update windows and the intervals of length delta.","section":"Section 6, IncidentResponse_GI"},{"comment":"The safety demonstration depends on the unspecified functions `calcCentAvoidTraj` and `calcTraj`, which are assumed to exist and produce safe trajectories, but whose contracts are never stated. The paper also does not rule out a post-`Update` situation in which the newly calculated trajectory's first point equals the current position, which would leave the `Waypoint` mode event enabled immediately after the `Update` mode event; this would again violate the handover requirement. Either an explicit assumption excluding that case, or a proof that `Update` disables `Waypoint`, is needed for the handover PO to hold. Without these details, the case study cannot be said to verify the system's safety, and Section 6's claim that the POs are 'trivial' is not justified.","section":"Section 5, Drone_Mch/Responder_Mch; Section 6"}],"minor_comments":[{"comment":"The word 'behviours' is a typo for 'behaviours'.","section":"Section 2"},{"comment":"The SwitchOff event's guard reads `respx = respy = respz = 0`, but `respz` is not a declared variable in Responder_Mch; it should presumably be `respx = respy = 0`.","section":"Section 5, Responder_Mch"},{"comment":"Many events are declared `STATUS asynch`, but Section 2 introduces mode events with `STATUS ordinary` and does not define `asynch`; the distinction (presumably asynchronous versus synchronised mode events) should be explained before first use.","section":"Section 5, Controller_Mch"},{"comment":"The set expression `S (ii \\bullet ii \\in dom(INITSCHED) | [INITSCHED(ii) . . .INITSCHED(ii)+\\delta])` is not defined; use a standard union/set comprehension and clarify whether the intervals are closed, open, or half-open so that they match the guards' strict inequalities.","section":"Section 6, IncidentResponse_GI"},{"comment":"The line `SYNCH DeActivateResponder1 ... Responder1_Mch.DeActivate1)` contains an unmatched closing parenthesis; remove it.","section":"Project file"},{"comment":"LaunchDrone1 assigns `drhazards := hazards`, but `drhazards` is not declared in Controller_Mch's variable list; it belongs to ControllerDrones_IF. The paper should clarify the read/write scope of CONNECTS variables so that the controller's ability to update interface variables is explicit.","section":"Section 5, LaunchDrone1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript relies almost entirely on the author's own prior publications for the semantics and proof obligations, and the case study is not machine-checked. The specific technical problem in major comment 1 is a concrete violation of the formalism's own handover condition and should be decisive for revision; it is not merely a disagreement about the framework's general viability. For a journal submission, the editor may also wish to require a substantial proof sketch of IncidentResponse_GI and an explicit statement of the assumptions on trajectory functions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is that the case study does not satisfy the framework's own mode/pliant handover requirement. After ActivateController sets mode to DISPATCH, LaunchDrone1, LaunchDrone2, LaunchResp1, LaunchResp2, and LaunchResp3 are all enabled. If any fires, the others remain enabled because their guards depend only on mode, membership sets, and the global time window. The paper's Section 2 semantics requires each mode event to disable all mode events; otherwise at the mode→pliant handover both kinds are enabled and the run aborts. The same problem appears in the UPDATEHAZ phase between UpdateDrone1 and UpdateResp1. So the model as written has no valid executions past the first mode event, and the global invariant IncidentResponse_GI is not established.\n\nWhat is genuinely useful here is the survey of multi-machine Hybrid Event-B and the architectural ideas: interfaces for shared variables, SYNCH for synchronized mode events, and a global invariant for system-level safety. The incident response scenario is a sensible test case, and the author is transparent about the lack of tool support.\n\nThe soft spots are not minor. Section 6 claims the proof obligations are 'rather trivial' and can be discharged 'by inspection,' but the handover PO is false. Many model details are suppressed (trajectory functions, instantiations), and the semantics is cited from the author's previous papers rather than independently validated. That said, the paper is clearly written and the survey is competent. The flaw is in the case study, not in the exposition.\n\nI would send this to peer review rather than desk reject: the error is exactly the kind a careful referee should catch, and fixing it (e.g., by partitioning the launch window or adding a phase variable) could make the case study genuinely supportive. As written, though, it is a conditional accept at best. For a workshop venue, I would want a revised version with the handover POs actually discharged.","headline":"The case study violates the paper's own mode/pliant handover condition, so the central suitability claim is not supported as written, though the survey of multi-machine Hybrid Event-B is competent.","tokens_in":17168,"tokens_out":7034,"would_cite":false,"duration_ms":59742,"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":"Multi-machine Hybrid Event-B proves a shared safety invariant for six autonomous agents","keywords":["Hybrid Event-B","multi-machine","autonomous systems","safety properties","formal verification","incident response","cyber-physical systems","refinement"],"falsifier":"Run the incident response model in a faithful simulator with the stated constants (δ=0.1, Δ=1, INITSCHED=⟨12,30,55⟩, DURATION=79.7) and search for a time outside every [INITSCHED(ii), INITSCHED(ii)+δ] window at which the controller's hazard set differs from any drone's or responder's; finding one would refute the invariant IncidentResponse_GI. Alternatively, mechanise the Hybrid Event-B proof obligations and exhibit a proof obligation from this model that cannot be discharged.","tokens_in":16055,"feed_emoji":"🤖","tokens_out":3849,"duration_ms":34715,"temperature":0.7,"pith_summary":"This paper argues that multi-machine Hybrid Event-B, an extension of the Event-B formal method that mixes discrete state changes with continuous time evolution, is well suited to specifying and verifying safety properties of autonomous systems. To support that claim, it models an incident response system with six cooperating but largely independent agents: a controller, two drones, and three responders. The centrepiece is a global safety invariant, IncidentResponse_GI, stating that outside the brief time windows in which hazard information is refreshed, all agents agree on the current set of hazards. The paper deliberately keeps the model simple so that the proof obligations are mostly trivial, and concludes that the formalism captures the intermittent-communication, multi-locus-of-control structure typical of autonomous systems.","feed_headline":"Six cooperating agents, one global safety invariant","feed_subtitle":"A controller, two drones, and three responders must hold the same hazard map; the paper models and verifies that.","key_machinery":"The load-bearing mechanism is the multi-machine Hybrid Event-B formalism: a conservative extension of Event-B in which discrete 'mode' events are interleaved with continuous 'pliant' events, and multiple machines interact through INTERFACE constructs, type-II invariants of the form U(u) ⇒ V(v), and SYNCH clauses that force specified mode events across machines to execute together. This combination lets a global property like incident-wide hazard agreement be decomposed into per-agent invariants plus synchronisation structure, with the global invariant IncidentResponse_GI closing the system-level argument.","core_discovery":"The central discovery, on the paper's own terms, is that multi-machine Hybrid Event-B can express a genuine system-level safety property that depends on the cooperation of all parts. In the incident response case study, each agent is its own machine, interfaces mediate shared hazard data and positions, synchronised mode events coordinate launch, update, and recall, and pliant events govern continuous navigation. The global invariant IncidentResponse_GI states that outside the δ-length update windows following the scheduled times in INITSCHED, the controller, both drones, and all three responders hold identical hazard sets. The paper's contribution is the demonstration that this architecture, with its type-I and type-II invariants and its global invariant construct, makes such a property natural to state and plausibly provable.","pith_inferences":["The same decomposition—per-agent machines plus synchronized update windows—could be applied to consensus-style safety properties in other distributed cyber-physical systems, where the key question is how long agents may hold stale views of shared state.","The δ-window structure suggests a quantitative safety metric: the maximum duration over which agents' views may diverge is bounded by the update interval; a testable extension would instrument a simulation to measure whether that bound is respected.","The global invariant is stated but not proved in the paper; a reader wanting to trust the safety property would need to see the derivation from the machine invariants, which the paper leaves as intended later-stage work."],"forward_implications":["If the formalism is as suitable as claimed, autonomous systems with multiple loci of control can be given structured safety arguments without flattening them into one monolithic transition system.","The incident response pattern—intermittent synchronized updates plus independent continuous behaviour—generalizes to other multi-agent scenarios such as search and rescue or warehouse fleets.","The global-invariant construct offers a dedicated place to state system-level safety properties that no single component can prove alone, which is exactly the kind of property certification regimes want from autonomous systems.","Because the model is deliberately simple, the proof obligations reduce to feasibility, invariant preservation, and handover checks that can be inspected by hand, suggesting the approach is tractable before tool support exists."],"supporting_citations":[{"why":"Core Hybrid Event-B I establishes the single-machine operational semantics and proof obligations for mode/pliant alternation that the case study builds on.","marker":"[6]"},{"why":"Core Hybrid Event-B II develops the multi-machine framework—interfaces, SYNCH, decomposition—that the incident response model depends on.","marker":"[7]"},{"why":"Core Hybrid Event-B III supplies the reasoning framework whose proof obligations would verify the model and its global invariant.","marker":"[4]"}],"fun_headline_variants":["Six agents, one shared hazard map, formally verified","Global safety invariant proven for multi-agent autonomy","Hybrid Event-B checks cooperative drone safety","Multi-machine design guarantees shared hazard view","One invariant, six agents: safety proven"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole safety argument rests on the proof-obligation framework of Hybrid Event-B from the author's earlier papers, which is cited rather than re-derived here and has no implemented tool support; a flaw or gap in those obligations would invalidate the claimed global invariant.","fun_headline_variants_meta":{"raw":{"variants":["Six agents, one shared hazard map, formally verified","Global safety invariant proven for multi-agent autonomy","Hybrid Event-B checks cooperative drone safety","Multi-machine design guarantees shared hazard view","One invariant, six agents: safety proven"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000251,"raw_usage":{"total_tokens":1502,"prompt_tokens":833,"completion_tokens":669,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":449,"completion_tokens_details":{"reasoning_tokens":602}},"tokens_in":449,"tokens_out":669,"duration_ms":6259,"temperature":1.0,"reasoning_tokens":602,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:27:17.707421+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the incident response model in a faithful simulator with the stated constants (δ=0.1, Δ=1, INITSCHED=⟨12,30,55⟩, DURATION=79.7) and search for a time outside every [INITSCHED(ii), INITSCHED(ii)+δ] window at which the controller's hazard set differs from any drone's or responder's; finding one would refute the invariant IncidentResponse_GI. Alternatively, mechanise the Hybrid Event-B proof obligations and exhibit a proof obligation from this model that cannot be discharged.","supporting_citations":[{"cited_title":"Banach, M","cited_arxiv_id":null,"evidence_quote":"Core Hybrid Event-B I establishes the single-machine operational semantics and proof obligations for mode/pliant alternation that the case study builds on."},{"cited_title":"Banach, M","cited_arxiv_id":null,"evidence_quote":"Core Hybrid Event-B II develops the multi-machine framework—interfaces, SYNCH, decomposition—that the incident response model depends on."}],"review_version":1}