ITL
© 1996-2016







1 Syntax

The key notion of ITL is an interval. An interval σ  is considered to be a (in)finite sequence of states σ0, σ1...  , where a state σi  is a mapping from the set of variables V ar  to the set of values V al  . The length |σ | of an interval σ0 ...σn  is equal to n  (one less than the number of states in the interval (this has always been a convention in ITL), i.e., a one state interval has length 0).

The syntax of ITL is defined in Table 1 where
z  is an integer value,
a  is a static integer variable (doesn’t change within an interval),
A  is a state integer variable (can change within an interval),
v  a static or state integer variable,
g  is a integer function symbol,
q  is a static Boolean variable (doesn’t change within an interval),
Q  is a state Boolean variable (can change within an interval),
h  is a predicate symbol.


Table 1: Syntax of ITL
|----------------------------------------------------|
|Expressions                                         |
|       e ::=  z|a|A |g (e1,...,en)|CA |finA              |
|   Formulae                                         |
|      f ::=   true|q|Q| h(e1,...,en)|f|f1 ∧ f2|∀v o f |
|             skip|f ;f |f*                           |
-------------------1--2-------------------------------