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

`!`: not.`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.`U`: until.`R`,`V`: release (the dual of until:`a R b`=`!(!a U !b)`)

### 4. Constants

`true`,`1``false`,`0`

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`.