For a more precise description of Spot's temporal operators, including PSL operators, GetSpot and read the included file doc/tl/tl.pdf.
The LTL parser used in Spot understands a mix of the syntaxes used by several other tools (notably Spin, Wring, ltl2ba), so you can use whichever you prefer. This is the reason why some operators have several variants. For instance Spot will understand <>a as well as GFa. Similarly, p0 U !p1 is just the same as p0=1Up1=0. However allowing formulae like GFa introduces some quirks in the way atomic propositions can be named.
1. Unary prefix operators
F and <>: eventually.
G and : always (a.k.a. henceforth, from now on, ...).
X and (): next.
2. Unary postfix operators
These two operators are needed to parse Wring's LTL formulae.
=0: negation for atomic propositions.
For an atomic proposition p, p=0 is equivalent to !p. However this =0 syntax can only be used for atomic propositions, while ! can be used in front of any formula.
=1: no-op for atomic propositions (i.e., p=1 is equivalent to just p).
3. Binary operators
&, &&, ., /\: and.
|, ||, +, \/: or.
=>, ->: implies.
<=>, <->: equivalence.
^, xor: xor.
R, V: release (the dual of until: a R b = !(!a U !b))
These are case-insensitive, while the other operators are not.
5. Naming atomic propositions
Any alphanumeric identifier that does not start with a digit or with the letter of a unary prefix operator (F, G, or X) can be used as an atomic proposition. Other propositions must be double-quoted. For instance if GFa is the name of an atomic proposition that must be true infinitely often, the LTL formula is GF"GFa".
As a special exception to the above rule, atomic propositions can start with F, G, or X without requiring quotes if the second character is a digit. This allow naming atomic propositions X0, X1, X2, etc. This also means that X(0) is not the same as X0 (but who would use X(0)?)
Note that infix operator letters do not break identifiers. So aUb is an atomic proposition, unlike the formulae a U b, (a)U(b), and even a=1Ub=1.