The syntax of finite ITL is defined in Table 1 where
z denotes an integer value,
A denotes a state integer variable,
b denotes a Boolean value,
Q denotes a state propositional variable,
ig denotes a integer function symbol,
bg denotes a Boolean function symbol,
V denotes state (integer or Boolean) variable,
ei denotes a Boolean or integer expression,
h denotes a predicate symbol.
Integer Expressions |
|
ie ::= |
z | A | ig(ie1,…,ien) | A | fin A |
Boolean Expressions | |
be ::= | b | Q | bg(be1,…,ben) | Q | fin Q |
Formulae |
|
f ::= |
true | h(e1,…,en) |¬f | f1 ∧ f2 |∀V f | skip | f1 ; f2 | f∗ |