{"id":"1f6bef47-c66c-4583-80ca-268481333eaf","arxiv_id":"2607.28679","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"First MIP and SMT encodings that synthesize multi-agent trajectories satisfying STL-GO specifications with time-varying interaction graphs, with soundness proofs and benchmarks.","lead":"This paper gives two automated ways to plan multi-agent paths that satisfy STL-GO, a logic for specifying where agents should be, when they should be there, and how they must stay connected through sensing, communication, and task graphs. The methods come with soundness proofs and are tested on drone search-and-rescue and grid-world benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"MIP Big-M separation margins make the MIP planner incomplete at boundaries; Theorem 7 omits the caveat, but this is a completeness/presentation issue, not a soundness flaw.","rationale":"The reader identifies the separation-margin assumption as the weakest point, and I agree that the paper needs to state it more carefully. However, the concern is not a soundness failure of Theorem 7: because the dead-zone values make the relevant Big-M constraints unsatisfiable, any feasible MIP assignment is automatically outside those zones, so the implication 'feasible => satisfies' remains true. The real issue is completeness: the MIP encoding can reject valid specifications whose satisfying trajectories use boundary-adjacent values, while the SMT encoding accepts them. This matters because Section III defines the planning problem without any robustness margin, so a user could reasonably expect the MIP planner to solve the stated problem. The paper's Limitation section only mentions determinism, not this dead-zone incompleteness. Thus the central soundness claim stands, but the MIP contribution is narrower than the presentation suggests. The reader's conditional verdict remains appropriate: the paper should restate the separation hypothesis in Theorem 7, add an explicit completeness caveat, and ideally release the benchmark/code for reproducibility. I would not reject or accept outright; the core MIP/SMT encodings and soundness arguments are credible and the SMT side is exact, so a conditional acceptance with those revisions is the right call.","tokens_in":24231,"tokens_out":23655,"duration_ms":224951,"concrete_test":"Take a one-agent, one-step instance with affine predicate mu(x):= x >= 0 and specification phi = F_{[0,1]} not mu (or simply evaluate not mu at t=0), and fix x_0 = -epsilon/2, inside the dead zone. The SMT/LRA encoding is satisfiable (mu is false, so not mu is true), while the MIP Big-M constraints for mu with z_mu=0 impose x <= -epsilon, violated, and with z_mu=1 impose x >= 0, violated; Gurobi should report infeasible. If this happens, the MIP encoding is incomplete at boundary values, confirming that Theorem 7 and the Limitations section must state the separation assumption and the resulting completeness caveat.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing concern is the gap between the stated planning problem (Section III, no robustness margin) and the MIP encoding's Big-M separation margins. Section IV-A and Appendix C encode atomic predicates with `a^T x - b >= -M(1-z)` and `<= -epsilon + M z`, and Eq. (5) uses `delta_w` margins for edge weights, with Appendix A explicitly assuming feasible predicate values avoid `(-epsilon,0)` and edge weights avoid `(w_min-delta_w,w_min) U (w_max,w_max+delta_w)`. For values inside a dead zone there is no assignment to the binary indicator, so the MIP becomes infeasible even when a perfectly valid STL-GO trajectory exists; the SMT encoding (Section V) is exact and will accept it. Thus the MIP encoding is sound (any feasible MIP solution maps to a satisfying trajectory, and no feasible solution can have a dead-zone value) but incomplete with respect to the problem statement. Theorem 7 states soundness without this caveat, and the Limitations section does not mention that MIP may reject valid instances. The abstract's 'soundness guarantees' is accurate for returned plans, but the paper's presentation invites the stronger reading that the MIP encoding solves the planning problem as defined.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper addresses the problem of synthesizing bounded-horizon open-loop plans for a multi-agent system subject to STL-GO specifications, a logic that extends STL with graph operators over time-varying interaction graphs. The authors present two encodings: a mixed-integer program (MIP) and a quantifier-free SMT instance in LRA+LIA. They prove soundness theorems (Thm. 7 and Thm. 9) by structural induction, showing that any feasible MIP/SMT solution yields a trajectory satisfying the STL-GO formula at the initial state. They implement a unified interface, evaluate both encodings on a multi-UAV search-and-rescue benchmark with ablations over team size and graph complexity, and compare STL-GO with HyperLTL on a grid-world benchmark, demonstrating a significant constraint blow-up for HyperLTL. Appendices contain full proofs and encoding details.","tokens_in":24616,"tokens_out":15003,"duration_ms":124765,"significance":"If correct, this is the first sound planner for STL-GO, a formalism that can express spatio-temporal and topological constraints over dynamic interaction graphs. The SMT encoding is exact and provides a clean completeness guarantee; the MIP encoding enables objective-driven planning. The paper ships detailed structural-induction proofs and a concrete HyperLTL comparison, both of which are valuable. The main caveat is that the MIP encoding is sound but not complete with respect to the stated planning problem unless a separation-margin condition is imposed; this does not invalidate the soundness direction but must be made explicit. Overall, this is a substantial contribution to formal multi-agent synthesis.","major_comments":[{"comment":"Theorem 7 states feasibility of the MIP implies satisfaction. The proof in Appendix A, however, relies on separation hypotheses absent from the theorem and from Section III: feasible atomic-predicate values avoid (−ε,0), and feasible edge weights avoid (w_min−δ_w,w_min)∪(w_max,w_max+δ_w). These hypotheses are needed for the Big-M constraints of Eq. (5)/Appendix C to admit a binary assignment. Without them, a satisfying trajectory may place a predicate value or edge weight in a dead zone, making the MIP infeasible (e.g., a communication-range constraint at the boundary). The SMT encoding of Section V handles these cases exactly. The MIP encoding is therefore sound but incomplete. Please add the separation condition as an explicit assumption in Section III and Theorem 7, or state in the Limitations that the MIP planner is sound but not complete and that SMT is the exact method. As written,","section":"Theorem 7 / Appendix A"},{"comment":"The definition of MIP-encodable graph constructors states that edge-existence predicates admit 'an exact mixed-integer representation.' This is only achievable if the affine comparisons involved are separated from the boundary by the margins ε and δ_w. Since these margins are not part of the definition, the term 'exact' overstates the situation. Please make the separation condition explicit in the definition, or rephrase as 'exact under a δ/ε-separation condition.' This clarifies that the completeness of the MIP encoding is conditional.","section":"Section IV-A"}],"minor_comments":[{"comment":"The experimental setup introduces contingency planning with scenario-indexed sequences and non-anticipation constraints, but the formal problem in Section III is open-loop. Please clarify that the soundness theorems apply to each open-loop branch of the contingency tree, and that the scenario-based construction is an additional step not covered by the formal statements.","section":"Section VI"},{"comment":"The Limitations section does not mention that the MIP encoding may be infeasible for valid instances due to the Big-M separation margins. A short remark would prevent users from misinterpreting an infeasible MIP as a proof of non-existence of a plan.","section":"Limitations"},{"comment":"The phrase 'with soundness guarantees' is technically accurate but could be clarified to say 'soundness guarantees for both encodings, with the MIP encoding's completeness conditioned on separation margins.'","section":"Abstract"},{"comment":"The definitions of φ_LL^ℓ and φ_LR^ℓ are identical and the role-partitioned restrictions are suppressed; a reader cannot tell how the locator/rescuer distinction enters. Please state the restricted target sets.","section":"Example 1 (continued)"}],"recommendation":"major_revision","confidential_remarks":"This is a well-executed paper with clear soundness proofs and useful experiments. The only substantive issue is the MIP separation-margin incompleteness, which should be resolved before publication. I recommend major revision. The SMT encoding is the exact method and should be clearly positioned as such."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about arXiv:2607.28679. First, the core contribution is new and credible: nobody has synthesized plans for STL-GO before, and the graph-operator encodings—time-varying weighted graphs, cardinality predicates, type-quantifiers—are real technical work, not a routine STL wrapper. Second, the MIP encoding has a completeness gap at boundary values that the paper does not state where it should. I agree with the stress-test: Theorem 7 says feasibility implies satisfaction, but the proof in Appendix A and the constraints in Section IV-A assume feasible edge weights avoid the δ_w margins and predicate values avoid (−ε, 0). So the MIP can be infeasible for perfectly valid instances. The SMT encoding is exact and side-steps this. That makes the issue a completeness/presentation flaw, not a soundness one. The abstract's 'soundness guarantees' is technically defensible, but the paper invites the stronger reading that the MIP solves the planning problem as defined in Section III. That needs to be restated in Theorem 7 and in the Limitations section.\n\nWhat the paper does well: the structural induction proofs in Appendices A and B are the right shape, and they cover the graph operators carefully. The SMT encoding is clean and exact. The experiments go beyond toy examples: the SwarmLab search-and-rescue setup with contingency branches and the HypRL grid-world comparison give a fair picture of where STL-GO pays off relative to HyperLTL. The ablation over graph complexity is informative, and the numbers match the expected trend—SMT faster, MIP needed for objectives. The paper also honestly compares against its own prior monitoring work and does not oversell the relationship. No circularity issue: [8] is used for semantics, not as evidence for the encoding.\n\nSoft spots, in proportion: the MIP boundary gap is the main one, and it is significant enough that the theorem statement and abstract need revision. The paper also does not release code or benchmarks, which matters for a paper whose experiments are the main evidence; I'd want that before publication. Table I shows MIP hitting time limits even on the smallest configurations with objectives; that is not a flaw, but it means the 'scalability' claims for MIP are weaker than the table's raw times suggest. Minor: the HyperLTL comparison is reasonable but the reification details in Appendix E are dense and could be summarized more cleanly in the main text.\n\nThis paper should get a serious referee. It opens a new problem (STL-GO planning) and gives two usable encodings with proofs. My recommendation: invite revision, ask the authors to restate the separation-margin hypothesis in Theorem 7, note the incompleteness in Limitations, and release code/benchmarks. The work is solid enough that this should be fixable without redoing the central results.","headline":"First sound MIP/SMT encodings for STL-GO planning with real graph-operator content; the MIP incompleteness at separation margins is a presentation-level gap, not a soundness flaw, and should be fixed before acceptance.","tokens_in":25056,"tokens_out":1326,"would_cite":true,"duration_ms":15933,"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":"Two solver encodings turn STL-GO specs into guaranteed plans","keywords":["STL-GO","multi-agent planning","signal temporal logic","graph operators","mixed-integer programming","satisfiability modulo theory","time-varying interaction graphs","formal synthesis"],"falsifier":"Take a two-agent instance where the only feasible trajectory has one agent exactly at the communication-range boundary (edge weight exactly equal to w_min). Run the MIP encoding from the paper; if it returns infeasible while a feasible trajectory exists, the soundness theorem's implicit separation-margin assumption is violated. Alternatively, brute-force enumerate all trajectories for a small grid instance and compare each MIP/SMT solution against direct evaluation of the STL-GO semantics.","tokens_in":24159,"feed_emoji":"🤖","tokens_out":4495,"duration_ms":39026,"temperature":0.7,"pith_summary":"This paper tackles the open problem of automatically planning multi-agent trajectories that satisfy STL-GO, a logic that combines spatio-temporal requirements with constraints over time-varying interaction graphs such as sensing, communication, and task topologies. Prior work used STL-GO only for runtime monitoring, given trajectories produced by some other planner. The authors show that when agent dynamics are affine and graph-constructor functions are piecewise affine with exact Boolean encodings, a bounded-horizon STL-GO planning problem can be compiled into either a mixed-integer program or an SMT instance. Their soundness theorems state that any feasible MIP solution or satisfiable SMT assignment yields a trajectory that genuinely satisfies the specification. Experiments on a search-and-rescue benchmark with multiple dynamic graphs demonstrate both encodings, and a comparison with HyperLTL shows STL-GO's graph operators avoid the quadratic constraint blow-up of reified agent quantifiers.","feed_headline":"Two solver encodings turn STL-GO specs into guaranteed plans","feed_subtitle":"Dynamic sensing, communication, and task graphs become solver constraints with provable correctness.","key_machinery":"The graph-operator encodings: for each graph type, per-agent eligibility variables mark which neighbors have an edge with weight in the specified interval and satisfy the inner subformula; a count variable tallies them; cardinality constraints enforce the required range; and a final disjunction or conjunction implements existential or universal quantification over graph types. In the MIP encoding this is done with binary Big-M constraints; in the SMT encoding with LRA biconditionals and ite-counting. This machinery converts the logic's neighborhood-cardinality semantics into solver-level arithmetic, which is what makes multi-graph, time-varying topology planning tractable.","core_discovery":"The central discovery is that planning under STL-GO reduces to finite constraint solving: each agent-local subformula's truth at each time step becomes a Boolean or binary variable, and the In/Out graph operators—which count neighbors satisfying a subformula with edge weights in an interval, over existential or universal quantification of graph types—are encoded exactly. The MIP encoding uses Big-M constraints with separation margins for edge-weight and predicate thresholds; the SMT encoding uses exact LRA+LIA biconditionals and integer ite-counting, avoiding those margins. Structural induction proves that the encoding variables mirror the STL-GO semantics exactly, so feasibility or satisfia","pith_inferences":["The separation-margin assumption in the MIP encoding is a practical robustness gap: missions that legitimately require an agent to sit exactly at a communication or sensing boundary could be wrongly declared infeasible; the SMT encoding does not have this weakness and could serve as an exact fallback or validator.","The same graph-operator machinery could be applied to other relational planning constraints—collision avoidance, formation maintenance, or bandwidth limits—by expressing them as interaction graphs, giving a uniform way to compile them into solvers.","The pointwise evaluation of agent quantifiers suggests a natural decomposition path toward decentralized planning: local formulas compile locally, with only graph-cardinality terms coupling agents.","One could test robustness quantitatively by perturbing trajectories near graph boundaries and checking whether MIP feasibility flips while SMT satisfiability does not; this would quantify the practical cost of Big-M margins."],"forward_implications":["STL-GO specifications become usable for synthesis, not just monitoring, so mission requirements over dynamic communication and task topologies can be guaranteed at plan time.","MIP encodings support objective functions, enabling optimal trajectory synthesis under STL-GO constraints, not merely feasible ones.","The SMT encoding is empirically more compact and faster, suggesting it scales to larger teams and more interaction graphs, while MIP remains the choice for cost-optimized plans.","Because the encoding is modular in graph constructors, any new interaction modality expressible as a piecewise-affine, Boolean-comparable function can be added without changing the core machinery.","The scenario-tree contingency planning construction yields plans that react to which emergencies activate, with branching only at observable distinctions."],"fun_headline_variants":["STL-GO planning made exact with MIP and SMT encodings","Two provable encodings for STL-GO multi-agent planning","Exact MIP and SMT solvers for STL-GO path planning","Reduce STL-GO specs to MIP or SMT for guaranteed plans","STL-GO planning solved exactly via two solver encodings"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The MIP soundness proof assumes that no feasible trajectory places an edge weight or atomic-predicate value exactly on the thresholds used by the Big-M encoding, so a valid plan requiring an agent to sit precisely at a communication-range boundary could make the MIP infeasible.","fun_headline_variants_meta":{"raw":{"variants":["STL-GO planning made exact with MIP and SMT encodings","Two provable encodings for STL-GO multi-agent planning","Exact MIP and SMT solvers for STL-GO path planning","Reduce STL-GO specs to MIP or SMT for guaranteed plans","STL-GO planning solved exactly via two solver encodings"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000438,"raw_usage":{"total_tokens":2091,"prompt_tokens":799,"completion_tokens":1292,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":543,"completion_tokens_details":{"reasoning_tokens":1206}},"tokens_in":543,"tokens_out":1292,"duration_ms":8446,"temperature":1.0,"reasoning_tokens":1206,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T00:42:04.507013+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a two-agent instance where the only feasible trajectory has one agent exactly at the communication-range boundary (edge weight exactly equal to w_min). Run the MIP encoding from the paper; if it returns infeasible while a feasible trajectory exists, the soundness theorem's implicit separation-margin assumption is violated. Alternatively, brute-force enumerate all trajectories for a small grid instance and compare each MIP/SMT solution against direct evaluation of the STL-GO semantics.","supporting_citations":[],"review_version":1}