V.5 Syntax First Order ITL

First Order ITL [Slide 156]

Summary of the syntax of Expressions:

• Integer values: 0,1,…,
• State integer variable: A,B,…
• Integer operators: +,−,∗,∗∗,mod,div,…
• Temporal integer variable: A, B,…, fin A,fin B,…
• Boolean values: true,false
• Boolean state variables: P,Q,…
• Temporal Boolean variable: P, Q,…, fin P,fin Q,…

Summary of the syntax of Formulae:

• Boolean predicates: e₁ = e₂,e₁≠e₂,e₁ < e₂,e₁ ≤ e₂, e₁ > e₂,e₁ ≥ e₂,…
• Boolean operators: ∧,∨,¬,⊃,≡,∀V f
• Temporal operators: skip,;,^∗,,,,…

First Order ITL [Slide 157]

Syntax of Integer Expressions in BNF:

where z is an integer constant and ig an integer operator.

Syntax of Boolean Expressions in BNF:

where b is a Boolean constant and bg a Boolean operator.

Syntax of First Order Formulae in BNF:

where h is a Boolean predicate over integer or Boolean expressions.

First Order ITL [Slide 158]

Derived formulae: