An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators
This work provides the first quantitative semantics for STL-GO, enabling robustness analysis for multi-agent systems with graph-based counting constraints, which is an incremental extension of existing spatio-temporal logic semantics.
The paper develops quantitative semantics for STL-GO, a logic for multi-agent systems, using a layered algebraic construction. The framework is implemented and evaluated on two multi-agent environments, demonstrating tradeoffs between accumulator choices and scalability.
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.