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.