Next-Time Coalition Logic

Abstract Coalition Logic (CL) can be seen as the next-time fragment of Alternating-time Temporal Logic (ATL). Modalities in ATL are combinations of strategy quantifiers and tense modalities “glued” together. In ATL* this requirement is relaxed, and the two types of modalities can be mixed freely, resulting in more expressive logics. That comes at a cost: for example, as far as we know, no complete axiomatisation of ATL* exists. In this paper we study the next-time fragment of ATL*: CL*. Like in ATL and unlike in CL, we must now consider strategies rather than just actions, and like in ATL* but unlike in ATL, it matters whether we use full-memory or just memoryless strategies. The question of whether CL* actually is more expressive than CL hinges on that choice. We characterise the relative expressive power of the two variants of CL* compared to CL, and give a sound and complete axiomatisation of CL* with full-memory strategies.

Authors

• Thomas Ågotnes
• Fengkui Ju

Keywords

No keywords are indexed for this paper.