Generalized alternating-time temporal logics I: Semantics

Alternating-time Temporal Logic ATL is a key framework for reasoning about strategic and coalitional ability. Built into standard ATL are several assumptions, including neverending interaction (the system never stops), joint action determinism (the next state is uniquely determined by the current state and actions chosen by all agents) and independence of choices (an agent’s choice does not depend on choices of other agents). Recently, combinations of these assumptions have been relaxed in the case of Coalition Logic – the next time fragment of ATL – resulting in eight different logics. In this paper we do the same for full ATL. We define a generalized semantics and prove some key semantic properties, laying the groundwork for axiomatic completeness. Along the way, we provide proofs of some semantic properties of standard ATL that are currently missing in the literature. In particular, we show that the interpretations based on positional and historical strategies are equivalent, in the general setting. This is “well known” for standard ATL, but perhaps surprisingly, it turns out that there is no proof of it in the literature. We also show that the semantics based on strategies and co-strategies are equivalent. All of this hinges on a fixed point characterization of “globally” and “until”, which we provide (the latter case is missing even for full ATL in the literature).

Authors

• Fengkui Ju
• Thomas Ågotnes
• Yinfeng Li
• Emiliano Lorini

Keywords

• Alternating-time temporal logic
• Positional strategies
• Historical strategies
• Co-strategies
• Fixed points