START = ltl_formula ltl_formula = ap | '(' ltl_formula ')' | unop ltl_formula | ltl_formula binop ltl_formula | '(' ltl_formula 'U' ltl_formula ')' | untemp ltl_formula unop = '!' | '~' binop = '&' | '|' | '->' | '<-' | '<->' untemp = 'X' | 'F' | 'G' ap = PLACE cmp INT | 'true' | 'false' cmp = '=' | '!='| '>=' | '>' | '<=' | '<' /* PLACE is name of a place*/