Linear Temporal Logic Syntax

Example LTL

ltl formula phi = G a => X ((not a) U b)

Syntax LTL

The syntax of LTL formulas always starts with ltl formula <name> =. After that, the actual formula is written. LTL formulas are constructed from the following primitives and operators:

• the literals, true and false;
• atomic propositions, e.g., p;
• conjunctions, formulas joined by the keyword and, e.g., p and q and r;
• disjunctions, formulas joined by the keyword or, e.g., p or q and r;
• the until operator U, e.g., p U q;
• the release operator R, e.g., p R q;
• the next operator X, e.g., X p;
• the eventually operator F, e.g., F p;
• the always operator G, e.g., G p;
• the negation operator not, e.g., not X q;
• the implication =>, e.g., p => X not p.
• parentheses can be used to group expressions, e.g., p and (q or r); without parentheses, the order of priority of operators is: negation, always, eventually, next, implication (which is right-associative), release, until, conjunction, disjunction.

The formula is optionally followed by a definition of the alphabet considered for the language of the formula, for example:

alphabet {a, b, c}

If no alphabet is explicitly specified, the alphabet is assumed to consist of all symbols mentioned in the definition.

Finally, an optional where clause can be used to introduce the atomic propositions. It uses the syntax as in the following example.

where 
    p = {a, b}
    q = {c}

The example above defines the atomic proposition p to refer to the set of symbols including a and b. If an atomic proposition p in a formula is not defined in the where clause, it is assumed to be defined as p = {p}.