On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts

TL;DR

This paper introduces a method to incorporate and remove binary preferences in ATL with strategy contexts, enabling reasoning about complex game-theoretic solution concepts through translations into QCTL.

Contribution

It presents a translation technique that preserves satisfaction while adding and eliminating preferences in ATL with strategy contexts, facilitating analysis of multiplayer games.

Findings

Preference elimination preserves satisfaction in models.

The specialized quantifier enables expressing solution concepts like Nash equilibrium.

Translation into QCTL allows reasoning about infinite multiplayer games.

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.