TATL: Tableaux for ATL*
- Initial Tableau
What are Tableaux for ATL*?
Tableaux for ATL* is the implementation of a tableau-based decision procedure for the full Alternating-time Temporal Logic (ATL*).
The Alternating-time temporal Logic (ATL) and its extension ATL* was introduced in 1997 and then in 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? 
- In 2014, S. Cerrito, V. Goranko and I (A. David) proposed an extension of the previous tableau-based decision procedure that deals with formulae of the ATL extension called ATL+.
- In 2015, I proposed a new extension that deals with formulae of the full ATL extension ATL*.
Please use the button "help" in the editor above to have explanation on how the tool works.
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
Serenella Cerrito, Amélie David and Valentin Goranko. Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. IJCAR'14, LNCS 8562, 277-291, 2014.
 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.
Old version of TATL, with computation for only ATL formulae, can be found here
How to input formulae
ATL* formulae are defined by the following grammar:
State formula F:= p | ¬F | (F1 ∧ F2) | (F1 ∨ F2) | (F1 → F2) | (F1 ↔ F2) 《A》P | [[A]]P
Path formula P: F | (P1 ∧ P2) | (P1 ∨ P2) | (P1 → P2) | (P1 ↔ P2) | ◯P | ☐P | ◊P | P1 Մ P2
where p is a proposition and A is a coalition, that is a set of agents.
To enter a formula, use:
- words of the form
[a-z][a-z 0-9]*to represent propositions ~(tilde) for the ¬ (negation) connector /\(slash & backslash) for the ∧ (and) connector \/(backslash & slash) for the ∨ (or) connector ->(hyphen & chevron) for the → (imply) connector << A >>to represent a coalition. Agents of the coalition are represented by positive numbers. All Agents must be inside a coalition and separated by a comma if there is more than one agent in the coalition. Write << >>to indicate that the coalition does not contain any agent. Xfor the ◯ (next) temporal operator Gfor the ☐ (always) temporal operator Ffor the ◊ (eventually) temporal operator Ufor the Մ (until) temporal operator
You can use the editing zone on top of the page in order to:
- enter one or several ATL* formulae (separated by ';') taking care to respect the grammar described above.
- select one of the pre-existing formulae. For that click first on the button "select a formula", then select one of the list of formulae (ATL or ATL*) and click on one of the formula of the pop-up. The selected formula is written in the editing zone and you can modify it if necessary.
Then, then click on the button "Launch" to launch the computation.
How to read results
The result will be display in the middle of the page in different tabs. When there is an error during the computation, the tab error will appear with some explanation. If the computation succeeds, three tabs appear:
- Statistics: which give the re-writting of the formula in negation normal form, the number of prestates and states generated for the initial tableau and the final tableau as will as the execution time.
- Initial tableau: it is the tableau obtained at the end of the construction phase and before the processus of elimination.
- Final tableau: it is the tableau obtained at the end of the elimination phase and therefore at the end of the whole computation.
In order to read the tableau:
Initial and final tableaux containpre-states and states. Pre-states are referred to as
Each pre-state or state is composed of a set of formulae and a set of successors. For states, successors are given with their associated actions vectors. An example of an action vector is for example