ATL* Tableau Solver

This tool checks whether a formula of ATL* is satisfiable: that is, whether there exists a concurrent game structure and a state where the formula is true. ATL reasons about what coalitions of agents can achieve in multi-agent systems, using operators like

\langle\!\langle A \rangle\!\rangle \Box p

(coalition

A

can ensure

p

always holds). ATL* extends ATL by allowing arbitrary path formulas inside coalition operators, e.g.

\langle\!\langle A \rangle\!\rangle (\Box p \wedge \Diamond q)

— coalition

A

has a strategy ensuring

p

always and

q

eventually, on the same path.

Based on Goranko & Shkatov (2009) · David (2015) · TATL

Formula

Solving...

Examples

Syntax Reference

p — atomic proposition

~p —

\neg p

(p & q) —

(p \wedge q)

(p | q) —

(p \vee q)

(p -> q) —

(p \to q)

<<a>>X p —

\langle\!\langle a \rangle\!\rangle \!\bigcirc p

(next)

<<a,b>>G p —

\langle\!\langle a,b \rangle\!\rangle \Box p

(always)

<<a>>F p —

\langle\!\langle a \rangle\!\rangle \Diamond p

(eventually, sugar for

\top \mathbin{\mathcal{U}} p

)

<<a>>(p U q) —

\langle\!\langle a \rangle\!\rangle (p \mathbin{\mathcal{U}} q)

(until)

<<>>X p —

\langle\!\langle \emptyset \rangle\!\rangle \!\bigcirc p

(empty coalition)

<<a>>(G p & F q) — ATL*: complex path formula

<<a>>(G F p) — ATL*: nested temporal operators

⋮

Results will appear here

Enter a formula on the left and click Check Satisfiability, or try one of the examples.

Tableau Details

Rendering graph...

Click to expand

How It Works

The Algorithm

The algorithm is a tableau-based decision procedure for ATL* (the full Alternating-time Temporal Logic) that works in three phases:

Construction (Pretableau)
Starting from the input formula, the algorithm builds a graph of prestates and states. A prestate is a set of formulas waiting to be expanded. Each prestate is expanded into one or more fully expanded, downward saturated states by applying logical decomposition rules (splitting conjunctions, branching on disjunctions, and applying gamma-decomposition to expand coalition path formulas into formula tuples). For the Next rule, each state’s next-time formulas (

\langle\!\langle A \rangle\!\rangle \!\bigcirc \varphi

and

[\![A]\!] \!\bigcirc \varphi

) are used to create successor prestates via move vectors — one for each combination of agent choices compatible with the coalition constraints. This builds the pretableau.

Prestate Elimination
Prestates served as intermediate construction artifacts. In this phase, every prestate is removed and edges are rewired: if state s pointed to prestate p, and p expanded to state t, then s now points directly to t. This produces the initial tableau: a graph consisting only of states and direct transition edges.

State Elimination
The algorithm iteratively removes “defective” states. Two types of defects are checked in a dovetailed loop:

E2: If a state requires a successor (via a move vector) but no matching successor exists, it is eliminated.
E3: Eventualities (arising from Until operators within coalition path formulas) must be realized: the algorithm computes residual path formulas to check whether a finite path of accessible states can witness the eventuality. States where an eventuality cannot be realized are eliminated.

This loop continues until no more states can be removed, yielding the final tableau.

The input formula is satisfiable if and only if the final tableau still contains a state that includes the input formula.

Operators at a glance

Operator	Syntax	Meaning
$\langle\!\langle A \rangle\!\rangle \!\bigcirc \varphi$	`<<a>>X p`	Coalition $A$ can ensure $\varphi$ at the next step
$\langle\!\langle A \rangle\!\rangle \Box \varphi$	`<<a>>G p`	Coalition $A$ can ensure $\varphi$ always holds
$\langle\!\langle A \rangle\!\rangle \Diamond \varphi$	`<<a>>F p`	Coalition $A$ can ensure $\varphi$ eventually holds
$\langle\!\langle A \rangle\!\rangle (\varphi \mathbin{\mathcal{U}} \psi)$	`<<a>>(p U q)`	Coalition $A$ can ensure $\varphi$ until $\psi$
$\langle\!\langle \emptyset \rangle\!\rangle \!\bigcirc \varphi$	`<<>>X p`	The empty coalition can ensure $\varphi$ next (holds on all paths)

Note: <<a>>F p is syntactic sugar for <<a>>(T U p), where T represents $\top$ .

References

Tableau-based decision procedures for logics of strategic ability in multi-agent systems
Valentin Goranko and Dmitry Shkatov (2009)
ACM Trans. Comput. Log. 11(1)

Deciding ATL* satisfiability by tableaux
Amélie David (2015, PhD thesis)
HAL tel-01176908

Original OCaml implementation: TATL on GitHub