# 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. [1][2]

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? [3]

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.

## Linux Binaries

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.

## Test Cases

In order to test this application, we use a set of 42 ATL-formulae that are available in the preselected mode. Details about these test cases are available in this file.

## Paper

Amélie DAVID. ** TATL: Implementation of ATL Tableau-Based Decision Procedure.** TABLEAUX, LNAI-8123, 97-103, 2013

## References

[1] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. **Alternating-time temporal logic.** FOCS 1997:100-109

[2] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. **Alternating-time temporal logic.** J. ACM, 49(5):672-713, 2002.

[3] Valentin Goranko and Dmitry Shkatov. **Tableau-based decision procedures for logics of strategic ability in multiagent systems.** ACM Trans. Comput. Log., 11(1), 2009.