ATL: expressivity, complexity... and variants.
François Laroussinie

In this talk, we will consider the Alternating-time Temporal Logic
(ATL).  We will present several results about its expressivity and
complexity depending the kind of multi-agent model used to interpret
ATL formulae (Concurrent Game Structures, Alternating Transition
Systems, Implicit Concurrent Game Structures,...).  We will also
present several real-time extensions of ATL and its models. In
particular we will discuss the way of combining concurrency and time.