Instructions

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.
• X for the ◯ (next) temporal operator
• G for the ☐ (always) temporal operator
• F for the ◊ (eventually) temporal operator
• U for 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 Px and states as Sx where x is a number. Initial tableau always begins with prestate P0, as well as final tableau for satisfiable formulae.

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 (0,1,0) if the formula contains 3 agents. Agents are automatically sorted by their number. Therefore the first move of the action vector corresponds to the choice of the player with the smallest number.