Multi-agent systems describe interactions of multiple entities called agents, often assumed to be intelligent and autonomous [1,14]. Alternating-time temporal logic (ATL ) and its fragment ATL [2] are logics which allow for reasoning about strategic interactions in such systems, by extending the framework of temporal logic with the gametheoretic notion of strategic ability. Hence, ATL enables to express statements about what agents or their groups can achieve. Such properties can be useful for specification, verification, and reasoning about interaction in agent systems [12,13], as well as about security and usability in e-voting protocols [4,9]. They have become especially relevant due to active development of algorithms and tools for verification [16], where the "correctness" property is given in terms of strategic ability. While model checking of ATL under perfect information seems to be feasible in practice [5], model checking of ATL under imperfect information [17] is still applicable only to small and medium size systems [10]. This lecture is about selected approaches which can make model checking ATL , ATL and its time extension TATL more efficient.
2 Model Reduction Methods for Variants of ATL Abstraction is a method which typically transforms large (or infinite) models into smaller (or finite) ones, but frequently defined over lattices of more that two truth values. We present multi-valued ATL (mv-ATL ), an expressive logic to specify strategic abilities in multi-agent systems [7]. We show how to identify constraints on mv-ATL formulas for which the general method for model-independent translation from multi-valued to two-valued model, can be suitably adapted to mv-ATL , Moreover, we present a modeldependent reduction that can be applied to all formulas of mv-ATL . In all cases, the complexity of verification increases only polynomially when new truth values are added to the evaluation domain.
Partial order reduction (POR) is another method used to alleviate the state space explosion in model checking [15]. We define a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information, and present some general complexity results for verification of strategic abilities in asynchronous systems [11]. A methodology for POR in verification of agents with imperfect information is discussed, based on the notion of traces introduced by Mazurkiewicz. We define the logic simple ATL , which is the restriction of ATL such that the strategic modalities cannot be nested and the next step modality is not allowed. Two semantics of simple ATL are considered and it is shown that for memoryless imperfect information contrary to memoryless perfect information, one can apply the partial order reduction techniques known for Linear-time Temporal Logic without the next step operator.
3 Timed ATL Finally, we discuss Timed Alternating-time Temporal Logic (TATL), a discrete-time extension of ATL. A new semantics, based on counting the number of visits in locations of the history, is introduced in addition to timed memoryful and memoryless ones [3]. We show that all the defined semantics are equivalent for TATL ≤,≥ , i.e., when = is not allowed in the formulas. We provide a strategy analysis revealing that it suffices to consider only two actions per location to verify any TATL ≤,≥ formula. This does not extend to TATL. The above results allow for building a hierarchy of strategies comparing the expressive power of the logics against ATL. We discuss a possible impact of this hierarchy on improving efficiency of model checking for TATL ≤,≥ .