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:

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:

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