Paper deep dive
An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators
Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy V. Deshmukh
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 7/9/2026, 8:31:29 AM
Summary
The paper introduces a layered algebraic framework for quantitative semantics of Spatio-Temporal Logic with Graph Operators (STL-GO), extending Signal Temporal Logic (STL) to multi-agent systems. It addresses the lack of quantitative semantics for STL-GO's counting-based graph operators by separating temporal and graph-operator aggregation via an abstract accumulator with monotone fold and readout. The framework is evaluated across four semantic instantiations on 2D and 3D multi-agent environments, demonstrating tradeoffs in scalability and robustness reporting.
Entities (18)
Relation Signals (14)
STL-GO → extends → Signal Temporal Logic (STL)
confidence 95% · Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers.
STL-GO → introduces → Graph operators
confidence 94% · via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers.
Graph operators → count → neighboring agents
confidence 92% · via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers.
Framework → uses → Layered algebraic construction
confidence 91% · We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout).
STREL → cannotcapture → counting constraints
confidence 90% · existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO’s graph operators.
Semantic instantiations → include → Boolean semantics
confidence 90% · under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.
Semantic instantiations → include →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO's graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.
Tags
Links
- Source: https://arxiv.org/abs/2606.28429v1
- Canonical: https://arxiv.org/abs/2606.28429v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
96,002 characters extracted from source content.
Expand or collapse full text
11institutetext: University of Southern California, Los Angeles, CA, USA 11email: sherylpa,kudalkar,wutianha,jdeshmuk@usc.edu 22institutetext: University of Texas at Austin, Austin, TX, USA 22email: anandbal@utexas.edu 33institutetext: ETH Zürich, Zürich, Switzerland 33email: llindemann@ethz.ch An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators Sheryl Paul Equal contribution. Vidisha Kudalkar∗ Anand Balakrishnan∗ Tianhao Wu Lars Lindemann Jyotirmoy V. Deshmukh Abstract Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO’s graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon. 1 Introduction Signal Temporal Logic [23] is widely used to describe objectives in many applications like in cyber-physical systems (CPS). Its applications span robot task objectives [32, 17], control synthesis [30], scenario generation [18] and CPS monitoring [8]. A key enabler of this success is the notion of quantitative semantics: which assign a real-valued robustness score to each trajectory, based on how well the trajectory satisfies the specification. A substantial body of work has explored such semantics, including classical robustness measures [11], spatial and temporal robustness [10, 1, 31], stochastic robustness distributions [7], and smooth approximations [24, 15, 27]. These have enabled a wide range of applications, including robustness-aware monitoring [16, 26], falsification [33], model predictive control [30], reinforcement learning [21, 29, 28, 3, 4], and signal classification [34]. Modern systems, however, are generally multi-agent. Applications such as robot swarms, networked CPS, distributed sensing, and social systems require reasoning not only about temporal evolution but also about interactions between agents, naturally captured by time-varying graphs encoding communication, sensing, or influence relationships. Hence, specifying multi-agent behavior requires combining temporal logic with relational and spatial reasoning over graphs. Several spatio-temporal logics have been proposed to address this need, including SSTL [26], SpaTeL [14], SaSTL [22], STREL [6, 25], STL-GO [35], and HyperLTL [12]. These logics have enabled monitoring [5, 26] and control synthesis [19, 2] of spatio-temporal cyber-physical systems. These logics differ in their treatment of spatial structure, expressiveness of quantification, and ability to handle dynamic relations. While Boolean semantics for these logics are generally well understood, quantitative semantics are less developed. Notably, STREL admits an elegant robustness interpretation based on min-max algebra [5], while other frameworks either lack quantitative semantics or rely on constructions that are difficult to interpret or extend. Among these, of particular interest to us is STL-GO, which significantly extends the expressiveness of prior frameworks by offering support for directed graph relations, multiple simultaneous graph layers, count-based constraints over neighbors, and quantification over both graphs and agents. However, this expressiveness introduces new challenges for quantitative semantics. In particular, graph operators in STL-GO require aggregating values over sets of neighbors subject to cardinality constraints. Such aggregation cannot be captured by standard semiring operations (e.g., min or max) alone. To illustrate the challenges, consider a team of agents subject to the requirement that each agent must have at least 3 neighbors within communication range R satisfying a property φ (Fig. 1). In STL-GO, this is expressed as ,[3,∞)∃φFA_V\;In^∃_G,[3,∞)\; . Plain STL lacks graph operators and multi-agent quantifiers; expressing this would require expanding the counting constraint into a conjunction over agents of disjunctions: ⋀i∈V⋁j1,j2,j3⊆V∖i⋀k=13(‖xjk−xi‖≤R∧φ(xjk)), _i∈ V\ _\j_1,j_2,j_3\ V \i\\ _k=1^3 (\|x^j_k-x^i\|≤ R\ \ (x^j_k) ), across all (N−13) N-13 neighbor subsets with explicit distance predicates. Applying min-max robustness to this expansion yields nested min /max operations that collapse to the margin of the 3rd-best neighbor of the worst-off agent, with the following limitations: (i) Count-margin insensitivity: whether a drone has exactly three qualifying neighbors or five, the robustness is identical so long as the third-best neighbor’s margin is the same, even though the latter configuration is far more resilient. (i) Edge-margin insensitivity: a drone just outside communication range that robustly satisfies the predicate is treated similarly to a drone that might be far away from the range, regardless of how close it is to qualifying as a neighbor. (i) Worst-case dominance: at the system level, the all-agent quantifier assigns robustness based on the single worst agent, discarding the fact that the vast majority may be performing well. Moreover, STREL cannot express the counting requirement at all; its spatial operators reason about path existence, not neighbor counts. Figure 1: Limitations of existing spatio-temporal robustness semantics. (a) Both scenarios satisfy “at least 3 neighbors satisfy φ ,” but A has zero spare neighbors and B has two; min-max robustness assigns both the same value. STREL cannot express this counting requirement. (b) The dashed-border agent satisfies φ but lies just outside range (d1=R+0.01d_1=R+0.01); the faded agent is far beyond d2=R+10d_2=R+10. Both are treated the same way by the robustness semantics. (c) The all-agent STL-GO quantifier FA_V assigns robustness according to the worst agent (−0.01-0.01), discarding 9 agents at +10+10. These limitations motivate the development of richer quantitative semantics for STL-GO that separately account for individual signal margins, the number of satisfying neighbors, and the robustness of the graph structure itself. Contributions. Our contributions are: (i) a layered algebraic semantics for STL-GO that separates temporal, graph, and multi-agent operators into distinct algebraic components, with temporal and Boolean operators functioning as in standard STL robustness; (i) an abstract accumulator for graph operators that factors into a monoid fold and a readout map, isolating counting-specific aggregation and admitting product spaces that propagate robustness values alongside qualifying agent sets; (i) multi-agent semantics in which agent quantifiers aggregate over an agent-indexed valuation space via semiring operations, completing the semantics for full STL-GO; (iv) soundness and completeness results showing that monotone folds and readouts preserve threshold semantics, with compositionality across all layers by structural induction; and (v) experimental evaluation of four semantic instantiations (Boolean, min-max, signed-deficit, and hybrid) on two multi-agent environments, demonstrating accumulator tradeoffs and scalability in agents and time horizon. 2 Preliminaries We first describe the multi-agent system and the spatio-temporal logic STL-GO. 2.1 Multi-Agent System We consider a multi-agent system consisting of a finite set of agents denoted by =1,…,N.V=\1,…,N\. Each agent i∈i has a state space X, and the joint system state at time t is denoted by t=(xt1,…,xtN)∈||,X_t=(x_t^1,…,x_t^N) ^|V|, where xti∈x_t^i is the state of agent i at time t. In addition to agent states, the system may include an external environment or world state wt∈w_t . Here, W represents the environment space. Agent interactions are modeled by a collection of time-varying, weighted directed graphs t=tτ∣τ∈,G_t=\G_t^τ τ \, where T denotes the set of all graph types, and each graph tτ=(,ℰtτ,wtτ)G_t^τ=(V,E_t^τ,w_t^τ) consists of: (i) a set of directed edges ℰtτ⊆×E_t^τ ×V, (i) a weight function wtτ:ℰtτ→ℝw_t^τ:E_t^τ . Each graph type τ∈τ represents a distinct interaction modality. A multi-agent execution trace is a sequence ℳ=(0,w0,0),(1,w1,1),…M=\(X_0,w_0,G_0),(X_1,w_1,G_1),…\ over discrete time steps t∈ℕt . We write (ℳ,i,t)(M,i,t) to denote evaluation of agent-local formulas at agent i∈i and time t, and (ℳ,t)(M,t) for multi-agent formulas evaluated over the joint system at time t. We write (ℳ,i,t)⊧φ(M,i,t) to denote that an agent-local formula φ is Boolean satisfied at agent i and time t and (ℳ,t)⊧ϕ(M,t) φ to denote that a multi-agent formula ϕφ is satisfied over the system.111We only consider traces over discrete-time in this work. 2.2 Signal Temporal Logic with Graph Operators (STL-GO) Spatio-Temporal Logic with Graph Operators (STL-GO) [35] extends STL [23] to reason simultaneously about spatio-temporal agent behavior and the topological relationships between agents encoded in interaction graphs. Its syntax and semantics are stratified into agent-local formulas φ and multi-agent formulas ϕφ. Agent-Local Formulas. The syntax for agent-local STL-GO formulas is: φ::=⊤∣μx∣¬φ∣φ∧φ∣φ[t1,t2]φ∣,EW,#φ∣,EW,#φ, \;::=\; \; \; _x\; \; \; \; \; \; \,\,U_[t_1,t_2]\,\, \; \;In_G,E^W,\# \; \;Out_G,E^W,\# , where μx:→ _x:X is an atomic predicate over a single agent’s state; ¬ and ∧ are the standard Boolean connectives; [t1,t2]\,U_[t_1,t_2]\, is the bounded Until operator from STL; and ,EW,#In_G,E^W,\#, ,EW,#Out_G,E^W,\# are the incoming and outgoing graph operators introduced by STL-GO, where W=[w1,w2]⊆ℝ∞W=[w_1,w_2] ^∞ is an edge-weight interval, E=[e1,e2]E=[e_1,e_2] with e1∈ℕ,e2∈ℕ∪+∞e_1 ,\ e_2 ∪\+∞\ constrains the count of qualifying edges, and #∈∃,∀\#∈\∃,∀\ quantifies over the graph collection tG_t. The semantics (ℳ,i,t)⊧φ(M,i,t) are defined inductively; Boolean and temporal clauses follow STL: (ℳ,i,t) (M,i,t) ⊧μx _x iff μx(ti), _x(s^i_t), (ℳ,i,t) (M,i,t) ⊧¬φ iff (ℳ,i,t)⊧̸φ, (M,i,t) , (ℳ,i,t) (M,i,t) ⊧φ1∧φ2 _1 _2 iff (ℳ,i,t)⊧φ1 and (ℳ,i,t)⊧φ2, (M,i,t) _1 and (M,i,t) _2, (ℳ,i,t) (M,i,t) ⊧φ1[t1,t2]φ2 _1\,\,U_[t_1,t_2]\,\, _2 iff ∃t′∈t⊕[t1,t2].(ℳ,i,t′)⊧φ2 ∃ t ∈ t [t_1,t_2].\;(M,i,t ) _2 ∧∀t′∈[t,t′].(ℳ,i,t′)⊧φ1. iff \;∀ t ∈[t,t ].\;(M,i,t ) _1. The graph operators count the neighbors of agent i that satisfy φ and lie within the weight interval W: (ℳ,i,t)⊧,EW,#φiff#τ∈t.|(j,i)∈ℰtτ∣wtτ(j,i)∈W,(ℳ,j,t)⊧φ|∈E (M,i,t) _G,E^W,\# \#\,G^τ _t.\; | \(j,i) _t^τ w_t^τ(j,i)∈ W,\;(M,j,t) \ |∈ E The Out operator is similarly defined except using (i,j)∈ℰtτ(i,j) _t^τ instead. Here #=∃\#=∃ requires the count condition to hold in some graph τ∈tG^τ _t; #=∀\#=∀ requires it in every graph. When edge weights are unconstrained, we abbreviate ,E#φIn_G,E^\# and ,E#φOut_G,E^\# (setting W=(−∞,∞)W=(-∞,∞)). Multi-Agent Formulas. Multi-agent STL-GO formulas ϕφ compose agent-local formulas and predicates over the joint system state: ϕ::=⊤∣μ∣i.φ∣¬ϕ∣ϕ∧ϕ∣ϕ[t1,t2]ϕ,φ\;::=\; \; \;μ\; \;i. \; \; φ\; \;φ φ\; \;φ\,\,U_[t_1,t_2]\,\,φ, where μ:||×→μ:X^|V|×W is an atomic predicate over the joint agent and world state, and i.φi. embeds the agent-local formula φ for agent i into the multi-agent context. The semantics (ℳ,t)⊧ϕ(M,t) φ follow the same structure as the agent-local case, with: (ℳ,t)⊧μ iff μ(t,wt), and (ℳ,t)⊧i.φ iff (ℳ,i,t)⊧φ.(M,t) μ iff μ(X_t,w_t), and (M,t) i. iff (M,i,t) . All remaining clauses (¬ , ∧ , [t1,t2]\,U_[t_1,t_2]\,) are identical in structure to the agent-local case. The derived operators [t1,t2]F_[t_1,t_2] and [t1,t2]G_[t_1,t_2] follow from Until as in STL. For convenience, the agent-universal and agent-existential shorthands are: φ≜⋀i∈i.φ, and φ≜⋁i∈i.φ.FA_V\, \; \; _i i. , and EX_V\, \; \; _i i. . The semantics of STL-GO presented so far assume the standard Boolean satisfaction semantics; i.e., for a given agent-centric STL-GO formula φ , or for a multi-agent STL-GO formula ϕφ, a given multi-agent execution trace either satisfies the given formulas or violates them. Quantitative semantics generalize the notion of Boolean semantics by defining a function that maps a formula and a multi-agent trace to some (signed) number that indicates a quantitative degree of satisfaction. Many different quantitative semantics for logics such as STL and STREL have been defined in the literature [11, 10, 31, 5]. Of particular relevance to this paper are generalization of quantitative semantics as operations defined using suitable algebras. We also define the quantitative semantics of STL-GO more generally using specific algebraic operations. Before we define them in the next section, we review some key ideas from algebra. 2.3 Background on Algebraic Structures Definition 1(Monoid). A monoid is a triple (M,⊕,e)(M, ,e) consisting of a set M, a binary operation ⊕:M×M→M, :M× M→ M, and an element e∈Me∈ M, such that for all a,b,c∈Ma,b,c∈ M: (a⊕b)⊕c=a⊕(b⊕c)(a b) c=a (b c) and a⊕e=e⊕a=a e=e a=a, i.e., all the elements satisfy the property of associativity and e acts as an identity element. Further, a commutative monoid is a monoid (M,⊕,e)(M, ,e) that additionally satisfies, for all a,b∈Ma,b∈ M: a⊕b=b⊕a.a b=b a. Definition 2(Semiring [13, 20]). A tuple =(K,⊕,⊗,⊥,⊤)K=(K, , , , ) is a semiring with underlying set K if (K,⊕,⊥)(K, , ) is a commutative monoid with identity ⊥ ; (K,⊗,⊤)(K, , ) is a monoid with identity ⊤ ; ⊗ distributes over ⊕ ; and ⊥ is an annihilator for ⊗ (i.e. k⊗⊥=⊥⊗k=⊥k = k= for all k∈Kk∈ K). A semiring K is commutative if ⊗ is also commutative, and simple if k⊕⊤=⊤k = for all k∈Kk∈ K. It is additively (resp. multiplicatively) idempotent if k⊕k=k k=k (resp. k⊗k=k k=k) for all k∈Kk∈ K. A semiring that is commutative, additively idempotent, and simple is called a constraint semiring (c-semiring). A c-semiring that is also multiplicatively idempotent induces a bounded distributive lattice, with ⊤ as supremum and ⊥ as infimum. Example 1. Consider the semiring (ℝ∪−∞,+∞,max,min,−∞,+∞)(R∪\-∞,+∞\, , ,-∞,+∞). Then (ℝ,max,−∞)(R, ,-∞) is a commutative monoid with identity −∞-∞, and (ℝ,min,+∞)(R, ,+∞) is a monoid with identity +∞+∞. By the distributivity of min over max , we have min(a,max(b,c)) (a, (b,c)) =max(min(a,b),min(a,c))= ( (a,b), (a,c)). The element −∞-∞ is an annihilator for min , since min(a,−∞)=−∞. (a,-∞)=-∞. Both operations are idempotent, i.e., max(a,a)=a (a,a)=a and min(a,a)=a (a,a)=a. The semiring is commutative, and simple since max(k,+∞)=+∞ (k,+∞)=+∞ for all k∈Kk∈ K. When considering a unary operator, ⊖:K→K :K→ K, on a bounded distributive lattice K, these operators give rise to a special case of a useful algebra: Definition 3(De Morgan Algebra [9]). A De Morgan algebra is a structure (K,⊕,⊗,⊖,⊥,⊤)(K, , , , , ) such that (K,⊕,⊗,⊥,⊤)(K, , , , ) is a bounded distributive lattice and ⊖ is a negation on K satisfying, for all a,b∈Ka,b∈ K: ⊖(a⊕b)=⊖a⊗⊖b,⊖(a⊗b)=⊖a⊕⊖b,⊖a=a. (a b)= a b,\ (a b)= a b,\ a=a. The two De Morgan algebras of primary interest here are: (i) The Boolean algebra (,∨,∧,¬,,)(B, , , ,0,1), giving qualitative (Boolean) satisfaction semantics. (i) The min-max algebra (ℝ∞,max,min,−,−∞,+∞)(R^∞, , ,-,-∞,+∞) over the extended reals, which recovers the quantitative (robustness) semantics of STL [11]. Since we are interested in the semantics of multi-agent systems, we will consider how such semirings can be extended to multiple components, and how we can generalize operations on multiple semirings. Let semirings be (Kℓ,⊕ℓ,⊗ℓ,⊥ℓ,⊤ℓ)ℓ=1m\(K_ , _ , _ , _ , _ )\_ =1^m and their product semiring is K:=∏ℓ=1mKℓK:= _ =1^mK_ , with componentwise operations: (x⊕y)ℓ:=xℓ⊕ℓyℓ,(x⊗y)ℓ:=xℓ⊗ℓyℓ(x y)_ :=x_ _ y_ ,\ (x y)_ :=x_ _ y_ and identities: ⊥:=(⊥ℓ)ℓ,⊤:=(⊤ℓ)ℓ. :=( _ )_ ,\ :=( _ )_ . From this, we can algebraically define the notion of a general commutative monoid operating on this product semiring as a semimodule. Definition 4(Semimodule). Let (K,⊕,⊗,⊥,⊤)(K, , , , ) be a semiring. A semimodule over K is a commutative monoid (S,⊕S,⊥S)(S, _S, _S) together with a scalar multiplication ⊗:K×S→S :K× S→ S, such that for all k,k′∈Kk,k ∈ K and s,s′∈Ss,s ∈ S: k⊗(s⊕Ss′) k (s _Ss ) =(k⊗s)⊕S(k⊗s′); =(k s) _S(k s ); (k⊕k′)⊗s=(k⊗s)⊕S(k′⊗s) (k k ) s=(k s) _S(k s) (k⊗k′)⊗s (k k ) s =k⊗(k′⊗s); =k (k s); ⊤⊗s=s;k⊗⊥S=⊥S s=s; k _S= _S Definition 5(K-Labeled Trace). Let (K,⊕,⊗,⊖,⊥,⊤)(K, , , , , ) be a De Morgan algebra and L a space universe. A K-labeled trace is a pair (σ,ν)(σ,ν) where σ=01⋯σ=S_0S_1·s is a finite sequence of spatial models and ν(i,l,μ)∈Kν(S_i,l,μ)∈ K is the value of atomic predicate μ at location l∈Ll∈ L in model iS_i. 3 Layered Algebraic Semantics for STL-GO In addition to the operators introduced by STL, STL-GO also introduces graph operators and multi-agent operators which require mechanisms beyond those required for defining standard STL robustness. While the latter includes only Boolean and temporal operators that can be governed by a single algebraic structure such as a De Morgan algebra or semiring, STL-GO requires multiple forms of algebraic structures. To capture this uniformly, we present STL-GO semantics as a layered algebraic construction. We begin with the temporal semantics, which provide the base algebraic structure. 3.1 Semirings for Temporal Operators We begin with ego-centric temporal operators for STL-GO which generalize robustness semantics of STL. Let (K,⊕,⊗,⊖,⊥,⊤)(K, , , , , ) be an algebra, where (K,⊕,⊥)(K, , ) is a commutative monoid, (K,⊗,⊤)(K, , ) is a monoid, ⊖ is an involutive negation satisfying De Morgan laws when present. The set K represents the space of semantic values assigned to formulas. Ego-centric boolean and temporal semantics. To evaluate a formula φ for agent i at time t, the ego-centric semantics ρi(σ,φ,t)∈K _i(σ, ,t)∈ K can be defined as: ρi(σ,μ,t) _i(σ,μ,t) =ν(t,i,μ),ρi(σ,φ1∧φ2,t)=ρi(σ,φ1,t)⊗ρi(σ,φ2,t), =ν(S_t,i,μ), _i(σ, _1 _2,t)= _i(σ, _1,t) _i(σ, _2,t), ρi(σ,¬φ,t) _i(σ, ,t) =⊖ρi(σ,φ,t),ρi(σ,φ1∨φ2,t)=ρi(σ,φ1,t)⊕ρi(σ,φ2,t), = \, _i(σ, ,t), _i(σ, _1 _2,t)= _i(σ, _1,t) _i(σ, _2,t), ρi(σ,φ1 _i(σ, _1 [t1,t2]φ2,t)=⨁t′∈t+[t1,t2](ρi(σ,φ2,t′)⊗⨂t′∈[t,t′]ρi(σ,φ1,t′)) \,U_[t_1,t_2]\, _2,t)= _t ∈ t+[t_1,t_2] ( _i(σ, _2,t ) _t ∈[t,\,t ] _i(σ, _1,t ) ) Derived operators such as F and G follow in the usual way. Example 2. Different choices of (K,⊕,⊗)(K, , ) yield different interpretations: (i) Boolean Semantics: K=0,1K=\0,1\, ⊕=∨ = , ⊗=∧ = recovers the classical qualitative satisfaction. (i) Min-max Semantics: K=ℝ∞K=R^∞, ⊕=max = , ⊗=min = recovers the standard STL robustness, where values represent perturbation margins. Recall the definition of product semirings. This construction allows formulas to simultaneously produce multiple semantic quantities. E.g., we may combine a robustness value with quantities such as counts, or relational data. The temporal semantics may be extended componentwise to this setting, ensuring consistency across outputs. This multi-output structure will be essential for defining graph operators which we describe below. 3.2 Multi-agent and Graph Operators Graph Operators. We now define the semantics of graph operators. Unlike temporal operators, which are induced directly by the semiring structure on K, graph operators require aggregation over dynamically defined neighborhoods of agents. This aggregation is not, in general, expressible purely in terms of the semiring operations (⊕,⊗)( , ). Let V denote the set of agents, and define S:=KS:=K^V. Each element s∈Ss∈ S assigns to every agent i∈i a semantic value s(i)∈Ks(i)∈ K. The space S inherits algebraic structure from K: (S,⊕,⊥)(S, , ) is a commutative monoid under addition: (s⊕s′)(i):=s(i)⊕s′(i)(s s )(i):=s(i) s (i), S is a semimodule over K with scalar multiplication defined: (k⊗s)(i):=k⊗s(i)(k s)(i):=k s(i). For a fixed trace σ, formula φ , and time t, the ego-centric semantics induce an element sφ,t∈S,sφ,t(i):=ρi(σ,φ,t)s_ ,t∈ S,\ s_ ,t(i):= _i(σ, ,t), which collects the local evaluations across all agents. Eligible Neighbors. For an agent i∈i , time t, graph type τ∈τ , and weight interval W, we define the sets of eligible neighbors: iτ,(t,W)=j∈∣(j,i)∈ℰtτ,wtτ(j,i)∈WN_i^τ,In(t,W)=\\,j (j,i) _t^τ,\;w_t^τ(j,i)∈ W\,\, iτ,(t,W)N_i^τ,Out(t,W) is defined similarly except with (i,j)∈ℰtτ(i,j) _t^τ. The graph operators act by restricting the global valuation sφ,t∈Ss_ ,t∈ S to the neighborhood of i, yielding a multiset of values: sφ,t(j)∣j∈iτ,∘(t,W)⊆K\s_ ,t(j) j _i^τ, (t,W)\ K where ∘∈, ∈\In,Out\. Aggregation Monoid. To combine neighbor values we introduce an aggregation space (M,⊞,e)(M, ,e), a commutative monoid. It serves as a domain for aggregating multisets of semantic values. Choices may include: M=KM=K with ⊞=⊕ = (idempotent reduction), M=ℤM=Z with ⊞=+ =+ (counting), M=ℝM=R with ⊞=+ =+ (averaging), product spaces M=K×M′M=K× M for hybrid semantics. Let E:K∗→MA_E:K^*→ M be a fold map that aggregates a multiset of neighbor values subject to the count constraint E, where K∗K^* denotes the set of finite multisets over K. Then for each graph type τ define: E(sφ,t(j)∣j∈iτ,∘(t,W))∈MA_E\! (\\,s_ ,t(j) j _i^τ, (t,W)\,\ )\;∈\;M with ∘∈, ∈\In,Out\. This folding operation summarizes the multiset of neighbor values into a single aggregate element of M. Different choices of EA_E induce different interpretations of the count constraint. Readout. To obtain a value compatible with the temporal semantics, we map the aggregated result back into K via a readout map h:M→Kh:M→ K. This yields, for each graph type τ: h(E(sφ,t(j)∣j∈iτ,∘(t,W)))∈Kh\! (A_E\! (\\,s_ ,t(j) j _i^τ, (t,W)\,\ ) )\;∈\;K with ∘∈, ∈\In,Out\. Quantification over Graphs. Finally, we aggregate across graph types using semiring operations: ∃K=⨁, and ∀K=⨂.Q_∃^K= , and Q_∀^K= . The graph operators are then defined as: ρi(σ,,EW,#φ,t)=#K(h(E(sφ,t(j)∣j∈iτ,(t,W))))τ∈ _i(σ,In_G,E^W,\# ,t)=Q_\#^K (h\! (A_E (\\,s_ ,t(j) j _i^τ,In(t,W)\,\ ) ) )_τ and similarly for the Out operator. For a fixed trace σ, formula φ , time t, and quantifier #∈∃,∀\#∈\∃,∀\, we define the induced local graph operator Ti#:S→KT_i^\#:S→ K by Ti#(s)=#K(h(E(s(j)∣j∈iτ,∘(t,W))))τ∈.T_i^\#(s)\;=\;Q_\#^K\! (\,h (A_E(\\,s(j) j _i^τ, (t,W)\,\) )\, )_τ . The graph operator semantics are then ρi(σ,,EW,#φ,t)=Ti#(sφ,t) _i(σ,In_G,E^W,\# ,t)=T_i^\#(s_ ,t), and analogously for Out. In this setting, graph aggregation is fully internal to the semiring, and the resulting operator preserves the algebraic structure of K. Multi-agent aggregation and quantifiers. In addition to neighborhood-based aggregation, STL-GO supports aggregation over the entire agent set. This yields the semantics of multi-agent quantifiers. Let sφ,t∈S=Ks_ ,t∈ S=K^V denote the agent-indexed valuation induced by a formula φ at time t, i.e., sφ,t(i):=ρi(σ,φ,t).s_ ,t(i):= _i(σ, ,t). We define a global aggregation map :S→K Acc:S→ K, which combines the values across all agents. The existential and universal quantifiers are obtained as special cases: ⊕(s)=⨁i∈s(i),⊗(s)=⨂i∈s(i). Acc_ (s)= _i s(i),\ Acc_ (s)= _i s(i). The semantics of multi-agent quantifiers are then: ρ(σ,φ,t)=⊕(sφ,t),ρ(σ,φ,t)=⊗(sφ,t).ρ(σ,EX_V\, ,t)= Acc_ (s_ ,t), ρ(σ,FA_V\, ,t)= Acc_ (s_ ,t). More generally, Acc may be instantiated as an arbitrary aggregation map, potentially factoring through an intermediate space MAM_A as in the graph-operator construction: S→MA→K.S\;→\;M_A\;→\;K. 3.3 Spatio-temporal Algebras The construction of Section 3.2 separates aggregation into an intermediate space M and a readout map h:M→Kh:M→ K. This enables the use of richer aggregation domains that carry additional structural information beyond scalar robustness. We now show how to construct such domains via product algebras, yielding ‘spatio-temporal implicants’ that generalize classical temporal semantics. Product aggregation spaces. Let (K,⊕,⊗)(K, , ) be the base semiring used for temporal semantics. We extend the aggregation space by introducing an auxiliary structure that tracks the origin of satisfaction. Let R:=(×)R:=P(V×T) where T denotes the time domain. Elements of R represent sets of agent-time pairs witnessing the satisfaction of a formula. We define the product aggregation space M:=K×RM:=K× R with componentwise aggregation (r1,R1)⊞(r2,R2):=(r1⊕r2,R1∪R2)(r_1,R_1)\; \;(r_2,R_2)\;:=\;(r_1 r_2,\;R_1∪ R_2). Thus, M simultaneously carries: (i) a scalar semantic value r∈Kr∈ K, (i) a relational component R⊆×R ×T. Spatio-temporal implicants. In classical temporal logic, implicants correspond to time indices at which a formula is satisfied. We extend this by interpreting the relational component R as a spatio-temporal implicant: a set that acts as a witness to the satisfaction of the formula. Our construction generalizes classic implicants by lifting them to the spatio-temporal domain: R⊆×,R ×T, allowing formulas to track both which agents and when they contribute to satisfaction. For example, for the ego agent i fixed by the enclosing graph operator, writing rj=ρj(σ,φ,t)r_j= _j(σ, ,t), we may define the fold as the ordered pair in M=K×RM=K× R: E(rj)=(⨁jrj,(j,t)∣j∈iτ,∘(t,W)),A_E(\r_j\)= (\, _jr_j,\;\\,(j,t) j _i^τ, (t,W)\,\\, ), where the first component is the scalar aggregate in K and the second is the witness set in R. More generally, R may track only those neighbors that contribute positively (e.g. rj≻⊥Kr_j _K). Readout and Coupling. The readout map h:M→Kh:M→ K allows the relational component to influence the final semantic value. A general form is: h(r,R)=Φ(r,π(R))h(r,R)= (r,\; _V(R) ), where π(R)=i∣∃t,(i,t)∈R _V(R)=\\,i ∃ t,\ (i,t)∈ R\,\ projects onto the set of participating agents, and Φ combines signal-level and structural information. For e.g., a hybrid robustness measure augments the scalar robustness r with a count-based term: h(r,R)=r+α(|π(R)|),h(r,R)=r+α (| _V(R)| ), where α∈ℝα is some constant. General Semiring Compositions. More generally, the product construction extends to arbitrary families of semirings: K=∏ℓ=1mKℓ,M=∏ℓ=1mMℓ,K= _ =1^mK_ ,\ M= _ =1^mM_ , with layer-specific aggregation and readout maps. This enables the simultaneous propagation of multiple semantic quantities, such as: (a) robustness values, (b) counts or densities, (c) witness sets, (d) probabilistic weights. Thus, STL-GO admits a unified algebraic semantics in which temporal, spatial, and structural information are propagated compositionally through product semiring constructions. For some examples of algebras to pick for different semantic objectives, the reader is encouraged to look at Appendix 0.A. 4 Structural Guarantees and Complexity We now characterize when the generalized aggregation framework described yields semantics that are consistent with Boolean satisfaction. Definition 6(Soundness and Completeness). We write σ,i,t⊧φσ,i,t to denote that agent i satisfies φ at time t along trace σ. In addition, we associate to each formula a quantitative semantics (robustness value) ρi(σ,φ,t)∈K, _i(σ, ,t)∈ K, which measures the degree of satisfaction of the formula in the underlying algebra K. The quantitative semantics defined by the function ρi(σ,φ,t)∈K _i(σ, ,t)∈ K is sound if ρi(σ,φ,t)≻⊥K⇒σ,i,t⊧φ, _i(σ, ,t) _K\; \;σ,i,t , and complete if σ,i,t⊧φ⇒ρi(σ,φ,t)⪰⊥K,σ,i,t \; \; _i(σ, ,t) _K, i.e., soundness ensures that positive robustness implies satisfaction, while completeness ensures all satisfying configurations are assigned non-negative robustness. Throughout we adopt the standard STL convention in which the threshold value ⊥K _K itself counts as satisfying, so that the boundary case ρi(σ,φ,t)=⊥K _i(σ, ,t)= _K is treated as (weak) satisfaction. The temporal semantics are sound and complete by classical results [11]; our goal is to identify conditions the graph-operator pipeline K∗→EM→ℎK^* A_EM hK preserves this property. Throughout, we assume that K is equipped with a partial order ⪯ compatible with the semiring operations, and write ⊥K _K for the threshold separating satisfaction from violation (e.g., 0∈ℝ∞0 ^∞ for the min-max algebra). Before turning to soundness and completeness, we first record a weaker but very general structural property of the layered semantics. Namely, if each stage of the graph-aggregation pipeline is monotone w.r.t. the natural orders on the semantic and aggregation spaces, the overall operator preserves the pointwise ordering of agent-wise valuations. This result is independent of any particular interpretation of the threshold ⊥K _K and applies to scalar, product, and hybrid semantics. Definition 7(Monotone map). A function f:X→Yf:X→ Y between partially ordered sets is monotone if x⪯x′⇒f(x)⪯f(x′).x x \; \;f(x) f(x ). Monotonicity implies that increasing the robustness of inputs does not decrease the value of the output. Theorem 4.1(Order preservation of layered aggregation). Let (K,⪯K)(K, _K) be a partially ordered semiring, and let S:=KS:=K^V be the induced semimodule of agent-indexed valuations equipped with the pointwise order s⪯Ss′⟺s(i)⪯Ks′(i)∀i∈.s _Ss \ \ s(i) _Ks (i)\;\;∀ i . Let (M,⪯M)(M, _M) be a partially ordered aggregation space. Fix an agent i∈i , time t, graph type τ∈τ , and consider the graph-aggregation pipeline S→resiτKiτ,∘(t,W)→EM→ℎK,S res_i^τK^N_i^τ, (t,W) A_EM hK, where resiτres_i^τ denotes restriction of an agent-wise valuation to the eligible neighborhood iτ,∘(t,W)N_i^τ, (t,W). Assume: (1) the restriction map resiτres_i^τ is order-preserving; (2) the fold map EA_E is monotone with respect to the product order on Kiτ,∘(t,W)K^N_i^τ, (t,W); (3) the readout map h:M→Kh:M→ K is monotone; (4) the graph-type quantifier #KQ_\#^K is monotone with respect to the pointwise order on K||K^|T|. Then the induced local graph operator Ti#:S→KT_i^\#:S→ K is monotone, i.e., s⪯Ss′⟹Ti#(s)⪯KTi#(s′).s _Ss \ \ T_i^\#(s) _KT_i^\#(s ). If this holds for every agent i∈i , then the induced global operator T:S→S,(T(s))(i):=Ti#(s),T:S→ S,\ (T(s))(i):=T_i^\#(s), is monotone with respect to the pointwise order on S. Proof. Refer to Appendix 0.B.1 for the proof. ∎ Theorem 4.1 is the structural basis for the results that follow. Proposition 1(Soundness and Completeness of Graph Aggregation). Let (K,⊕,⊗,⊖,⊥K,⊤K)(K, , , , _K, _K) be a partially ordered De Morgan algebra with order ⪯ . Let (M,⊞,e)(M, ,e) be a commutative monoid with order ⪯M _M, and let E:K∗→M,h:M→KA_E:K^*→ M, h:M→ K define the aggregation pipeline for a count constraint E=[e1,e2]E=[e_1,e_2]. Define the composed map FE:=h∘E:K∗→K.F_E:=h _E:K^*→ K. Assume: (1) For each input rjr_j, rj≻⊥K⟺neighbor j satisfies φ;r_j _K\; \;neighbor j satisfies ; (2) For every configuration rj\r_j\, if c+=|j:rj≻⊥K|c^+=|\j:r_j _K\|, c+∈[e1,e2]⇒FE(rj)⪰⊥Kc^+∈[e_1,e_2]\; \;F_E(\r_j\) _K, and c+∉[e1,e2]⇒FE(rj)≺⊥K.c^+∉[e_1,e_2]\; \;F_E(\r_j\) _K. Then the induced graph operator is sound and complete. Consequently, since by Assumption 1 c+=|j:σ,j,t⊧φ|c^+= |\\,j:σ,j,t \,\ |, the quantitative sign agrees with Boolean satisfaction: FE(rj)⪰⊥K⟺(ℳ,i,t)⊧,EW,#φ,F_E(\r_j\) _K\; \;(M,i,t) _G,E^W,\# , where the threshold value ⊥K _K is treated as satisfying, in keeping with the boundary convention of Definition 6. Proof. Refer to Appendix 0.B.2 for the proof. ∎ Lemma 1(Quantifiers preserve threshold semantics). Let (K,⊕,⊗,⊖,(K, , , , ⊥K,⊤K) _K, _K) be an ordered De Morgan algebra, and let V be finite. Assume that for all finite families xii∈I⊆K\x_i\_i∈ I K, ⨁i∈Ixi≻⊥K⇔∃i∈I:xi≻⊥K, and ⨂i∈Ixi≻⊥K⇔∀i∈I:xi≻⊥K. _i∈ Ix_i _K ∃ i∈ I:x_i _K, and _i∈ Ix_i _K ∀ i∈ I:x_i _K. Then the multi-agent quantifiers satisfy: ρ(σ,φ,t)≻⊥K⇔∃i∈:ρi(σ,φ,t)≻⊥K, and ρ(σ,EX_V\, ,t) _K ∃ i : _i(σ, ,t) _K, and ρ(σ,φ,t)≻⊥K⇔∀i∈:ρi(σ,φ,t)≻⊥K.ρ(σ,FA_V\, ,t) _K ∀ i : _i(σ, ,t) _K. Consequently, if the agent-local semantics of φ are sound and complete, then so are the multi-agent quantifiers φEX_V\, and φFA_V\, .222The strict separation (≻⊥K _K) used in the equivalences above is consistent with the weak completeness convention of Definition 6: a boundary input xi=⊥Kx_i= _K leaves both sides of the relevant equivalence false (for ⨂=min = ) or is absorbed by a strictly positive term (for ⨁=max = ), so no satisfying configuration is misclassified. Proof. Refer to Appendix 0.B.3 for the proof. ∎ Theorem 4.2(End-to-end soundness and completeness). Assume that: (1) atomic predicate valuations are sound and complete, i.e., for every atomic predicate μ, ρi(σ,μ,t)≻⊥K⇔σ,i,t⊧μ, _i(σ,μ,t) _K σ,i,t μ, (2) the temporal/Boolean operators admit an interpretation over (K,⊕,⊗,⊖,⊥K,⊤K)(K, , , , _K, _K) that is sound and complete with respect to the Boolean STL semantics; (3) each graph operator satisfies Proposition 1; (4) the multi-agent quantifiers satisfy Lemma 1, and the graph-type quantifiers satisfy Proposition 1; then for every STL-GO formula ϕφ, ρ(σ,ϕ,t)≻⊥K⟺σ,t⊧ϕ,ρ(σ,φ,t) _K σ,t φ, that is, the quantitative semantics are sound and complete with respect to the Boolean semantics. Proof. Refer to Appendix 0.B.4 for the proof. ∎ The preceding results establish soundness and completeness by verifying that each syntactic construct (temporal and graph operators, and quantifiers) preserves correspondence between quantitative robustness and Boolean satisfaction. Monitoring Algorithm and Runtime Complexity. In Algorithm 1 we describe a bottom-up procedure (with respect to the specification syntax) that computes the robustness of a given finite multi-agent trace, generalizing the Boolean STL-GO monitor of [35]. Algorithm 1 Quantitative monitoring of STL-GO 1:Trace σ; formula ϕφ; algebra K; accumulator EA_E, readout h. 2:for all subformulae ψ of ϕφ, bottom-up; agents i; times t do 3: switch root operator of ψ do 4: case μ (predicate): ρi(σ,ψ,t)←ν(t,i,μ) _i(σ,ψ,t)←ν(S_t,i,μ) 5: end case 6: case ¬,∧,[t1,t2] , ,\,U_[t_1,t_2]\, (Boolean/temporal): apply ⊖,⊗ , , and the [t1,t2]\,U_[t_1,t_2]\, recurrence over K 7: end case 8: case ,EX_V,FA_V (quantifier): apply ⨁i,⨂i _i, _i over K 9: end case 10: case ,EW,#ψ1In_G,E^W,\# _1 / ,EW,#ψ1Out_G,E^W,\# _1 (graph): 11: ρi(σ,ψ,t)←#K(h(E(ρj(σ,ψ1,t)∣j∈iτ,∘(t,W))))τ∈ _i(σ,ψ,t) ^K_\# (\,h(A_E(\ _j(σ, _1,t) j ^τ, _i(t,W)\))\, )_τ 12: end case 13: end switch 14:end for 15:return ρ(σ,ϕ,⋅)ρ(σ,φ,·) Theorem 4.3(Monitoring complexity). Let φ be an STL-GO formula of size |φ|| |, evaluated over N agents, horizon T, and M graph types. Let Δ:=maxi,t,τ|iτ,∘(t,W)| := _i,\,t,\,τ |N^τ, _i(t,W) | denote the largest number of eligible neighbors any agent i has in any graph type τ at any time t. Assume that (i) all temporal operators use fixed-size bounded windows, (i) the eligible-neighbor sets iτ,∘(t,W)N^τ, _i(t,W) are precomputed, and (i) each accumulator update, readout, and semiring operation takes O(1)O(1) time. Then Algorithm 1 computes the robustness signal ρ(σ,φ,⋅)ρ(σ, ,·) in O(|φ|NTMΔ)O\! (| |\,N\,T\,M\, ) time. Proof. Refer to Appendix 0.B.5 for the proof. ∎ 5 Experiments (a) ||=100|V|=100 (b) ||=20,Ns=14,Nf=6|V|=20,N_s=14,N_f=6 Figure 2: (a) Environment 1: 50x50 space with 100 agents, (b) Environment 2: 3D environment with 14 agents on the sphere, and 6 agents in space. We evaluate the STL-GO robustness semantics on two multi-agent simulation environments with distinct dynamics and interaction structures: The two environments are chosen to stress different aspects of the semantics. Environment 1: 2D Bounded Region. We simulate N∈10,20,50,100N∈\10,20,50,100\ agents over T=50T=50 discrete timesteps moving in a bounded planar region [−50,50]2⊂ℝ2[-50,50]^2 ^2. Each agent’s state is ti=(xti,yti,θti)∈ℝ2×[0,2π)s^i_t=(x^i_t,y^i_t,θ^i_t) ^2×[0,2π), comprising position and heading angle. The dynamics follow a stochastic Dubins-car model: xt+1i=xti+vticosθt+1iΔt,yt+1i=yti+vtisinθt+1iΔt,θt+1i=(θti+ωtiΔt)mod2π,x^i_t+1=x^i_t+v^i_t θ^i_t+1 t,\ \ y^i_t+1=y^i_t+v^i_t θ^i_t+1 t,\ \ θ^i_t+1=(θ^i_t+ω^i_t t) 2π, where vti∼Unif[0,10]v^i_t [0,10] and ωti∼Unif[−π/4,π/4]ω^i_t [-π/4,π/4] are linear and angular velocities. (See Fig. 2(a)). The 2D Dubins-car region models a planar multi-robot team (e.g. ground search-and-rescue or distributed sensing), where the sensing/communication graphs are dense and time-varying, stressing the graph-operator aggregation over large neighborhoods. Environment 2: 3D Sphere and Free Space. This environment is inspired by Earth-satellite systems, with two agent classes: ground stations constrained to a spherical surface and satellites moving freely in 3D space (T=50T=50, Fig. 2(b)). Sphere-constrained agents (NsN_s). Each agent’s state is parameterized by spherical angles (θti,ϕti)(θ^i_t,φ^i_t) on a sphere of radius RsR_s, with Cartesian position given by (xti,yti,zti)=Rs(sinθticosϕti,sinθtisinϕti,cosθti)(x^i_t,\,y^i_t,\,z^i_t)=R_s\,( θ^i_t φ^i_t,\; θ^i_t φ^i_t,\; θ^i_t). The dynamics follow a random angular walk with Δθti,Δϕti∼Unif[−π/8,π/8] θ^i_t, φ^i_t [-π/8,π/8] applied additively. Free-space agents (NfN_f). These agents move freely in ℝ3R^3, initialized at some radius RfR_f from the origin. At each timestep, small perturbations are applied in spherical coordinates: Δϕti,Δθti∼Unif[−π/100,π/100] φ^i_t, θ^i_t [-π/100,π/100] and Δrti∼Unif[−0.1,0.1] r^i_t [-0.1,0.1], producing slow drifting trajectories near their initial radii. This system models a heterogeneous space-asset network (ground stations on a sphere, free-flying satellites), where connectivity is sparse and geometry-driven, stressing the multi-graph quantification and edge-weight constraints spanning the dense/sparse and homogeneous/heterogeneous regimes that arise in real distributed CPS. Interaction Graphs. At each timestep, three interaction graphs are computed from the pairwise Euclidean distances dijt=‖ti−tj‖2d^t_ij=\|p^i_t-p^j_t\|_2: (i) Distance graph tdistG^dist_t: a weighted complete graph with edge weight wijt=dijtw^t_ij=d^t_ij for i≠ji≠ j. (i) Sensing graph tsenseG^sense_t: an unweighted graph with edge (i,j)(i,j) iff dijt≤Rsensed^t_ij≤ R_sense and j is within the field of view of i, i.e. the angle between the relative position tj−tip^j_t-p^i_t and i’s heading vector (cosθti,sinθti)( θ^i_t, θ^i_t) is at most a half-angle β. (i) Communication graph tcommG^comm_t: an unweighted graph with edge (i,j)(i,j) iff dijt≤Rcommd^t_ij≤ R_comm. The topology of all the graphs changes at every timestep as agents move. Specifications. We consider the following STL-GO specifications of increasing complexity, parameterized by a nesting depth ℓ≥0 ≥ 0. Incoming reachability (φℓr-in ^r-in_ ): The specifications φℓr-in ^r-in_ (Eq. 1) is defined by recursively nesting the In operator over the sensing graph tsenseG^sense_t, with edge-count bound E=[1,4]E=[1,4] and unconstrained weights W=[−∞,∞]W=[-∞,∞]. It asserts that there exists an agent which, at some time within [0,10][0,10], can be reached from a goal-satisfying agent via ℓ successive incoming edges over the sensing graph. ψ0 _0 =tsense,EW,∃,ψℓ+1=tsense,EW,∃ψℓ,φℓr-in=[0,10]ψℓ, =In_G^sense_t,E^W,∃\, goal,\; _ +1=In_G^sense_t,E^W,∃\, _ ,\; ^r-in_ =EX_V\,F_[0,10]\, _ ,\; (1) Bi-directional reachability(φℓbi-dir ^bi-dir_ ): The formulas φℓbi-dir ^bi-dir_ (Eq. 2) necessitate bi-directional reachability over tsense,tcommG^sense_t,G^comm_t, with E=[1,2]E=[1,2] and W=[−∞,∞]W=[-∞,∞]. The recursively defined subformulas ψℓψ out_ and ψℓψ in_ check reachability to a goal-satisfying agent via ℓ outgoing and incoming hops, respectively. Thus, φℓbi-dir ^bi-dir_ asserts that, within [0,10][0,10], there exists an agent that can both reach and be reached by a goal-satisfying agent in ℓ hops. ψ0 ψ out_0 =tsense,tcomm,EW,∃,ψℓ+1=tsense,tcomm,EW,∃ψℓ =Out_\G^sense_t,G^comm_t\,E^W,∃\, goal, ψ out_ +1=Out_\G^sense_t,G^comm_t\,E^W,∃\,ψ out_ (2) ψ0 ψ in_0 =tsense,tcomm,EW,∃,ψℓ+1=tsense,tcomm,EW,∃ψℓ, =In_\G^sense_t,G^comm_t\,E^W,∃\, goal, ψ in_ +1=In_\G^sense_t,G^comm_t\,E^W,∃\,ψ in_ , φℓbi-dir ^bi-dir_ =[0,10](ψℓ∧ψℓ),ℓ=0,1,… =EX_V\,F_[0,10] (ψ out_ ψ in_ ), =0,1,… Figure 3: Robustness values across semantics for a sampled trajectory. Alternating Spatio-temporal operators (φℓr-sp ^r-sp_ ): These specifications (Eq. 3) interleave spatial and temporal operators in alternation over tdist,tsense,tcommG^dist_t,G^sense_t,G^comm_t graphs with edge-count bound E=[1,20]E=[1,20] and weight interval W=[0,20]W=[0,20]. At each nesting level ℓ , a temporal operator =, T=\F,G\ is applied first, followed by a spatial operator =, S=\In,Out\. This allows the specification to encode diverse spatio-temporal patterns. The atomic predicate goal holds at agent i iff its position lies within the goal region goal⊂ℝdG_goal ^d. At each nesting level ℓ , the temporal operator ℓ∈, T_ ∈\F,G\ and the spatial operator ℓ∈,EW,∃,,EW,∃ S_ ∈\In_G,E^W,∃,Out_G,E^W,∃\ alternate, and the graph type is drawn cyclically from tdist,tsense,tcomm\G^dist_t,G^sense_t,G^comm_t\. ψ0sp=,ψℓ+1sp=ℓℓψℓsp,φℓr-sp=[0,10]ψℓsp,ℓ=0,1,…ψ^sp_0= goal, ψ^sp_ +1= T_ \; S_ \;ψ^sp_ , ^r-sp_ =EX_VF_[0,10]\,ψ^sp_ , =0,1,… (3) These formulae isolate the semantic target of the operators: φℓr-in ^r-in_ stresses nested incoming count-constrained reachability; φℓbi-dir ^bi-dir_ adds multi-graph bidirectional reachability; and φℓr-sp ^r-sp_ interleaves temporal and spatial operators to exercise layered composition. The recursive nesting depth ℓ controls the scaling complexity. Evaluation Metrics and Methodology. For each environment, we evaluate STL-GO specifications under four semantic instantiations: (i) Boolean: classical qualitative satisfaction (K=K=B), yielding a binary verdict; (i) Min-max: standard STL robustness with the accumulator Emm=min(r(e1),−r(e2+1))A^m_E= (r_(e_1),-r_(e_2+1)); (i) Signed-deficit: the counting accumulator Ecd(rj)=c−e1A^cd_E(\r_j\)=c-e_1 if c<e1c<e_1, min(c−e1,e2−c) (c-e_1,\,e_2-c) if e1≤c≤e2e_1≤ c≤ e_2, and e2−ce_2-c if c>e2c>e_2, where c=|j:rj⪰⊥K|c=|\j:r_j _K\| counts satisfying neighbors; (iv) Hybrid: the deficit-corrected accumulator Eh=r(k)+αEcd(rj)A^h_E=r_(k)+ ^cd_E(\r_j\) (writing k:=e1k:=e_1 for the count threshold), combining min-max and signed-deficit with exchange-rate parameter α>0α>0. Signed-deficit counts c=|j:rj⪰⊥K|c=|\j:r_j _K\| using the non-strict threshold, so a nested subformula satisfied at zero margin is still counted, and is sound and complete under the non-strict (⪰ ) convention. All share the same temporal De Morgan algebra for temporal operators and differ in the graph-operator accumulator. We measure the wall-clock T(s) to evaluate the full STL-GO specification for all agents at all timesteps, averaged over 100 independently generated trajectories and graph sequences. To assess scalability, we vary two parameters independently: (i) the number of agents ||∈10,20,50,100|V|∈\10,20,50,100\ with fixed T=50T=50, which affects neighbor set sizes and the cost of the accumulator and multi-agent quantifiers; and (i) the time horizon T∈10,20,50,100T∈\10,20,50,100\ with fixed ||=20|V|=20, which affects the cost of temporal operators. For each configuration, we report average monitoring time per trajectory across 100 runs, broken down by semantic instantiation. Table 1: Results across φℓr-in ^r-in_ , φℓbi-dir ^bi-dir_ (denoted φℓb-d ^b-d_ ), and φℓr-sp ^r-sp_ over increasing recursive depths. For each, we report the percentage of satisfying trajectories (Sat.%), the robustness range [min,max][ , ] over the 100 trajectories, and computation time (T, seconds) for 100 trajectories, at fixed horizon T=50T=50. For Boolean semantics this range lies in 0,1\0,1\, so [0,1][0,1] indicates mixed verdicts and [1,1][1,1] universal satisfaction. φℓr-in ^r-in_ and φℓb-d ^b-d_ use the 2D environment (||=100|V|=100); φℓr-sp ^r-sp_ uses the 3D environment (Ns=14N_s=14, Nf=6N_f=6). Robustness and time are rounded to the nearest integer. Spec Sat.% Bool. Min-Max Sign.-Def. Hybrid [min,max][ , ] T(s) [min,max][ , ] T(s) [min,max][ , ] T(s) [min,max][ , ] T(s) φ0r-in ^r-in_0 94 [0,1][0,1] 3 [−7,9][-7,9] 3 [−1,1][-1,1] 3 [−17,25][-17,25] 3 φ1r-in ^r-in_1 67 [0,1][0,1] 3 [−16,9][-16,9] 3 [−1,1][-1,1] 3 [−36,19][-36,19] 3 φ2r-in ^r-in_2 55 [0,1][0,1] 3 [−16,9][-16,9] 3 [−1,1][-1,1] 3 [−46,26][-46,26] 3 φ3r-in ^r-in_3 54 [0,1][0,1] 3 [−16,9][-16,9] 3 [−1,1][-1,1] 3 [−56,28][-56,28] 3 φ4r-in ^r-in_4 54 [0,1][0,1] 3 [−16,9][-16,9] 3 [−1,1][-1,1] 4 [−66,36][-66,36] 3 φ0b-d ^b-d_0 100 [1,1][1,1] 12 [3,10][3,10] 11 [0,0][0,0] 11 [4,20][4,20] 11 φ1b-d ^b-d_1 100 [1,1][1,1] 30 [3,10][3,10] 28 [0,0][0,0] 27 [7,30][7,30] 27 φ2b-d ^b-d_2 100 [1,1][1,1] 81 [3,10][3,10] 73 [0,0][0,0] 71 [8,40][8,40] 76 φ0r-sp ^r-sp_0 65 [0,1][0,1] 1 [−18,10][-18,10] 1 [−1,1][-1,1] 1 [−28,20][-28,20] 1 φ1r-sp ^r-sp_1 10 [0,1][0,1] 1 [−14,9][-14,9] 1 [−1,0][-1,0] 1 [−34,19][-34,19] 1 φ2r-sp ^r-sp_2 26 [0,1][0,1] 6 [−19,10][-19,10] 6 [−1,1][-1,1] 6 [−49,37][-49,37] 6 φ3r-sp ^r-sp_3 6 [0,1][0,1] 71 [−6,10][-6,10] 69 [−1,0][-1,0] 68 [−46,30][-46,30] 75 (a) Ablation on time horizon T. T Bool M SD Hyb. 10 0.29 0.31 0.32 0.30 20 0.62 0.71 0.73 0.74 50 2.31 3.24 2.84 3.07 100 6.70 10.65 9.58 9.68 (b) Ablation on number of agents. |||V| Bool M SD Hyb. 10 1.21 1.25 1.27 1.51 20 2.16 3.09 2.86 2.87 50 9.31 10.10 9.90 10.38 100 25.35 26.68 27.61 26.19 Table 2: Ablation: wall-clock time T(s) for φ2r-in ^r-in_2 over 100 trajectories, varying time horizon T (left, fixed ||=20|V|=20) and number of agents |||V| (right, fixed T=50T=50). Semantics: Boolean (Bool), Min-max (M), Signed-Deficit (SD), Hybrid (Hyb.). Results and Discussion. From Table 1 we see that across all specifications the four semantics produce identical Boolean outcomes (Sat./Vio.), confirming that the quantitative semantics preserve correctness with respect to Boolean satisfaction; Fig. 3 visualizes this for a sampled trajectory.333Boolean is drawn as a post-step switching only at integer samples, while the quantitative curves are linearly interpolated; a Min-Max zero-crossing and the Boolean transition may thus appear shifted by up to one timestep, even though they agree in sign at each sampled t. Runtimes are similar for the simpler φℓr-in ^r-in_ , while differences grow with complexity in φℓbi-dir ^bi-dir_ and φℓr-sp ^r-sp_ , signed-deficit typically being fastest due to its simpler aggregation. The hybrid semantics is slightly more expensive but provides richer information: its larger range reflects the count-based term, which grows with the number of participating agents rather than being bounded by extrema. We emphasize that the four semantics compute different quantities and are not meant to compete on a single axis; the timing comparison quantifies the overhead of the richer accumulators relative to the Boolean baseline, establishing acceptable cost. Table 2 reports the effect of time horizon T and number of agents |||V| on runtime for the spec φ2r-in ^r-in_2. We fix φ2r-in ^r-in_2 as the ablation baseline because it exercises nested graph operators without the large constant factors of the bi-directional family, making it ideal for isolating the effects of T and |||V|. Across |||V|, all four semantics scale near-identically, with differences within run-to-run variation. The clearest separation appears in the time horizon T, where the Boolean semantics scales best and the three quantitative accumulators track one another closely. Conclusions. We introduced a unified algebraic framework for quantitative semantics of STL-GO, separating temporal reasoning, graph aggregation, and multi-agent quantification. A key insight is that graph-based aggregation cannot, in general, be captured by standard semiring operations alone; instead, the structure of the aggregator determines whether the quantitative semantics align with Boolean satisfaction, and under appropriate conditions we obtain compositional soundness and completeness. Our experiments show that these semantics preserve Boolean correctness while incurring only modest overhead and scaling predictably with problem size. The proposed framework relies on the choice of aggregation operators, which must be threshold-aligned with Boolean semantics. While we identify suitable classes (e.g., order-statistic and hybrid), systematic construction of expressive and well-behaved (e.g., smooth) aggregators remains open. Future work includes developing efficient algorithms, designing smooth aggregators, and extending the framework to stochastic multi-agent settings. References [1] T. Akazaki and I. Hasuo (2015) Time robustness in mtl and expressivity in hybrid system falsification. In International Conference on Computer Aided Verification, p. 356–374. Cited by: §1. [2] S. Alsalehi, N. Mehdipour, E. Bartocci, and C. Belta (2021) Neural network-based control for multi-agent systems from spatio-temporal specifications. In 2021 60th IEEE Conference on Decision and Control (CDC), p. 5110–5115. Cited by: §1. [3] A. Balakrishnan and J. V. Deshmukh (2019) Structured reward shaping using signal temporal logic specifications. In 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), Vol. , p. 3481–3486. External Links: Document Cited by: §1. [4] A. Balakrishnan, S. Jaksic, E. Aguilar, D. Nickovic, and J. Deshmukh (2022) Poster abstract: model-free reinforcement learning for symbolic automata-encoded objectives. In Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, HSCC ’22, New York, NY, USA. External Links: ISBN 9781450391962, Link, Document Cited by: §1. [5] A. Balakrishnan, S. Paul, S. Silvetti, L. Nenzi, and J. V. Deshmukh (2025) Monitoring spatially distributed cyber-physical systems with alternating finite automata. In Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control, HSCC ’25, New York, NY, USA. External Links: ISBN 9798400715044, Link, Document Cited by: §1, §2.2. [6] E. Bartocci, L. Bortolussi, M. Loreti, and L. Nenzi (2017-09) Monitoring mobile and spatially distributed cyber-physical systems. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE ’17, New York, NY, USA, p. 146–155. External Links: Document, ISBN 978-1-4503-5093-8 Cited by: §1. [7] E. Bartocci, L. Bortolussi, L. Nenzi, and G. Sanguinetti (2013) On the robustness of temporal properties for stochastic models. arXiv preprint arXiv:1309.0866. Cited by: §1. [8] H. Chen, S. Lin, S. A. Smolka, and N. Paoletti (2022) An stl-based formulation of resilience in cyber-physical systems. In International Conference on Formal Modeling and Analysis of Timed Systems, p. 117–135. Cited by: §1. [9] R. Cignoli and M. S. D. Gallego (1983-06) Dualities for some de morgan algebras with operators and lukasiewicz algebras. Journal of the Australian Mathematical Society 34 (3), p. 377–393. External Links: Document, ISSN 0263-6115 Cited by: Definition 3. [10] A. Donzé and O. Maler (2010) Robust satisfaction of temporal logic over real-valued signals. In Formal Modeling and Analysis of Timed Systems, K. Chatterjee and T. A. Henzinger (Eds.), Lecture Notes in Computer Science, Berlin, Heidelberg, p. 92–106. External Links: Document, ISBN 978-3-642-15297-9 Cited by: §1, §2.2. [11] G. E. Fainekos and G. J. Pappas (2009-09) Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410 (42), p. 4262–4291. External Links: Document, ISSN 0304-3975 Cited by: 1st item, §1, §2.2, §2.3, §4. [12] B. Finkbeiner and M. Zimmermann (2016) The first-order logic of hyperproperties. arXiv preprint arXiv:1610.04388. Cited by: §1. [13] J. S. Golan (1999) Semirings and their applications. Springer Netherlands, Dordrecht. External Links: Document, ISBN 978-90-481-5252-0 978-94-015-9333-5 Cited by: Definition 2. [14] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Gros, and C. Belta (2015) SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, p. 189–198. Cited by: §1. [15] I. Haghighi, N. Mehdipour, E. Bartocci, and C. Belta (2019) Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In 2019 IEEE 58th Conference on Decision and Control (CDC), p. 4361–4366. Cited by: §1. [16] S. Jakšić, E. Bartocci, R. Grosu, T. Nguyen, and D. Ničković (2018-08) Quantitative monitoring of stl with edit distance. Formal Methods in System Design 53 (1), p. 83–112. External Links: Document, ISSN 1572-8102 Cited by: §1. [17] R. Karagulle, C. Vasile, and N. Ozay (2025) Safe and optimal learning from preferences via weighted temporal logic with applications in robotics and formula 1. arXiv preprint arXiv:2511.08502. Cited by: §1. [18] V. Kudalkar, N. Hashemi, S. Mukhopadhyay, S. Mallick, C. Budnik, P. Nagaraja, and J. V. Deshmukh (2024) Sampling-based and gradient-based efficient scenario generation. In International Conference on Runtime Verification, p. 70–88. Cited by: §1. [19] V. Kudalkar, S. Ponguluri, A. Balakrishnan, and J. V. Deshmukh (2026) Sampling-based multi-agent path planning guided by spatio-temporal logic mission objectives. In Proceedings of the International Conference on Automated Planning and Scheduling, Vol. 36, p. 133–141. Cited by: §1. [20] W. Kuich and A. Salomaa (1986) Semirings, automata, languages. Springer Berlin Heidelberg, Berlin, Heidelberg. External Links: ISBN 978-3-642-69959-7 Cited by: Definition 2. [21] X. Li, C. Vasile, and C. Belta (2017) Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. Cited by: §1. [22] M. Ma, E. Bartocci, E. Lifland, J. Stankovic, and L. Feng (2020) SaSTL: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS), p. 51–62. Cited by: §1. [23] O. Maler and D. Nickovic (2004) Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Y. Lakhnech and S. Yovine (Eds.), Berlin, Heidelberg, p. 152–166. External Links: ISBN 978-3-540-30206-3 Cited by: §1, §2.2. [24] N. Mehdipour, C. Vasile, and C. Belta (2019) Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In 2019 American Control Conference (ACC), p. 1690–1695. Cited by: §1. [25] L. Nenzi, E. Bartocci, L. Bortolussi, and M. Loreti (2022-01) A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. Logical Methods in Computer Science Volume 18, Issue 1. External Links: Document, ISSN 1860-5974 Cited by: §1. [26] L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, and M. Massink (2018-10) Qualitative and quantitative monitoring of spatio-temporal properties with sstl. Logical Methods in Computer Science Volume 14, Issue 4. External Links: Document, Link Cited by: §1, §1. [27] Y. V. Pant, H. Abbas, and R. Mangharam (2017) Smooth operator: control using the smooth robustness of temporal logic. In 2017 IEEE Conference on Control Technology and Applications (CCTA), p. 1235–1240. Cited by: §1. [28] S. Paul, A. Balakrishnan, X. Qin, and J. V. Deshmukh (2024) Multi-agent path finding forătimed tasks using evolutionary games. In Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, J. Hillston, S. Soudjani, and M. Waga (Eds.), Cham, p. 302–321. Cited by: §1. [29] S. Paul and J. V. Deshmukh (2024-10) Survival of the fittest: evolutionary adaptation of policies for environmental shifts. In ECAI 2024, External Links: ISBN 9781643685489, ISSN 1879-8314, Link, Document Cited by: §1. [30] V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, and S. A. Seshia (2014) Model predictive control with signal temporal logic specifications. In 53rd IEEE Conference on Decision and Control, p. 81–87. Cited by: §1. [31] A. Rodionova, E. Bartocci, D. Nickovic, and R. Grosu (2016) Temporal logic as filtering. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, p. 11–20. Cited by: §1, §2.2. [32] G. Silano, A. Afifi, M. Saska, and A. Franchi (2025) STL-based motion planning and uncertainty-aware risk analysis for human-robot collaboration with a multi-rotor aerial vehicle. arXiv preprint arXiv:2509.10692. Cited by: §1. [33] M. Waga (2020) Falsification of cyber-physical systems with robustness-guided black-box checking. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, p. 1–13. Cited by: §1. [34] C. Yoo and C. Belta (2017) Rich time series classification using temporal logic. In Robotics: Science and Systems, Cited by: §1. [35] Y. Zhao, X. Yu, B. Hoxha, G. Fainekos, J. Deshmukh, and L. Lindemann (2025) STL-go: spatio-temporal logic with graph operators for distributed systems with multiple network topologies. ACM Transactions on Embedded Computing Systems 24 (5s), p. 1–23. Cited by: §1, §2.2, §4. Appendix Appendix 0.A Compositional Behavior of Algebraic Semantics Table 3: Algebraic instantiations of the aggregation pipeline for different semantics. (id = Identity). For the Hybrid row, the ⊞=(max,+) =( ,+) column gives the monoid operations on M=K×ℤM=K×Z; the first component is read out as the order statistic r(k)r_(k) (the k-th largest value, k:=e1k:=e_1), not a plain max -fold of the multiset. Semantics K (⊕,⊗)( , ) M ⊞ EA_E h Boolean B (∨,∧)( , ) B ∨ ⋁S⊆Ni|S|=e1⋀j∈Srj _ subarraycS N_i\\ |S|=e_1 subarray _j∈ Sr_j idid Min-max ℝ∞R^∞ (max,min)( , ) ℝ∞R^∞ max min(r(e1),−r(e2+1)) (r_(e_1),-r_(e_2+1) ) idid Sign.-def. ℝ∞R^∞ −- ℤZ ++ c−e1,c<e1min(c−e1,e2−c),e1≤c≤e2e2−c,c>e2 casesc-e_1,&c<e_1\\ (c-e_1,\,e_2-c),&e_1≤ c≤ e_2\\ e_2-c,&c>e_2 cases idid Hybrid ℝ∞R^∞ (max,min)( , ) K×ℤK×Z (max,+)( ,\,+) (r(k),Ecd) (r_(k),\,A^cd_E ) r(k)+αEcdr_(k)+α\,A^cd_E The algebraic semantics of STL-GO are parametric with respect to the underlying algebraic structures used for temporal, graph-based, and multi-agent aggregation. Different choices of these structures induce distinct interpretations of satisfaction, enabling logical, cost-based, and probabilistic reasoning within a unified framework. We summarize the principal design choices below. 0.A.1 Semiring choices. The temporal and multi-agent layers are governed by a De Morgan algebra (or semiring) (K,⊕,⊗,⊖,⊥,⊤)(K, , , , , ). Different instantiations yield different semantics: • Lattice-based semirings. (K,⊕,⊗)∈(,∨,∧),(ℝ∞,max,min)(K, , )∈\(B, , ),\;(R^∞, , )\. Both operations are idempotent: a⊕a=a a=a and a⊗a=a a=a, forming a bounded distributive lattice. A De Morgan negation exists (¬ for Boolean, −- for min-max), so the semantics of negation ρi(σ,¬φ,t)=⊖ρi(σ,φ,t) _i(σ, ,t)= \, _i(σ, ,t) are well-defined without restriction. The Boolean algebra yields qualitative satisfaction; the min-max algebra yields the standard STL robustness, where the value measures the perturbation margin [11]. • Tropical semirings. (K,⊕,⊗)∈(ℝ+∪∞,min,+),(ℝ∪−∞,max,+)(K, , )\!∈\!\(R^+∪\∞\, ,+),(R∪\-∞\, ,+)\. Here ⊕ selects the best alternative while ⊗=+ =+ accumulates values along a conjunction or temporal sequence, rather than taking a bottleneck. Multiplication is not idempotent (a+a≠a+a≠ a), and no De Morgan negation exists: one cannot define ⊖ satisfying ⊖(a⊕b)=⊖a⊗⊖b (a b)= a b when ⊕ and ⊗ have different algebraic structure. • Probabilistic and counting semirings. (ℝ≥0,+,×,0,1)(R_≥ 0,+,×,0,1), or its restriction to [0,1][0,1]. Neither operation is idempotent: p+p≠p+p≠ p and p×p≠p× p≠ p. A negation ⊖(p)=1−p (p)=1-p can be defined on [0,1][0,1], but it satisfies De Morgan’s laws only under an independence assumption (Pr(¬A)=1−Pr(A) ( A)=1- (A) is exact, but Pr(A∨B)=Pr(A)+Pr(B) (A B)= (A)+ (B) requires disjointness). The interpretation is probabilistic: conjunction multiplies probabilities and disjunction sums them, giving a satisfaction likelihood under stochastic dynamics. This family is relevant when agent behavior is modeled stochastically and one seeks to evaluate Pr(σ⊧ϕ) (σ φ) or an expected robustness. Table 4 summarizes the key properties. Table 4: Semiring families for the temporal and multi-agent layers. Family ⊕ /⊗ Idemp. De Morgan. ⊖ Cont. Interpretation Boolean ∨ / ∧ ✓ ✓ ✗ qualitative satisfaction Min-max max / min ✓ ✓ ✓ perturbation margin Tropical min / ++ ⊕ only ✗ ✓ cumulative cost Probabilistic ++ / × ✗ partial ✓ satisfaction likelihood 0.A.2 Graph aggregation choices. The graph operators aggregate a multiset of neighbor robustness values r1,…,rm\r_1,…,\\ r_m\⊂K⊂ K into a single value E(r1,…,rm)∈KA_E^K(r_1,…,r_m)∈ K, subject to the count constraint E=[e1,e2]E=[e_1,e_2]. This aggregation is not fixed by the semiring; we identify some examples, distinguished by the algebraic structure of their underlying aggregation. • Idempotent reducers. [ (K,max,min)(K, , ) or min-max selection]. Let rj=ρj(σ,φ,t)r_j= _j(σ, ,t) denote the robustness of φ at neighbor j, and sort the values in decreasing order: r(1)≥r(2)≥⋯≥r(m)r_(1)≥ r_(2)≥·s≥ r_(m), with the convention r(k)=−∞r_(k)=-∞ for k>mk>m. For a count interval E=[e1,e2]E=[e_1,e_2], define [e1,e2]os(r1,…,rm)=min(r(e1),−r(e2+1)).A_[e_1,e_2]^os(r_1,…,r_m)\;=\; \! (r_(e_1),\;-r_(e_2+1) ). The first term r(e1)r_(e_1) is positive iff at least e1e_1 neighbors have positive robustness; the second term −r(e2+1)-r_(e_2+1) is positive iff at most e2e_2 do. Their minimum is positive iff both conditions hold, i.e., iff the count of satisfying neighbors lies in [e1,e2][e_1,e_2]. The value measures the perturbation margin of the critical neighbor: how much the e1e_1-th best neighbor’s state can change before the count drops below e1e_1. It is sound ( i.e. the sign agrees with Boolean verdict), continuous in agent states. • Counting-based aggregators. [(ℤ,+,0,−)(Z,+,0,-), an abelian group]. Let c=|j:rj⪰⊥K|c=|\j:r_j _K\| and define [e1,e2]cd(r1,…,rm)=c−e1c<e1,min(c−e1,e2−c)e1≤c≤e2,e2−c>e2.A_[e_1,e_2]^cd(r_1,…,r_m)\;=\; casesc-e_1&c<e_1,\\ (c-e_1,\;e_2-c)&e_1≤ c≤ e_2,\\ e_2-c&c>e_2. cases The value measures the count surplus or deficit: how many neighbors could switch their Boolean verdict before the cardinality constraint breaks. A value of +3+3 means three neighbors could switch their Boolean verdict before the constraint breaks. It is discontinuous: a single neighbor’s robustness crossing zero induces a unit jump. • Averaging and linear aggregators. [(ℝ,+,⋅, 0,1)(R,+,·\,,\,0,1) with normalization by count]. We may define it as: [e1,e2]avg(r1,…,rm)=1m∑j=1mrj.A_[e_1,e_2]^avg(r_1,…,r_m)\;=\; 1m _j=1^mr_j. This measures the average quality of neighbor satisfaction, giving a smooth global summary that weights all neighbors equally rather than focusing on the critical one. It does not directly enforce the count constraint E. It is continuous and differentiable, but does not recover the Boolean semantics in general (a positive average does not imply that e1e_1 neighbors are individually satisfied). • Smooth or fuzzy aggregators. They include parameterized approximations, typically involving exp , log , or sigmoid functions. For example, a product-of-sigmoids ∏jσ(βrj) _jσ(β\,r_j) provides a smooth approximation to counting. They are differentiable everywhere, making them amenable to gradient-based optimization and learning. It has no clean algebraic characterization; soundness holds only approximately, with the approximation quality controlled by the temperature parameter β. Table 5 summarizes the key properties. Table 5: Accumulator families for the graph-operator layer. Family Sound Continuous Semiring Interpretation -derived min-max ✓ ✓ ✓ critical-neighbor margin Signed-deficit ✓ ✗ ✗ count surplus/deficit Averaging ✗ ✓ ✗ mean neighbor quality Smooth/fuzzy approx. ✓ ✗ differentiable surrogate Layer-wise composition. These algebraic choices may be applied uniformly across all layers, or selected independently for temporal, graph, and multi-agent aggregation. A uniform choice yields a consistent interpretation across time, structure, and agents, while heterogeneous choices allow greater flexibility, such as combining logical temporal reasoning with count-based graph aggregation. Appendix 0.B Theoretical Results 0.B.1 Proof of Theorem 1 Proof. Let s,s′∈Ss,s ∈ S with s⪯Ss′.s _Ss . By definition of the pointwise order on S, this means s(j)⪯Ks′(j)∀j∈.s(j) _Ks (j)\ ∀ j . Fix an agent i∈i and a graph type τ∈τ . Applying the restriction map to the eligible neighborhood Niτ,∘(t,W)N_i^τ, (t,W) yields resiτ(s)⪯resiτ(s′)res_i^τ(s) _i^τ(s ) in the product order on KNiτ,∘(t,W)K^N_i^τ, (t,W), since restriction simply selects a subset of coordinates and is order-preserving by assumption (1). By monotonicity of the fold map EA_E, we obtain E(resiτ(s))⪯ME(resiτ(s′)).A_E (res_i^τ(s) ) _MA_E (res_i^τ(s ) ). Applying the monotone readout map h:M→Kh:M→ K gives h(E(resiτ(s)))⪯Kh(E(resiτ(s′))).h\! (A_E (res_i^τ(s) ) ) _Kh\! (A_E (res_i^τ(s ) ) ). Thus, for every graph type τ, the corresponding per-type output is order-preserved. Collecting these values over all graph types produces two tuples in K||K^|T|, say (xτ)τ∈⪯(xτ′)τ∈, (x_τ )_τ (x _τ )_τ , again in the pointwise order. By monotonicity of the graph-type quantifier #KQ_\#^K, we conclude that Ti#(s)=#K((xτ)τ∈)⪯K#K((xτ′)τ∈)=Ti#(s′).T_i^\#(s)=Q_\#^K ((x_τ)_τ ) _KQ_\#^K ((x _τ)_τ )=T_i^\#(s ). Hence the local graph operator is monotone. If the same reasoning applies for every agent i∈i , then ∀i∀ i, (T(s))(i)=Ti#(s)⪯KTi#(s′)=(T(s′))(i).(T(s))(i)=T_i^\#(s) _KT_i^\#(s )=(T(s ))(i). Therefore T(s)⪯ST(s′),T(s) _ST(s ), which proves monotonicity of the global operator T:S→ST:S→ S. ∎ 0.B.2 Proof of Proposition 1 Proof. Fix an agent i, time t, graph type τ, and let τ=(ρj(σ,φ,t))j∈iτ,∘(t,W)r^τ= ( _j(σ, ,t) )_j _i^τ, (t,W) be the tuple of input values for that graph type. By Condition (1), rjτ≻⊥K⇔σ,j,t⊧φr_j^τ _K σ,j,t . Hence, c+(τ)=|j∈iτ,∘(t,W):σ,j,t⊧φ|,c^+(r^τ)= |\j _i^τ, (t,W):σ,j,t \ |, i.e., the number of positive inputs is exactly the number of satisfying neighbors. Now apply Condition (2): c+(τ)∈[e1,e2]⇔FE(τ)≻⊥K.c^+(r^τ)∈[e_1,e_2] F_E(r^τ) _K. Therefore, for each graph type τ, the quantitative output is positive if and only if the Boolean count constraint is satisfied. For existential graph-type quantification, the operator is ∃K=⨁τ∈.Q_∃^K= _τ . By sign-correctness of ⊕ , ⨁τxτ≻⊥K⇔∃τ:xτ≻⊥K. _τx_τ _K ∃τ\;:\;x_τ _K. Hence, ρi(σ,,EW,∃φ,t)≻⊥K _i(σ,In_G,E^W,∃ ,t) _K if and only if there exists a graph type τ for which the Boolean interval-count condition holds. This is exactly the Boolean semantics of the existential graph-type quantifier. We can similarly show the case for universal graph-type quantification using the ⨂ operator. The argument for outgoing operators is identical, replacing iτ,inN_i^τ,in by iτ,outN_i^τ,out. Thus the graph operators are sound and complete. ∎ 0.B.3 Proof for Lemma 1 Proof. By definition of the multi-agent semantics, ρ(σ,φ,t)=⨁i∈ρi(σ,φ,t),ρ(σ,φ,t)=⨂i∈ρi(σ,φ,t).ρ(σ,EX_V\, ,t)= _i _i(σ, ,t), ρ(σ,FA_V\, ,t)= _i _i(σ, ,t). Applying the assumed sign-correctness of finite ⊕ - and ⊗ -aggregations yields ρ(σ,φ,t)≻⊥K⇔∃i∈:ρi(σ,φ,t)≻⊥K,ρ(σ,EX_V\, ,t) _K ∃ i :\; _i(σ, ,t) _K, ρ(σ,φ,t)≻⊥K⇔∀i∈:ρi(σ,φ,t)≻⊥K.ρ(σ,FA_V\, ,t) _K ∀ i :\; _i(σ, ,t) _K. If the local semantics of φ are sound and complete, then ρi(σ,φ,t)≻⊥K⇒σ,i,t⊧φ,σ,i,t⊧φ⇒ρi(σ,φ,t)⪰⊥K. _i(σ, ,t) _K σ,i,t , σ,i,t _i(σ, ,t) _K. Combining these equivalences with the Boolean semantics of EX_V and FA_V gives soundness and completeness of the quantified formulas. ∎ 0.B.4 Proof for Theorem 2 Proof. The proof follows by structural induction on the formula ϕφ. Base case. If ϕφ is an atomic predicate, the result holds by assumption (1). Inductive step. Assume the claim holds for all immediate subformulas of ϕφ. If ϕφ is obtained from its subformulas using a Boolean or temporal operator, then the result follows directly from assumption (2), since the temporal/Boolean fragment is sound and complete over K. If ϕφ is obtained using a graph operator, then by the inductive hypothesis the inputs to the graph aggregation have the correct sign with respect to the Boolean semantics of the subformula. Hence the conditions of Proposition 1 apply, and the graph operator preserves soundness and completeness. If ϕφ is obtained by graph-type quantification or by multi-agent quantification, the result follows from Lemma 1, since these quantifiers preserve threshold semantics. If ϕφ is an agent embedding i.ψi.ψ, then ρ(σ,i.ψ,t)=ρi(σ,ψ,t)ρ(σ,i.ψ,t)= _i(σ,ψ,t), and the result follows immediately from the inductive hypothesis. Since all formation rules preserve soundness and completeness, the result holds for all STL-GO formulas ϕφ. ∎ 0.B.5 Proof of Theorem 4.3 Proof. Algorithm 1 performs a single bottom-up traversal of the parse tree, visiting each of the |φ|| | subformulae once, and for every subformula computes robustness values for all N agents and T time steps. Predicate, Boolean, temporal, and quantifier nodes require only constant-time algebraic operations per evaluation under the fixed-window assumption (i), yielding O(NT)O(NT) work per node. For a graph operator, each evaluation at agent i and time t iterates over the M graph types and folds the robustness values of the eligible neighbors iτ,∘(t,W)N^τ, _i(t,W), of which there are at most Δ . By assumptions (i) and (i), retrieving the neighbor set is free and each accumulator update and readout is O(1)O(1), so the fold costs O(Δ)O( ) per graph type and O(MΔ)O(M ) per (i,t)(i,t) pair. The graph-type quantifier Q#KQ^K_\# then combines the M per-type results in O(M)O(M), dominated by the fold. Thus a graph-operator node costs O(NTMΔ)O(NTM ). Since graph-operator nodes dominate all other node types, summing over the |φ|| | subformulae gives total runtime O(|φ|NTMΔ)O(| |\,N\,T\,M\, ). 444Since Δ≤N−1 ≤ N-1 always, this gives the worst-case bound O(|φ|N2TM)O(| |\,N^2\,T\,M); for sparse interaction graphs Δ≪N N and the cost is substantially lower. ∎ 0.B.6 General compositional soundness and completeness Theorem 0.B.1. Let K be a partially ordered set with threshold ⊥K _K, and define the positive and non-positive regions K+:=x∈K:x≻⊥K,K−:=x∈K:x⪯⊥K.K^+:=\x∈ K:x _K\,\ \ K^-:=\x∈ K:x _K\. Consider a compositional semantics in which each formula ϕφ is interpreted by a map ρ(σ,ϕ,t)∈K,ρ(σ,φ,t)∈ K, constructed recursively from: (i)atomic predicate valuations, (i) a collection of operators F:Kn→KF:K^n→ K applied to subformula values. Assume: 1. For every atomic predicate μ, ρ(σ,μ,t)∈K+⇔σ,t⊧μ;ρ(σ,μ,t)∈ K^+ σ,t μ; 2. for every semantic operator F:Kn→KF:K^n→ K, there exists a Boolean operator f:0,1n→0,1f:\0,1\^n→\0,1\ such that for all inputs x1,…,xn∈Kx_1,…,x_n∈ K, F(x1,…,xn)∈K+⇔f(x1∈K+,…,xn∈K+)=1.F(x_1,…,x_n)∈ K^+ f(1_x_1∈ K^+,…,1_x_n∈ K^+)=1. Then for every formula ϕφ, ρ(σ,ϕ,t)∈K+⇔σ,t⊧ϕ.ρ(σ,φ,t)∈ K^+ σ,t φ. That is, the quantitative semantics are sound and complete with respect to the Boolean semantics. Proof. The proof is by structural induction on the formula ϕφ. Base case. If ϕφ is an atomic predicate, the claim holds by assumption (1). Inductive step. Suppose ϕ=F(ϕ1,…,ϕn)φ=F( _1,…, _n) for some operator F. By the induction hypothesis, ρ(σ,ϕj,t)∈K+⇔σ,t⊧ϕjfor all j.ρ(σ, _j,t)∈ K^+ σ,t _j all j. Applying assumption (2), ρ(σ,ϕ,t)=F(ρ(σ,ϕ1,t),…,ρ(σ,ϕn,t))∈K+ρ(σ,φ,t)=F (ρ(σ, _1,t),…,ρ(σ, _n,t) )∈ K^+ if and only if f(σ,t⊧ϕ1,…,σ,t⊧ϕn)=1,f(1_σ,t _1,…,1_σ,t _n)=1, which is precisely the Boolean semantics of ϕφ. Thus the claim holds for ϕφ, completing the induction. ∎ Appendix 0.C Min-Max Robustness: Instantiation and Limitations We now instantiate the three-tier algebraic semantics with the min-max algebra (ℝ∞,max,min,−,−∞,+∞)(R^∞, , ,-,-∞,+∞) and the min-max accumulator, giving concrete robustness formulas for every operator in STL-GO. We then examine a family of examples that expose a structural limitation of the min-max accumulator and propose a parameterized alternative. Ego-centric STL-GO temporal operators. For agent i, trace σ, and time t: ρi(σ,μ,t) _i(σ,μ,t) =ν(t,i,μ), =ν(S_t,i,μ), ρi(σ,¬φ,t) _i(σ, ,t) =−ρi(σ,φ,t), =- _i(σ, ,t), ρi(σ,φ1∧φ2,t) _i(σ, _1 _2,t) =min(ρi(σ,φ1,t),ρi(σ,φ2,t)), = \! ( _i(σ, _1,t),\; _i(σ, _2,t) ), ρi(σ,φ1∨φ2,t) _i(σ, _1 _2,t) =max(ρi(σ,φ1,t),ρi(σ,φ2,t)), = \! ( _i(σ, _1,t),\; _i(σ, _2,t) ), ρi(σ,[t1,t2]φ,t) _i(σ,F_[t_1,t_2]\, ,t) =maxt′∈t+[t1,t2]ρi(σ,φ,t′), = _t ∈ t+[t_1,t_2]\; _i(σ, ,t ), ρi(σ,[t1,t2]φ,t) _i(σ,G_[t_1,t_2]\, ,t) =mint′∈t+[t1,t2]ρi(σ,φ,t′), = _t ∈ t+[t_1,t_2]\; _i(σ, ,t ), ρi(σ,φ1[t1,t2]φ2,t) _i(σ, _1\,\,U_[t_1,t_2]\,\, _2,t) =maxt′∈t+[t1,t2]min(ρi(σ,φ2,t′),mint′∈[t,t′]ρi(σ,φ1,t′)). = _t ∈ t+[t_1,t_2]\; \! ( _i(σ, _2,t ),\; _t ∈[t,\,t ]\, _i(σ, _1,t ) ). (4) The labelling function ν(t,i,μ)ν(S_t,i,μ) returns the signed distance of agent i’s state from the predicate boundary: positive if μ(ti)μ(s^i_t) holds, negative otherwise, with magnitude proportional to the margin. Graph operators. Fix agent i, time t, graph type τ, and let N=iτ,in(t,W)N=N_i^τ,in(t,W) be the set of qualifying incoming neighbors (those connected to i by an edge with weight in W). Let rj=ρj(σ,φ,t)r_j= _j(σ, ,t) for each j∈Nj∈ N, and sort these values as r(1)≥⋯≥r(|N|)r_(1)≥·s≥ r_(|N|), with the convention r(k)=−∞r_(k)=-∞ for k>|N|k>|N|. Then: ρi(σ,,EW,∃φ,t) _i(σ,In_G,E^W,∃ ,t) =maxτ:τ∈tmin(r(e1)τ,−r(e2+1)τ), = _τ:\,G^τ _t\; \! (r^τ_(e_1),\;-r^τ_(e_2+1) ), (5) ρi(σ,,EW,∀φ,t) _i(σ,In_G,E^W,∀ ,t) =minτ:τ∈tmin(r(e1)τ,−r(e2+1)τ). = _τ:\,G^τ _t\; \! (r^τ_(e_1),\;-r^τ_(e_2+1) ). (6) The outgoing operators ,EW,#Out_G,E^W,\# are identical with iτ,outN_i^τ,out in place of iτ,inN_i^τ,in. Multi-agent operators. ρ(σ,φ,t) ρ(σ,FA_V\, ,t) =mini∈ρi(σ,φ,t), = _i \; _i(σ, ,t), ρ(σ,φ,t) ρ(σ,EX_V\, ,t) =maxi∈ρi(σ,φ,t). = _i \; _i(σ, ,t). (7) The remaining multi-agent temporal operators (¬ , ∧ , ∨ , [t1,t2]\,U_[t_1,t_2]\,) follow the same min/max structure as the STL-GO operators. Limitations The min-max accumulator reports a single value: the margin of the k-th best neighbor, regardless of how many neighbors are satisfying or violating. This makes it insensitive to the count deficit: configurations that differ dramatically in the number of violating neighbors can receive identical robustness. Example.Fix |N|=6|N|=6 neighbors and the threshold k=e1=5k=e_1=5 (“at least 5 neighbors satisfy ψ”). Consider the neighbor robustness multisets in Table 6: S1S_1 has all six neighbors satisfying robustly; S2S_2 has exactly five at margin +10+10; S3S_3 also has five satisfying, but the 5th-best has margin only +0.5+0.5 (a much more fragile satisfaction); S4S_4–S6S_6 have 4,3,24,3,2 satisfying neighbors respectively, each at ±10± 10. Table 6: Neighbor robustness configurations (k=5k=5, |N|=6|N|=6). Neighbor robustness values S1S_1 +10,+10,+10,+10,+10,+10\+10,\;+10,\;+10,\;+10,\;+10,\;+10\ S2S_2 +10,+10,+10,+10,+10,−10\+10,\;+10,\;+10,\;+10,\;+10,\;-10\ S3S_3 +10,+10,+10,+10,+0.5,−10\+10,\;+10,\;+10,\;+10,\;+0.5,\;-10\ S4S_4 +10,+10,+10,+10,−10,−10\+10,\;+10,\;+10,\;+10,\;-10,\;-10\ S5S_5 +10,+10,+10,−10,−10,−10\+10,\;+10,\;+10,\;-10,\;-10,\;-10\ S6S_6 +10,+10,−10,−10,−10,−10\+10,\;+10,\;-10,\;-10,\;-10,\;-10\ S1S_1–S3S_3 satisfy the constraint (c+≥5c^+≥ 5); S4S_4–S6S_6 violate it (c+<5c^+<5). Ideally, the robustness should be: • positive for S1S_1–S3S_3, with S1>S2>S3>0S_1>S_2>S_3>0; • negative and decreasingly so from S4S_4 through S6S_6, reflecting the growing count deficit. Under the (i) min-max accumulator, S1S_1 and S2S_2 both receive +10+10: the accumulator cannot distinguish having one spare neighbor from having zero. S3S_3 receives +0.5+0.5, correctly reflecting its fragile 5th neighbor, but S4S_4 through S6S_6 all receive −10-10: a configuration missing one neighbor is indistinguishable from one missing five. The order statistic captures how robustly the critical neighbor satisfies ψ, but is entirely blind to how many neighbors are satisfying or missing. Under the (i) signed-deficit accumulator (c+−kc^+-k), the values +1, 0, 0, -1, -2, -3 provide a monotone gradation reflecting the count surplus or deficit (for this example e2=∞e_2=∞, so cdA^cd reduces to the single-sided c−e1c-e_1). However, S2S_2 and S3S_3 both receive exactly 0 despite S2S_2 being far more robust than S3S_3—the signed deficit discards all signal-margin information. We propose a (i) hybrid accumulator: r(k)+α(c+−k)r_(k)+α\,(c^+-k), combining the order statistic for signal-level margin with the scaled count deficit for sensitivity to the number of satisfying neighbors. The parameter α>0α>0 controls the exchange rate between signal margin (in robustness units) and count margin (in number of agents). As shown in Table 7: (a) S1>S2>S3>0S_1>S_2>S_3>0 for all α>0α>0: the surplus neighbor in S1S_1 is reflected as a bonus of +α+α, and S2S_2 vs. S3S_3 are distinguished by the critical neighbor’s margin (+10+10 vs. +0.5+0.5). (b) S4S_4 through S6S_6 are strictly decreasing, with the spacing growing with α: larger α amplifies the count-deficit penalty. (c) Within a fixed deficit level, the min-max term r(k)r_(k) still distinguishes configurations by the margin of the critical neighbor. Table 7: Accumulator comparison (k=5k=5, |N|=6|N|=6). ✓ : satisfies; ×: violates. Set Bool. c+c^+ Min-max. Sgn-def. Hybrid r(k)+α(c+−k)r_(k)+α(c^+-k) r(5)r_(5) c+−kc^+-k α=1α=1 α=5α=5 α=10α=10 S1S_1 ✓ 6 +10+10 +1+1 +11+11 +15+15 +20+20 S2S_2 ✓ 5 +10+10 0 +0 +10+10 +10+10 +10+10 S3S_3 ✓ 5 +0.5+0.5 0 +0 +0.5+0.5 +0.5+0.5 +0.5+0.5 S4S_4 × 4 −10-10 −1-1 −11-11 −15-15 −20-20 S5S_5 × 3 −10-10 −2-2 −12-12 −20-20 −30-30 S6S_6 × 2 −10-10 −3-3 −13-13 −25-25 −40-40