Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO

# Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO
Source: [https://arxiv.org/html/2607.28679](https://arxiv.org/html/2607.28679)
Sheryl Paul1,∗, Vidisha Kudalkar1,∗, Anand Balakrishnan2, Lars Lindemann3, Alberto Speranzon4, Jyotirmoy V\. Deshmukh1

###### Abstract

Multi\-agent planning problems arise in a variety of engineering applications, such as multi\-robot wildfire fighting and unmanned aerial inspection in factories\. A particular challenge is the existence of spatio\-temporal \(i\.e\., when and/or where an agent should do what\) and topological constraints \(i\.e\., how agents should interact\), as typically formalized via the notion of graphs\. Over the last years, various frameworks have been proposed that can capture such constraints via spatio\-temporal logics\. We focus here on*spatio\-temporal logic with graph operators \(STL\-GO\)*, a recent formalism that supports reasoning about multiple agents and their topologies, such as sensing, communication, and task topologies\. In this paper, we consider the problem of planning multi\-agent paths that satisfy constraints written in STL\-GO\. This problem is particularly challenging due to the need of encoding multiple, potentially time\-varying graphs via the graph operators inherent to STL\-GO\. We present two encodings of this problem, one based on mixed\-integer programming \(MIP\) and another based on satisfiability modulo theory \(SMT\), with soundness guarantees\. We provide a unified interface for specifying agent constraints, their graph topologies, and the STL\-GO specification, enabling seamless use of both methods and facilitating direct comparison between them\. We evaluate both encodings on a multi\-UAV search\-and\-rescue benchmark, ablating over team size and graph complexity, highlighting the expressiveness of the proposed encodings under dynamic multi\-graph interactions\.

## IIntroduction

Classical temporal logic specifications, such as LTL or STL, are well suited for expressing time\-based properties of individual system trajectories\. However, in multi\-agent systems \(MAS\), desired mission behavior may depend not only on when events occur but also on inter\-agent communication, spatial relationships, and task dependencies\. Furthermore, mission objectives may need to reason about how these inter\-agent relations evolve over time\. A useful model is thus to treat a multi\-agent system as a collection of directed or undirected graphs, where nodes represent agents with dynamic behavior and time\-varying edges across multiple graphs capture distinct kinds of inter\-agent relationships\.

![Refer to caption](https://arxiv.org/html/2607.28679v1/x1.png)Figure 1:Motivation scenario: a heterogeneous multi\-agent system coordinating wildfire response over a satellite terrain map\.Yellow dronesare*locator*agents that patrol the region to monitor fire spread and detect emergencies \(marked by red circles\)\. Thepurple droneis the*rescuer*agent tasked with reaching survivors and transporting them to the rescue center \(white tent\)\.Orange arrowsindicate*sensing*: a locator drone detects an emergency site\.Blue arrowsrepresent*inter\-agent communication*links through which locators share situational awareness\.Red arrowsdenote*task assignment*: the detected emergency is assigned to the rescuer\.Green arrowstrace the*rescue path*: the rescuer navigates first to the emergency location, then to the rescue center\. Our goal is to synthesize agent trajectories that satisfy a*spatio\-temporal reachability specification*encoding these coordination requirements with formal correctness guarantees\.Recent work has focused on spatio\-temporal logic formalisms such as SSTL\[bortolussi2014specifying,nenzi2015qualitative\], SaSTL\[ma2020sastl\], SpaTeL\[haghighi2015spatel\], STREL\[STREL,STRELDynamicNetworks\], Census STL\[xu2016census\]and STL\-GO\[stlgo\]\. Among these formalisms, STL\-GO allows specifying multi\-agent behaviors over multiple inter\-agent relational structures: it supports simultaneous quantification over distinct time\-varying agent relationships\. As a motivational example \(Fig\.[1](https://arxiv.org/html/2607.28679#S1.F1)\), consider a wildfire\-response setting in which: “*Every emergency situation must be sensed by a locator agent within bounded time; upon sensing, the locator must communicate the emergency to connected agents and upon contact with a rescuer, assign that rescuer to the emergency\. The rescuer must then reach the emergency location and perform the rescue action and return to a safe location\.*” This specification reasons over three distinct topologies at once \(sensing, communication, and task\-assignment\), and also constrains the number of neighbors satisfying a desired property\. Such types of specifications are a first step to formalizing the behavior of practical multi\-agent systems such as those used for search\-and\-rescue, environmental monitoring under limited communication, and distributed sensing in uncertain terrains\.

STREL provides path\-based reachability and escape operators over a chosen dynamic weighted spatial model, while Census STL counts agents within a population; neither directly combines STL\-GO’s typed neighborhood\-cardinality operators with explicit quantification over collections of interaction graphs\. Hyperproperty logics such as HyperLTL\[hsu2025hyprl,wang2020hyperproperties,finkbeiner2023logics\]can also express relational properties across agents, but require lifting agent\-level quantifiers outside any temporal operator\. Consequently, temporal changes in agent sets and interaction relations must be represented through explicit propositions and finite\-domain expansion\. We use HyperLTL as a relational specification comparison grounded in prior planning work, rather than as a general\-purpose baseline for multi\-agent systems in Section[VII](https://arxiv.org/html/2607.28679#S7)\.

In prior work\[stlgo\], the authors focus on runtime monitoring of STL\-GO specifications, assuming that agents’ spatio\-temporal behaviors are decided by some given planner; how such plans can be synthesized is not addressed\. The main problem we consider in this paper is open\-loop, centralized, bounded\-horizon planning for a multi\-agent system subject to STL\-GO specifications where the agent and environment dynamics are deterministic and known\. We focus on this case as a foundational baseline: a tractable centralized encoding is a prerequisite for decentralized extensions and, to our knowledge, no such encoding exists for STL\-GO\.

There has been substantial work on planning multi\-agent systems subject to temporal logic specifications such as LTL\[OnlineMultiRobotLTL,SMTMultiRobotSafeLTL\], STL\[FormalMethodsMultiAgent,MultiAgentSTLWaypoints\], ATL\[ATL\]and CaTL\[CaTLPlus\]\. Existing work can be broadly categorized as follows:*constraint\-solving/SMT\-based synthesis*, which encodes temporal logic constraints symbolically and reasons about feasibility or correctness using SAT/SMT solvers\[shoukry2016scalable,shoukry2017linear\];*Mixed\-Integer Programming \(MIP\)*approaches, which formulate motion planning and control synthesis under temporal logic constraints as optimization problems over continuous dynamics and binary decision variables\[SMTMultiRobotSafeLTL,MultiAgentSTLWaypoints\];*reactive synthesis*, which focuses on strategy synthesis and correctness guarantees in adversarial or game\-theoretic settings, commonly using ATL or related formalisms\[ATL\]; and*learning\-based solvers*\[NNSTREL,formats\]\.

Inspired by prior work on SMT\- and MIP\-based planning, we present SMT and MIP encodings of the centralized planning problem under STL\-GO specifications\. A key difference from prior encoding methods is that we explicitly handle weighted, time\-varying interaction graphs whose structure is induced by the joint state of agents and environment; this requires encoding multi\-graph quantification and neighborhood\-cardinality predicates as solver constraints\.

Contributions\.\(i\) We present MIP and SMT encodings of STL\-GO that support multi\-graph existential and universal quantification and neighborhood\-cardinality predicates over time\-varying interaction graphs, with soundness guarantees\. \(ii\) We provide a unified interface for specifying agents, interaction graphs, STL\-GO formulas, and an objective function that compiles to MIP/SMT\-encoded plans, also enabling direct empirical comparison\. \(iii\) We empirically evaluate the encodings on a multi\-UAV search\-and\-rescue benchmark using Gurobi and Z3, ablating over team size and interaction\-graph complexity\. \(iv\) We additionally evaluate the encodings on a structurally different grid\-world benchmark adapted from HypRL\[hsu2025hyprl\]\. The results compare solve time and encoding size across the MIP and SMT backends\. We further show that the same specifications, encoded in HyperLTL, incur either a linear blow\-up in formula size or an alternation in the quantifier prefix, motivating STL\-GO’s pointwise agent\-level quantification\.

The remainder of the paper is organized as follows\. Section[II](https://arxiv.org/html/2607.28679#S2)introduces the multi\-agent system model, interaction graphs, and STL\-GO\. Section[III](https://arxiv.org/html/2607.28679#S3)formalizes the bounded\-horizon planning problem for multi\-agent systems subject to STL\-GO specifications\. Sections[IV](https://arxiv.org/html/2607.28679#S4)and[V](https://arxiv.org/html/2607.28679#S5)present our solver\-based synthesis approaches, describing the translation of STL\-GO specifications into MIP and SMT encodings, respectively\. We evaluate both approaches through simulations and present our results in Section[VI](https://arxiv.org/html/2607.28679#S6), and discuss related work and conclusions in Section[VII](https://arxiv.org/html/2607.28679#S7)\.

## IIPreliminaries

### II\-AMulti\-Agent System Model

Let𝒱=\{1,…,N\}\\mathcal\{V\}=\\\{1,\\ldots,N\\\}be a set of agents whose spatio\-temporal behavior evolves over a discrete time domain𝕋⊂ℕ\\mathbb\{T\}\\subset\\mathbb\{N\}\. We consider a homogeneous MAS in which each agenti∈𝒱i\\in\\mathcal\{V\}has a state vector𝐱ti∈𝒳\\mathbf\{x\}^\{i\}\_\{t\}\\in\\mathcal\{X\}, at timettwhere𝒳\\mathcal\{X\}is the shared state space\. The state variables encode attributes local to an agent, such as physical configuration and internal resources\. The joint state of all agents at timet∈𝕋t\\in\\mathbb\{T\}is denoted𝐗t=\(𝐱t1,…,𝐱tN\)∈𝒳N\\mathbf\{X\}\_\{t\}=\(\\mathbf\{x\}\_\{t\}^\{1\},\\ldots,\\mathbf\{x\}\_\{t\}^\{N\}\)\\in\\mathcal\{X\}^\{N\}\. While we focus on the homogeneous setting for notational clarity, the encoding extends to role\-typed heterogeneity, as used in the search\-and\-rescue example below\.

The MAS environment is modeled as a discrete\-time dynamical system with state𝐰t∈𝒲\\mathbf\{w\}\_\{t\}\\in\\mathcal\{W\}, where𝒲\\mathcal\{W\}encodes attributes such as map geometry \(static or dynamic\), obstacles, and adversarial features \(e\.g\., communication disruption\)\. The environment evolves deterministically according to𝐰t\+1=f​\(𝐰t\)\\mathbf\{w\}\_\{t\+1\}=f\(\\mathbf\{w\}\_\{t\}\), whereffand the initial world state𝐰0\\mathbf\{w\}\_\{0\}are known\. Thus, the finite trajectory\{𝐰t\}t=0T\\\{\\mathbf\{w\}\_\{t\}\\\}\_\{t=0\}^\{T\}is fixed when a planning instance is constructed\.111Real\-world environments may exhibit stochasticity, in which case a synthesized plan can only be guaranteed to satisfy the specification with high probability\. We do not address this setting here, but the tools developed in this paper can serve as a building block for stochastic extensions\.

Each agent is governed by a transition dynamics functionFFthat is shared across all agents \(since the MAS is homogeneous\)\. At each timett, agentiiselects a control input𝐮ti∈𝒰\\mathbf\{u\}\_\{t\}^\{i\}\\in\\mathcal\{U\}from an admissible input domain𝒰\\mathcal\{U\}, and its successor state is

𝐱t\+1i=F​\(𝐱ti,𝐮ti,𝐰t\)\.\\mathbf\{x\}\_\{t\+1\}^\{i\}=F\(\\mathbf\{x\}\_\{t\}^\{i\},\\mathbf\{u\}\_\{t\}^\{i\},\\mathbf\{w\}\_\{t\}\)\.\(1\)Stacking the componentwise dynamics gives the joint successor state

𝐗t\+1=F​\(𝐗t,𝐔t,𝐰t\),\\mathbf\{X\}\_\{t\+1\}=F\(\\mathbf\{X\}\_\{t\},\\mathbf\{U\}\_\{t\},\\mathbf\{w\}\_\{t\}\),\(2\)where𝐔t=\(𝐮t1,…,𝐮tN\)\\mathbf\{U\}\_\{t\}=\(\\mathbf\{u\}\_\{t\}^\{1\},\\ldots,\\mathbf\{u\}\_\{t\}^\{N\}\)is the joint control input\.

###### Example 1\.

Consider a system of𝒱=\{1,…,N\}\\mathcal\{V\}=\\left\\\{1,\\ldots,N\\right\\\}robots, where the state of agenti∈𝒱i\\in\\mathcal\{V\}is𝐱ti:=\(𝐩ti,θti,𝜿ti\)\\mathbf\{x\}^\{i\}\_\{t\}:=\\left\(\\mathbf\{p\}^\{i\}\_\{t\},\\theta^\{i\}\_\{t\},\\boldsymbol\{\\kappa\}^\{i\}\_\{t\}\\right\)where:𝐩ti=\[xti,yti\]⊤∈ℝ2\\mathbf\{p\}^\{i\}\_\{t\}=\[x^\{i\}\_\{t\},\\,y^\{i\}\_\{t\}\]^\{\\top\}\\in\\mathbb\{R\}^\{2\}is the position of the agent,θti∈\[0,2​π\)\\theta^\{i\}\_\{t\}\\in\[0,2\\pi\)is the orientation, and𝜿ti\\boldsymbol\{\\kappa\}^\{i\}\_\{t\}can refer to a collection of time\-varying resources and capabilities such as the battery level\. At each timett, each agent selectsuti:=\(vti,ωti\)∈𝒰u^\{i\}\_\{t\}:=\(v^\{i\}\_\{t\},\\omega^\{i\}\_\{t\}\)\\in\\mathcal\{U\}withvti∈\[vmin,vmax\]v^\{i\}\_\{t\}\\in\[v\_\{\\min\},v\_\{\\max\}\]andωti∈\[ωmin,ωmax\]\\omega^\{i\}\_\{t\}\\in\[\\omega\_\{\\min\},\\omega\_\{\\max\}\]the linear and angular velocities\. For sampling timeΔ​t\>0\\Delta t\>0and a unicycle model,222The unicycle dynamics in this example are illustrative\. The MIP and SMT encodings and the reported experiments use discrete\-time affine motion dynamics\. Accommodating the displayed nonlinear model would instead require a piecewise\-affine approximation or an SMT theory of nonlinear real arithmetic\.position and orientation update asxt\+1i=xti\+Δ​t​vti​cos⁡\(θti\)x^\{i\}\_\{t\+1\}=x^\{i\}\_\{t\}\+\\Delta t\\,v^\{i\}\_\{t\}\\cos\(\\theta^\{i\}\_\{t\}\),yt\+1i=yti\+Δ​t​vti​sin⁡\(θti\)y^\{i\}\_\{t\+1\}=y^\{i\}\_\{t\}\+\\Delta t\\,v^\{i\}\_\{t\}\\sin\(\\theta^\{i\}\_\{t\}\),θt\+1i=wrap\[0,2​π\)​\(θti\+Δ​t​ωti\)\\theta^\{i\}\_\{t\+1\}=\\mathrm\{wrap\}\_\{\[0,2\\pi\)\}\(\\theta^\{i\}\_\{t\}\+\\Delta t\\,\\omega^\{i\}\_\{t\}\)\.

To encode the rich interaction and potential coupling between each agent, its perception of the world state, and their effect on decision making in the system, we define the notion of*interaction graphs*\[stlgo\]\.

###### Definition 2\(Interaction Graph\)\.

An interaction graph𝒢t𝚝𝚢𝚙𝚎\\mathcal\{G\}^\{\\mathtt\{type\}\}\_\{t\}is a directed and weighted graph𝒢t𝚝𝚢𝚙𝚎:=\(𝒱,ℰt𝚝𝚢𝚙𝚎,wt𝚝𝚢𝚙𝚎\),\\mathcal\{G\}^\{\\mathtt\{type\}\}\_\{t\}:=\(\\mathcal\{V\},\\mathcal\{E\}^\{\\mathtt\{type\}\}\_\{t\},w^\{\\mathtt\{type\}\}\_\{t\}\),whereℰt𝚝𝚢𝚙𝚎⊆𝒱×𝒱\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}\\subseteq\\mathcal\{V\}\\times\\mathcal\{V\}is the edge set, andwt𝚝𝚢𝚙𝚎:ℰt𝚝𝚢𝚙𝚎→ℝ≥0w\_\{t\}^\{\\mathtt\{type\}\}:\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}\\to\\mathbb\{R\}\_\{\\geq 0\}assigns edge attributes \(e\.g\., distance, cost, signal quality\)\. Different interaction modalities are modeled by distinct graph types𝚝𝚢𝚙𝚎∈𝒯:=\{𝚝𝚢𝚙𝚎1,…,𝚝𝚢𝚙𝚎M\}\\mathtt\{type\}\\in\\mathcal\{T\}:=\\left\\\{\\mathtt\{type\}\_\{1\},\\ldots,\\mathtt\{type\}\_\{M\}\\right\\\}\. The collection of all interaction graphs at timettis𝓖t:=\{𝒢t𝚝𝚢𝚙𝚎∣𝚝𝚢𝚙𝚎∈𝒯\}\\boldsymbol\{\\mathcal\{G\}\}\_\{t\}:=\\\{\\mathcal\{G\}\_\{t\}^\{\\mathtt\{type\}\}\\mid\\mathtt\{type\}\\in\\mathcal\{T\}\\\}\.

###### Example 3\.

Examples of interaction graphs include: \(i\) Adistance graph𝒢td=\(𝒱,ℰtd,wtd\)\\mathcal\{G\}\_\{t\}^\{d\}=\\left\(\\mathcal\{V\},\\mathcal\{E\}\_\{t\}^\{d\},w\_\{t\}^\{d\}\\right\)is a complete directed graph whereℰtd=𝒱×𝒱∖\{\(i,i\)∣i∈𝒱\}\\mathcal\{E\}\_\{t\}^\{d\}=\\mathcal\{V\}\\times\\mathcal\{V\}\\setminus\\\{\(i,i\)\\mid i\\in\\mathcal\{V\}\\\}\(all ordered pairs wherei≠ji\\neq j\) andwtdw\_\{t\}^\{d\}is the distance between agentsiiandjjat timett\. \(ii\) Asensing graph𝒢ts=\(𝒱,ℰts,wts\)\\mathcal\{G\}^\{s\}\_\{t\}=\(\\mathcal\{V\},\\mathcal\{E\}^\{s\}\_\{t\},w^\{s\}\_\{t\}\)encodes whether agentiican sense agentjjat timettand\(i,j\)∈ℰts\(i,j\)\\in\\mathcal\{E\}^\{s\}\_\{t\}\. \(iii\) Acommunication graph𝒢tc=\(𝒱,ℰtc,wtc\)\\mathcal\{G\}\_\{t\}^\{c\}=\(\\mathcal\{V\},\\mathcal\{E\}^\{c\}\_\{t\},w^\{c\}\_\{t\}\)where\(i,j\)∈ℰtc\(i,j\)\\in\\mathcal\{E\}^\{c\}\_\{t\}if and only if agentiican communicate with agentjj\. \(iv\) Atask\-dependency graph𝒢ttask=\(𝒱,ℰttask,wttask\),\\mathcal\{G\}^\{\\mathrm\{task\}\}\_\{t\}=\(\\mathcal\{V\},\\mathcal\{E\}^\{\\mathrm\{task\}\}\_\{t\},w^\{\\mathrm\{task\}\}\_\{t\}\),indicates that agentjjdepends on agentiifor task execution, where\(i,j\)∈ℰttask\(i,j\)\\in\\mathcal\{E\}^\{\\mathrm\{task\}\}\_\{t\}\.

### II\-BSpatio\-Temporal Logic with Graph Operators \(STL\-GO\)

STL\-GO\[stlgo\]extends Signal Temporal Logic \(STL\)\[stl\-dejan\]with graph operators to enable reasoning about both spatio\-temporal and*topological*relationships between agents\. The syntax and semantics of STL\-GO are split into agent\-local formulas and multi\-agent compositional formulas\.

#### II\-B1Agent\-Local Formulas

For formulas that specify behavior local to the perspective of a single agent, we use the recursive syntax:

φ::=⊤∣μx∣¬φ∣φ∧φ∣φ𝐔Iφ∣In𝓖,EW,\#φ∣Out𝓖,EW,\#φ\.\\varphi::=\\top\\mid\\mu\_\{x\}\\mid\\neg\\varphi\\mid\\varphi\\wedge\\varphi\\mid\\varphi\\,\\mathbf\{U\}\_\{I\}\\,\\varphi\\mid\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}\\varphi\\mid\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}\\varphi\.Here,μx\\mu\_\{x\}represents an atomic predicate of the formμx:𝒳→𝔹\\mu\_\{x\}:\\mathcal\{X\}\\to\\mathbb\{B\}that maps the state of an agent to a Boolean value; logical negation¬φ\\neg\\varphiand logical conjunctionφ∧φ\\varphi\\land\\varphiare defined as usual; and𝐔I\\mathbf\{U\}\_\{I\}is the until operator over an intervalI=\[a,b\]I=\[a,b\]as defined in STL\[stl\-dejan\]\.333We also use the standard derivationsφ1∨φ2:=¬\(¬φ1∧¬φ2\)\\varphi\_\{1\}\\lor\\varphi\_\{2\}:=\\neg\(\\neg\\varphi\_\{1\}\\land\\neg\\varphi\_\{2\}\),φ1⇒φ2:=¬φ1∨φ2\\varphi\_\{1\}\\Rightarrow\\varphi\_\{2\}:=\\neg\\varphi\_\{1\}\\lor\\varphi\_\{2\},𝐅I​φ:=⊤𝐔I​φ\\mathbf\{F\}\_\{I\}\\varphi:=\\top\\,\\mathbf\{U\}\_\{I\}\\,\\varphi, and𝐆I​φ:=¬𝐅I​¬φ\\mathbf\{G\}\_\{I\}\\varphi:=\\neg\\mathbf\{F\}\_\{I\}\\neg\\varphi\.

STL\-GO introduces the*incoming*In𝓖,EW,\#\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}and*outgoing*Out𝓖,EW,\#\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}graph operators, whereW=\[w1,w2\]⊆ℝW=\[w\_\{1\},w\_\{2\}\]\\subseteq\\mathbb\{R\}constrains the edge weights\. The cardinality constraintEEis specified by endpointse1∈ℕe\_\{1\}\\in\\mathbb\{N\},e2∈ℕ∪\{∞\}e\_\{2\}\\in\\mathbb\{N\}\\cup\\\{\\infty\\\}, withe1≤e2e\_\{1\}\\leq e\_\{2\}, and is defined asE=\[e1,e2\]ℕ:=\{k∈ℕ∣e1≤k≤e2\}E=\[e\_\{1\},e\_\{2\}\]\_\{\\mathbb\{N\}\}:=\\\{k\\in\\mathbb\{N\}\\mid e\_\{1\}\\leq k\\leq e\_\{2\}\\\}\. Thus,E=\[1,∞\)ℕE=\[1,\\infty\)\_\{\\mathbb\{N\}\}, for example, requires at least one qualifying edge\. Finally,\#∈\{∃,∀\}\\\#\\in\\\{\\exists,\\forall\\\}denotes existential or universal quantification over the graph types in𝒯\\mathcal\{T\}, equivalently over the graph instances in𝓖t\\boldsymbol\{\\mathcal\{G\}\}\_\{t\}\.

Letℳ​𝒜\\mathcal\{MA\}denote the finite execution induced by the multi\-agent system, the environment, and the chosen control sequence\. We write\(ℳ​𝒜,i,t\)⊧φ\(\\mathcal\{MA\},i,t\)\\models\\varphito denote Boolean satisfaction of the agent\-local formulaφ\\varphiat agentiiand timett\.

Graph operators allow an agent to reason about the trajectories of its neighboring agents\. The incoming operatorIn𝓖,EW,∃​φ\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\exists\}\\varphiasserts that there exists at least one graph instance𝒢t𝚝𝚢𝚙𝚎∈𝓖t\\mathcal\{G\}\_\{t\}^\{\\mathtt\{type\}\}\\in\\boldsymbol\{\\mathcal\{G\}\}\_\{t\}for which the count of incoming edges\(j,i\)\(j,i\)to agentiisatisfying bothwt𝚝𝚢𝚙𝚎​\(j,i\)∈Ww\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\\in Wand\(ℳ​𝒜,j,t\)⊧φ\(\\mathcal\{MA\},j,t\)\\models\\varphilies inEE\. The universal versionIn𝓖,EW,∀​φ\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\forall\}\\varphirequires the same property to hold across all graph instances𝒢t𝚝𝚢𝚙𝚎∈𝓖t\\mathcal\{G\}\_\{t\}^\{\\mathtt\{type\}\}\\in\\boldsymbol\{\\mathcal\{G\}\}\_\{t\}\. Similarly, the outgoing operatorOut𝓖,EW,∃​φ\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\exists\}\\varphistates that there exists a graph instance for which the analogous count over outgoing edges\(i,j\)\(i,j\)from agentiilies inEE\. If weights are not of interest, we setW:=\(−∞,∞\)W:=\(\-\\infty,\\infty\)and write the simplified formsIn𝓖,E\#​φ\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{\\\#\}\\varphiandOut𝓖,E\#​φ\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{\\\#\}\\varphi\.

Formally, writingt⊕I:=\{t\+τ:τ∈I\}t\\oplus I:=\\\{t\+\\tau:\\tau\\in I\\\}, we define the recursive semantics below\.444We use strong bounded\-horizon semantics: ift\+b\>Tt\+b\>T, an until or eventually obligation overI=\[a,b\]I=\[a,b\]cannot be discharged within the encoded horizon and is therefore false\. Because𝐆I​φ:=¬𝐅I​¬φ\\mathbf\{G\}\_\{I\}\\varphi:=\\neg\\mathbf\{F\}\_\{I\}\\neg\\varphi, the derived globally formula is true in this boundary case\.

\(ℳ​𝒜,i,t\)⊧⊤always,\(ℳ​𝒜,i,t\)⊧μxiff​μx​\(𝐱ti\),\(ℳ​𝒜,i,t\)⊧¬φiff​\(ℳ​𝒜,i,t\)⊧̸φ,\(ℳ​𝒜,i,t\)⊧φ1∧φ2iff​\(ℳ​𝒜,i,t\)⊧φ1∧\(ℳ​𝒜,i,t\)⊧φ2,\(ℳ​𝒜,i,t\)⊧φ1​𝐔\[a,b\]​φ2iff​t\+b≤T,∃t′∈t⊕\[a,b\]​s\.t\.\(ℳ​𝒜,i,t′\)⊧φ2∧∀t′′∈\[t,t′\)\.\(ℳ​𝒜,i,t′′\)⊧φ1,\(ℳ​𝒜,i,t\)⊧In𝓖,EW,\#​φiff​\#​𝚝𝚢𝚙𝚎∈𝒯​s\.t\.\|\{\(j,i\)∈ℰt𝚝𝚢𝚙𝚎:wt𝚝𝚢𝚙𝚎\(j,i\)∈W,\(ℳ𝒜,j,t\)⊧φ\}\|∈E,\(ℳ​𝒜,i,t\)⊧Out𝓖,EW,\#​φiff​\#​𝚝𝚢𝚙𝚎∈𝒯​s\.t\.\|\{\(i,j\)∈ℰt𝚝𝚢𝚙𝚎:wt𝚝𝚢𝚙𝚎\(i,j\)∈W,\(ℳ𝒜,j,t\)⊧φ\}\|∈E\.\\begin\{array\}\[\]\{l@\{\\;\}l\}\(\\mathcal\{MA\},i,t\)\\models\\top&\\text\{always\},\\\\ \(\\mathcal\{MA\},i,t\)\\models\\mu\_\{x\}&\\text\{iff \}\\mu\_\{x\}\(\\mathbf\{x\}\_\{t\}^\{i\}\),\\\\ \(\\mathcal\{MA\},i,t\)\\models\\neg\\varphi&\\text\{iff \}\(\\mathcal\{MA\},i,t\)\\not\\models\\varphi,\\\\ \(\\mathcal\{MA\},i,t\)\\models\\varphi\_\{1\}\\land\\varphi\_\{2\}&\\text\{iff \}\(\\mathcal\{MA\},i,t\)\\models\\varphi\_\{1\}\\\\ &\\quad\\land\(\\mathcal\{MA\},i,t\)\\models\\varphi\_\{2\},\\\\ \(\\mathcal\{MA\},i,t\)\\models\\varphi\_\{1\}\\,\\mathbf\{U\}\_\{\[a,b\]\}\\,\\varphi\_\{2\}&\\text\{iff \}t\+b\\leq T,\\exists t^\{\\prime\}\\in t\\oplus\[a,b\]\\text\{ s\.t\. \}\\\\ &\\quad\(\\mathcal\{MA\},i,t^\{\\prime\}\)\\models\\varphi\_\{2\}\\\\ &\\quad\\land\\ \\forall t^\{\\prime\\prime\}\\in\[t,t^\{\\prime\}\)\.\\,\(\\mathcal\{MA\},i,t^\{\\prime\\prime\}\)\\models\\varphi\_\{1\},\\\\ \(\\mathcal\{MA\},i,t\)\\models\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}\\varphi&\\text\{iff \}\\\#\\,\\mathtt\{type\}\\in\\mathcal\{T\}\\ \\text\{s\.t\.\}\\\\ &\\quad\\left\|\\left\\\{\(j,i\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}:w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\\in W,\\right\.\\right\.\\\\ &\\quad\\left\.\\left\.\(\\mathcal\{MA\},j,t\)\\models\\varphi\\right\\\}\\right\|\\in E,\\\\ \(\\mathcal\{MA\},i,t\)\\models\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\\#\}\\varphi&\\text\{iff \}\\\#\\,\\mathtt\{type\}\\in\\mathcal\{T\}\\ \\text\{s\.t\.\}\\\\ &\\quad\\left\|\\left\\\{\(i,j\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}:w\_\{t\}^\{\\mathtt\{type\}\}\(i,j\)\\in W,\\right\.\\right\.\\\\ &\\quad\\left\.\\left\.\(\\mathcal\{MA\},j,t\)\\models\\varphi\\right\\\}\\right\|\\in E\.\\end\{array\}

#### II\-B2Multi\-Agent Formulas

STL\-GO uses the following recursive grammar to define properties over multiple agents:

ϕ::=⊤∣μ∣i\.φ∣¬ϕ∣ϕ∧ϕ∣ϕ𝐔Iϕ∣𝐅𝐀φ∣𝐄𝐗φ,\\phi::=\\top\\mid\\mu\\mid i\.\\varphi\\mid\\neg\\phi\\mid\\phi\\wedge\\phi\\mid\\phi\\mathbf\{U\}\_\{I\}\\phi\\mid\\mathbf\{FA\}\\,\\varphi\\mid\\mathbf\{EX\}\\,\\varphi,whereφ\\varphiis an agent\-local formula, andμ\\mu\(without the subscriptxx\) denotes an atomic predicate of the formμ:𝒳\|𝒱\|×𝒲→𝔹\\mu:\\mathcal\{X\}^\{\\lvert\\mathcal\{V\}\\rvert\}\\times\\mathcal\{W\}\\to\\mathbb\{B\}\. Such predicates are analogous to the agent\-local predicatesμx\\mu\_\{x\}, but are defined over the joint agent and world state\(𝐗t,𝐰t\)\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)\.

Multi\-agent formulas allow properties to be specified across agents using logical connectives and over time using temporal operators\. The operatori\.φi\.\\varphiembeds an agent\-local formula into a multi\-agent formula\. The operators𝐅𝐀\\mathbf\{FA\}and𝐄𝐗\\mathbf\{EX\}denote universal and existential quantification, respectively, over the full agent set𝒱\\mathcal\{V\}, with𝐅𝐀​φ:=⋀i∈𝒱i\.φ\\mathbf\{FA\}\\varphi:=\\bigwedge\_\{i\\in\\mathcal\{V\}\}i\.\\varphiand𝐄𝐗​φ:=⋁i∈𝒱i\.φ\\mathbf\{EX\}\\varphi:=\\bigvee\_\{i\\in\\mathcal\{V\}\}i\.\\varphi\.

Formally, we write\(ℳ​𝒜,t\)⊧ϕ\(\\mathcal\{MA\},t\)\\models\\phito denote that the STL\-GO formulaϕ\\phiis satisfied by the finite executionℳ​𝒜\\mathcal\{MA\}at timett\. Its semantics are defined inductively as follows:

\(ℳ​𝒜,t\)⊧⊤always,\(ℳ​𝒜,t\)⊧μiff​μ​\(𝐗t,𝐰t\),\(ℳ​𝒜,t\)⊧i\.φiff​\(ℳ​𝒜,i,t\)⊧φ,\(ℳ​𝒜,t\)⊧¬ϕiff​\(ℳ​𝒜,t\)⊧̸ϕ,\(ℳ​𝒜,t\)⊧ϕ1∧ϕ2iff​\(ℳ​𝒜,t\)⊧ϕ1∧\(ℳ​𝒜,t\)⊧ϕ2,\(ℳ​𝒜,t\)⊧ϕ1​𝐔\[a,b\]​ϕ2iff​t\+b≤T​and​∃t′∈t⊕\[a,b\]s\.t\.​\(ℳ​𝒜,t′\)⊧ϕ2∧∀t′′∈\[t,t′\)\.\(ℳ​𝒜,t′′\)⊧ϕ1,\(ℳ​𝒜,t\)⊧𝐅𝐀​φiff​∀i∈𝒱\.\(ℳ​𝒜,i,t\)⊧φ,\(ℳ​𝒜,t\)⊧𝐄𝐗​φiff​∃i∈𝒱\.\(ℳ​𝒜,i,t\)⊧φ\.\\begin\{array\}\[\]\{l@\{ \}l\}\(\\mathcal\{MA\},t\)\\models\\top&\\text\{always\},\\\\ \(\\mathcal\{MA\},t\)\\models\\mu&\\text\{iff \}\\mu\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\),\\\\ \(\\mathcal\{MA\},t\)\\models i\.\\varphi&\\text\{iff \}\(\\mathcal\{MA\},i,t\)\\models\\varphi,\\\\ \(\\mathcal\{MA\},t\)\\models\\neg\\phi&\\text\{iff \}\(\\mathcal\{MA\},t\)\\not\\models\\phi,\\\\ \(\\mathcal\{MA\},t\)\\models\\phi\_\{1\}\\land\\phi\_\{2\}&\\text\{iff \}\(\\mathcal\{MA\},t\)\\models\\phi\_\{1\}\\\!\\land\\\!\(\\mathcal\{MA\},t\)\\\!\\models\\\!\\phi\_\{2\},\\\\ \(\\mathcal\{MA\},t\)\\models\\phi\_\{1\}\\,\\mathbf\{U\}\_\{\[a,b\]\}\\,\\phi\_\{2\}&\\text\{iff \}t\+b\\leq T\\text\{ and \}\\exists t^\{\\prime\}\\in t\\oplus\[a,b\]\\\\ &\\quad\\text\{s\.t\. \}\(\\mathcal\{MA\},t^\{\\prime\}\)\\models\\phi\_\{2\}\\\\ &\\quad\\land\\ \\forall t^\{\\prime\\prime\}\\in\[t,t^\{\\prime\}\)\.\\,\(\\mathcal\{MA\},t^\{\\prime\\prime\}\)\\models\\phi\_\{1\},\\\\ \(\\mathcal\{MA\},t\)\\models\\mathbf\{FA\}\\varphi&\\text\{iff \}\\forall i\\in\\mathcal\{V\}\.\\,\(\\mathcal\{MA\},i,t\)\\models\\varphi,\\\\ \(\\mathcal\{MA\},t\)\\models\\mathbf\{EX\}\\varphi&\\text\{iff \}\\exists i\\in\\mathcal\{V\}\.\\,\(\\mathcal\{MA\},i,t\)\\models\\varphi\.\\end\{array\}
In our example, let us consider the UAVs to be assigned a search\-and\-rescue mission with agents being assigned one of two roles: ‘locators’ℒ⊆𝒱\\mathcal\{L\}\\subseteq\\mathcal\{V\}and ‘rescuers’ℛ⊆𝒱\\mathcal\{R\}\\subseteq\\mathcal\{V\}\.

Emergency events may arise at any site in a fixed set of candidate locations and must be detected by the locator agents and assigned to one or more rescuers\. The rescuer must resolve the emergency within bounded time, i\.e\., reach the emergency location and carry the rescued individual to the rescue center\. Let𝒞⊂ℝ2\\mathcal\{C\}\\subset\\mathbb\{R\}^\{2\}denote the rescue center andℳ\\mathcal\{M\}a fixed set of possible emergency sites, with eachm∈ℳm\\in\\mathcal\{M\}having position𝐩tm∈ℝ2\\mathbf\{p\}^\{m\}\_\{t\}\\in\\mathbb\{R\}^\{2\}\. LetεE,εC\>0\\varepsilon\_\{E\},\\varepsilon\_\{C\}\>0be distance tolerances for reaching an emergency and the rescue center, respectively\. Forℓ∈ℒ\\ell\\in\\mathcal\{L\},r∈ℛr\\in\\mathcal\{R\}, andm∈ℳm\\in\\mathcal\{M\}, we define the atomic predicatesφmemg​\(t\)⇔emergencymis active att\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\(t\)\\iff\\text\{emergency $m$ is active at $t$\},φr,mnear​\(t\)⇔‖𝐩tr−𝐩tm‖≤εE\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}\(t\)\\iff\\\|\\mathbf\{p\}^\{r\}\_\{t\}\-\\mathbf\{p\}^\{m\}\_\{t\}\\\|\\leq\\varepsilon\_\{E\},φratC​\(t\)⇔dist​\(𝐩tr,𝒞\)≤εC\\varphi^\{\\mathrm\{atC\}\}\_\{r\}\(t\)\\iff\\mathrm\{dist\}\(\\mathbf\{p\}^\{r\}\_\{t\},\\mathcal\{C\}\)\\leq\\varepsilon\_\{C\},φrcarry​\(t\)⇔rescuerrcarries a rescued individual\\varphi^\{\\mathrm\{carry\}\}\_\{r\}\(t\)\\iff\\text\{rescuer $r$ carries a rescued individual\}\. Letφℓ,r,mtask​\(t\)\\varphi^\{\\mathrm\{task\}\}\_\{\\ell,r,m\}\(t\)denote that locatorℓ\\ellassigns rescuerrrspecifically to emergencymmat timett\. LetE≥1:=\[1,∞\)ℕE\_\{\\geq 1\}:=\[1,\\infty\)\_\{\\mathbb\{N\}\}\. The emergency\-sensing predicate is a joint geometric predicate, while the remaining predicates below are agent\-local predicates derived using the STL\-GO graph operators:555For the communication predicates, the experimental implementation uses role\-partitioned restrictions of the communication graph:φℓLL\\varphi^\{\\mathrm\{LL\}\}\_\{\\ell\}restricts target neighbors to locators, whereasφℓLR\\varphi^\{\\mathrm\{LR\}\}\_\{\\ell\}restricts target neighbors to rescuers\. The compact notation below suppresses these target\-role restrictions\.

φmsense​\(t\)\\displaystyle\\varphi^\{\\mathrm\{sense\}\}\_\{m\}\(t\):=⋁ℓ∈ℒ\(‖𝐩tℓ−𝐩tm‖≤rsense\)\\displaystyle:=\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\left\(\\\|\\mathbf\{p\}\_\{t\}^\{\\ell\}\-\\mathbf\{p\}\_\{t\}^\{m\}\\\|\\leq r\_\{\\mathrm\{sense\}\}\\right\)φℓLL​\(t\)\\displaystyle\\varphi^\{\\mathrm\{LL\}\}\_\{\\ell\}\(t\):=Out\{𝒢c\},E≥1∃⊤\\displaystyle:=\\mathrm\{Out\}\_\{\\\{\\mathcal\{G\}^\{c\}\\\},E\_\{\\geq 1\}\}^\{\\exists\}\\,\\topφℓLR​\(t\)\\displaystyle\\varphi^\{\\mathrm\{LR\}\}\_\{\\ell\}\(t\):=Out\{𝒢c\},E≥1∃⊤\\displaystyle:=\\mathrm\{Out\}\_\{\\\{\\mathcal\{G\}^\{c\}\\\},E\_\{\\geq 1\}\}^\{\\exists\}\\,\\topWe encode the following specification: Once an emergency is detected, at least one locator must assign a rescuer within bounded timeTassignT\_\{\\mathrm\{assign\}\}:

ϕassign:=𝐆​⋀m∈ℳ\(φmemg∧φmsense⇒𝐅\[0,Tassign\]​⋁ℓ∈ℒ⋁r∈ℛφℓ,r,mtask\)\.\\displaystyle\\phi\_\{\\mathrm\{assign\}\}:=\\mathbf\{G\}\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\left\(\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\\wedge\\varphi^\{\\mathrm\{sense\}\}\_\{m\}\\Rightarrow\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\;\\bigvee\_\{r\\in\\mathcal\{R\}\}\\varphi^\{\\mathrm\{task\}\}\_\{\\ell,r,m\}\\right\)\.

## IIIProblem Statement

In this paper, we are interested in an*open\-loop planning*666Here, “open\-loop” refers to the finite control sequence synthesized along each realized execution branch\. In the experiments, multiple such sequences are synthesized jointly to form a finite contingency tree; observations select among precomputed branches, while the selected branch itself is executed open loop\.or*bounded synthesis*problem for multi\-agent systems, that is, our goal is to synthesize a finite sequence of control inputs to a system of multiple homogeneous agents over a bounded horizon, such that they satisfy a formal specification\.

More concretely, we consider a system of agents𝒱=\{1,…,N\}\\mathcal\{V\}=\\left\\\{1,\\ldots,N\\right\\\}with state space𝒳\\mathcal\{X\}and joint input𝐔t=\(𝐮t1,…,𝐮tN\)∈𝒰N\\mathbf\{U\}\_\{t\}=\(\\mathbf\{u\}\_\{t\}^\{1\},\\dots,\\mathbf\{u\}\_\{t\}^\{N\}\)\\in\\mathcal\{U\}^\{N\}, operating in a world with state space𝒲\\mathcal\{W\}\. Each agent evolves in discrete time according to a known, deterministic, homogeneous dynamics functionF:𝒳×𝒰×𝒲→𝒳F:\\mathcal\{X\}\\times\\mathcal\{U\}\\times\\mathcal\{W\}\\to\\mathcal\{X\}\. For the encodings presented in this paper, we restrictFFto be affine in the agent state, control input, and world state\. We assume that the initial joint state𝐗0\\mathbf\{X\}\_\{0\}and the finite world trajectory\{𝐰t\}t=0T\\\{\\mathbf\{w\}\_\{t\}\\\}\_\{t=0\}^\{T\}are fixed and known when the planning instance is constructed\.

Letϕ\\phibe an STL\-GO formula interpreted over the MASℳ​𝒜\\mathcal\{MA\}under the induced graph\-collection sequence\{𝓖t\}t=0T\\\{\\boldsymbol\{\\mathcal\{G\}\}\_\{t\}\\\}\_\{t=0\}^\{T\}over a bounded horizonT∈ℕT\\in\\mathbb\{N\}\. Then, our goal is to synthesize an open\-loop control sequence\{𝐔t\}t=0T−1\\\{\\mathbf\{U\}\_\{t\}\\\}\_\{t=0\}^\{T\-1\}such that the resulting execution\{𝐗t\}t=0T\\\{\\mathbf\{X\}\_\{t\}\\\}\_\{t=0\}^\{T\}according to the dynamics in[Equation 2](https://arxiv.org/html/2607.28679#S2.E2)satisfies the specification at the initial state, i\.e\.,\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\. One may optionally minimize a performance objectiveJ​\(\{𝐗t\}t=0T,\{𝐔t\}t=0T−1\)J\(\\\{\\mathbf\{X\}\_\{t\}\\\}\_\{t=0\}^\{T\},\\\{\\mathbf\{U\}\_\{t\}\\\}\_\{t=0\}^\{T\-1\}\)\(e\.g\., control effort, total path length, etc\.\), yielding an*optimal*bounded synthesis problem\.

We identify a class of multi\-agent systems with state\-dependent interaction graphs characterized by*graph constructor functions*, for which the bounded synthesis can be framed as an optimization\-based or satisfaction problem without much change in how the problem itself is encoded\.

###### Definition 4\(Graph Constructor Function\)\.

For a given interaction modality𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, a graph constructor functionΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}maps an element of𝒳\|𝒱\|×𝒲\\mathcal\{X\}^\{\|\\mathcal\{V\}\|\}\\times\\mathcal\{W\}to a directed, weighted graph on𝒱\\mathcal\{V\}\. At timett, we write𝒢t𝚝𝚢𝚙𝚎=Γ𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)=\(𝒱,ℰt𝚝𝚢𝚙𝚎,wt𝚝𝚢𝚙𝚎\)\\mathcal\{G\}\_\{t\}^\{\\mathtt\{type\}\}=\\Gamma^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)=\(\\mathcal\{V\},\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\},w\_\{t\}^\{\\mathtt\{type\}\}\)\. Thus, for every ordered pair\(i,j\)\(i,j\), the constructor determines whether\(i,j\)∈ℰt𝚝𝚢𝚙𝚎\(i,j\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}and, when the edge exists, its weightwt𝚝𝚢𝚙𝚎​\(i,j\)w\_\{t\}^\{\\mathtt\{type\}\}\(i,j\)\.

###### Example 5\.

Let𝚝𝚢𝚙𝚎=d\\mathtt\{type\}=ddenote a distance\-based interaction modality\.Γd​\(𝐗t,𝐰t\)\\Gamma^\{d\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)maps to the function\(i,j\)↦d1​\(𝐱ti,𝐱tj\)\(i,j\)\\mapsto d\_\{1\}\(\\mathbf\{x\}^\{i\}\_\{t\},\\mathbf\{x\}^\{j\}\_\{t\}\), where𝐱ti\\mathbf\{x\}^\{i\}\_\{t\}and𝐱tj\\mathbf\{x\}^\{j\}\_\{t\}denote the 2D \(or 3D\) coordinates of agentsiiandjjandd1d\_\{1\}is theℓ1\\ell\_\{1\}distance\.777d1​\(a,b\)=∑k=1n\|ak−bk\|d\_\{1\}\(a,b\)=\\sum\_\{k=1\}^\{n\}\|a^\{k\}\-b^\{k\}\|wherekkindexes thennspatial dimensions\.

Under the determinism and homogeneity assumptions above, and restrictingΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}to an encodable class \(made precise in Sections[IV](https://arxiv.org/html/2607.28679#S4)and[V](https://arxiv.org/html/2607.28679#S5)\), the bounded synthesis problem can be transformed into a finite set of constraints suitable for satisfiability checking \(e\.g\. SMT\), or optimization \(e\.g\. MIP\), by introducing:\(i\)decision variables for\{𝐱ti\}t=0T\\\{\\mathbf\{x\}\_\{t\}^\{i\}\\\}\_\{t=0\}^\{T\}and\{𝐮ti\}t=0T−1\\\{\\mathbf\{u\}\_\{t\}^\{i\}\\\}\_\{t=0\}^\{T\-1\},\(ii\)auxiliary binary variables encoding the truth of various subformulas ofϕ\\phifor each agent and time instant\(iii\)constraints enforcing the dynamics, graph construction predicates, and the STL\-GO semantics of Boolean, temporal, and graph operators over the bounded horizon\.While we focus on homogeneous agent dynamics, the encoding extends to role\-typed heterogeneity, as used in the locator/rescuer split of the running example\.

Assumptions\.We focus on*centralized*,*open\-loop*planning under*deterministic*environment dynamics\. Decentralized planning under partial observability and local observation is the ultimate target, but we consider the centralized, fully observable setting as a foundational step; a tractable encoding in this setting will serve as a prerequisite for decentralized extensions which we relegate to future work\. Additionally, we assume that agents execute the synthesized open\-loop plan*autonomously*, and the deterministic environment dynamics let us reason about feasibility and correctness without probabilistic semantics\.

In the following sections we present a systematic modeling and synthesis framework that compiles the planning problem above, with its multiple interaction graphs, into mixed\-integer programs or satisfiability problems for centralized planning\. Due to space constraints, we will introduce the novel graph\-related encodings, and refer the reader to the complete encodings described in the Appendices[C](https://arxiv.org/html/2607.28679#A3)and[D](https://arxiv.org/html/2607.28679#A4)\.

## IVMIP\-based Encoding for STL\-GO Planning

### IV\-AEncoding System Specifications

System Dynamics\.We restrict ourselves to deterministic, homogeneous dynamics that are affine in the agent state, agent input, and world state so that the bounded synthesis problem admits an MIP encoding\. Specifically, let the dynamics be

𝐱t\+1i=F​\(𝐱ti,𝐮ti,𝐰t\):=A​𝐱ti\+B​𝐮ti\+E​𝐰t\+c,\\displaystyle\\mathbf\{x\}^\{i\}\_\{t\+1\}=F\(\\mathbf\{x\}^\{i\}\_\{t\},\\mathbf\{u\}^\{i\}\_\{t\},\\mathbf\{w\}\_\{t\}\):=A\\mathbf\{x\}^\{i\}\_\{t\}\+B\\mathbf\{u\}^\{i\}\_\{t\}\+E\\mathbf\{w\}\_\{t\}\+c,\(3\)wherei∈𝒱,t=0,…,T−1,i\\in\\mathcal\{V\},\\ \\ t=0,\\ldots,T\-1,andA,B,EA,B,Eandcchave appropriate dimensions\.

State and input constraints\.We assume agent states and control inputs to lie within hyper\-rectangular sets, so that they are bounded componentwise as:

xmin≤𝐱ti≤xmax,and​umin≤𝐮ti≤umax,∀i,t\.x\_\{\\min\}\\leq\\mathbf\{x\}^\{i\}\_\{t\}\\leq x\_\{\\max\},\\text\{ and \}u\_\{\\min\}\\leq\\mathbf\{u\}^\{i\}\_\{t\}\\leq u\_\{\\max\},\\quad\\forall i,t\.\(4\)
Interaction Graphs\.At each timett, interaction graphs are constructed from the joint agent state𝐗t∈𝒳N\\mathbf\{X\}\_\{t\}\\in\\mathcal\{X\}^\{N\}and world state𝐰t∈𝒲\\mathbf\{w\}\_\{t\}\\in\\mathcal\{W\}via the graph constructor functionΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}of Definition[4](https://arxiv.org/html/2607.28679#Thmtheorem4)\. For each ordered pair\(i,j\)∈𝒱×𝒱\(i,j\)\\in\\mathcal\{V\}\\times\\mathcal\{V\},i≠ji\\neq j, the existence of a directed edge\(i,j\)\(i,j\)is represented by a Boolean variable, while edge weights are real\-valued\. Specifically, writeηi,j𝚝𝚢𝚙𝚎:𝒳\|𝒱\|×𝒲→𝔹\\eta\_\{i,j\}^\{\\mathtt\{type\}\}:\\mathcal\{X\}^\{\|\\mathcal\{V\}\|\}\\times\\mathcal\{W\}\\to\\mathbb\{B\}for the edge\-existence predicate andei,j𝚝𝚢𝚙𝚎:𝒳\|𝒱\|×𝒲→ℝ≥0e\_\{i,j\}^\{\\mathtt\{type\}\}:\\mathcal\{X\}^\{\|\\mathcal\{V\}\|\}\\times\\mathcal\{W\}\\to\\mathbb\{R\}\_\{\\geq 0\}for the edge\-weight expression\. Then\(i,j\)∈ℰt𝚝𝚢𝚙𝚎\(i,j\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}if and only ifηi,j𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)\\eta\_\{i,j\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)holds, and an existing edge has weightwt𝚝𝚢𝚙𝚎​\(i,j\)=ei,j𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)w\_\{t\}^\{\\mathtt\{type\}\}\(i,j\)=e\_\{i,j\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)\.

To ensure compatibility with solver\-based synthesis, we restrict attention to graph constructors whose edge\-existence predicates admit exact mixed\-integer encodings and whose edge\-weight functions are piecewise affine in\(𝐗t,𝐰t\)\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)\. LetPWA​\(𝒳\|𝒱\|×𝒲\)\\mathrm\{PWA\}\(\\mathcal\{X\}^\{\|\\mathcal\{V\}\|\}\\times\\mathcal\{W\}\)denote the set of piecewise\-affine functions over the joint agent and world state\. We say that a graph constructorΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}is MIP\-encodable if, for every ordered pair\(i,j\)\(i,j\),ηi,j𝚝𝚢𝚙𝚎\\eta\_\{i,j\}^\{\\mathtt\{type\}\}is a Boolean combination of affine comparisons with an exact mixed\-integer representation andei,j𝚝𝚢𝚙𝚎∈PWA​\(𝒳\|𝒱\|×𝒲\)e\_\{i,j\}^\{\\mathtt\{type\}\}\\in\\mathrm\{PWA\}\(\\mathcal\{X\}^\{\|\\mathcal\{V\}\|\}\\times\\mathcal\{W\}\)\. The encoding introducesai,j,t𝚝𝚢𝚙𝚎∈\{0,1\}a\_\{i,j,t\}^\{\\mathtt\{type\}\}\\in\\\{0,1\\\}withai,j,t𝚝𝚢𝚙𝚎=1a\_\{i,j,t\}^\{\\mathtt\{type\}\}=1if and only ifηi,j𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)\\eta\_\{i,j\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)holds\. Atomic affine comparisons are encoded using two\-sided Big\-MMconstraints with valid bounds and the required numerical separation margins; Boolean connectives are translated into linear constraints over binary variables\.

### IV\-BEncoding Agent\-Local Operators

Logical and Temporal Operators\.The encodings of atomic predicates, logical operators, and temporal operators closely follow established formulations in the literature\[stl\-to\-milp1,stl\-to\-milp2\]\. They are included in Appendix[C](https://arxiv.org/html/2607.28679#A3)for completeness and correctness\.

Graph Operator Encodings\.For agentiiat timett, the incoming operatorψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphiis evaluated for each graph type𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}\. Its per\-type count contains the incoming neighborsj≠ij\\neq isuch that agentjjsatisfiesφ\\varphiand the graph\-constructor weightΓ𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)​\(j,i\)\\Gamma^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)\(j,i\)lies in the admissible intervalW=\[wmin,wmax\]W=\[w\_\{\\min\},w\_\{\\max\}\]; the count must lie in\[e1,e2\]\[e\_\{1\},e\_\{2\}\]\. The symbol\#∈\{∃,∀\}\\\#\\in\\\{\\exists,\\forall\\\}denotes existential or universal quantification over𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}\. The MIP encoding ofIn\\mathrm\{In\}proceeds in three steps for a fixed graph type, plus a fourth step that combines per\-type encodings under the modal quantifier\.

1. 1\.Eligible incoming edges\.For eachj∈𝒱∖\{i\}j\\in\\mathcal\{V\}\\setminus\\\{i\\\}, introduce binary variablesλj,i,tlow,𝚝𝚢𝚙𝚎\\lambda\_\{j,i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}andλj,i,thigh,𝚝𝚢𝚙𝚎\\lambda\_\{j,i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}, indicating satisfaction of the lower and upper weight bounds, respectively, and an eligibility variableγj,i,t𝚝𝚢𝚙𝚎\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\. We impose wt𝚝𝚢𝚙𝚎​\(j,i\)\\displaystyle w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)≥wmin−M​\(1−λj,i,tlow,𝚝𝚢𝚙𝚎\),\\displaystyle\\geq w\_\{\\min\}\-M\\bigl\(1\-\\lambda\_\{j,i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\\bigr\),\(5\)wt𝚝𝚢𝚙𝚎​\(j,i\)\\displaystyle w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)≤wmin−δw\+M​λj,i,tlow,𝚝𝚢𝚙𝚎,\\displaystyle\\leq w\_\{\\min\}\-\\delta\_\{w\}\+M\\lambda\_\{j,i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\},wt𝚝𝚢𝚙𝚎​\(j,i\)\\displaystyle w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)≤wmax\+M​\(1−λj,i,thigh,𝚝𝚢𝚙𝚎\),\\displaystyle\\leq w\_\{\\max\}\+M\\bigl\(1\-\\lambda\_\{j,i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}\\bigr\),wt𝚝𝚢𝚙𝚎​\(j,i\)\\displaystyle w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)≥wmax\+δw−M​λj,i,thigh,𝚝𝚢𝚙𝚎,\\displaystyle\\geq w\_\{\\max\}\+\\delta\_\{w\}\-M\\lambda\_\{j,i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\},γj,i,t𝚝𝚢𝚙𝚎≤aj,i,t𝚝𝚢𝚙𝚎,\\displaystyle\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\\leq a\_\{j,i,t\}^\{\\mathtt\{type\}\},γj,i,t𝚝𝚢𝚙𝚎≤λj,i,tlow,𝚝𝚢𝚙𝚎,γj,i,t𝚝𝚢𝚙𝚎≤λj,i,thigh,𝚝𝚢𝚙𝚎,\\displaystyle\\quad\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\\leq\\lambda\_\{j,i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\},\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\\leq\\lambda\_\{j,i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\},γj,i,t𝚝𝚢𝚙𝚎\\displaystyle\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}≥aj,i,t𝚝𝚢𝚙𝚎\+λj,i,tlow,𝚝𝚢𝚙𝚎\+λj,i,thigh,𝚝𝚢𝚙𝚎−2,\\displaystyle\\geq a\_\{j,i,t\}^\{\\mathtt\{type\}\}\+\\lambda\_\{j,i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\+\\lambda\_\{j,i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}\-2,whereδw\>0\\delta\_\{w\}\>0is a fixed numerical separation margin\. We assume that feasible edge weights areδw\\delta\_\{w\}\-separated from the outside of each interval boundary: a weight belowwminw\_\{\\min\}is at mostwmin−δww\_\{\\min\}\-\\delta\_\{w\}, and a weight abovewmaxw\_\{\\max\}is at leastwmax\+δww\_\{\\max\}\+\\delta\_\{w\}\. Under this convention, \([5](https://arxiv.org/html/2607.28679#S4.E5)\) enforces γj,i,t𝚝𝚢𝚙𝚎=1⇔\(aj,i,t𝚝𝚢𝚙𝚎=1∧wmin≤wt𝚝𝚢𝚙𝚎​\(j,i\)≤wmax\)\.\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}=1\\Leftrightarrow\\left\(a\_\{j,i,t\}^\{\\mathtt\{type\}\}=1\\land w\_\{\\min\}\\leq w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\\leq w\_\{\\max\}\\right\)\.
2. 2\.Count neighbors satisfyingφ\\varphi\.Letzφ,j,t∈\{0,1\}z\_\{\\varphi,j,t\}\\in\\\{0,1\\\}denote satisfaction of subformulaφ\\varphiby agentjjat timett\. Introduceyj,i,tφ,𝚝𝚢𝚙𝚎∈\{0,1\}y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}\\in\\\{0,1\\\}encodingγj,i,t𝚝𝚢𝚙𝚎∧zφ,j,t\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\\wedge z\_\{\\varphi,j,t\}: yj,i,tφ,𝚝𝚢𝚙𝚎≤γj,i,t𝚝𝚢𝚙𝚎,yj,i,tφ,𝚝𝚢𝚙𝚎≤zφ,j,t,yj,i,tφ,𝚝𝚢𝚙𝚎≥γj,i,t𝚝𝚢𝚙𝚎\+zφ,j,t−1\.\\displaystyle y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}\\leq\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\},\\quad y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}\\leq z\_\{\\varphi,j,t\},\\quad y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}\\geq\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\+z\_\{\\varphi,j,t\}\-1\. \(6\)and define the cardinalityci,tIn,φ,𝚝𝚢𝚙𝚎:=∑j≠iyj,i,tφ,𝚝𝚢𝚙𝚎\.c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}:=\\sum\_\{j\\neq i\}y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}\.
3. 3\.Cardinality enforcement\.First supposee2<∞e\_\{2\}<\\infty\. Sinceci,tIn,φ,𝚝𝚢𝚙𝚎c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}is integer\-valued, introduce binariesαi,tlow,𝚝𝚢𝚙𝚎\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}andαi,thigh,𝚝𝚢𝚙𝚎\\alpha\_\{i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}, indicatingci,tIn,φ,𝚝𝚢𝚙𝚎<e1c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}<e\_\{1\}andci,tIn,φ,𝚝𝚢𝚙𝚎\>e2c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}\>e\_\{2\}, respectively: ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≤e1−1\+M​\(1−αi,tlow,𝚝𝚢𝚙𝚎\),\\displaystyle\\leq e\_\{1\}\-1\+M\\bigl\(1\-\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\\bigr\),\(7\)ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≥e1−M​αi,tlow,𝚝𝚢𝚙𝚎,\\displaystyle\\geq e\_\{1\}\-M\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\},ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≥e2\+1−M​\(1−αi,thigh,𝚝𝚢𝚙𝚎\),\\displaystyle\\geq e\_\{2\}\+1\-M\\bigl\(1\-\\alpha\_\{i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}\\bigr\),ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≤e2\+M​αi,thigh,𝚝𝚢𝚙𝚎\.\\displaystyle\\leq e\_\{2\}\+M\\alpha\_\{i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}\.The per\-type satisfaction variable is encoded as zψ,i,t𝚝𝚢𝚙𝚎\\displaystyle z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}≤1−αi,tlow,𝚝𝚢𝚙𝚎,zψ,i,t𝚝𝚢𝚙𝚎≤1−αi,thigh,𝚝𝚢𝚙𝚎,\\displaystyle\\leq 1\-\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\},\\quad z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}\\leq 1\-\\alpha\_\{i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\},\(8\)zψ,i,t𝚝𝚢𝚙𝚎\\displaystyle z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}≥1−αi,tlow,𝚝𝚢𝚙𝚎−αi,thigh,𝚝𝚢𝚙𝚎\.\\displaystyle\\geq 1\-\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\-\\alpha\_\{i,t\}^\{\\mathrm\{high\},\\mathtt\{type\}\}\. For a lower\-bounded interval\[e1,∞\)ℕ\[e\_\{1\},\\infty\)\_\{\\mathbb\{N\}\}, only the lower violation variable is required: ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≤e1−1\+M​\(1−αi,tlow,𝚝𝚢𝚙𝚎\),\\displaystyle\\leq e\_\{1\}\-1\+M\\bigl\(1\-\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\\bigr\),\(9\)ci,tIn,φ,𝚝𝚢𝚙𝚎\\displaystyle c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}≥e1−M​αi,tlow,𝚝𝚢𝚙𝚎,zψ,i,t𝚝𝚢𝚙𝚎=1−αi,tlow,𝚝𝚢𝚙𝚎\.\\displaystyle\\geq e\_\{1\}\-M\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\},\\quad z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}=1\-\\alpha\_\{i,t\}^\{\\mathrm\{low\},\\mathtt\{type\}\}\.
4. 4\.Quantifying OperatorsThe existential operatorψ=In𝓖,EW,∃​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\exists\}\\varphirequires that at least one graph type in𝒯\\mathcal\{T\}satisfies the counting property\. For each𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, the per\-type encoding above produces a satisfaction variablezψ,i,t𝚝𝚢𝚙𝚎z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}; we then enforce the disjunction over types: zψ,i,t≥zψ,i,t𝚝𝚢𝚙𝚎​∀𝚝𝚢𝚙𝚎∈𝒯,zψ,i,t≤∑𝚝𝚢𝚙𝚎∈𝒯zψ,i,t𝚝𝚢𝚙𝚎\.\\displaystyle z\_\{\\psi,i,t\}\\geq z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}\\ \\forall\\mathtt\{type\}\\in\\mathcal\{T\},\\quad z\_\{\\psi,i,t\}\\leq\\sum\_\{\\mathtt\{type\}\\in\\mathcal\{T\}\}z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}\. \(10\)These constraints ensurezψ,i,t=1z\_\{\\psi,i,t\}=1iff some graph satisfies the property\.

The universal operatorψ=In𝓖,EW,∀​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},E\}^\{W,\\forall\}\\varphirequires that all graph types in𝒯\\mathcal\{T\}satisfy the counting property\. This is encoded using a conjunction instead of the disjunction over graph types\.

zψ,i,t≤zψ,i,t𝚝𝚢𝚙𝚎​∀𝚝𝚢𝚙𝚎∈𝒯,zψ,i,t≥1−\|𝒯\|\+∑𝚝𝚢𝚙𝚎∈𝒯zψ,i,t𝚝𝚢𝚙𝚎\.\\displaystyle z\_\{\\psi,i,t\}\\leq z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}\\;\\;\\forall\\mathtt\{type\}\\in\\mathcal\{T\},\\quad z\_\{\\psi,i,t\}\\geq 1\-\|\\mathcal\{T\}\|\+\\sum\_\{\\mathtt\{type\}\\in\\mathcal\{T\}\}z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}\.

\(11\)The outgoing operator is obtained from the incoming case by replacing\(j,i\)\(j,i\)with\(i,j\)\(i,j\)throughout\.

###### Lemma 6\.

The planning problem for agent\-local STL\-GO specifications, for multi\-agent systems whose agent dynamics are described by discrete\-time affine difference equations, can be encoded into a MIP such that any satisfying assignment yields a trajectory satisfying the specification\.

###### Proof\.

In the interest of space, we provide a proof sketch, with the full proof in Appendix[A](https://arxiv.org/html/2607.28679#A1)\. We establish the invariant

zψ,i,t=1⇔\(ℳ​𝒜,i,t\)⊧ψz\_\{\\psi,i,t\}=1\\iff\(\\mathcal\{MA\},i,t\)\\models\\psi\(12\)for every agent\-local subformulaψ\\psi, agentii, and timett, by structural induction onψ\\psi\.

1. 1\.The dynamics constraint \([3](https://arxiv.org/html/2607.28679#S4.E3)\) is an equality, so feasible assignments correspond to valid trajectories ofFF\.
2. 2\.Atomic predicates, Boolean connectives, and the until operator are encoded by standard Big\-MMand unrolling constructions\[stl\-to\-milp1,stl\-to\-milp2\]\.
3. 3\.Forψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphi, MIP\-encodability ofΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}, for each𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, provides exact edge indicators and PWA weight expressions\. Constraint \([5](https://arxiv.org/html/2607.28679#S4.E5)\) enforces thatγj,i,t𝚝𝚢𝚙𝚎=1\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}=1iff\(j,i\)∈ℰt𝚝𝚢𝚙𝚎\(j,i\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}and its weight lies inWW\. Constraint \([6](https://arxiv.org/html/2607.28679#S4.E6)\) then counts exactly those eligible neighbors that satisfyφ\\varphi\. Equations \([7](https://arxiv.org/html/2607.28679#S4.E7)\)–\([8](https://arxiv.org/html/2607.28679#S4.E8)\) encode a finite cardinality interval, while \([9](https://arxiv.org/html/2607.28679#S4.E9)\) encodes\[e1,∞\)ℕ\[e\_\{1\},\\infty\)\_\{\\mathbb\{N\}\}\. Finally, \([10](https://arxiv.org/html/2607.28679#S4.E10)\)–\([11](https://arxiv.org/html/2607.28679#S4.E11)\) encode existential or universal quantification over graph types\. The outgoing case is symmetric\.

Conjoining all constraints, the planning problem for agent\-local STL\-GO specifications is the feasibility of a MIP whose decision variables include the per\-step actions\. ∎

### IV\-CEncoding Multi\-Agent Quantifiers

Existential Quantification over agents\.The existential quantifier𝐄𝐗​φ\\mathbf\{EX\}\\varphiholds when at least one agenti∈𝒱i\\in\\mathcal\{V\}satisfiesφ\\varphi\. Letψ:=𝐄𝐗​φ\\psi:=\\mathbf\{EX\}\\varphi\. We encodeψ\\psias:

zψ,t≥zφ,i,t,∀i∈𝒱;zψ,t≤∑i∈𝒱zφ,i,tz\_\{\\psi,t\}\\geq z\_\{\\varphi,i,t\},\\ \\ \\forall i\\in\\mathcal\{V\};\\ \\ z\_\{\\psi,t\}\\leq\\sum\_\{i\\in\\mathcal\{V\}\}z\_\{\\varphi,i,t\}\(13\)
Universal Quantification over agents\.The universal quantifier𝐅𝐀​φ\\mathbf\{FA\}\\varphiholds whenφ\\varphiholds for all agentsi∈𝒱i\\in\\mathcal\{V\}\. Letψ:=𝐅𝐀​φ\\psi:=\\mathbf\{FA\}\\varphi\. We encodeψ\\psias:

zψ,t≤zφ,i,t,∀i∈𝒱;zψ,t≥1−\|𝒱\|\+∑i∈𝒱zφ,i,tz\_\{\\psi,t\}\\leq z\_\{\\varphi,i,t\},\\ \\ \\forall i\\in\\mathcal\{V\};\\qquad z\_\{\\psi,t\}\\geq 1\-\|\\mathcal\{V\}\|\+\\sum\_\{i\\in\\mathcal\{V\}\}z\_\{\\varphi,i,t\}\(14\)
###### Theorem 7\.

For an STL\-GO specificationϕ\\phiand horizonTT, if the multi\-agent system dynamics and graph constructor are MIP\-encodable as described above, and the corresponding MIP encoding is feasible, then the resulting state trajectory\{𝐗t\}t=0T\\\{\\mathbf\{X\}\_\{t\}\\\}\_\{t=0\}^\{T\}satisfiesϕ\\phi, i\.e\.,\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\.

###### Proof Sketch\.

Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6)establishes \([12](https://arxiv.org/html/2607.28679#S4.E12)\) for agent\-local subformulas\. We extend it to multi\-agent subformulasψ\\psiaszψ,t=1⇔\(ℳ​𝒜,t\)⊧ψz\_\{\\psi,t\}=1\\iff\(\\mathcal\{MA\},t\)\\models\\psiby structural induction: joint atomic predicates, embeddingi\.φi\.\\varphi, Boolean connectives, and until reuse the agent\-local arguments on multi\-agent variables;𝐄𝐗\\mathbf\{EX\}and𝐅𝐀\\mathbf\{FA\}are encoded as disjunction and conjunction over\{zφ,i,t\}i∈𝒱\\\{z\_\{\\varphi,i,t\}\\\}\_\{i\\in\\mathcal\{V\}\}\(Section[IV\-C](https://arxiv.org/html/2607.28679#S4.SS3)\), matching the semantics by the agent\-local invariant\. Feasibility withzϕ,0=1z\_\{\\phi,0\}=1as a constraint yields\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\. The full proof is in Appendix[A](https://arxiv.org/html/2607.28679#A1)\. ∎

## VSMT\-based Encoding for STL\-GO Planning

We encode the multi\-agent planning problem as a quantifier\-free SMT instance in the theory of Linear Real Arithmetic with integers \(LRA \+ LIA\), where a satisfying assignment yields a control sequence whose execution satisfies the STL\-GO specification\.

### V\-AEncoding System Specifications

State and Control Constraints\.To ensure physical and operational feasibility, agent states are constrained to a hyper\-rectangular workspace𝒳ws⊂ℝnx\\mathcal\{X\}\_\{\\mathrm\{ws\}\}\\subset\\mathbb\{R\}^\{n\_\{x\}\}with componentwise bounds, and control inputs are bounded componentwise by actuator limits \(e\.g\., maximum velocity, thrust, steering angle\)\.

⋀t=0T⋀i∈𝒱\(𝐱min≤xti≤𝐱max\),⋀t=0T−1⋀i∈𝒱\(𝐮min≤uti≤𝐮max\)\\bigwedge\_\{t=0\}^\{T\}\\bigwedge\_\{i\\in\\mathcal\{V\}\}\\left\(\\mathbf\{x\}\_\{\\min\}\\leq x\_\{t\}^\{i\}\\leq\\mathbf\{x\}\_\{\\max\}\\right\),\\;\\bigwedge\_\{t=0\}^\{T\-1\}\\bigwedge\_\{i\\in\\mathcal\{V\}\}\\left\(\\mathbf\{u\}\_\{\\min\}\\leq u\_\{t\}^\{i\}\\leq\\mathbf\{u\}\_\{\\max\}\\right\)\(15\)
System Dynamics\.We assume the system follows deterministic discrete\-time affine dynamics:888The encoding and soundness result presented here use affine dynamics and LRA\+LIA\. The same structural translation could instead be instantiated using an SMT solver over nonlinear arithmetic, such as dReal, to support non\-affine dynamics; we leave that extension for future work\.

𝐱t\+1i=A​𝐱ti\+B​𝐮ti\+E​𝐰t\+c∀i∈𝒱,∀t=0,1,…,T−1\\mathbf\{x\}\_\{t\+1\}^\{i\}=A\\mathbf\{x\}\_\{t\}^\{i\}\+B\\mathbf\{u\}\_\{t\}^\{i\}\+E\\mathbf\{w\}\_\{t\}\+c\\quad\\forall i\\in\\mathcal\{V\},\\quad\\forall t=0,1,\\ldots,T\-1\(16\)
Interaction Graphs\.We focus on interaction graphs whose structure and edge weights depend only on the joint agent state and world state via the graph constructor function\. For each timettand ordered pair\(i,j\)\(i,j\), letηi,j𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)\\eta\_\{i,j\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)be the edge\-existence predicate and letei,j𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)e\_\{i,j\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)compute the corresponding edge weight\. We sayΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}is*SMT\-encodable*if, for every\(i,j\)\(i,j\),ηi,j𝚝𝚢𝚙𝚎\\eta\_\{i,j\}^\{\\mathtt\{type\}\}is a Boolean formula over LRA\+LIA andei,j𝚝𝚢𝚙𝚎e\_\{i,j\}^\{\\mathtt\{type\}\}is an LRA term\. Both can then be encoded directly in the quantifier\-free SMT instance\.

### V\-BEncoding Agent\-local Operators

For each subformulaψ\\psiof specificationφ\\varphi, agenti∈𝒱i\\in\\mathcal\{V\}, and timet∈Tt\\in T, we introduce a Boolean variablezψ,ti∈\{⊤,⊥\}z\_\{\\psi,t\}^\{i\}\\in\\\{\\top,\\bot\\\}with the intended semantics

zψ,ti=⊤⟺\(ℳ𝒜,i,t\)⊧ψz\_\{\\psi,t\}^\{i\}=\\top\\;\\Longleftrightarrow\\;\(\\mathcal\{MA\},i,t\)\\models\\psi\(17\)The encoding of atomic predicates, logical operators, and temporal operators closely follow established formulations in the literature\[momtaz2023monitoring,prabhakar2018automatic\]\. They are included in Appendix[D](https://arxiv.org/html/2607.28679#A4)for completeness and correctness\.

Graph Operators\.

Forψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphi, the SMT encoding proceeds in three steps for each fixed graph type𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, plus a fourth step that combines the per\-type encodings under the modal quantifier\#\\\#\.

1. 1\.Eligible incoming edges\.For each graph type𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, agentsi,j∈𝒱i,j\\in\\mathcal\{V\}withi≠ji\\neq j, and timett, introduce a Boolean variablebj,i,t𝚝𝚢𝚙𝚎b\_\{j,i,t\}^\{\\mathtt\{type\}\}, indicating that\(j,i\)\(j,i\)is an edge in the graph instance𝒢t𝚝𝚢𝚙𝚎\\mathcal\{G\}\_\{t\}^\{\\mathtt\{type\}\}and that its weight lies inWW\. bj,i,t𝚝𝚢𝚙𝚎↔\\displaystyle b\_\{j,i,t\}^\{\\mathtt\{type\}\}\\;\\leftrightarrow\\;\(ηj,i𝚝𝚢𝚙𝚎\(𝐗t,𝐰t\)\\displaystyle\\Bigl\(\\eta\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)∧wmin≤ej,i𝚝𝚢𝚙𝚎\(𝐗t,𝐰t\)≤wmax\)\.\\displaystyle\\quad\\wedge\\;w\_\{\\min\}\\leq e\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)\\leq w\_\{\\max\}\\Bigr\)\.\(18\) whereηj,i𝚝𝚢𝚙𝚎\\eta\_\{j,i\}^\{\\mathtt\{type\}\}is the edge\-existence predicate andej,i𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)e\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)is the edge\-weight supplied by the graph constructor\. If weights are not of interest andW=\(−∞,∞\)W=\(\-\\infty,\\infty\), the weight comparisons are omitted\.
2. 2\.Count neighbors satisfyingφ\\varphi\.Letzφ,tjz^\{j\}\_\{\\varphi,t\}be a boolean variable to denote satisfaction of subformulaφ\\varphiby agentjjat timett\. This is encoded as nj,i,t𝚝𝚢𝚙𝚎=bj,i,t𝚝𝚢𝚙𝚎∧zφ,tjn^\{\\mathtt\{type\}\}\_\{j,i,t\}=b^\{\\mathtt\{type\}\}\_\{j,i,t\}\\wedge z^\{j\}\_\{\\varphi,t\}\(19\)
3. 3\.Cardinality\.For each graph type𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, define an integer variableci,t𝚝𝚢𝚙𝚎c^\{\\mathtt\{type\}\}\_\{i,t\}counting eligibleφ\\varphi\-satisfying incoming neighbors: ci,t𝚝𝚢𝚙𝚎=∑j≠i𝗂𝗍𝖾​\(nj,i,t𝚝𝚢𝚙𝚎,1,0\),\\displaystyle c^\{\\mathtt\{type\}\}\_\{i,t\}=\\sum\_\{j\\neq i\}\\mathsf\{ite\}\(n^\{\\mathtt\{type\}\}\_\{j,i,t\},1,0\), \(20\)The per\-type satisfaction variable is constrained by zψ,ti,𝚝𝚢𝚙𝚎↔\{e1≤ci,t𝚝𝚢𝚙𝚎≤e2,e2<∞,e1≤ci,t𝚝𝚢𝚙𝚎,e2=∞\.z\_\{\\psi,t\}^\{i,\\mathtt\{type\}\}\\;\\leftrightarrow\\;\\begin\{cases\}e\_\{1\}\\leq c\_\{i,t\}^\{\\mathtt\{type\}\}\\leq e\_\{2\},&e\_\{2\}<\\infty,\\\\ e\_\{1\}\\leq c\_\{i,t\}^\{\\mathtt\{type\}\},&e\_\{2\}=\\infty\.\\end\{cases\}\(21\)
4. 4\.Quantification over Graph Types\.For\#=∃\\\#=\\existsthe satisfaction ofψ\\psiat agentiiis the disjunction over types of the per\-type satisfactions; zψ,ti=⋁𝚝𝚢𝚙𝚎∈𝒯zψ,ti,𝚝𝚢𝚙𝚎\(\#=∃\),z^\{i\}\_\{\\psi,t\}\\;=\\;\\bigvee\_\{\\mathtt\{type\}\\in\\mathcal\{T\}\}z^\{i,\\mathtt\{type\}\}\_\{\\psi,t\}\\quad\(\\\#=\\exists\),\(22\)

For\#=∀\\\#=\\forallit is the conjunction instead of the disjunction\. The encoding of theOut𝓖,\[e1,e2\]W,\#​φ\\mathrm\{Out\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphioperator is obtained from the incoming case by substituting\(j,i\)\(j,i\)with\(i,j\)\(i,j\)in steps 1–3\.

###### Lemma 8\.

The planning problem for agent\-local STL\-GO specifications, for multi\-agent systems whose agent dynamics are described by discrete\-time affine difference equations and whose graph constructors are SMT\-encodable, can be encoded into a quantifier\-free SMT instance such that any satisfying assignment yields a trajectory satisfying the specification\.

###### Proof sketch\.

We establish the invariant

zψ,ti=⊤⇔\(ℳ𝒜,i,t\)⊧ψz^\{i\}\_\{\\psi,t\}=\\top\\iff\(\\mathcal\{MA\},i,t\)\\models\\psi\(23\)for every agent\-local subformulaψ\\psi, agentii, and timett, by structural induction onψ\\psi\. The dynamics constraint \([16](https://arxiv.org/html/2607.28679#S5.E16)\) is an equality in the SMT variables, so any satisfying assignment corresponds to a valid trajectory ofFF\. Atomic predicates, Boolean connectives, and the until operator are encoded by direct LRA constraints and finite unrolling over the bounded horizon\[momtaz2023monitoring,prabhakar2018automatic\]\. Forψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphi, SMT\-encodability ofΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}, for each𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, ensures the edge\-existence predicate and edge weight are LRA\+LIA expressions; \([18](https://arxiv.org/html/2607.28679#S5.E18)\)–\([21](https://arxiv.org/html/2607.28679#S5.E21)\) enforcezψ,ti,𝚝𝚢𝚙𝚎=⊤z^\{i,\\mathtt\{type\}\}\_\{\\psi,t\}=\\topiff the count of eligibleφ\\varphi\-satisfying neighbors lies in\[e1,e2\]\[e\_\{1\},e\_\{2\}\], and \([22](https://arxiv.org/html/2607.28679#S5.E22)\) lifts this to\#\\\#\-quantification over graph types\. The outgoing case is symmetric\. The full proof is in Appendix[B](https://arxiv.org/html/2607.28679#A2)\. ∎

### V\-CEncoding Multi\-Agent Quantifiers

The existential quantifier𝐄𝐗​φ\\mathbf\{EX\}\\varphiindicates the existence of at least one agenti∈𝒱i\\in\\mathcal\{V\}for whichφ\\varphiholds\. For a formulaψ:=𝐄𝐗​φ\\psi:=\\mathbf\{EX\}\\varphi, we encodeψ\\psiaszψ,t=⋁i∈𝒱zφ,tiz\_\{\\psi,t\}=\\bigvee\_\{i\\in\\mathcal\{V\}\}z^\{i\}\_\{\\varphi,t\}\. The universal quantifier𝐅𝐀​φ\\mathbf\{FA\}\\varphiis similarly defined using⋀i∈𝒱\\bigwedge\_\{i\\in\\mathcal\{V\}\}instead of⋁i∈𝒱\\bigvee\_\{i\\in\\mathcal\{V\}\}\.

###### Theorem 9\.

For an STL\-GO specificationϕ\\phiand horizonTT, if the multi\-agent system dynamics and graph constructor are SMT\-encodable as described above, and if the SMT instance is satisfiable, then any satisfying assignment yields a trajectory\{𝐗t\}t=0T\\\{\\mathbf\{X\}\_\{t\}\\\}\_\{t=0\}^\{T\}such that\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\.

###### Proof Sketch\.

Lemma[8](https://arxiv.org/html/2607.28679#Thmtheorem8)establishes \([23](https://arxiv.org/html/2607.28679#S5.E23)\) for agent\-local subformulas\. We extend it to multi\-agent subformulasψ\\psiaszψ,t=⊤⇔\(ℳ𝒜,t\)⊧ψz\_\{\\psi,t\}=\\top\\iff\(\\mathcal\{MA\},t\)\\models\\psiby structural induction: joint atomic predicates, embeddingi\.φi\.\\varphi, Boolean connectives, and until reuse the agent\-local arguments on multi\-agent variables;𝐄𝐗\\mathbf\{EX\}and𝐅𝐀\\mathbf\{FA\}are encoded as described above, matching the semantics by the agent\-local invariant\. Satisfiability of the SMT instance withzϕ,0=⊤z\_\{\\phi,0\}=\\topas a constraint yields\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\. The full proof is in Appendix[B](https://arxiv.org/html/2607.28679#A2)\. ∎

## VIExperiments and Results

![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trace_5loc_none.png)\(a\)No objective
![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trace_5loc_l1.png)\(b\)Linear objective
![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trace_5loc_l2.png)\(c\)Quadratic objective

Figure 2:Effect of objective function on agent trajectories \(5 locators, 2 rescuers\)\. With no objective \(a\), the MIP returns an arbitrary feasible solution\. A linear objective \(b\) and quadratic objective \(c\) progressively guide the rescuer toward more direct paths to the emergency sites\.![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trajectories_5loc_l1.png)\(a\)5 locators, 2 rescuers
![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trajectories_7loc_l1.png)\(b\)7 locators, 3 rescuers
![Refer to caption](https://arxiv.org/html/2607.28679v1/images/trajectories_9loc_l1.png)\(c\)9 locators, 3 rescuers

Figure 3:Scalability across team sizes under a linear objective\. Increasing the number of locators improves coverage of the monitored region, while the rescuers adapt their paths to the denser set of detected emergencies\.TABLE I:Ablation and scalability results \(solve time, number of variables and number of constraints\) on SwarmLab search\-and\-rescue contingency\-planning simulations across MIP and SMT encodings\. \(\|ℒ\|\|\\mathcal\{L\}\|and\|ℛ\|\|\\mathcal\{R\}\|indicate the number of locator and rescuer agents respectively\. Reported times are totals over the scenario sweep \(\|Ω\|=4\|\\Omega\|\{=\}4for\|ℒ\|=5\|\\mathcal\{L\}\|\{=\}5,\|Ω\|=8\|\\Omega\|\{=\}8otherwise\); reported model sizes are those of the largest per\-scenario program\.†Per\-scenario time limit reached; best incumbent reported\. SMT is satisfaction\-only; objective ablations apply only to MIP\.\)MIP \(No Objective\)MIP \(Linear Objective\)MIP \(Quad\. Objective\)SMTCondition\|𝓛\|\\boldsymbol\{\|\\mathcal\{L\}\|\}\|𝓡\|\\boldsymbol\{\|\\mathcal\{R\}\|\}Time \(s\)\|Vars\|\|Constr\|Time \(s\)\|Vars\|\|Constr\|Time \(s\)\|Vars\|\|Constr\|Time \(s\)\|Vars\|\|Constr\|STL only\(No graph operators\)526960k125k1862†60k126k2591†60k126k0\.6621\.3k23\.2k73177105k146k3759†106k148k5216†106k148k1\.4923\.8k26\.6k93277146k210k3877†147k212k5300†147k212k1\.7435\.2k38\.5k𝒢s\\mathcal\{G\}^\{s\}\(Sensing\)5215174k143k1919†74k144k2659†74k144k2\.1323\.2k25\.2k73240135k185k3846†136k187k5311†136k187k3\.1527\.9k30\.7k93401182k257k4016†183k259k5434†183k259k2\.6140\.1k43\.4k𝒢s\+𝒢c\\mathcal\{G\}^\{s\}\+\\mathcal\{G\}^\{c\}\(Sens\. \+ Comm\.\)5217581k153k2032†81k154k2635†81k154k1\.2925\.2k27\.1k73362155k209k3940†155k211k5393†155k211k1\.8032\.1k34\.8k93459204k284k4154†206k287k5786†206k287k4\.0645\.1k48\.4k𝒢s,𝒢c,𝒢task\\mathcal\{G\}^\{s\},\\mathcal\{G\}^\{c\},\\mathcal\{G\}^\{\\mathrm\{task\}\}\(Sens\. \+ Comm \+ Task\)5234086k161k1201†87k162k2234†86k161k3\.5622\.0k24\.0k73775172k230k3750†173k232k5809†173k232k5\.6846\.9k49\.8k931480225k307k4973†226k309k5997†226k309k16\.5058\.2k61\.6kWe implement a planner for the aforementioned search\-and\-rescue example\. Letℳ\\mathcal\{M\}denote a fixed set of known assembly areas where emergencies may occur\. At planning time, the location of every assembly area is known, but it is unknown whether each assembly area contains an active emergency\. Locator agents patrol the assembly areas and observe their activation statuses when they enter the sensing range\. An active emergency must then be communicated, assigned to one or more rescuers, and resolved within bounded time by transporting the rescued individual to the rescue center𝒞\\mathcal\{C\}\. To account for potential emergencies, we construct plans for all possible emergency\-activation scenarios\.

The experimental instances use role\-specific admissible control sets while retaining the same motion\-model structure for all agents\.999Locator controls satisfy𝐮tℓ∈𝒰ℒ\\mathbf\{u\}\_\{t\}^\{\\ell\}\\in\\mathcal\{U\}\_\{\\mathcal\{L\}\}, whereas rescuer controls satisfy𝐮tr∈𝒰ℛ\\mathbf\{u\}\_\{t\}^\{r\}\\in\\mathcal\{U\}\_\{\\mathcal\{R\}\}, with the maximum rescuer speed strictly lower than the maximum locator speed\. Thus, the experimental role distinction includes different mobility limits in addition to different mission obligations\.

LetΩ⊆\{0,1\}\|ℳ\|\\Omega\\subseteq\\\{0,1\\\}^\{\|\\mathcal\{M\}\|\}denote the set of scenarios, whereωm=1\\omega\_\{m\}=1indicates that assembly areammcontains an active emergency in scenarioω\\omega, andωm=0\\omega\_\{m\}=0indicates that it does not\. If all activation combinations are considered, then\|Ω\|=2\|ℳ\|\|\\Omega\|=2^\{\|\\mathcal\{M\}\|\}\.

For each scenarioω∈Ω\\omega\\in\\Omega, the encoding contains a corresponding state and control sequence\. These scenario\-indexed sequences are solved jointly\. Scenarios with identical locator observation histories must have identical control inputs, i\.e\., if scenariosω\\omegaandω′\\omega^\{\\prime\}are indistinguishable from the agents at timett, then𝐔tω=𝐔tω′\\mathbf\{U\}\_\{t\}^\{\\omega\}=\\mathbf\{U\}\_\{t\}^\{\\omega^\{\\prime\}\}\. The plans may branch only after a locator observation distinguishes the scenarios\.

The resulting solution is a contingent plan represented as a finite scenario tree\. At runtime, the agents initially execute the common plan prefix\. When a locator observes whether an assembly area is active, the branch consistent with that observation is selected, and execution continues along that branch\. Further observations may select subsequent branches\.

The predicates and specifications below are instantiated for everyω∈Ω\\omega\\in\\Omega\. We suppress the scenario superscript when it is clear from context\. In scenarioω\\omega,φmemg\\varphi\_\{m\}^\{\\mathrm\{emg\}\}is true iffωm=1\\omega\_\{m\}=1\.

We introduce the following atomic predicates:φmemg\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\(emergency active\),φr,mnear\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}\(rescuer near emergency\),φratC\\varphi^\{\\mathrm\{atC\}\}\_\{r\}\(rescuer at rescue center\), andφrcarry\\varphi^\{\\mathrm\{carry\}\}\_\{r\}\(rescuer carrying an individual\)\. The joint geometric predicateφmsense\\varphi^\{\\mathrm\{sense\}\}\_\{m\}states that at least one locator lies within sensing range of emergencymm\. Graph\-derived predicates capture the remaining collective and relational conditions:φℓLL\\varphi^\{\\mathrm\{LL\}\}\_\{\\ell\}\(locator\-to\-locator communication\) andφℓLR\\varphi^\{\\mathrm\{LR\}\}\_\{\\ell\}\(locator\-to\-rescuer communication\)\. Letφℓ,r,mtask\\varphi\_\{\\ell,r,m\}^\{\\mathrm\{task\}\}denote the predicate that locatorℓ\\ellhas assigned rescuerrrspecifically to emergencymmat the current time\. Its truth implies that the corresponding task edge\(ℓ,r\)∈ℰttask\(\\ell,r\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathrm\{task\}\}is active\.

We fix horizonsTdet,Tassign,Trelay,Treach,Tdeliver∈ℕT\_\{\\mathrm\{det\}\},T\_\{\\mathrm\{assign\}\},T\_\{\\mathrm\{relay\}\},T\_\{\\mathrm\{reach\}\},T\_\{\\mathrm\{deliver\}\}\\in\\mathbb\{N\}\. The specifications for the mission are then outlined as follows\.

1. 1\.Bounded emergency detection\.Every emergency must be detected by the locator swarm within bounded time: ϕdetect:=𝐆​⋀m∈ℳ\(φmemg⇒𝐅\[0,Tdet\]​φmsense\)\.\\phi\_\{\\mathrm\{detect\}\}:=\\mathbf\{G\}\\;\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\Big\(\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\\Rightarrow\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{det\}\}\]\}\\;\\varphi^\{\\mathrm\{sense\}\}\_\{m\}\\Big\)\.
2. 2\.Detection\-to\-relay\.Once an emergency is detected, the information must be communicated to either another locator or a rescuer within bounded time: ϕrelay:=𝐆​⋀m∈ℳ\(φmemg∧φmsense⇒𝐅\[0,Trelay\]​⋁ℓ∈ℒ\(φℓLL∨φℓLR\)\)\.\\displaystyle\\phi\_\{\\mathrm\{relay\}\}:=\\mathbf\{G\}\\;\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\Big\(\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\\wedge\\varphi^\{\\mathrm\{sense\}\}\_\{m\}\\Rightarrow\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{relay\}\}\]\}\\,\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\(\\varphi^\{\\mathrm\{LL\}\}\_\{\\ell\}\\,\\vee\\,\\varphi^\{\\mathrm\{LR\}\}\_\{\\ell\}\)\\Big\)\.
3. 3\.Detection\-to\-assignment\.Once an emergency is detected, at least one locator must assign a rescuer within bounded time: ϕassign:=𝐆​⋀m∈ℳ\(φmemg∧φmsense⇒𝐅\[0,Tassign\]​⋁ℓ∈ℒ⋁r∈ℛφℓ,r,mtask\)\.\\displaystyle\\phi\_\{\\mathrm\{assign\}\}:=\\mathbf\{G\}\\;\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\Big\(\\varphi^\{\\mathrm\{emg\}\}\_\{m\}\\wedge\\varphi^\{\\mathrm\{sense\}\}\_\{m\}\\Rightarrow\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\;\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\;\\bigvee\_\{r\\in\\mathcal\{R\}\}\\varphi^\{\\mathrm\{task\}\}\_\{\\ell,r,m\}\\Big\)\.
4. 4\.Rescuer response time\.If a locator assigns a rescuer, that rescuer must reach the emergency within a bounded time: ϕreach:=𝐆⋀ℓ∈ℒ⋀r∈ℛ⋀m∈ℳ\(φℓ,r,mtask∧φmemg⇒\\displaystyle\\phi\_\{\\mathrm\{reach\}\}:=\\mathbf\{G\}\\bigwedge\_\{\\ell\\in\\mathcal\{L\}\}\\bigwedge\_\{r\\in\\mathcal\{R\}\}\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\Big\(\\varphi\_\{\\ell,r,m\}^\{\\mathrm\{task\}\}\\wedge\\varphi\_\{m\}^\{\\mathrm\{emg\}\}\\Rightarrow𝐅\[0,Treach\]φr,mnear\)\.\\displaystyle\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{reach\}\}\]\}\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}\\Big\)\.
5. 5\.Rescue and deliver\.After reaching the emergency, the rescuer must deliver the rescued individual to the rescue center: ϕdeliver\\displaystyle\\phi\_\{\\mathrm\{deliver\}\}:=𝐆⋀ℓ∈ℒ⋀r∈ℛ⋀m∈ℳ\(φℓ,r,mtask∧φr,mnear⇒\\displaystyle=\\mathbf\{G\}\\;\\bigwedge\_\{\\ell\\in\\mathcal\{L\}\}\\bigwedge\_\{r\\in\\mathcal\{R\}\}\\bigwedge\_\{m\\in\\mathcal\{M\}\}\\Big\(\\varphi\_\{\\ell,r,m\}^\{\\mathrm\{task\}\}\\wedge\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}\\Rightarrow𝐅\[0,Tdeliver\]\(φrcarry∧φratC\)\)\.\\displaystyle\\quad\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{deliver\}\}\]\}\\;\(\\varphi^\{\\mathrm\{carry\}\}\_\{r\}\\wedge\\varphi^\{\\mathrm\{atC\}\}\_\{r\}\)\\Big\)\.

For each scenarioω∈Ω\\omega\\in\\Omega, letϕω\\phi^\{\\omega\}denote the conjunction of the five mission specifications above under the activation assignmentω\\omega\. The scenario\-based planning problem requires⋀ω∈Ωϕω\\bigwedge\_\{\\omega\\in\\Omega\}\\phi^\{\\omega\}\. All experiments were conducted using Gurobi\[gurobi\]\(for MIP\) and Z3\[z3\]\(for SMT\), and were executed on a compute cluster with 16 CPU cores and 64 GB of memory\. The simulations were performed using a customized SwarmLab\[swarmlab\]framework, extended to incorporate our environment and dynamics and to execute the synthesized trajectories\.101010Satellite terrain image courtesy of NASA Earth Observatory \([https://earthobservatory\.nasa\.gov](https://earthobservatory.nasa.gov/)\)\.

Effect of objective function\.Figure[2](https://arxiv.org/html/2607.28679#S6.F2)shows the effect of the objective on rescuer trajectories with 5 locators and 2 rescuers\. Without an objective \(a\), the MIP returns an arbitrary feasible plan; the linear objective \(b\) and quadratic objective \(c\) progressively shape the rescuer toward more direct paths\.111111The linear objective is the rescuerL1L\_\{1\}path costJ1=∑r∈ℛ∑t=0T−1‖𝐩t\+1r−𝐩tr‖1J\_\{1\}=\\sum\_\{r\\in\\mathcal\{R\}\}\\sum\_\{t=0\}^\{T\-1\}\\\|\\mathbf\{p\}\_\{t\+1\}^\{r\}\-\\mathbf\{p\}\_\{t\}^\{r\}\\\|\_\{1\}\. The quadratic objective is the squaredL2L\_\{2\}step costJ2=∑r∈ℛ∑t=0T−1‖𝐩t\+1r−𝐩tr‖22J\_\{2\}=\\sum\_\{r\\in\\mathcal\{R\}\}\\sum\_\{t=0\}^\{T\-1\}\\\|\\mathbf\{p\}\_\{t\+1\}^\{r\}\-\\mathbf\{p\}\_\{t\}^\{r\}\\\|\_\{2\}^\{2\}\.Since SMT is satisfaction\-only, this comparison is specific to the MIP encoding and motivates retaining MIP for objective\-driven planning despite its larger encoding footprint\.

Scalability Evaluation with Increasing Graph Complexity and Team Size\.We evaluate the incremental impact of graph\-dependent constraints on planning complexity by progressively increasing specification complexity while keeping the environment, dynamics, and objective fixed\. Starting from a baseline of STL predicates \(no graph operators\), we add \(i\) sensing\-neighborhood constraints from a time\-varying sensing graph, \(ii\) communication\-neighborhood constraints from a time\-varying communication graph, and \(iii\) task constraints from a time\-varying task graph\. For each case, we further vary the number of locator and rescuer agents\. \(See Fig\.[3](https://arxiv.org/html/2607.28679#S6.F3)\)

Results\.Results are presented in Table[I](https://arxiv.org/html/2607.28679#S6.T1), which compares the numbers of variables and constraints and the time taken to find a solution across all ablations for both methods\. STL specifications without graph operators scale comparatively well across both solvers and serve as a clear baseline\. Adding sensing graphs increases complexity by coupling continuous agent states with logical satisfaction; communication graphs amplify this effect by enforcing pairwise proximity constraints that require joint reasoning over agent configurations; task graphs with decision\-dependent assignments yield a large increase in solve time and problem size for both solvers\. Quantitatively, SMT encodings result in fewer variables and constraints and exhibit faster solve times\. MIP encodings, despite larger size and longer solve times, are required for objective\-driven planning \(Fig\.[2](https://arxiv.org/html/2607.28679#S6.F2)\); for the hardest configuration \(\|ℒ\|=9,\|ℛ\|=3\|\\mathcal\{L\}\|=9,\|\\mathcal\{R\}\|=3, all graphs, quadratic objective\), the time limit was reached before optimality could be established, and Table[I](https://arxiv.org/html/2607.28679#S6.T1)reports the best incumbent\.

## VIIDiscussion

Related Work\.STL has been widely used for multi\-agent control and planning via optimization\-based synthesis, including robustness\-aware feedback formulations\[FormalMethodsMultiAgent,PPCSTL\]and MIP encodings with abstractions such as timed waypoints\[MultiAgentSTLWaypoints\]\. These approaches focus on individual agent trajectories and continuous dynamics, and do not explicitly capture graph\-based spatial relations or collective constraints\. To incorporate spatial structure, spatio\-temporal logics such as STREL introduce graph\-based reachability and escape operators\[STREL,STRELDynamicNetworks\], enabling the specification and monitoring of collective behaviors\. Learning\-based and synthesis approaches from STREL have also been explored\[NNSTREL\], but these works do not address optimization\-based planning via MIP or SMT\.

Several works employ SMT\- or SAT\-based encodings for multi\-agent planning under temporal logic constraints\. Compositional synthesis from safe LTL fragments using SMT improves scalability and correctness guarantees\[SMTMultiRobotSafeLTL\], while online or incremental planning under LTL has also been studied\[OnlineMultiRobotLTL\]\. Optimization\-based planning has further been explored via lazy SMT and MIP formulations\[shoukry2016scalable,SMTMultiRobotSafeLTL\]and SAT\-based convex optimization\[shoukry2017linear\], while MIP\-based waypoint formulations enable long\-horizon multi\-agent STL planning\[MultiAgentSTLWaypoints\]\. Capability Temporal Logic \(CaTL\) integrates temporal logic with task allocation, routing, and resource constraints for heterogeneous teams\[ProbabilisticCaTLCoordination,CaTLResourceConstraints\], typically formulating planning as a combinatorial optimization problem over assignments and schedules\. While CaTL adopts a centralized planning perspective similar to ours, its operators focus on capabilities and task satisfaction rather than spatio\-temporal reasoning over interaction graphs\.

Comparison with HyperLTL\.Hyperproperties have also been used to describe specifications for multi\-agent systems\[hsu2025hyprl,wang2020hyperproperties,finkbeiner2023logics\]\. Closest to our setting is the work of\[wang2020hyperproperties\], who use HyperLTL to plan for multi\-robot systems with relational objectives, and HypRL\[hsu2025hyprl\], which learns control policies from hyperproperty specifications in the decentralized model\-free setting \(ours is centralized and model\-based\)\.

Beyond this, HyperLTL is a propositional logic: it admits only Boolean atomic propositions, and joint predicates over multiple agents reduce to syntactic sugar for disjunctions of single\-agent predicates over discrete, grid\-like environments\. Encoding our specifications in HyperLTL also requires*reifying*every pointwise agent choice appearing inside a temporal operator, since HyperLTL admits only trace quantifiers at the outermost prefix\. For example, the locator and rescuer choices in the assignment specificationϕassign\\phi\_\{\\mathrm\{assign\}\}are expanded as disjunctions over the fixed setsℒ\\mathcal\{L\}andℛ\\mathcal\{R\},

ϕassign=∀πm\.𝐆\(φemg,πm∧φsense,πm⇒𝐅\[0,Tassign\]⋁ℓ∈ℒ⋁r∈ℛ𝗍𝖺𝗌𝗄πℓ,πr,πm\),\\phi\_\{\\mathrm\{assign\}\}=\\begin\{multlined\}\\forall\\pi\_\{m\}\.\\,\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\\!\\Rightarrow\\\!\\\\ \\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\\!\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\\!\\bigvee\_\{r\\in\\mathcal\{R\}\}\\\!\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\Big\),\\end\{multlined\}\\forall\\pi\_\{m\}\.\\,\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\\!\\Rightarrow\\\!\\\\ \\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\\!\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\\!\\bigvee\_\{r\\in\\mathcal\{R\}\}\\\!\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\Big\),or a Skolemization that lifts the existentials to the prefix at the cost of one alternation, yielding a∀∃\\forall\\existsformula outside the alternation\-free fragment\. The reach and delivery formulas, by contrast, use fixed universal prefixes but require joint predicates such asφℓ,r,mtask\\varphi^\{\\mathrm\{task\}\}\_\{\\ell,r,m\}andφr,mnear\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}to be represented as multi\-trace atomic propositions\. STL\-GO evaluates these finite agent choices pointwise and supports joint predicates directly; the full reifications are deferred to Appendix[E](https://arxiv.org/html/2607.28679#A5)\.

Additionally, to compare the encodings of HyperLTL and STL\-GO empirically, we adapt the wildfire\-rescue grid\-world benchmark from HypRL\[hsu2025hyprl\], where the authors consider𝒩×𝒩\\mathcal\{N\}\\times\\mathcal\{N\}grids where3≤𝒩≤103\\leq\\mathcal\{N\}\\leq 10\. A firefighter agent must extinguish all fire cells while a medic agent rescues all victim cells; the two agents must stay within a bounded communication range, and the medic cannot enter a fire cell until the firefighter has extinguished it\. We encode the mission in HyperLTL and STL\-GO and solve each under MIP and SMT backends; the full specification and encoding details are reported in Appendix[E](https://arxiv.org/html/2607.28679#A5)\. The results in Table[II](https://arxiv.org/html/2607.28679#S7.T2)show that as the grid grows, HyperLTL encodings incur anO​\(T⋅N4\)O\(T\\cdot N^\{4\}\)constraint blow\-up from the pairwise\-cell enumeration required by the communication\-range constraint: byN=10N\{=\}10, HyperLTL \+ SMT generates 355k constraints versus 2\.4k for STL\-GO \+ SMT\. STL\-GO’s graph operators encode the same coordination through real\-valued predicates, with constraint counts growing linearly inTT\.

TABLE II:Comparison of HyperLTL and STL\-GO encodings on𝒩×𝒩\\mathcal\{N\}\{\\times\}\\mathcal\{N\}grids \(T=4​\(𝒩−1\)\+2T=4\(\\mathcal\{N\}\{\-\}1\)\+2\)\.𝒩\\mathcal\{N\}Method\|Var\.\|\|Constr\.\|Time \(s\)5×\\times5HyperLTL \+ SMT388\.6k0\.10STL\-GO \+ SMT3958880\.15HyperLTL \+ MIP1\.0k8\.8k0\.20STL\-GO \+ MIP1\.2k12\.7k0\.107×\\times7HyperLTL \+ SMT5454\.2k0\.61STL\-GO \+ SMT6711\.4k0\.34HyperLTL \+ MIP2\.8k54\.7k2\.39STL\-GO \+ MIP3\.0k65\.3k0\.3510×\\times10HyperLTL \+ SMT78355\.1k4\.26STL\-GO \+ SMT1\.2k2\.4k0\.99HyperLTL \+ MIP8\.2k356\.2k4\.47STL\-GO \+ MIP8\.5k387\.5k1\.96Conclusions\.We presented a synthesis framework for spatio\-temporal logical specifications with graph operators on multi\-agent systems\. The MIP and SMT encodings of STL\-GO enable centralized planning over dynamic interaction graphs, with soundness guarantees\. Our simulations demonstrate trajectory synthesis under complex STL\-GO specifications involving multiple dynamic graphs and role\-typed agents\.

Limitations and Future Work\.Our soundness guarantees rely on deterministic environment and agent dynamics\. In stochastic settings, the synthesized plans can only be guaranteed to satisfy the specification with some probability, and encodings for distributionally robust formulations are an extension\. As we synthesize open\-loop control sequences, embedding encodings inside a receding\-horizon loop or learning policies that respect STL\-GO specifications are open directions\. Furthermore, decentralized synthesis under partial observability, together with decomposition strategies to mitigate the combinatorial growth in the number of graphs, remains for future work\.

## VIIIAcknowledgements

This work was supported by the National Science Foundation under Grant IIS\-SLES\-2417075 and Lockheed Martin Advanced Technology Laboratories\.

## References

## Appendix ATheoretical Results for MIP Encoding

### A\-AProof of Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6)\(MIP, Agent\-Local\)

###### Proof\.

We prove the invariant \([12](https://arxiv.org/html/2607.28679#S4.E12)\) for every agent\-local subformulaψ\\psi, agentii, and timett, by structural induction onψ\\psi\.

Dynamics\.Constraint \([3](https://arxiv.org/html/2607.28679#S4.E3)\) is an equality in the decision variables; any feasible assignment to\{𝐱ti,𝐮ti\}i,t\\\{\\mathbf\{x\}^\{i\}\_\{t\},\\mathbf\{u\}^\{i\}\_\{t\}\\\}\_\{i,t\}corresponds to a trajectory ofFF, with \([4](https://arxiv.org/html/2607.28679#S4.E4)\) restricting states and inputs to their admissible sets\.

Base case \(ψ=μx\\psi=\\mu\_\{x\}\)\.The Big\-MMencoding \(Appendix[C](https://arxiv.org/html/2607.28679#A3)\) introduceszμx,i,t∈\{0,1\}z\_\{\\mu\_\{x\},i,t\}\\in\\\{0,1\\\}withMMlarger thansupx∈\[𝐱min,𝐱max\]\|a⊤​x−b\|\\sup\_\{x\\in\[\\mathbf\{x\}\_\{\\min\},\\mathbf\{x\}\_\{\\max\}\]\}\|a^\{\\top\}x\-b\|and assumes feasible predicate values avoid the separation interval\(−ε,0\)\(\-\\varepsilon,0\)\. It enforceszμx,i,t=1⇔a⊤​𝐱ti≥bz\_\{\\mu\_\{x\},i,t\}=1\\iff a^\{\\top\}\\mathbf\{x\}^\{i\}\_\{t\}\\geq b, which is the definition of\(ℳ​𝒜,i,t\)⊧μx\(\\mathcal\{MA\},i,t\)\\models\\mu\_\{x\}\.

Boolean connectives and until operator\.Negation usesz¬φ,i,t=1−zφ,i,tz\_\{\\neg\\varphi,i,t\}=1\-z\_\{\\varphi,i,t\}; conjunction and disjunction use standard linear encodings; whent\+b≤Tt\+b\\leq T, until uses witness\-time indicatorsβτ,ti\\beta^\{i\}\_\{\\tau,t\}enforcing the existence ofτ∈t⊕I\\tau\\in t\\oplus Iwithzφ2,i,τ=1z\_\{\\varphi\_\{2\},i,\\tau\}=1andzφ1,i,τ′=1z\_\{\\varphi\_\{1\},i,\\tau^\{\\prime\}\}=1for allτ′∈\[t,τ\)\\tau^\{\\prime\}\\in\[t,\\tau\); whent\+b\>Tt\+b\>T, its satisfaction variable is fixed to zero\[stl\-to\-milp1,stl\-to\-milp2\]\.

Graph operator \(ψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphi\)\.We establish the invariant for each graph type𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, then extend to the modal quantifier\.

*\(i\) Eligibility\.*By MIP\-encodability ofΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}, the edge indicatoraj,i,t𝚝𝚢𝚙𝚎a\_\{j,i,t\}^\{\\mathtt\{type\}\}exactly representsηj,i𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)\\eta\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)and the weightwt𝚝𝚢𝚙𝚎​\(j,i\)w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)is a PWA expression in the MIP variables\. WithM\>max⁡\(\|wmin\|,\|wmax\|\)\+sup\|wt𝚝𝚢𝚙𝚎​\(j,i\)\|M\>\\max\(\|w\_\{\\min\}\|,\|w\_\{\\max\}\|\)\+\\sup\|w\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\|and the stated separation margin, \([5](https://arxiv.org/html/2607.28679#S4.E5)\) enforcesγj,i,t𝚝𝚢𝚙𝚎=1\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}=1if and only if\(j,i\)∈ℰt𝚝𝚢𝚙𝚎\(j,i\)\\in\\mathcal\{E\}\_\{t\}^\{\\mathtt\{type\}\}andwt𝚝𝚢𝚙𝚎​\(j,i\)∈Ww\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\\in W\.

*\(ii\) Conjunction\.*\([6](https://arxiv.org/html/2607.28679#S4.E6)\) is the standard linear encoding ofyj,i,tφ,𝚝𝚢𝚙𝚎=γj,i,t𝚝𝚢𝚙𝚎∧zφ,j,ty\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}=\\gamma\_\{j,i,t\}^\{\\mathtt\{type\}\}\\wedge z\_\{\\varphi,j,t\}; by inductive hypothesis onφ\\varphiatjj,yj,i,tφ,𝚝𝚢𝚙𝚎=1y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}=1iff edge\(j,i\)\(j,i\)is eligible and\(ℳ​𝒜,j,t\)⊧φ\(\\mathcal\{MA\},j,t\)\\models\\varphi\.

*\(iii\) Cardinality\.*The integer countci,tIn,φ,𝚝𝚢𝚙𝚎=∑j≠iyj,i,tφ,𝚝𝚢𝚙𝚎c\_\{i,t\}^\{\\mathrm\{In\},\\varphi,\\mathtt\{type\}\}=\\sum\_\{j\\neq i\}y\_\{j,i,t\}^\{\\varphi,\\mathtt\{type\}\}is the cardinality of the qualifying neighbor set\. Sinceccis integer\-valued, the strict inequalitiesc<e1c<e\_\{1\}andc\>e2c\>e\_\{2\}are equivalent toc≤e1−1c\\leq e\_\{1\}\-1andc≥e2\+1c\\geq e\_\{2\}\+1; thus, the unit integer separation in \([7](https://arxiv.org/html/2607.28679#S4.E7)\)–\([8](https://arxiv.org/html/2607.28679#S4.E8)\) enforceszψ,i,t𝚝𝚢𝚙𝚎=1⇔c∈\[e1,e2\]z\_\{\\psi,i,t\}^\{\\mathtt\{type\}\}=1\\iff c\\in\[e\_\{1\},e\_\{2\}\]\.

*\(iv\) Quantification over types\.*\([10](https://arxiv.org/html/2607.28679#S4.E10)\) for\#=∃\\\#=\\existsand \([11](https://arxiv.org/html/2607.28679#S4.E11)\) for\#=∀\\\#=\\forallare the standard disjunction and conjunction encodings over per\-type variables\. The outgoing case is obtained by substituting\(j,i\)\(j,i\)with\(i,j\)\(i,j\)in \(i\)–\(iii\)\.

By induction, \([12](https://arxiv.org/html/2607.28679#S4.E12)\) holds for every subformula at every\(i,t\)\(i,t\); the encoding assertszϕ,i,0=1z\_\{\\phi,i,0\}=1for the agent\-local root, so feasibility yields\(ℳ​𝒜,i,0\)⊧ϕ\(\\mathcal\{MA\},i,0\)\\models\\phi\. ∎

### A\-BProof of Theorem[7](https://arxiv.org/html/2607.28679#Thmtheorem7)

###### Proof\.

We extend \([12](https://arxiv.org/html/2607.28679#S4.E12)\) to multi\-agent subformulas aszψ,t=1⇔\(ℳ​𝒜,t\)⊧ψz\_\{\\psi,t\}=1\\iff\(\\mathcal\{MA\},t\)\\models\\psi, by structural induction on the multi\-agent grammar\.

Joint atomic predicate \(ψ=μ\\psi=\\mu\)\.The Big\-MMencoding applied toμ​\(𝐗t,𝐰t\)\\mu\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)enforceszμ,t=1⇔μ​\(𝐗t,𝐰t\)z\_\{\\mu,t\}=1\\iff\\mu\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)by the same argument as the agent\-local atomic case\.

Embedding \(ψ=i\.φ\\psi=i\.\\varphi\)\.The encoding setszi\.φ,t:=zφ,i,tz\_\{i\.\\varphi,t\}:=z\_\{\\varphi,i,t\}, which by Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6)equals the truth ofφ\\varphiat\(i,t\)\(i,t\)\.

Boolean connectives and until operator\.Identical in form to the agent\-local cases of Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6), applied to multi\-agent variables\.

Multi\-agent quantifiers \(ψ=𝐄𝐗​φ,𝐅𝐀​φ\\psi=\\mathbf\{EX\}\\varphi,\\mathbf\{FA\}\\varphi\)\.The encodings in Section[IV\-C](https://arxiv.org/html/2607.28679#S4.SS3)enforcezψ,t=1⇔⋁i∈𝒱zφ,i,t=1z\_\{\\psi,t\}=1\\iff\\bigvee\_\{i\\in\\mathcal\{V\}\}z\_\{\\varphi,i,t\}=1andzψ,t=1⇔⋀i∈𝒱zφ,i,t=1z\_\{\\psi,t\}=1\\iff\\bigwedge\_\{i\\in\\mathcal\{V\}\}z\_\{\\varphi,i,t\}=1\. By Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6), these match the multi\-agent semantics\.

By induction the invariant holds at the root:zϕ,0=1⇔\(ℳ​𝒜,0\)⊧ϕz\_\{\\phi,0\}=1\\iff\(\\mathcal\{MA\},0\)\\models\\phi, and feasibility withzϕ,0=1z\_\{\\phi,0\}=1as a constraint yields\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\. ∎

## Appendix BTheoretical Results of SMT Encoding

### B\-AProof of Lemma[8](https://arxiv.org/html/2607.28679#Thmtheorem8)\(SMT, Agent\-Local\)

###### Proof\.

We prove the invariant \([23](https://arxiv.org/html/2607.28679#S5.E23)\) for every agent\-local subformulaψ\\psi, agentii, and timett, by structural induction onψ\\psi\. The argument mirrors the proof of Lemma[6](https://arxiv.org/html/2607.28679#Thmtheorem6), with Big\-MMencodings replaced by LRA biconditionals\.

Dynamics\.Constraint \([16](https://arxiv.org/html/2607.28679#S5.E16)\) is an equality in the SMT variables; any satisfying assignment corresponds to a trajectory ofFF, with \([15](https://arxiv.org/html/2607.28679#S5.E15)\) restricting states and inputs\.

Base case, Boolean connectives, and until operator\.Atomic predicates usezμx,ti=\(a⊤​𝐱ti−b≥0\)z^\{i\}\_\{\\mu\_\{x\},t\}=\(a^\{\\top\}\\mathbf\{x\}^\{i\}\_\{t\}\-b\\geq 0\)\. Boolean connectives use the corresponding propositional biconditionals\. Whent\+b≤Tt\+b\\leq T, until is unrolled over the bounded horizon aszψ,ti=⋁τ=t\+at\+b\(zφ2,τi∧⋀k=tτ−1zφ1,ki\)z^\{i\}\_\{\\psi,t\}=\\bigvee\_\{\\tau=t\+a\}^\{t\+b\}\\big\(z^\{i\}\_\{\\varphi\_\{2\},\\tau\}\\wedge\\bigwedge\_\{k=t\}^\{\\tau\-1\}z^\{i\}\_\{\\varphi\_\{1\},k\}\\big\); whent\+b\>Tt\+b\>T, its satisfaction variable is fixed to⊥\\bot\[momtaz2023monitoring,prabhakar2018automatic\]\. Each case transfers \([23](https://arxiv.org/html/2607.28679#S5.E23)\) via the inductive hypothesis\.

Graph operator \(ψ=In𝓖,\[e1,e2\]W,\#​φ\\psi=\\mathrm\{In\}\_\{\\boldsymbol\{\\mathcal\{G\}\},\[e\_\{1\},e\_\{2\}\]\}^\{W,\\\#\}\\varphi\)\.For each𝚝𝚢𝚙𝚎∈𝒯\\mathtt\{type\}\\in\\mathcal\{T\}, SMT\-encodability ofΓ𝚝𝚢𝚙𝚎\\Gamma^\{\\mathtt\{type\}\}ensures that the edge\-existence predicateηj,i𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)\\eta\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)is an LRA\+LIA Boolean formula and the weightej,i𝚝𝚢𝚙𝚎​\(𝐗t,𝐰t\)e\_\{j,i\}^\{\\mathtt\{type\}\}\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)is an LRA expression\.

*\(i\) Eligibility\.*\([18](https://arxiv.org/html/2607.28679#S5.E18)\) assertsbj,i,t𝚝𝚢𝚙𝚎↔\(ηj,i𝚝𝚢𝚙𝚎∧wmin≤e𝚝𝚢𝚙𝚎≤wmax\)b^\{\\mathtt\{type\}\}\_\{j,i,t\}\\leftrightarrow\(\\eta^\{\\mathtt\{type\}\}\_\{j,i\}\\wedge w\_\{\\min\}\\leq e^\{\\mathtt\{type\}\}\\leq w\_\{\\max\}\), givingbj,i,t𝚝𝚢𝚙𝚎=⊤b^\{\\mathtt\{type\}\}\_\{j,i,t\}=\\topif and only if\(j,i\)\(j,i\)is an edge andwt𝚝𝚢𝚙𝚎​\(j,i\)∈Ww\_\{t\}^\{\\mathtt\{type\}\}\(j,i\)\\in W\.

*\(ii\) Conjunction\.*\([19](https://arxiv.org/html/2607.28679#S5.E19)\) assertsnj,i,t𝚝𝚢𝚙𝚎=bj,i,t𝚝𝚢𝚙𝚎∧zφ,tjn^\{\\mathtt\{type\}\}\_\{j,i,t\}=b^\{\\mathtt\{type\}\}\_\{j,i,t\}\\wedge z^\{j\}\_\{\\varphi,t\}; by inductive hypothesis,nj,i,t𝚝𝚢𝚙𝚎=⊤n^\{\\mathtt\{type\}\}\_\{j,i,t\}=\\topiff edge\(j,i\)\(j,i\)is eligible and\(ℳ​𝒜,j,t\)⊧φ\(\\mathcal\{MA\},j,t\)\\models\\varphi\.

*\(iii\) Cardinality\.*\([21](https://arxiv.org/html/2607.28679#S5.E21)\) assertszψ,ti,𝚝𝚢𝚙𝚎=\(e1≤ci,t𝚝𝚢𝚙𝚎≤e2\)z^\{i,\\mathtt\{type\}\}\_\{\\psi,t\}=\(e\_\{1\}\\leq c^\{\\mathtt\{type\}\}\_\{i,t\}\\leq e\_\{2\}\), whereci,t𝚝𝚢𝚙𝚎c^\{\\mathtt\{type\}\}\_\{i,t\}, defined by \([20](https://arxiv.org/html/2607.28679#S5.E20)\), counts the qualifying neighbors via𝗂𝗍𝖾\\mathsf\{ite\}\.

*\(iv\) Quantification over types\.*\([22](https://arxiv.org/html/2607.28679#S5.E22)\) asserts the disjunctive biconditional for\#=∃\\\#=\\exists; replacing the disjunction with a conjunction yields the biconditional for\#=∀\\\#=\\forall\. The outgoing case is obtained by substituting\(j,i\)\(j,i\)with\(i,j\)\(i,j\)in \(i\)–\(iii\)\.

By induction, \([23](https://arxiv.org/html/2607.28679#S5.E23)\) holds for every subformula at every\(i,t\)\(i,t\); the encoding assertszϕ,0i=⊤z^\{i\}\_\{\\phi,0\}=\\topfor the agent\-local root, so satisfiability yields\(ℳ​𝒜,i,0\)⊧ϕ\(\\mathcal\{MA\},i,0\)\\models\\phi\. ∎

### B\-BProof of Theorem[9](https://arxiv.org/html/2607.28679#Thmtheorem9)\(SMT, Multi\-Agent\)

###### Proof\.

We extend \([23](https://arxiv.org/html/2607.28679#S5.E23)\) to multi\-agent subformulas aszψ,t=⊤⇔\(ℳ𝒜,t\)⊧ψz\_\{\\psi,t\}=\\top\\iff\(\\mathcal\{MA\},t\)\\models\\psi, by structural induction on the multi\-agent grammar\.

Joint atomic predicate \(ψ=μ\\psi=\\mu\)\.The LRAzμ,t=μ​\(𝐗t,𝐰t\)z\_\{\\mu,t\}=\\mu\(\\mathbf\{X\}\_\{t\},\\mathbf\{w\}\_\{t\}\)matches the multi\-agent atomic semantics\.

Embedding \(ψ=i\.φ\\psi=i\.\\varphi\)\.The encoding setszi\.φ,t:=zφ,tiz\_\{i\.\\varphi,t\}:=z^\{i\}\_\{\\varphi,t\}, which by Lemma[8](https://arxiv.org/html/2607.28679#Thmtheorem8)equals the truth ofφ\\varphiat\(i,t\)\(i,t\)\.

Boolean connectives and until operator\.Identical in form to the agent\-local cases of Lemma[8](https://arxiv.org/html/2607.28679#Thmtheorem8), applied to multi\-agent variables\.

Multi\-agent quantifiers \(ψ=𝐄𝐗​φ,𝐅𝐀​φ\\psi=\\mathbf\{EX\}\\varphi,\\mathbf\{FA\}\\varphi\)\.The encoding of the multi\-agent quantifiers𝐄𝐗\\mathbf\{EX\}and𝐅𝐀\\mathbf\{FA\}assertszψ,t=⋁i∈𝒱zφ,tiz\_\{\\psi,t\}=\\bigvee\_\{i\\in\\mathcal\{V\}\}z^\{i\}\_\{\\varphi,t\}andzψ,t=⋀i∈𝒱zφ,tiz\_\{\\psi,t\}=\\bigwedge\_\{i\\in\\mathcal\{V\}\}z^\{i\}\_\{\\varphi,t\}\. By Lemma[8](https://arxiv.org/html/2607.28679#Thmtheorem8), these match the multi\-agent quantifier semantics\.

By induction the invariant holds at the root:zϕ,0=⊤⇔\(ℳ𝒜,0\)⊧ϕz\_\{\\phi,0\}=\\top\\iff\(\\mathcal\{MA\},0\)\\models\\phi, and satisfiability withzϕ,0=⊤z\_\{\\phi,0\}=\\topas a constraint yields\(ℳ​𝒜,0\)⊧ϕ\(\\mathcal\{MA\},0\)\\models\\phi\. ∎

## Appendix CFull Mixed Integer Encoding for STL\-GO

Predicate Encoding\.Atomic predicates in STL\-GO formulas are inequalities of the formψ:=μ​\(xti\)\\psi:=\\mu\(x\_\{t\}^\{i\}\)whereμ​\(xti\)≡a⊤​xti−b≥0\\mu\(x\_\{t\}^\{i\}\)\\equiv a^\{\\top\}x\_\{t\}^\{i\}\-b\\geq 0, representing a geometric or logical condition on the agent’s state \(for instance, being within a goal region or a communication range\)\. Each predicateψ\\psiis associated with a binary variablezψ,ti∈\{0,1\}z\_\{\\psi,t\}^\{i\}\\in\\\{0,1\\\}indicating whetherψ\\psiholds for agentiiat timett\. The relationship between the constraint and the binary indicator is established using the Big\-MMmethod:

a⊤​xti−b≥−M​\(1−zψ,ti\);a⊤​xti−b≤−ε\+M​zψ,tia^\{\\top\}x\_\{t\}^\{i\}\-b\\geq\-M\(1\-z\_\{\\psi,t\}^\{i\}\);\\quad a^\{\\top\}x\_\{t\}^\{i\}\-b\\leq\-\\varepsilon\+Mz\_\{\\psi,t\}^\{i\}whereM\>0M\>0is a sufficiently large constant andε\>0\\varepsilon\>0is a small positive separation margin\. We assume feasible predicate values do not lie in\(−ε,0\)\(\-\\varepsilon,0\)\. These constraints ensure thatzψ,ti=1z\_\{\\psi,t\}^\{i\}=1if and only ifψ\\psiholds\.

Logical Operators\.

Letψ=Op⁡\(φ1,…,φm\)\\psi=\\operatorname\{Op\}\(\\varphi\_\{1\},\\ldots,\\varphi\_\{m\}\)denote a formula obtained by applying a logical operator to subformulasφ1,…,φm\\varphi\_\{1\},\\ldots,\\varphi\_\{m\}\. For each agentiiand timett, we introduce a binary variablezψ,ti∈\{0,1\}z\_\{\\psi,t\}^\{i\}\\in\\\{0,1\\\}encoding the truth value ofψ\\psi\. Standard linear encodings are used:

- •Negation: \(ψ=¬φ\\psi=\\neg\\varphi\)zψ,ti=1−zφ,ti\.z\_\{\\psi,t\}^\{i\}=1\-z\_\{\\varphi,t\}^\{i\}\.
- •Conjunction:\(ψ=⋀j=1mφj\\psi=\\bigwedge\_\{j=1\}^\{m\}\\varphi\_\{j\}\)zψ,ti≤zφj,ti​∀j,zψ,ti≥1−m\+∑j=1mzφj,ti\.z\_\{\\psi,t\}^\{i\}\\leq z\_\{\\varphi\_\{j\},t\}^\{i\}\\ \\forall j,\\ \\ z\_\{\\psi,t\}^\{i\}\\geq 1\-m\+\\sum\_\{j=1\}^\{m\}z\_\{\\varphi\_\{j\},t\}^\{i\}\.
- •Disjunction:\(ψ=⋁j=1mφj\\psi=\\bigvee\_\{j=1\}^\{m\}\\varphi\_\{j\}\)zψ,ti≥zφj,ti​∀j,zψ,ti≤∑j=1mzφj,ti\.z\_\{\\psi,t\}^\{i\}\\geq z\_\{\\varphi\_\{j\},t\}^\{i\}\\ \\forall j,\\ \\ z\_\{\\psi,t\}^\{i\}\\leq\\sum\_\{j=1\}^\{m\}z\_\{\\varphi\_\{j\},t\}^\{i\}\.

Temporal Operators\.

Temporal modalities in STL\-GO are represented over bounded time horizons using recursive constraints on binary variables\. The fundamental operator is*until*\(𝐔\\mathbf\{U\}\);*eventually*\(𝐅\\mathbf\{F\}\) and*always*\(𝐆\\mathbf\{G\}\) are defined as𝐅I​φ:=⊤𝐔I​φ\\mathbf\{F\}\_\{I\}\\varphi:=\\top\\,\\mathbf\{U\}\_\{I\}\\,\\varphiand𝐆I​φ:=¬𝐅I​¬φ\\mathbf\{G\}\_\{I\}\\varphi:=\\neg\\mathbf\{F\}\_\{I\}\\neg\\varphi\.

- •Until\.Forψ=φ1​𝐔\[a,b\]​φ2\\psi=\\varphi\_\{1\}\\,\\mathbf\{U\}\_\{\[a,b\]\}\\,\\varphi\_\{2\}andt\+b≤Tt\+b\\leq T, satisfaction requires thatφ2\\varphi\_\{2\}becomes true at some timeτ∈\[t\+a,t\+b\]\\tau\\in\[t\+a,t\+b\]and thatφ1\\varphi\_\{1\}holds at every time in\[t,τ\)\[t,\\tau\)\. Introduce auxiliary variablesβτ,ti∈\{0,1\}\\beta\_\{\\tau,t\}^\{i\}\\in\\\{0,1\\\}, one for each candidate witness time: βτ,ti≤zφ2,τi,βτ,ti≤zφ1,ki∀k∈\[t,τ−1\],βτ,ti≥zφ2,τi\+∑k=tτ−1zφ1,ki−\(τ−t\),zψ,ti≥βτ,ti∀τ∈\[t\+a,t\+b\],zψ,ti≤∑τ=t\+at\+bβτ,ti\.\\begin\{gathered\}\\beta\_\{\\tau,t\}^\{i\}\\leq z\_\{\\varphi\_\{2\},\\tau\}^\{i\},\\\\ \\beta\_\{\\tau,t\}^\{i\}\\leq z\_\{\\varphi\_\{1\},k\}^\{i\}\\quad\\forall k\\in\[t,\\tau\-1\],\\\\ \\beta\_\{\\tau,t\}^\{i\}\\geq z\_\{\\varphi\_\{2\},\\tau\}^\{i\}\+\\sum\_\{k=t\}^\{\\tau\-1\}z\_\{\\varphi\_\{1\},k\}^\{i\}\-\(\\tau\-t\),\\\\ z\_\{\\psi,t\}^\{i\}\\geq\\beta\_\{\\tau,t\}^\{i\}\\quad\\forall\\tau\\in\[t\+a,t\+b\],\\\\ z\_\{\\psi,t\}^\{i\}\\leq\\sum\_\{\\tau=t\+a\}^\{t\+b\}\\beta\_\{\\tau,t\}^\{i\}\.\\end\{gathered\}\(24\)Fort\+b\>Tt\+b\>T, the strong bounded\-horizon semantics are enforced byzψ,ti=0z\_\{\\psi,t\}^\{i\}=0\.
- •Eventually\.Forψ=𝐅\[a,b\]​φ\\psi=\\mathbf\{F\}\_\{\[a,b\]\}\\varphi, apply the derivation𝐅\[a,b\]​φ:=⊤𝐔\[a,b\]​φ\\mathbf\{F\}\_\{\[a,b\]\}\\varphi:=\\top\\,\\mathbf\{U\}\_\{\[a,b\]\}\\,\\varphiand the encoding simplifies sincez⊤,ti=1z\_\{\\top,t\}^\{i\}=1always holds: Fort\+b≤Tt\+b\\leq T, impose zψ,ti\\displaystyle z\_\{\\psi,t\}^\{i\}≥zφ,τi\\displaystyle\\geq z\_\{\\varphi,\\tau\}^\{i\}∀τ∈\[t\+a,t\+b\],\\displaystyle\\forall\\tau\\in\[t\+a,t\+b\],\(25\)zψ,ti\\displaystyle z\_\{\\psi,t\}^\{i\}≤∑τ=t\+at\+bzφ,τi\.\\displaystyle\\leq\\sum\_\{\\tau=t\+a\}^\{t\+b\}z\_\{\\varphi,\\tau\}^\{i\}\.Fort\+b\>Tt\+b\>T, imposezψ,ti=0z\_\{\\psi,t\}^\{i\}=0\. This ensureszψ,ti=1z\_\{\\psi,t\}^\{i\}=1ifφ\\varphiholds at least once within\[t\+a,t\+b\]\[t\+a,t\+b\]\.
- •Globally:Forψ=𝐆\[a,b\]​φ\\psi=\\mathbf\{G\}\_\{\[a,b\]\}\\varphi, apply the derivation𝐆\[a,b\]​φ:=¬𝐅\[a,b\]​¬φ\\mathbf\{G\}\_\{\[a,b\]\}\\varphi:=\\neg\\mathbf\{F\}\_\{\[a,b\]\}\\neg\\varphi\. Fort\+b≤Tt\+b\\leq T, impose zψ,ti\\displaystyle z\_\{\\psi,t\}^\{i\}≤zφ,τi\\displaystyle\\leq z\_\{\\varphi,\\tau\}^\{i\}∀τ∈\[t\+a,t\+b\],\\displaystyle\\forall\\tau\\in\[t\+a,t\+b\],\(26\)zψ,ti\\displaystyle z\_\{\\psi,t\}^\{i\}≥∑τ=t\+at\+bzφ,τi−\(b−a\)\.\\displaystyle\\geq\\sum\_\{\\tau=t\+a\}^\{t\+b\}z\_\{\\varphi,\\tau\}^\{i\}\-\(b\-a\)\.Fort\+b\>Tt\+b\>T, imposezψ,ti=1z\_\{\\psi,t\}^\{i\}=1\. This enforceszψ,ti=1z\_\{\\psi,t\}^\{i\}=1only ifφ\\varphiholds at all times in\[t\+a,t\+b\]\[t\+a,t\+b\]\.

## Appendix DFull SMT Encoding for STL\-GO

Atomic Predicates\.For each atomic predicateμ\\mu, we associate a Boolean satisfaction variablezμ,ti∈\{𝑡𝑟𝑢𝑒,𝑓𝑎𝑙𝑠𝑒\}z\_\{\\mu,t\}^\{i\}\\in\\\{\\mathit\{true\},\\mathit\{false\}\\\}, to indicate the satisfaction ofμ\\mufor agentiiat timett\. We encode the semantics of the predicate by asserting the following logical equivalence in the Theory of Linear Real Arithmetic \(LRA\):

zμ,ti=𝑡𝑟𝑢𝑒↔\(a⊤​xti−b≥0\)\.z\_\{\\mu,t\}^\{i\}=\\mathit\{true\}\\;\\leftrightarrow\\;\(a^\{\\top\}x\_\{t\}^\{i\}\-b\\geq 0\)\.This constraint couples the discrete Boolean structure with the continuous state vectorxtix\_\{t\}^\{i\}, allowing the solver to reason about system states\.

Logical operators\.

- •Negation\.We encode a formulaψ=¬φ\\psi=\\neg\\varphiby imposing the constraint zψ,ti=¬zφ,tiz\_\{\\psi,t\}^\{i\}=\\neg z\_\{\\varphi,t\}^\{i\}\(27\)for each agentiiand timett\. This enforces that the negated formula holds at\(i,t\)\(i,t\)if and only if the inner subformula does not hold at\(i,t\)\(i,t\)\.
- •Conjunction\.For a formulaψ=φ1∧φ2\\psi=\\varphi\_\{1\}\\wedge\\varphi\_\{2\}, we add the constraint zψ,ti=zφ1,ti∧zφ2,tiz\_\{\\psi,t\}^\{i\}=z\_\{\\varphi\_\{1\},t\}^\{i\}\\wedge z\_\{\\varphi\_\{2\},t\}^\{i\}\(28\)
- •Disjunction\.Similarly,ψ=φ1∨φ2\\psi=\\varphi\_\{1\}\\vee\\varphi\_\{2\}is encoded as zψ,ti=zφ1,ti∨zφ2,tiz\_\{\\psi,t\}^\{i\}=z\_\{\\varphi\_\{1\},t\}^\{i\}\\vee z\_\{\\varphi\_\{2\},t\}^\{i\}\(29\)

Temporal operators\.Temporal operators are encoded by imposing constraints onzψ,tiz\_\{\\psi,t\}^\{i\}to satisfy subformulas within the time interval\. We eliminate temporal quantifiers by unrolling them into finite conjunctions and disjunctions over the bounded time horizon, thereby generating a quantifier\-free encoding\.

- •Until\.For a formulaψ=φ1​𝐔\[a,b\]​φ2\\psi=\\varphi\_\{1\}\\,\\mathbf\{U\}\_\{\[a,b\]\}\\,\\varphi\_\{2\}, its discrete\-time semantics is captured by the constraint zψ,ti=\{⋁τ=t\+at\+b\(zφ2,τi∧⋀k=tτ−1zφ1,ki\),t\+b≤T,𝑓𝑎𝑙𝑠𝑒,t\+b\>T\.z\_\{\\psi,t\}^\{i\}=\\begin\{cases\}\\displaystyle\\bigvee\_\{\\tau=t\+a\}^\{t\+b\}\\left\(z\_\{\\varphi\_\{2\},\\tau\}^\{i\}\\wedge\\displaystyle\\bigwedge\_\{k=t\}^\{\\tau\-1\}z\_\{\\varphi\_\{1\},k\}^\{i\}\\right\),&t\+b\\leq T,\\\\ \\mathit\{false\},&t\+b\>T\.\\end\{cases\}\(30\)This enforces thatφ2\\varphi\_\{2\}becomes true at some timeτ\\tauwithin the interval, and thatφ1\\varphi\_\{1\}holds continuously until that time\.
- •Eventually\.Consider a formulaψ=𝐅\[a,b\]​φ\\psi=\\mathbf\{F\}\_\{\[a,b\]\}\\varphi, where0≤a≤b0\\leq a\\leq b, the Eventually operator holds at timettif and only if the inner subformula holds at least once within the time interval\. We encode this operator by the constraint zψ,ti=\{⋁τ=t\+at\+bzφ,τi,t\+b≤T,𝑓𝑎𝑙𝑠𝑒,t\+b\>T\.z\_\{\\psi,t\}^\{i\}=\\begin\{cases\}\\displaystyle\\bigvee\_\{\\tau=t\+a\}^\{t\+b\}z\_\{\\varphi,\\tau\}^\{i\},&t\+b\\leq T,\\\\ \\mathit\{false\},&t\+b\>T\.\\end\{cases\}\(31\)
- •Always\.We encode the formulaψ=𝐆\[a,b\]​φ\\psi=\\mathbf\{G\}\_\{\[a,b\]\}\\varphiby zψ,ti=\{⋀τ=t\+at\+bzφ,τi,t\+b≤T,𝑡𝑟𝑢𝑒,t\+b\>T\.z\_\{\\psi,t\}^\{i\}=\\begin\{cases\}\\displaystyle\\bigwedge\_\{\\tau=t\+a\}^\{t\+b\}z\_\{\\varphi,\\tau\}^\{i\},&t\+b\\leq T,\\\\ \\mathit\{true\},&t\+b\>T\.\\end\{cases\}\(32\)This ensures that the Always operator holds at timettexactly when the inner subformula holds at all time steps within the interval\.

## Appendix EComparison to HyperLTL

The specifications introduced in Section[II](https://arxiv.org/html/2607.28679#S2)are stated in STL\-GO, where agent\-level quantifiers such as𝐄𝐗\\mathbf\{EX\}are evaluated over𝒱\\mathcal\{V\}*pointwise*at the temporal instant under consideration\. The mission also uses finite conjunctions over the fixed locator, rescuer, and emergency\-site sets, together with predicates derived from the time\-varying task graph\. HyperLTL, by contrast, quantifies exclusively over*traces*at the outermost prefix, so any agent\-level quantifier that appears inside a temporal operator in STL\-GO must be*reified*: it must be lifted out of the temporal scope and re\-expressed using outer trace quantifiers, auxiliary atomic propositions, or finite disjunctions over a fixed agent universe\. This appendix makes the cost of that reification explicit\.

### E\-AReification conventions

We fix the locator setℒ\\mathcal\{L\}, rescuer setℛ\\mathcal\{R\}, and emergency\-site setℳ\\mathcal\{M\}at design time, and associate one trace variable with each corresponding entity:πℓ\\pi\_\{\\ell\}forℓ∈ℒ\\ell\\in\\mathcal\{L\},πr\\pi\_\{r\}forr∈ℛr\\in\\mathcal\{R\}, andπm\\pi\_\{m\}form∈ℳm\\in\\mathcal\{M\}\. Emergency activation is represented byφemg,πm\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}, while𝗍𝖺𝗌𝗄πℓ,πr,πm\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}is true when locatorℓ\\ellassigns rescuerrrspecifically to emergency sitemm\. The predicatesφmemg\\varphi^\{\\mathrm\{emg\}\}\_\{m\},φmsense\\varphi^\{\\mathrm\{sense\}\}\_\{m\},φℓLL\\varphi^\{\\mathrm\{LL\}\}\_\{\\ell\},φℓLR\\varphi^\{\\mathrm\{LR\}\}\_\{\\ell\},φr,mnear\\varphi^\{\\mathrm\{near\}\}\_\{r,m\},φrcarry\\varphi^\{\\mathrm\{carry\}\}\_\{r\}, andφratC\\varphi^\{\\mathrm\{atC\}\}\_\{r\}are tagged with the trace\(s\) on which they are evaluated\.

We consider two reification strategies\. The usual approach expands every inner agent\-level existential into a finite disjunction over the fixed agent universe, keeping the quantifier prefix purely universal\. The*Skolemized*strategy lifts inner existentials to outer trace quantifiers, exposing the witness traces explicitly at the cost of one quantifier alternation per lifted existential\.

### E\-BReified HyperLTL specifications

##### Bounded emergency detection

The original STL\-GO formula contains no inner existential, so the idiomatic and Skolemized reifications coincide:

ϕdetectHL:=\\displaystyle\\phi\_\{\\mathrm\{detect\}\}^\{\\mathrm\{HL\}\}\\;:=\\;∀πm\.𝐆\(φemg,πm⇒\\displaystyle\\forall\\pi\_\{m\}\.\\;\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Tdet\]φsense,πm\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{det\}\}\]\}\\,\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\Big\)\.\(33\)The finite conjunction⋀m∈ℳ\\bigwedge\_\{m\\in\\mathcal\{M\}\}becomes the universal trace quantifier∀πm\\forall\\pi\_\{m\}\.

##### Detection\-to\-relay

The inner existential∃ℓ∈ℒ\\exists\\ell\\in\\mathcal\{L\}must be reified\. The idiomatic form expands it as a disjunction overℒ\\mathcal\{L\}:

ϕrelayidio:=\\displaystyle\\phi\_\{\\mathrm\{relay\}\}^\{\\mathrm\{idio\}\}\\;:=\\;∀πm\.𝐆\(φemg,πm∧φsense,πm⇒\\displaystyle\\forall\\pi\_\{m\}\.\\;\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Trelay\]⋁ℓ∈ℒ\(φLL,πℓ∨φLR,πℓ\)\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{relay\}\}\]\}\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\(\\varphi^\{\\mathrm\{LL\},\\pi\_\{\\ell\}\}\\vee\\varphi^\{\\mathrm\{LR\},\\pi\_\{\\ell\}\}\)\\Big\)\.\(34\)The Skolemized form lifts the locator existential to the outer prefix, introducing one quantifier alternation:

ϕrelaySkol:=\\displaystyle\\phi\_\{\\mathrm\{relay\}\}^\{\\mathrm\{Skol\}\}\\;:=\\;∀πm\.∃πℓ\.𝐆\(φemg,πm∧φsense,πm⇒\\displaystyle\\forall\\pi\_\{m\}\.\\;\\exists\\pi\_\{\\ell\}\.\\;\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Trelay\]\(φLL,πℓ∨φLR,πℓ\)\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{relay\}\}\]\}\(\\varphi^\{\\mathrm\{LL\},\\pi\_\{\\ell\}\}\\vee\\varphi^\{\\mathrm\{LR\},\\pi\_\{\\ell\}\}\)\\Big\)\.\(35\)The two reifications are not semantically equivalent: the original STL\-GO formula admits a witness locator that may depend on bothmmand the temporal instanttt, whereas \([E\-B](https://arxiv.org/html/2607.28679#A5.Ex22)\) forces a single witness locator trace per emergency for the entire horizon, and \([E\-B](https://arxiv.org/html/2607.28679#A5.Ex21)\) is faithful only because the disjunction is re\-evaluated at each instant\. Capturing the original semantics exactly would require either the disjunctive form \([E\-B](https://arxiv.org/html/2607.28679#A5.Ex21)\) or a Skolemization in which the witness varies withtt, which HyperLTL cannot express without further auxiliary machinery\.

##### Detection\-to\-assignment

The reifications follow the same pattern\. Idiomatic:

ϕassignidio:=\\displaystyle\\phi\_\{\\mathrm\{assign\}\}^\{\\mathrm\{idio\}\}\\;:=\\;∀πm\.𝐆\(φemg,πm∧φsense,πm⇒\\displaystyle\\forall\\pi\_\{m\}\.\\;\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Tassign\]⋁ℓ∈ℒ⋁r∈ℛ𝗍𝖺𝗌𝗄πℓ,πr,πm\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\bigvee\_\{\\ell\\in\\mathcal\{L\}\}\\bigvee\_\{r\\in\\mathcal\{R\}\}\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\Big\)\.\(36\)Skolemized:

ϕassignSkol:=\\displaystyle\\phi\_\{\\mathrm\{assign\}\}^\{\\mathrm\{Skol\}\}\\;:=\\;∀πm\.∃πℓ\.∃πr\.𝐆\(φemg,πm∧φsense,πm⇒\\displaystyle\\forall\\pi\_\{m\}\.\\;\\exists\\pi\_\{\\ell\}\.\\;\\exists\\pi\_\{r\}\.\\;\\mathbf\{G\}\\Big\(\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{sense\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Tassign\]𝗍𝖺𝗌𝗄πℓ,πr,πm\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{assign\}\}\]\}\\,\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\Big\)\.\(37\)

##### Rescuer response time

The fixed conjunctions over locators, rescuers, and emergency sites become universal trace quantifiers\. The emergency\-specific assignment predicate preserves the association between the assigned rescuer and site:

ϕreachHL:=\\displaystyle\\phi\_\{\\mathrm\{reach\}\}^\{\\mathrm\{HL\}\}\\;:=\\;∀πℓ\.∀πr\.∀πm\.𝐆\(𝗍𝖺𝗌𝗄πℓ,πr,πm∧φemg,πm⇒\\displaystyle\\forall\\pi\_\{\\ell\}\.\\,\\forall\\pi\_\{r\}\.\\,\\forall\\pi\_\{m\}\.\\;\\mathbf\{G\}\\Big\(\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{emg\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Treach\]φnear,πr,πm\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{reach\}\}\]\}\\varphi^\{\\mathrm\{near\},\\pi\_\{r\},\\pi\_\{m\}\}\\Big\)\.\(38\)

##### Rescue and deliver

The same universal prefix gives the direct reification:

ϕdeliverHL:=\\displaystyle\\phi\_\{\\mathrm\{deliver\}\}^\{\\mathrm\{HL\}\}\\;:=\\;∀πℓ\.∀πr\.∀πm\.𝐆\(𝗍𝖺𝗌𝗄πℓ,πr,πm∧φnear,πr,πm⇒\\displaystyle\\forall\\pi\_\{\\ell\}\.\\,\\forall\\pi\_\{r\}\.\\,\\forall\\pi\_\{m\}\.\\;\\mathbf\{G\}\\bigg\(\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\\wedge\\varphi^\{\\mathrm\{near\},\\pi\_\{r\},\\pi\_\{m\}\}\\Rightarrow𝐅\[0,Tdeliver\]\(φcarry,πr∧φatC,πr\)\)\.\\displaystyle\\quad\\mathbf\{F\}\_\{\[0,T\_\{\\mathrm\{deliver\}\}\]\}\\\!\(\\varphi^\{\\mathrm\{carry\},\\pi\_\{r\}\}\\wedge\\varphi^\{\\mathrm\{atC\},\\pi\_\{r\}\}\)\\bigg\)\.\(39\)

### E\-CSources of the succinctness loss

Two principal structural costs are imposed by reification, and both are visible in the formulas above\.

First, every pointwise agent choice in STL\-GO—whether expressed by𝐄𝐗\\mathbf\{EX\}over𝒱\\mathcal\{V\}or by a finite role\-restricted disjunction—becomes either a finite disjunction whose size scales with the corresponding agent universe or an outer trace quantifier that raises the alternation depth\. In the disjunctive form, the propositional matrix grows asΘ​\(\|ℒ\|\)\\Theta\(\|\\mathcal\{L\}\|\)forϕrelay\\phi\_\{\\mathrm\{relay\}\}andΘ​\(\|ℒ\|​\|ℛ\|\)\\Theta\(\|\\mathcal\{L\}\|\\,\|\\mathcal\{R\}\|\)forϕassign\\phi\_\{\\mathrm\{assign\}\}\. The role\-restricted choices in both formulas remain inside the temporal operator, preserving their pointwise dependence on the time and emergency; the assignment formula also preserves the emergency\-specific locator–rescuer association\. In the Skolemized form, the matrix remains compact but the prefix acquires a universal–existential alternation\. By contrast, the fixed conjunctions inϕreach\\phi\_\{\\mathrm\{reach\}\}andϕdeliver\\phi\_\{\\mathrm\{deliver\}\}translate to universal trace prefixes and introduce no alternation\.

Second, joint predicates such asφr,mnear\\varphi^\{\\mathrm\{near\}\}\_\{r,m\}andφℓ,r,mtask\\varphi^\{\\mathrm\{task\}\}\_\{\\ell,r,m\}that depend on the states of multiple agents map naturally onto STL\-GO via predicate functions over agent\-state tuples at the outer level\. In HyperLTL they require atomic propositions tagged with multiple path variables, written above asφnear,πr,πm\\varphi^\{\\mathrm\{near\},\\pi\_\{r\},\\pi\_\{m\}\}and𝗍𝖺𝗌𝗄πℓ,πr,πm\\mathsf\{task\}^\{\\pi\_\{\\ell\},\\pi\_\{r\},\\pi\_\{m\}\}\. This is a non\-standard extension; in strict HyperLTL one must either replicate each predicate across the participating traces with consistency constraints or precompute it as a Boolean signal on a designated system trace, in either case adding further auxiliary atomic propositions\.

Taken together, the reification yields HyperLTL formulas whose propositional matrix scales linearly with the locator universe for relay and with the locator–rescuer product for assignment \(idiomatic form\), or whose quantifier prefixes acquire an alternation \(Skolemized form\)\. The remaining formulas stay universally quantified but retain the multi\-trace predicate overhead\.

### E\-DExperimental comparison with HyperLTL

We evaluate STL\-GO against a HyperLTL baseline on the wildfire\-rescue grid\-world benchmark of HypRL\[hsu2025hyprl\]\. The environment is an𝒩×𝒩\\mathcal\{N\}\\times\\mathcal\{N\}grid\. Two heterogeneous agents, a firefighter \(FF\) and a medical responder \(Med\), are deployed from a shared initial cell in the top\-left corner\. Letℱ𝒩\\mathcal\{F\}\_\{\\mathcal\{N\}\}and𝒱𝒩\\mathcal\{V\}\_\{\\mathcal\{N\}\}denote, respectively, the fire and victim cells for an𝒩×𝒩\\mathcal\{N\}\\times\\mathcal\{N\}instance; their cardinalities scale with𝒩\\mathcal\{N\}, with fire cells placed along the anti\-diagonal and victim cells along the middle row\.

The mission is governed by four sub\-specifications\. ObjectivesO1andO2require FF to eventually visit every fire zone \(extinguishing it\) and Med to eventually visit every victim cell respectively\. Coordination constraintC1enforces that the agents remain within Manhattan communication range𝒩−1\\mathcal\{N\}\-1at all times\. Safety constraintC2imposes a temporal precedence: Med may not enter any fire zone until FF has already visited that cell\. The HyperLTL specification uses a∀πF​F\.∃πM​e​d\\forall\\pi\_\{FF\}\.\\,\\exists\\pi\_\{Med\}prefix and joint multi\-trace propositions:

ϕRescue\\displaystyle\\phi\_\{\\mathrm\{Rescue\}\}:=∀πF​F\.∃πM​e​d\.\(ψfire∧ψsave∧ψdist∧ψsafe\)\\displaystyle\\;:=\\;\\forall\\pi\_\{FF\}\.\\exists\\pi\_\{Med\}\.\\,\(\\psi\_\{\\mathrm\{fire\}\}\\wedge\\psi\_\{\\mathrm\{save\}\}\\wedge\\psi\_\{\\mathrm\{dist\}\}\\wedge\\psi\_\{\\mathrm\{safe\}\}\)O1:​ψfire\\displaystyle\\textbf\{O1: \}\\;\\psi\_\{\\mathrm\{fire\}\}:=⋀q∈ℱ𝒩𝐅​\(qπF​F\)\\displaystyle\\;:=\\;\\bigwedge\_\{q\\in\\mathcal\{F\}\_\{\\mathcal\{N\}\}\}\\mathbf\{F\}\(q^\{\\pi\_\{FF\}\}\)O2:​ψsave\\displaystyle\\textbf\{O2: \}\\;\\psi\_\{\\mathrm\{save\}\}:=⋀q∈𝒱𝒩𝐅​\(qπM​e​d\)\\displaystyle\\;:=\\;\\bigwedge\_\{q\\in\\mathcal\{V\}\_\{\\mathcal\{N\}\}\}\\mathbf\{F\}\(q^\{\\pi\_\{Med\}\}\)C1:​ψdist\\displaystyle\\textbf\{C1: \}\\;\\psi\_\{\\mathrm\{dist\}\}:=𝐆​\(‖LocationπF​F−LocationπM​e​d‖1<𝒩\)\\displaystyle\\;:=\\;\\mathbf\{G\}\\left\(\\left\\\|\\mathrm\{Location\}^\{\\pi\_\{FF\}\}\-\\mathrm\{Location\}^\{\\pi\_\{Med\}\}\\right\\\|\_\{1\}<\\mathcal\{N\}\\right\)C2:​ψsafe\\displaystyle\\textbf\{C2: \}\\;\\psi\_\{\\mathrm\{safe\}\}:=⋀q∈ℱ𝒩\(¬qπM​e​d​𝐔​qπF​F\)\\displaystyle\\;:=\\;\\bigwedge\_\{q\\in\\mathcal\{F\}\_\{\\mathcal\{N\}\}\}\(\\neg q^\{\\pi\_\{Med\}\}\\;\\mathbf\{U\}\\;q^\{\\pi\_\{FF\}\}\)The equivalent STL\-GO specification captures the same mission using STL\-GO operators: a shared fire\-status state variable collapses the per\-cell until ofC2into the constraintloc​\[Med,q,t\]\+fire​\[q,t\]≤1\\mathrm\{loc\}\[\\mathrm\{Med\},q,t\]\+\\mathrm\{fire\}\[q,t\]\\leq 1for eachq∈ℱ𝒩q\\in\\mathcal\{F\}\_\{\\mathcal\{N\}\}, and the singleton communication\-graph collection\{𝒢tc\}\\\{\\mathcal\{G\}^\{c\}\_\{t\}\\\}with the operatorOut\{𝒢c\},\[1,∞\)∃⊤\\mathrm\{Out\}^\{\\exists\}\_\{\\\{\\mathcal\{G\}^\{c\}\\\},\[1,\\infty\)\}\\topat FF enforcesC1via a single distance constraint per timestep\.