Deciding ATL* satisfiability by tableaux

International audienceWe propose a tableau-based decision procedure for the full Alternating-time Temporal Logic ATL∗. We extend our procedure for ATL+ in order to deal with nesting of temporal operators. As a side effect, we obtain a new and conceptually simple tableau method for CTL∗. The worst case complexity of our procedure is 3EXPTIME, which is suboptimal compared to the 2EXPTIME complexity of the problem. However our method is human-readable and easily implementable. A web application and binaries for our procedure are available at http:// atila.ibisc.univ-evry.fr/tableau ATL star/