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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Next-Time Coalition Logic

  • Thomas Ågotnes,
  • Fengkui Ju

摘要

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.