6.2 Input file format for LTL formulas

lbtt passes each LTL formula to each LTL-to-Büchi translator in a file containing an LTL formula in a prefix notation followed by a single newline. The precise grammar for the LTL formulas (in a BNF-style notation) is as follows:

     formula  ::=  `t'
                                                  // ``true''
                |  `f'
                                                  // ``false''
                |  `p'[0---9]+
                                                  // atomic proposition with
                                                  // a nonnegative integer
                                                  // identifier
                |  `!' sp formula
                                                  // negation
                |  `X' sp formula
                                                  // ``next time''
                |  `F' sp formula
                                                  // ``finally''
                |  `G' sp formula
                                                  // ``globally''
                |  `&' sp formula sp formula
                                                  // conjunction
                |  `|' sp formula sp formula
                                                  // disjunction
                |  `i' sp formula sp formula
                                                  // implication
                |  `e' sp formula sp formula
                                                  // equivalence
                |  `^' sp formula sp formula
                                                  // exclusive or
                |  `U' sp formula sp formula
                                                  // ``(strong) until''
                |  `V' sp formula sp formula
                                                  // ``(weak) release''
                |  `W' sp formula sp formula
                                                  // ``weak until''
                |  `M' sp formula sp formula
                                                  // ``strong release''
                |  `B' sp formula sp formula
                                                  // ``before''
     

(The quoted characters denote the characters themselves; sp denotes any nonempty string of white space. Lines containing a // are comments and are not part of the grammar. All atomic propositions in the formula have a nonnegative numeric identifier.)

For example, the LTL formula (in lbtt's infix syntax)

     (p0 U p1) -> (<> [] (! p2 <-> p3))

would be expressed in the form

     i U p0 p1 F G e ! p2 p3

in an output file.

If your translator does not support all of the above operators, edit the configuration file (see Configuration file) or use the command line options (see Command line options) to prevent lbtt from generating random LTL formulas with these operators.