These operators are to be read as: atomic (p)roposition, and (^), negation (-), (U)ntil, ne(X)t, (F)inally, (G)lobally/always, on (A)ll paths/futures, there (E)xists a path, or (|), implies (>), strategy ({n..m}), and co-strategy ([n..m]). If p is an uppercase letter: P, Q, R, then p is interpreted as a (non-local) path atom rather than a state atom.
The tableau determines the number of agents based on the largest agent# found in the formula. For example, (P^-{1}P)^{2}Q and P^-{2}P are satisfiable but P^-{1}P is not. Some more examples 1, 2, ...