On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts
Dimitar P. Guelev
TL;DR
The paper tackles reasoning about infinite multiplayer games with qualitative preferences on plays within ${\rm ATL}_{\mathit{sc}}^*$ and strategy contexts. It develops a satisfaction-preserving translation to ${\rm QCTL}^*$ by (i) converting CGMs to $M^{\mathbf{1}}$ and unfolding to trees, (ii) encoding strategies as state variables, and (iii) eliminating the binary preference operator under a finite-index, preference-indiscernibility assumption; it further introduces a restricted second-order path quantification ${\mathop{\exists}}_{\sim}$ and analyzes how to extend the framework to ${\rm ATL}_{\mathit{sc}}^*$ with per-player preferences. The approach yields a practical route to reason about solution concepts such as Nash equilibrium and secure equilibrium via translations to ${\rm QCTL}^*$, avoiding bespoke algorithms for extended logics. An illustrative Nash-equilibrium example shows how an ${\rm ATL}_{\mathit{sc}}^*$ with ${<}$ can be systematically translated into ${\rm QCTL}^*$, enabling algorithmic analysis through an established intermediate logic.
Abstract
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.