ATL* Tableau Solver

System

Formula

Agents

Solving...

Examples

Syntax Reference

p — atomic proposition (lowercase)

~p —

\neg p

(p & q) —

(p \wedge q)

(p | q) —

(p \vee q)

(p -> q) —

(p \to q)

X p —

\bigcirc p

next: p holds at the next state

G p —

\Box p

globally: p holds at every state

F p —

\Diamond p

finally: p holds at some state

(p U q) —

(p \mathbin{\mathcal{U}} q)

until: p holds until q does, and q must

(p R q) —

(p \mathbin{\mathcal{R}} q)

release: q holds up to and including the first p

A formula is read along a single infinite path, so no path quantifiers are used. It is satisfiable when some path satisfies it.

p — atomic proposition (lowercase)

~p —

\neg p

(p & q) —

(p \wedge q)

(p | q) —

(p \vee q)

(p -> q) —

(p \to q)

AX p —

\forall\bigcirc p

p at every next state

EX p —

\exists\bigcirc p

p at some next state

AG p —

\forall\Box p

p everywhere on every path

EG p —

\exists\Box p

some path with p throughout

AF p —

\forall\Diamond p

every path reaches p

EF p —

\exists\Diamond p

some path reaches p

A[p U q] —

\forall(p \mathbin{\mathcal{U}} q)

until, on every path

E[p U q] —

\exists(p \mathbin{\mathcal{U}} q)

until, on some path

Every temporal operator must be paired with a quantifier: AG p, never G p, and A[p U q], never (p U q). Round brackets also work: A(p U q). Unpaired operators are CTL*, not CTL.

p — atomic proposition (lowercase)

~p —

\neg p

(p & q) —

(p \wedge q)

(p | q) —

(p \vee q)

(p -> q) —

(p \to q)

A(...) —

\forall \pi

on every path

E(...) —

\exists \pi

on some path

Inside a quantifier: X

\bigcirc

, G

\Box

, F

\Diamond

, U

\mathcal{U}

, R

\mathcal{R}

E(G F p) —

\exists\Box\Diamond p

nesting is allowed

E(G p & F q) — one path satisfying both

A[G F p] — brackets group like parentheses

Unlike CTL, a quantifier may be applied to any path formula, so temporal operators can be nested and combined. Every temporal operator must still sit inside an A or an E.

p — atomic proposition (lowercase)

~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

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)

ATL* Tableau Solver

Results will appear here

Tableau Details

How It Works

The Algorithm

Operators at a glance

References