Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games

TL;DR

This paper extends temporal logic to better model and analyze temporary coalitions and rational behaviors in infinite multiplayer games, incorporating preferences and coalition structures without losing decidability.

Contribution

It introduces a novel extension of CTL* with coalition quantification, temporary coalition modeling, and a temporal preference operator, along with complete axiomatisations.

Findings

Decidability remains intact despite the extensions.

Enhanced logic can specify rationality and coalition dynamics.

Framework supports complex objectives in multiplayer game analysis.

Abstract

We propose enhancing the use of propositions for denoting decisions and strategies as established in temporal languages such as CTL*, if interpreted on concurrent game models. The enhancement enables specifying varying coalition structure. In quantified CTL* this technique also enables quantifying over coalition structure, and we use it to quantify over an extended form of strategy profiles which capture temporary coalitions. We also extend CTL* by a temporal form of a binary preference operator that can be traced back to the work of Von Wright. The resulting extension of quantified CTL* can be used to spell out conditions on the rationality of behaviour in concurrent multiplayer games such as what appear in solution concepts, with players having multiple individual objectives and preferences on them, and with the possibility to form temporary coalitions taken in account. We propose complete axiomatisations for the extension of CTL* by the temporal preference operator. The decidability of the logic is not affected by that extension.