What is Tableaux for ATL?
Tableaux for ATL is the implementation of a tableau-based decision procedure for the Alternating-time Temporal Logic (ATL).
ATL was introduced in 1997 and 2002 by R. Alur, T.A. Henzinger and O. Kupferman in order to describe properties of open reactive systems. 
In 2009, V. Goranko and D. Shkatov proposed a tableau method to test satisfiability for ATL formulae, that is to answer by yes or no to the following question : given a ATL formula, does it exist a model for this formula? 
Tableaux for ATL have been implemented in Ocaml for computation and PHP for the graphical user interface.
To use this application, 3 options are available :
- type your own formula
- select a formula among a set of pre-selected formulae
- use the random generator of formulae
The first two options return the satisfiability of the formula, as well as its pre-tableau and tableau. The third option only returns the satisfiability of each generated formula.
You can download the linux binaries here for a command line use of the tools.
Uncompress and use the command ./tatl --help to get the different syntaxes for wizard mode, one formula mode and random formulae mode.
Amélie DAVID. TATL: Implementation of ATL Tableau-Based Decision Procedure. TABLEAUX, LNAI-8123, 97-103, 2013
 Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. FOCS 1997:100-109
 Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002.
 Valentin Goranko and Dmitry Shkatov. Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log., 11(1), 2009.