We show how to add and eliminate binary preference on plays in Alternating-time Temporal Logic (ATL) with strategy contexts on Concurrent Game Models (CGMs) by means of a translation which preserves satisfaction in models where preference-indiscernibility between plays is an equivalence relation of finite index. The elimination technique also works for a companion second-order path quantifier, which makes quantified path variables range over sets of plays that are closed under preference-indiscernibility. We argue that the preference operator and the specialized quantifier facilitate formulating interesting solution concepts such as Nash equilibrium and secure equilibrium in a straightforward way. We also present a novel translation from ATL with strategy contexts to Quantified Computation Tree Logic (QCTL). Together with the translation which eliminates preference and the specialized form of quantification, this translation allows reasoning about infinite multiplayer synchronous games on CGMs to be translated from the proposed extension of ATL with strategy contexts into QCTL. The setting is related to that of ordered objectives in the works of Bouyer, Brenguier, Markey and Ummels, except that our focus is on the use of the temporal logic languages mentioned above, and we rely on translations into QCTL for the algorithmic solutions.

翻译：我们展示了如何在具有策略上下文的交替时序逻辑（ATL）中，通过对并发博弈模型（CGMs）进行可满足性保持的翻译，来添加和消除对博弈路径的二元偏好关系，其中偏好不可区分性需为有限索引的等价关系。该消除技术同样适用于配套的二阶路径量词，该量词使被量化的路径变量取值范围限定在偏好不可区分性下封闭的博弈路径集合上。我们认为，偏好算子与特化量词有助于以直接方式表述纳什均衡与安全均衡等具有重要意义的解概念。我们还提出了一种从带策略上下文的ATL到量化计算树逻辑（QCTL）的新颖翻译方法。结合消除偏好及特化量化形式的翻译，该翻译使得对CGMs上无限多人同步博弈的推理，可以从所提出的带策略上下文的ATL扩展形式转化为QCTL。该框架与Bouyer、Brenguier、Markey和Ummels研究中涉及的有序目标设定相关，不同之处在于我们的研究重点在于使用上述时序逻辑语言，并依赖翻译至QCTL来获得算法解决方案。