带有平均收益保证的交替时间时序逻辑
Alternating-Time Temporal Logic with Mean-Payoff Guarantees
AI总结：
本文提出带合取平均收益约束的ATL*扩展ATL*_mp，分析其模型检验复杂度、记忆层级等性质，证明有限记忆策略可实现低于完美记忆上确界的所有阈值，还关联了合作理性验证。
AI中文摘要：
交替时间时序逻辑及其扩展提供了多种结合策略推理与定量推理的方式。我们研究一种特定的结合：一个联盟是否存在单一策略，该策略能在执行时序目标的同时保证给定的长期平均收益阈值。我们引入ATL*_mp，这是ATL*在加权并发游戏结构上的扩展，其中每个策略模态都带有合取式的平均收益约束。时序和定量要求必须对剩余智能体的所有行为成立，而此类策略的存在性通常无法简化为单独考虑这两项要求。对于一维约束，在完美记忆和有限记忆语义下，模型检验均为2EXPTIME完全问题，与ATL*一致。对于纯定量片段及限制为ATL或GR(1)时序目标的片段，模型检验复杂度更低。对于多维合取约束，在有限记忆语义下的模型检验仍为2EXPTIME完全问题。我们证明无记忆、有限记忆和完美记忆能力构成严格层级，同时有限记忆策略仍能达到严格低于完美记忆上确界的所有阈值。我们给出所需内存的紧线性上下界，其为阈值分母的函数，即使在游戏和时序监控器固定时也成立。我们给出该逻辑可表达的若干属性示例，包括带性能保证的时序综合，以及聚合和多准则目标。我们还将该逻辑与合作理性验证关联，表明它可表达与固定收益基线的有益偏差，但无法直接复现二值偏好下核心的标准ATL*编码。
英文摘要：
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.
