Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Alternating-time temporal logic and its extensions provide several ways of combining strategic and quantitative reasoning. We study a particular combination: whether a coalition has a single strategy that enforces a temporal objective while guaranteeing given long-run mean-payoff thresholds. We introduce ATL_mp, an extension of ATL over weighted concurrent game structures in which each strategic modality carries a conjunctive mean-payoff constraint. The temporal and quantitative requirements must hold against every behaviour of the remaining agents, and the existence of such a strategy cannot in general be reduced to the two requirements considered separately. For one-dimensional constraints, model checking is 2EXPTIME-complete under both perfect-recall and finite-memory semantics, matching ATL*. For the pure quantitative fragment and fragments restricted to ATL or GR(1) temporal objectives, model checking has lower complexity. With multi-dimensional conjunctive constraints, model checking under finite-memory semantics remains 2EXPTIME-complete. We show that memoryless, finite-memory, and perfect-recall abilities form a strict hierarchy, while finite-memory strategies still achieve every threshold strictly below the perfect-recall supremum. We give tight linear upper and lower bounds on the required memory as a function of the denominator of the threshold, even when the game and temporal monitor are fixed. We give several examples of properties expressible in the logic, including temporal synthesis with performance guarantees and aggregate and multi-criteria objectives. We also relate the logic to cooperative rational verification, showing that it can express beneficial deviations from fixed payoff baselines, but not directly reproduce the standard ATL* encoding of the core for dichotomous preferences.

Autonomous agents acting in realistic Multi-Agent Systems (MAS) should be able to adapt during their execution. Standard strategic logics, such as Alternating-time Temporal Logic (ATL), model agents' state- or history-dependent behaviour. However, the dynamic treatment of agents' available actions and their knowledge of required actions is still rarely addressed. In this paper, we introduce ATL with Dynamic Actions (ATL-D), which models the process of granting and revoking actions, and its extension ATEL-D, which captures how such updates affect agents' knowledge. Beyond the conceptual contribution, we provide several technical results: we analyse the expressivity of our logic in relation to ATL, study its relation to normative systems, and provide complexity results for relevant computational problems.

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.