MLTL Grammar

expression  : expression AND expression
            | expression OR expression
            | NEG expression
            | GLOBAL LBRACK NUMBER RBRACK expression
            | GLOBAL LBRACK NUMBER COMMA NUMBER RBRACK expression
            | FUTURE LBRACK NUMBER RBRACK expression
            | FUTURE LBRACK NUMBER COMMA NUMBER RBRACK expression
            | expression UNTIL LBRACK NUMBER RBRACK expression
            | expression UNTIL LBRACK NUMBER COMMA NUMBER RBRACK expression
            | expression WEAK_UNTIL LBRACK NUMBER RBRACK expression
            | expression WEAK_UNTIL LBRACK NUMBER COMMA NUMBER RBRACK expression

precedence = (
    ('left', 'AND', 'OR'),
    ('left', 'GLOBAL', 'FUTURE', 'UNTIL','WEAK_UNTIL'), 
    ('left', 'NEG'),
    ('left', 'LPAREN', 'RPAREN','ATOMIC','LBRACK','RBRACK'),
)

For more details on operator definitions, see the website of [1]

[1]

Brian Kempa, Pei Zhang, Phillip H. Jones, Joseph Zambreno, and Kristin Yvonne Rozier. Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. In Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science (LNCS), 196–214. Vienna, Austria, September 2020. Springer. URL: http://research.temporallogic.org/papers/KZJZR20.pdf.