Next: , Previous: Definitions, Up: Definitions

### A.1 LTL formulas

lbtt uses the traditional definition for propositional linear temporal logic. Let AP be a finite set of atomic propositions. The set of propositional linear temporal logic formulas is defined inductively as follows:

• All atomic propositions in AP and the Boolean constant `true' are LTL formulas.
• If `f1' and `f2' are LTL formulas, then `! f1', `X f1', `(f1 \/ f2)' and `(f1 U f2)' are LTL formulas.

The semantics of linear temporal logic (i.e., a satisfiability relation) is defined over infinite sequences x = <y(0), y(1), y(2), ...> over subsets of AP as follows:

• x satisfies `true' for all sequences x.
• x satisfies an atomic proposition `p' if and only if `p' belongs to y(0), the first element of the sequence x.
• x satisfies `! f' if and only if it is not the case that x satisfies `f'.
• x satisfies `f1 \/ f2' if and only if x satisfies `f1' or x satisfies `f2'.
• x satisfies `X f' if and only if <y(1), y(2), y(3), ...> satisfies `f'.
• x satisfies `f1 U f2' if and only if there exists an i >= 0 such that <y(i), y(i+1), y(i+2), ...> satisfies `f2' and for all 0 <= j < i, <y(j), y(j+1), y(j+2), ...> satisfies `f1'.

lbtt also supports the following operators and Boolean constants, the definitions of which can be given in terms of the previously defined operators:

• “false”: `false' := `! true'
• logical conjunction: `(f1 /\ f2)' := `! (! f1 \/ ! f2)'
• logical implication: `(f1 -> f2)' := `(! f1 \/ f2)'
• logical equivalence: `(f1 <-> f2)' := `((f1 -> f2) /\ (f2 -> f1))'
• logical “exclusive or”: `(f1 xor f2)' := `! (f1 <-> f2)'
• temporal “finally”: `<> f' := `(true U f)'
• temporal “globally”: `[] f' := `! <> ! f'
• temporal “(weak) release”: `(f1 V f2)' := `! (! f1 U ! f2)'
• temporal “weak until”: `(f1 W f2)' := `((f1 U f2) \/ [] f1)'
• temporal “strong release”: `(f1 M f2)' := `((f1 V f2) /\ <> f1)'
• temporal “before”: `(f1 B f2)' := `! (! f1 U f2)'