Home One formula Preselected formulae Random formulae

One Formula

How to use

ATL formulae are defined by the following grammar:

F:= p | ¬F | (F1 ∧ F2) | (F1 ∨ F2) | (F1 → F2) | 《A》◯F | 《A》☐F | 《A》◊F | 《A》F1 Մ F2

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
  • ( ) (brackets) to define priorities inside the formula. By default, the order of priority is
    ¬ > 《A》◯ = 《A》☐ = 《A》◊ > 《A》Մ > ∧ > ∨ > →. → is right associative.